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.
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.