В настоящее время я должен изучить Coq и не знаю, как бороться с or
:
Как простой пример, я не вижу, как это доказать:
Theorem T0: x \/ ~x.
Буду очень признателен, если кто-нибудь сможет мне помочь.
Для справки я использую этот шпаргалку .
Также пример доказательства, которое я имею в виду: здесь для двойного отрицания:
Require Import Classical_Prop.
Parameters x: Prop.
Theorem T7: (~~x) -> x.
intro H.
apply NNPP.
exact H.
Qed.
NNPP
Это типforall p:Prop, ~ ~ p -> p.
, так что это обман, чтобы использовать его, чтобы доказатьT7
. При импортеClassical_Prop
вы получаетеAxiom classic : forall P:Prop, P \/ ~ P.
apply classic.
решает вашу цель заT0
.Ответы:
Вы не можете доказать это в «ванильном» Coq, потому что он основан на интуиционистской логике :
Есть несколько способов справиться с такой ситуацией.
Введите закон исключенной середины в качестве аксиомы:
Больше нет необходимости доказывать что-либо после этого.
Ввести некоторую аксиому, эквивалентную закону исключенного среднего, и доказать их эквивалентность. Вот только несколько примеров.
Устранение двойного отрицания является одной из таких аксиом:
Закон Пирса является еще одним примером:
Или используйте один из законов де Моргана :
источник
Axiom peirce
: в его нынешнем виде это не закон Пирса (и на самом деле,trivial
чтобы доказать).Как вам сообщили другие, ваша тавтология не является тавтологией, если вы не принимаете классическую логику. Но так как вы делаете тавтологию над разрешимыми значениями истинности, вы можете использовать
bool
вместоProp
. Тогда ваша тавтология гласит:источник