The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

That's perfect, thanks.

On Fri, Aug 9, 2019 at 4:13 PM Christian Doczkal <christian.doczkal AT ens-lyon.fr> wrote:

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