The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

This is a very basic question, and might be better to ask your teacher
(if you're taking a course).

Otherwise the hint to be given is that, if your goal is something like:

a = b

And you *know* that b = a, then you can prove the former by
reflexivity (the coq tactic "reflexivity" captures this, along with a
number of automation tactics which already apply it).

So now your goal is:

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

So you want to prove that if c = true, then true = c.  The second can
be proven by reflexivity, but you need c = true within the context.
To do this, you can introduce the assumption into the context using
"intros" again.  The rest of the proof is similar, and on your own.

Kris


On Wed, Oct 23, 2013 at 11:33 AM, mukesh tiwari
<mukeshtiwari.iiitm AT gmail.com>
 wrote:
> 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