Ssreflect Users Discussion List

[Chantal KELLER <>]

Thank you Georges for your answer. Then, what is the better way I could
see T as a ringType? (E can be a ringType.)

Chantal.




Le 06/10/2014 19:10, Georges Gonthier a écrit :
>   I'm afraid not, but you will be able to use eqType for E, and you will be 
> able to eliminate instances of eqT using rewrite (sameP (reflect_eqT_embed 
> _ _) eqP) (which you can assign to a lemma if you find yourself doing this 
> a lot).
> 
>    - Georges
> 
> -----Original Message-----
> From:  
> [] On Behalf Of Chantal Keller
> Sent: 06 October 2014 18:03
> To: 
> Subject: [ssreflect] eqType without syntactic equality?
> 
> Hi,
> 
> I have a type T for which I would like to consider an equality less 
> restrictive than the syntactic one. Thus, I have:
> 
> Definition eqT : T -> T -> bool := ...
> 
> but I cannot prove:
> 
> forall x y, reflect (x = y) (eqT x y)
> 
> Nonetheless, I can embed T into an eqType E such that:
> 
> Definition E : eqType := ...
> Definition embed : T -> E := ...
> Lemma reflect_eqT_embed : forall x y,
>   reflect (embed x = embed y) (eqT x y).
> 
> Would it be possible to benefit from the eqType library for the type T in 
> some way?
> 
> Thanks,
> Chantal.
>