Udowadnianie tautologii za pomocą coq

12

Obecnie muszę się nauczyć Coq i nie wiem, jak sobie radzić z or:

Jako przykład, choć jest to tak proste, nie widzę, jak udowodnić:

Theorem T0: x \/ ~x.

Byłbym bardzo wdzięczny, gdyby ktoś mógł mi pomóc.

Dla porównania używam tego ściągawki .

Mam też przykład dowodu, który mam na myśli: tutaj dla podwójnej negacji:

Require Import Classical_Prop.

Parameters x: Prop.

Theorem T7: (~~x) -> x. 
intro H. 
apply NNPP. 
exact H. 
Qed.
logic coq Imago
źródło
NNPPjest typ forall p:Prop, ~ ~ p -> p., więc oszustwo polega na tym, żeby to udowodnić T7. Podczas importu Classical_PropotrzymujeszAxiom classic : forall P:Prop, P \/ ~ P.
Anton Trunov
Więc apply classic.rozwiązuje twój cel T0.
Anton Trunov

Odpowiedzi:

14

Nie można tego udowodnić w „waniliowym” Coq, ponieważ opiera się na intuicyjnej logice :

Z teorii teoretycznej logika intuicyjna jest ograniczeniem logiki klasycznej, w której prawo wykluczenia eliminacji środkowej i podwójnej negacji nie jest prawidłowymi regułami logicznymi.

Istnieje kilka sposobów poradzenia sobie z taką sytuacją.

  • Wprowadź prawo wykluczonego środka jako aksjomat:

    Axiom excluded_middle : forall P:Prop, P \/ ~ P.

    Po tym punkcie nie trzeba już niczego udowadniać.

  • Wprowadź pewien aksjomat równoważny prawu wykluczonego środka i udowodnij ich równoważność. Oto tylko kilka przykładów.

    • Eliminacja podwójnej negacji jest jednym z takich aksjomatów:

      Axiom dne : forall P:Prop, ~~P -> P.

    • Prawo Peirce'a to kolejny przykład:

      Axiom peirce : forall P Q:Prop, ((P -> Q) -> P) -> P.

    • Lub skorzystaj z jednego z praw De Morgana :

      Axiom de_morgan_and : forall P Q:Prop, ~(~P /\ ~Q) -> P \/ Q.
Anton Trunov
źródło
Do tej pory bardzo dziękuję Nie znam wszystkiego, co napisałeś, ale to sprawdzę. Używam coqIde i faktycznie dostałem dowód na podwójną negację, dodałem go do opisu problemu, aby uzyskać większą jasność później. Spodziewałem się, że istnieje analogiczny sposób rozwiązania powyższego problemu. Może powinienem podać jeden przykład.
Imago
1
@AntonTrunov musisz dodać trochę nawiasów do swojego Axiom peirce: w tej chwili nie jest to prawo Peirce'a (i faktycznie ma trivialto udowodnić).
Gallais
@gallais Dzięki za wykrycie tego! Naprawiony.
Anton Trunov
6

Jak poinformowali cię inni, twoja tautologia nie jest tautologią, chyba że przyjmiesz logikę klasyczną. Ale ponieważ robisz tautologie dotyczące rozstrzygających wartości prawdy, możesz użyć boolzamiast tego Prop. Zatem twoja tautologia obejmuje:

Require Import Bool.

Lemma how_about_bool: forall (p : bool), Is_true (p || negb p).
Proof.
  now intros [|].
Qed.
Andrej Bauer
źródło