3つのargsの否定とそれをカバーする定理のCoq構文

Question

以下の3つの引数の否定と定義を与えて、簡単に異なるケースを証明することができますが、 Coqを使用します。 Forall b1 b2 b3：boolのうちの1つがfalseであればtrueを返し、3つが真であればfalseを返します。どのように私はCoqでこの前提を書くのですか？私は分割などの戦術を使用して連結などを分割することができますか？

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

以下のような「ifとonly」式を使用することができます。 文を逆に読むと、nandb3がfalseを返す場合、唯一可能なのはすべての入力が真である場合です。そして、直読はまったく簡単です。

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. 

その後、我々はちょうど仕事の残りの部分はintuition戦術を行い、破壊に少し助けて。

Answer 2

解答はmath-compで提供されますが、基本的には独自の帰納的帰納法And3を定義し、Antonによって概説された等価性を証明します。次に、ケースとコンストラクタを使用して3つの目標に取り組むことができます。参照：

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