The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

There are a few ways.
1. intro c_eq_true; symmetry; exact c_eq_true.
This gets the first equality, rewrites the goal to match the assumption by 
property of equality, and says the goal is just the assumption.

2. intro c_eq_true; rewrite c_eq_true; reflexivity.
Uses the equality assumption to get a goal of true = true, which holds by 
reflexivity.

3. intros; subst; reflexivity.
The same, but uses a more powerful tactic that rewrites away non-circular 
equalities so you don't have to write assumption names.

And many more.

The second subgoal you just simpl and the assumption is the goal, so simpl; 
auto. should work.
-Ian

----- Original Message -----
From: "mukesh tiwari" 
<mukeshtiwari.iiitm AT gmail.com>
To: 
coq-club AT inria.fr
Sent: Wednesday, October 23, 2013 11:33:16 AM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] Proof from Software foundations.



Hello all, 
I am learning Coq and trying to prove this theorem from Software Foundations 
by Benjamin Pierce[1]. 

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

Till now I came upto this and not able to solve this further. 
Proof. 
intros b c. 
destruct b. 
simpl. 

I am getting this. 

2 subgoals, subgoal 1 (ID 291) 

c : bool 
============================ 
c = true -> true = c 

subgoal 2 (ID 290) is: 
andb false c = orb false c -> false = c 





Could some one please give me some hint to prove this theorem. 


Regards, 
Mukesh Tiwair 


[1] http://www.cis.upenn.edu/~bcpierce/sf/Basics.html