The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-08-10T12:49:22-05:00, Andrew Hirsch wrote:

> You can use the tactic simpl to run coq compuations in Gallina. So,
> in this case, you can use simpl in H to run the andb and orb
> functions, and you end up getting 
>
> H: c = false
>
> You can get the result you want from there.

Thanks for that.  I now have

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

Proof.
  intros b c H.
  destruct b.
  simpl in H.
  rewrite -> H.
  reflexivity.

  simpl in H.
  rewrite -> H.
  reflexivity.
Qed.
----------------------------------------------------------------------

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/