Coq syntax for theorem covering cases of negation of and with three args

Question

Given the following definition of the negation of and with three arguments, I can prove different cases easily, but I'd like to write this proof in one forall statement somehow using Coq. Forall b1 b2 b3 : bool one of them being false returns true and all three being true returns false. How do I write this premise in Coq so I can use tactics like split to break up the conjunction, etc?

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.

Anton Trunov Anton Trunov · Accepted Answer · 2016-04-11T18:21:00

You can use the 'if and only if' formulation, like below. If you read the statement backwards it says: if nandb3 gives you false, then the only possible case is when all the inputs are true. And the direct reading is completely 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.

Then we just help a little bit with destructions, the rest of the work does the intuition tactic.

Coq syntax for theorem covering cases of negation of and with three args

2 Answers