The Coq mailing list

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

I am trying to learn Coq from Benjamin Pierce's book on software
foundations.  While doing the exercise andb_eq_orb at

http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab31

I did this:

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

Proof.
  intros b c H.
  destruct b.
----------------------------------------------------------------------


This leads to the following goals:

----------------------------------------------------------------------
2 subgoals
  
  c : bool
  H : andb true c = orb true c
  ============================
   true = c

subgoal 2 is:
 false = c
----------------------------------------------------------------------

Now, by definition `orb true c = true' , and `andb true c = c', so I
want to say

rewrite <- orb.
rewrite <- andb.
rewrite <- H.
reflexivity.
Qed.

This, however, produces an error message.  Is there a way to rewrite
terms in a proof using the definition of a function?

Thanks and best regards,
Raghu.

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