The Coq mailing list

[Taral <taralx AT gmail.com>]

On Wed, Mar 4, 2009 at 8:38 AM, Ian Lynagh 
<igloo AT earth.li>
 wrote:
> 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.

That's right. The reason is that the induction steps do not substitute
into hypotheses, so you have to keep it in the goal as an implication
until you're done with your induction steps.

> 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).

Exactly. In Ltac, this is the difference between "case" and "case_eq".
I think it's a serious shortcoming of C-zar that it doesn't generate
the equality.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown