The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi Taral,

Thanks for taking a look at my problem!

On Tue, Mar 03, 2009 at 02:53:18PM -0800, Taral wrote:
> On Tue, Mar 3, 2009 at 2:43 PM, Taral 
> <taralx AT gmail.com>
>  wrote:
> > You need to expose (commute (up, uq)) before taking cases on it. Also,
> > you cannot extract the hypothesis if you are going to case on a
> > subexpression.

You mean I can't do the
    be such that (namedCommute (p, q) = Some (q', p')).
step, right? It's not obvious to me why that shouldn't also work.

> Does anyone know why "per cases on A. suppose it is B." doesn't just
> introduce "A = B" as a hypothesis?

If I understand you correctly, this is one of the things that confuses
me too. e.g. in the following lemma, the last line goes orange, whereas
I would expect it to be green:

Lemma Foo : forall (x : bool), ((x = true) \/ (x = false)).
proof.
let x : bool.
per cases on x.
suppose it is true.
then (x = true).


Thanks
Ian