The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 10/04/2012 15:22, Adam Chlipala a écrit :
> On 04/10/2012 08:51 AM, 
> franck.barbier AT franckbarbier.com
>  wrote:
> > I wonder why (PS : I'm not a Coq expert at all) I cannot apply
> > (bidirectional)
> > substitutions between inhabitants of 'sig isConcrete' and '{x : Class |
> > isConcrete x}'.
>
> Because Coq's definitional equality doesn't identify those types as
> equal, at least before version 8.4, which I hear adds some support for
> an eta rule in the definitional equality. Look at the definition of the
> subset type notation, and you'll see it introduces an extra function
> abstraction.
>
> P.S.: I believe you could have sent a _much_ smaller code example to
> illustrate your question. In the future, you'll be substantially more
> likely to get useful replies if you minimize examples.

Yes,

in 8.4, the conversion is OK.


Variables (A:Type)(P:A->Prop).


Lemma L1: (sig P) -> {a:A | P a}.
intro z;exact z.
Qed.

Lemma L2 : {a:A | P a} -> (sig P) .
intro z;exact z.
Qed.

Pierre