The Coq mailing list

[Andrew Polonsky <andrew.polonsky AT gmail.com>]

Thank you all for the elucidation and Pierre -- thanks for the quick proof.

I guess I erroneously hoped that graF being Set-valued could make the
goal provable w/out JMeq.

Thanks again,
Andrew

On Fri, Feb 24, 2012 at 11:12, Vincent Siles 
<vincent.siles AT ens-lyon.org>
 wrote:
> Nice proof, I didn't know about generalize_eqs_vars !
>
> You should mention that this proof introduces an axiom about JMeq:
>
> JMeq_eq : forall (A : Type) (x y : A), JMeq x y -> x = y
>
> V.
>
> Le 24 février 2012 11:07, Pierre Courtieu 
>Â <Pierre.Courtieu AT cnam.fr>
>  a écrit :
>> Hello, here is a script proving your goal in v8.3 and v8.4 (14975). It
>> makes use of JMeq but the statement of the lemma is the one you want.
>>
>> Tactic dependent generalize_eqs_vars does not seem to be documented
>> but one should be able to do the same by hand.
>>
>> Bests
>> P.C.
>> ------------8X-------------------
>> Require Export JMeq.
>>
>> Variable A:Type.
>> Variable F: A -> A.
>> Inductive graF : A -> A -> Type := io_pair (a:A) : graF a (F a).
>>
>> Goal forall (a:A) (g: graF a (F a)), g = (io_pair a).
>> intros a g.
>> dependent generalize_eqs_vars g.
>> intros g0 H H0.
>> induction g.
>> apply JMeq_eq.
>> auto.
>> Qed.