The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Note that, due to cumulativity, Xeq *is* already a crelation. So the 
following works for me: 

Require Import Setoid CRelationClasses CMorphisms.
Section X.
Variables (X : Type) (Xeq : X -> X -> Prop) (Xlt : X -> X -> Type).
Instance Xeq_equiv : CRelationClasses.Equivalence Xeq. Admitted.
Instance Xlt_morph : CMorphisms.Proper (Xeq==>Xeq==>iffT) Xlt. Admitted.

Goal forall x y z: X, Xeq x y -> Xlt x z -> Xlt y z.
Proof. intros x y z E L. rewrite <- E. exact L. Qed.
End X.

Best,
Christian

On 8/9/19 1:20 PM, Vincent Semeria wrote:
> Indeed, I managed to do a rewriting in Type using CMorphisms directly.
> 
> However, Xeq is a relation in Prop and when I try to mix
> Instance Xeq_equiv : RelationClasses.Equivalence Xeq.
> Instance Xlt_morph : CMorphisms.Proper (Xeq==>Xeq==>iffT) Xlt.
> 
> then the rewrite fails again with this error
> Tactic failure: setoid rewrite failed: Unable to satisfy the following 
> constraints:
> UNDEFINED EVARS:
>  ?X34==[x y z H H0 |- crelation X] (internal placeholder) {?c}
> 
> so it wants a crelation in Type.
> 
> I think it would be a pity to generalize Xeq in sort Type, is there a way 
> to rewrite a CMorphism over a RelationClasses.Equivalence ?
> 
> 
> On Fri, Aug 9, 2019 at 12:12 PM Christian Doczkal 
> <christian.doczkal AT ens-lyon.fr
>  
> <mailto:christian.doczkal AT ens-lyon.fr>>
>  wrote:
> 
>     Hi,
> 
>     I'm not sure about the Add Parametric Morphism command, but for 
> rewriting it suffices to declare type class instances for 
> Equivalence/PreOrder/etc. and the right instances of "Proper". These come 
> in two variants:
> 
>     RelationClasses and Morphisms deal with relations in Prop
> 
>     CRelationClasses and CMorphisms deal with relations in Type
> 
>     Just make sure you are importing the right libraries and things should 
> work.
> 
>     Hope this helps!
> 
>     Best,
>     Christian
> 
>     On 8/9/19 12:04 PM, Vincent Semeria wrote:
>     > Dear Coq clubbers,
>     >
>     > I currently work on some ordered setoids (X, Xeq, Xlt) and for 
> performance reasons I'd like the order to be in sort Type :
>     > Xlt : X -> X -> Type.
>     >
>     > Then I can store some information in Xlt, to speed up later functions 
> that take Xlt as arguments. For example this is what C-CoRN does for the 
> real numbers.
>     >
>     > However the compatibility between order and equality won't compile in 
> sort Type :
>     > Add Parametric Morphism : Xlt
>     >     with signature Xeq ==> Xeq ==> iff
>     >       as Xlt_morph.
>     >
>     > because iff wants a Prop. Even if I define
>     > Definition iffT (A B:Type) := prod (A -> B) (B -> A)
>     >
>     > then Add Parametric Morphism complains that it wants a relation Type, 
> ie a Type -> Type -> Prop.
>     >
>     > The documentation only mentions relations in sort Prop,
>     > https://coq.inria.fr/refman/addendum/generalized-rewriting.html
>     >
>     > Is there a way to do this ?
>     >
>     > Thanks,
>     > Vincent
>     >
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature