The Coq mailing list

[Andrew Hirsch <akhirsch AT gwmail.gwu.edu>]

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.

-Andrew

On Sat, Aug 10, 2013 at 12:17 PM, N. Raghavendra <raghu AT hri.res.in> wrote:

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/