coqproofproof-of-correctness

How would I prove that b = c if (andb b c = orb b c) in coq?


I'm new to coq and I'm trying to prove this...

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) -> (b = c).

Here is my proof, but I get stuck when I get to the goal (false = true -> false = true).

Proof.
intros b c.
induction c.
destruct b.
reflexivity.
simpl.
reflexivity.

I'm not sure how I would rewrite that expression so I can use reflexivity. But even if I do that, I'm not sure it will lead to the proof.

I was able to solve the prove if I started with the hypothesis b = c though. Namely...

Theorem andb_eq_orb_rev :
  forall (b c : bool),
  (b = c) -> (andb b c = orb b c).
Proof.
intros.
simpl.
rewrite H.
destruct c.
reflexivity.
reflexivity.
Qed.

But I can't figure out how to solve if I start with the hypothesis that has boolean functions.


Solution

  • You don't need induction, since bool is not a recursive data structure. Just go through the different cases for the values of b and c. Use destruct to do that. In two cases the hypothesis H will be of the type true = false, and you can finish the proof with inversion H. In the other two cases, the goal will be of the type true = true and it can be solved with reflexivity.

    Theorem andb_eq_orb : forall b c, andb b c = orb b c -> b = c.
    Proof. destruct b,c;  intro H; inversion H; reflexivity. Qed.