Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Rewriting in sort Type

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting in sort Type


Chronological Thread 
  • From: Vincent Semeria <vincent.semeria AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Rewriting in sort Type
  • Date: Fri, 9 Aug 2019 13:20:45 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vincent.semeria AT gmail.com; spf=Pass smtp.mailfrom=vincent.semeria AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f54.google.com
  • Ironport-phdr: 9a23:Fu7y1RAIIQYnJokPTiwOUyQJP3N1i/DPJgcQr6AfoPdwSPv8pMbcNUDSrc9gkEXOFd2Cra4d0ayP6v+rAjJIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+roQnMtMQajoVvJ6cswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9UrxyhqB5/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+aYYEEuoPPfxfr4n4v1YBohq+BQ+wC+zxzD9ImmL907Ak3OQkDw7Gxg0gEMgTu3nTstX1NaESXvyrw6nO0TXPdehW1in46IfWaBAhoOuDUKl/ccrU00YvFgfFgk+MpoziOjOYz+IAuHWV4epnUOKgkW8nqwdprziuwMcskIjJiZgPxlDK7yV0xps+K96gSENjf9KoDJ9duzuZOoZ2WM8uXXxktDogxrAGtpO2ejUBxo49yB7FcfOHdpCF4hL9W+aVJjd1nHdld6i+hxa26ESgzfH8WtSt3FZEridIncPAtn8K1xzU5ciHTuVy8l291jaI0gDf8uBEIUYqmqrHM5Mt3KI8m54JvUnAHiL6glv6gLKKekk++uWl5PzrYrD8qZ+dM490hBv+MqMrmsGnH+Q4Mw4OUHSF9uS6yL3v51b5T6tPjvIoiKnZsYrVKN8Upq68GQBV04Ij5wyjADeh1dQUhWMHI05deBKbk4jpPEnDL+z/DfemmlijjDNrx+3dMbD6GZXMLn3DkK/7crpn6k5czhAzzdFF6J5OBLEBOqG7Zkikv9vBSxQ9LgacwuD9Cdw72JlNd3iIB/qnMaXZvFmUrtkiJuSWZYZd7Cj8LfMo4eKolnI8lEUcdIGm2JIWbDazGfEwcBbRWmblntpUSTRChQE5VuG/0ATTAw4WXG67WucH3h9+DYunCYnZQYX02e6O2S66GttdYWUUUwnRQ0etTJ2NXrI3UAzXIsJllWZZB72oSotk0g338QGnl/xoKe3b/iBevpXmhoAsu7/j0Coq/DkxNPyzlnmXRjgtzGwNTj4ymqt4pB4lxw==
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> 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
>



Archive powered by MHonArc 2.6.18.

Top of Page