CODEWITHSUNDEEP
coqcoq-tactic
David Farthing
David Farthing

Reputation: 247

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

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.

Upvotes: 0

Views: 347

Answers (2)

ejgallego
ejgallego

Reputation: 6852

A solution is provide in math-comp, basically you define your own inductive And3 and prove an equivalence as outlined by Anton. Then, you can use case and the constructor to work on the 3 goals. See:

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

Upvotes: 0

Anton Trunov
Anton Trunov

Reputation: 15404

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.

Upvotes: 1

Related Questions