Доказательство по логическим значениям, false = true

Question

В настоящее время я нахожусь в главе 5 «Основы программного обеспечения», но почувствовал необходимость вернуться к первой главе, чтобы прояснить пару вещей. В частности, есть упражнение, которое я не совсем усвоил, в котором нас просят дважды использовать деструкцию, чтобы доказать результат по булевым. Здесь он меняется с именами и другими деталями.

Inductive bool: Type := 
|true: bool 
|false: bool. 

Definition fb (b1:bool) (b2:bool) : bool := 
match b1, b2 with 
| false, false => false 
| _, _ => true 
end. 

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
intros [] [] H. 
- rewrite <- H. reflexivity. 
- reflexivity. 
- rewrite <- H. reflexivity. 
- reflexivity. 
Qed. 

Когда на первое клеща, контекст и целях является нонсенсом:

H : fb true true = false 
______________________________________(1/1) 
true = false 

Второй галочка гипотеза неверна. Третий тик - это тот же вздор, что и первый. Только четвертый тик разумен с:

H : fb false false = false 
______________________________________(1/1) 
false = false 

Я понимаю, что по правилам перезаписи все это работает. Однако у меня такое впечатление, что мы уходим от узкого пути истины для пустыни ложности. Точнее, и AFAIK, ложная гипотеза может быть сделана для доказательства ЛЮБОГО утверждения, истинного или ложного. Здесь мы используем его, чтобы доказать, что false = true, ОК, почему нет, но все же это заставляет меня чувствовать себя несколько неудобно. Я бы не ожидал, что помощник по доказательству разрешит это.

Разрабатывая немного

В типичном доказательстве от противного, я выбрал бы гипотезу случайным образом, и выводит цели, пока не найдет ни тавтологию или противоречие. Затем я заключил бы, была ли моя гипотеза верной или ложной.

Что здесь происходит, в случаях 1 (то же самое для случая 3), Кок начинается с гипотезы, что является ложным:

H : fb true true = false 

применяет его к цели, что является противоречием:

true = false 

и объединяет их, чтобы найти тавтологию.

Это не способ рассуждения, о котором я знаю. Это напоминает студенческие «шутки», где, начиная с 0 = 1, может быть доказан любой абсурдный результат по натуральным числам.

Followup

Так сегодня утром во время моего коммутируют я думал о том, что я только что написал выше. Теперь я считаю, что случаи 1 и 3 являются правильными доказательствами от противного. Действительно, H является ложным, и мы используем его для доказательства цели, которая является ложной. Гипотезы (значения a и b) должны быть отклонены. Меня могло смутить то, что, используя переписывание, мы делаем часть пути «назад», начиная с цели.

Я немного нерешенным для случая 2, который гласит:

H : fb true false = false 
______________________________________(1/1) 
false = false 

который в основном false -> true, тавтология под «принцип взрыва». Я не думаю, что это можно было бы использовать так прямо в доказательстве.

Хорошо, не уверен, что я полностью понял, что находится под капотом, но доверие к Coq не тронуто. Обязательно продолжайте и вернитесь к главе 5. Спасибо всем за ваши комментарии.

Answer 1

Прежде всего, спасибо за предоставление автономного кода.

Я понимаю ваше беспокойство, доказывающее цель, используя rewrite, когда вы знаете, что то, что вы действительно должны делать, - это получить противоречие из гипотез. Тем не менее, это неверно. Верно, что при таких предположениях вы можете доказать эту цель.

Однако я также считаю, что это не делает подлинный скрипт действительно удобочитаемым. В вашем примере вы рассматриваете все возможные случаи, и бывает, что три из этих четырех невозможны. Когда мы читаем ваше доказательство, мы не можем этого видеть. Чтобы было ясно, что вы в невозможном случае, есть несколько тактик, которые полезны, чтобы сказать «посмотрите, теперь я собираюсь доказать противоречие, чтобы исключить этот случай».

Один из них: exfalso. Он заменит текущую цель на False (поскольку все может быть получено от False, как упоминалось в комментарии @ejgallego).

Второй - absurd, чтобы сказать: «Теперь я собираюсь доказать какое-то утверждение и его отрицание» (это в основном эквивалентно доказательству False).

Третий, которого достаточно в вашем случае, является discriminate. Он пытается найти в гипотезах противоречивое равенство, например true = false.

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    intros [] [] H. 
    - discriminate. 
    - discriminate. 
    - discriminate. 
    - reflexivity. 
Qed. 

---

Теперь, только так вы знаете, discriminate и reflexivity оба судимы easy тактикой. Таким образом, следующее доказательство будет работать так же хорошо (но он не показывает, что происходит, и, таким образом, выпадает из рамки данного вопроса):

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    intros [] [] H; easy. 
Qed. 

и это синтаксический сахар для того же доказательства:

Theorem th: forall a b: bool, 
    fb a b = false -> b = false. 
Proof. 
    now intros [] [] H. 
Qed.