Coq-Syntax für Theorem über Fälle der Negation von und mit drei Argumenten

Question

Angesichts der folgenden Definition der Negation von und mit drei Argumente, kann ich verschiedene Fälle leicht beweisen, aber ich möchte diesen Beweis in einer einzigen Aussage irgendwie schreiben mit Coq. Forall b1 b2 b3: bool eine von ihnen ist falsch zurück wahr und alle drei wahr ist false zurück. Wie schreibe ich diese Prämisse in Coq, damit ich Taktiken wie Split verwenden kann, um die Konjunktion aufzulösen?

Definition negb (b:bool) : bool := 
match b with 
| true => false 
| false => true 
end. 

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool := 
    match b1 with 
    | true => 
     match b2 with 
     | true => b3 
     | false => false 
     end 
    | false => false 
    end. 

Definition nandb3 (b1:bool)(b2:bool)(b3:bool):bool := 
negb (andb3 b1 b2 b3). 


Example nandb1: (nandb3 true false true) = true. 
Proof. reflexivity. Qed. 

Example nandb2: (nandb3 false true true) = true. 
Proof. reflexivity. Qed. 

Answer 1

Sie können die Formulierung "Wenn und nur wenn" wie unten verwenden. Wenn Sie die Anweisung rückwärts lesen, heißt es: Wenn nandb3 Ihnen den Wert false gibt, dann ist der einzige mögliche Fall, wenn alle Eingaben wahr sind. Und das direkte Lesen ist völlig trivial.

Lemma nandb3_property : forall b1 b2 b3, 
    b1 = true /\ b2 = true /\ b3 = true <-> 
    nandb3 b1 b2 b3 = false. 
Proof. 
    intros b1 b2 b3. 
    destruct b1; destruct b2; destruct b3; intuition. 
Qed. 

Dann helfen wir nur ein wenig mit destructions, der Rest der Arbeit erledigt die intuition Taktik.

Answer 2

Eine Lösung ist in Mathe-Comp, im Grunde definieren Sie Ihre eigenen induktiven And3 und beweisen eine Äquivalenz wie von Anton skizziert. Dann können Sie case und den Konstruktor verwenden, um an den 3 Zielen zu arbeiten. Siehe:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrbool.v#L757