coq

2зной

1ответ

Функция 'f' появилась в моем доказательстве. Мне нужно показать, что он равен нулю, когда оба его аргумента равны числу. На самом деле функция f эквивалентна «большей или равной» функции «geq». Я испо

5зной

2ответ

Coq в: Переписывание, если условие

Я пытаюсь научиться математический язык доказательства Coq, но я столкнулся некоторые проблемы, пытаясь что-то доказать, что я сводится к следующему глупое заявление: Lemma foo: forall b: bool, b = tr

1зной

1ответ

Как напечатать все определенные символы в Coq?

Есть ли способ распечатать все доступные (существующие в этой точке) символы вместе с их типами в Coq? Я знаю о запросе Print All., но он только показывает символы, определенные в текущем скрипте, за

2зной

1ответ

В coq, как сделать доказательства, содержащие суммы и средства?

Например, как доказательство в Coq, что: или что:

3зной

5ответ

Coq: Докажите, что произведение n и (S n) равно

Учитывая процедуру even, я хочу доказать, что even (n * (S n)) = true для всех натуральных чисел n. Использование индукции, это легко увидеть true для корпуса n = 0. Однако случай (S n) * (S (S n)) тр

0зной

2ответ

Как переписать negb true на false в Coq?

Как переписать negb true в false в Coq? Я искал в библиотеках для просто способ переписать negb true в false. Однако я не нашел ничего полезного. Я знаю simpl., но я предпочитаю более простой синтакси