coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting in sort Type

From: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Rewriting in sort Type
Date: Fri, 9 Aug 2019 12:11:34 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Autocrypt: addr=christian.doczkal AT ens-lyon.fr; prefer-encrypt=mutual; keydata= mQINBFIuNbYBEADAiZlQsnkRrXHOkaZ2mZIVNxzcBha3+HhZ8IhtxF4t5QXRNWFLtdwBuE8u D0GMB/Lacm/LujwcI756cPM/7PhrUFAyn1IrYHYsK4/O5gBEgbSBRjD0X8mJ0V3oIm/PtjMC YiXBJwzOMNXOeWp+HcyCR0eh2sQD94gbF9SUOKDoamNB3DbLEHKjYPJ9O3zQw/Xai624OXB0 Wk5yIW77I1mGWhwbWxeHOJ/NmhHEU38YfbxXSzCLeMv98bNTej4oA+cPtMZ94AZOSy/oroMh rsr6wA9PL7NS+B1kRbgv6a5KL9latAI7zPeXcVsYw076rL850PLez/SXDuIr9mud4v8Zvcp9 65vTK4lTAD4C4vneNRGt4iwCOIgGsAN6BgqEgr7EwLX8dAX57OXPKZj0/0TdCbu+qsoSrQ3u +Ul6k374jFeIndqg/e9NiJbHjYAuug3cZZ6mH24SXWtTd4hGWi6f26tQQcRyGiduZkw5Wn26 g0UVgps7o2zHwlp9LJVjL3pCw7a9tKOfZaH+h7dV5JsA/Oq+7F3PhTbyNagi4A9igw+0qU+n Ws/nZDVMRiUv+1HY4PG8q6iEGSfHHjwW8InYS+Ah3stTddJ0sLc+0AGutx8ueTE2Ks14c4c8 aNW5y9bNFI/6/UQmOOwGmBeYC/kjZhjhsC3dTJ9uX4pXlMhpLQARAQABtDFDaHJpc3RpYW4g RG9jemthbCA8Y2hyaXN0aWFuLmRvY3prYWxAZW5zLWx5b24uZnI+iQJUBBMBCAA+AhsDBQsJ CAcCBhUKCQgLAgQWAgMBAh4BAheAFiEE6jiiZvHNwp19meaCj7B3SJxkuY0FAluX/3QFCQtK /T4ACgkQj7B3SJxkuY24UQ/+L9DFIx/Z8+SGhA6h8+JvfM/N3l2IT9fsDfPTLVLoyYk6j0CR T/DTGOzmh9fCCcYJbxeNeR63vwo13B0nCKfJE1sudpJCqM/6xMMeq4IcQo4Sump24iP3V9Dg iicyXowcaMTAonwadhRyGoykdXWkaHTLLbFtuF10oO0geoyM0gy/quVmONvDZVDX6WRk0DHN vx/fRCnr3pHFm1TDp5XatQbxwDH7MqX7zS5P9onkro3lqIJiekXyPeeUVZn1OWI4Ai8RgUTZ w5RNgoj/iPtCdu0yVrL5EwEikSRrrPwqp/VLNw+hslgrdI9rtv6bf2x4AshjBoi/S4MUt3s5 3hTiLhkxMeD6iPFv70SKYdYqkhN1Y7owb0L4u9/gdODvCOofo97mv0UCTvY0hpDpiyYDM/tr 6fwSVGObSYLmjzVjrwWB1gQaDsn+ghSwwGutGEHSPdwHIy4e5qCYDaUPRWSdfxfGx3ZOO9f4 s28ufT9tJbvZK2/DPpxhGEcVQE+vMoopWJma8NoZW4IbQzqg/8vFd4w9MsMDqDsbhgOlKtpv 3GEixafUMF5wJDHEpYQaWKWf1lLg7u8FIefCaJC9E/0Wl7XhmhYx0wPQ71fOhEGmf7P1DUdy OTrZtS+O3RcM54zQjlK9lweIOPYpwW8BvgNI4+E/ev1Fv31duTniNbxSeku5Ag0EUi41tgEQ ALKCkrZVjm7Jr6wZkeYMPs+OCtICbILfcRODKsM/JxEdcxbr99UA5GGi94OXGxvkQf5yLQxG hCzrLJVbrpBvl+stg72/8DrYGCCSl72gxLTTInfFxEvH3xGpBP/oMXdGjk+jxWA48opzsaar Bd9PxvFNZoWjB9jdgzBPpNMa/ykw4ATVC2fzC5xuo4fwUsl1Wu8DFLbMVwSHGXCqmV6QYUXf 0i3EKnNkKRH3a3rd7JsrC0/6lBL8sLoT54K3J6NGii6dzalhOycsSI4R8czclof3RIy5Mh/Z /rqv4d0OgY2b7QOYnGrITVtyC5UqzGMZx0dnQr5Bm7YOHaCML/LjMoYj2ovFh2zjaU6I/smx 3stVkMRpmqB7/cYPktkpGV8K9S0l6Cgiepn9pymU0/NCBFKXrPuoorKz0+X6j6YsSy7PJ1KC EIh2nSPdhB7/4ezw3DB/COfTE8EY+xbPpTF4DfI+4ARrbP953C4Z2JC7xHUGqH+D/TQ2qYiT mfHdZTrzvWYHCERApZKq1Erdpl7mHfFnwyoDB8OqS9QWfwz3Ql8TeoFPP5LdS4PHkEqog2vH j6njJnLDLUcU5OGKVrGiu8qdMGyIJNeyY6eGcl+4RR+iNJaCVSwLDB+otbxCg2cemGAfvTI4 GGpwxXuf8/r8JL9l9Jgr/zw2WroiZwOJDhPpABEBAAGJAjwEGAECACYCGwwWIQTqOKJm8c3C nX2Z5oKPsHdInGS5jQUCW5f/dAUJC0r9PgAKCRCPsHdInGS5jbhiEACnBN29HGmlJLqLyh3H /lbZDKXWQg1KzlTiMcL/EUwrUhYLK0Lm9tsHNggQfqtnAJTW+0g/Q9wGsLDAyTaHtgPUym8j FWtPv45YfHElSwdUSzy80ZKxcw5WsD4ofpvKite4j7ehzegJF0nJ1JlPFGwRDaRoVig+cQDq jtK3fCOflsTgIcqt4gB/44x79zWSfdqag64RLMmthVWq+eRCQzFNaOH6nSUcpmXe/OTMRYx3 weqsmtLAm4kcHRdGR6bmlmOcng5gleT2TImwiW3KbRzDGFIzj/gcx6XvsonEdKGv/VgUWYvq xSnktd9/YWVUQaj+XN+C7S2p8VThkwzTxbG30jU8rgjCgci3dObipm5wkvXdI2Ojrk5wz2yD tQS1DHjE4GeC0fP2XinC3IeH8uXl1ggCxH7emzETZgM+hiM1Ijt4M80nhjbMB989q8CheOhl T/6R0G7BWKAoFo/nx+KqzWNoRX2tWPaNrbxiPdTwe3l6imJ0LYqMoNGG52+WCE98JsihXE5x 62m2vEFztbJ/CyyyIAgcdQdnVeh9N2Bhx99LdKWmxb1DLGi4nsBdtlOr4nGHbO36PbBvPp0U hMGMe8UQs41NBGp2u4avbPdQYcMBdURHHgcVPMUTQIN7D1zGPNKw/31f11BY4o3BdbLXAggJ 3dGbm2ZAnj3OQRK3Sg==
Ironport-phdr: 9a23:soAtXhU3/pacycLOmPk4xgnVx5LV8LGtZVwlr6E/grcLSJyIuqrYbBaEt8tkgFKBZ4jH8fUM07OQ7/m6HzVZvt3b6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrswndrNQajZZgJ6o+1BfFvGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJhzY7aYJybOvlwcKzTctwVR3ZOU91eVyBdGI6yaJcDAuQDMOtesoLzp0EOrRy7BQS0Gu7vyiVIhn7t3a0m0uQuCwfG1xEuEdIJrHvVrdb1O70WUeuoy6TH0TXDb+lX2Tfm9IjIcwouofeWUb1tdsre1UguFwDfgVWUsoHqITWV1v8Uv2if7+tgUuSvh3QpqwFruzWiwNonhIfOhoIQ0F/E9CN5zZ40Jd2+Uk57YMSrHIFetyGAMYZ9X8AsQ3lwtSonxbAKpYS3cSoIxZg92hLSav6Kf5KW7h79SuqdOTR1iGx/dL6hhxu+7FKsxvPhWsS3ylpGszRJn9rKu3sQzRLc8NKHReF4/kq52TaAyQTT6uZcLEAwj6XUMIUuzaAqmpUNt0TDBTb6mEH2ja+RcEUo4Oao6/7/brXnoJ+TKZN0hxnjPqkhhsCzG+Y1PwoUU2SG+Omx1qfv8VPnTLlUlvE2l7PWsJHeJcQVvK65BApV354/5Ba/FTem0c8YnWUGLF1ffhKLlZXmO1bSL/H5DvewmVCsnSx1yPDAJb3tG5HNL3jEkLfnZ7p95VRcxBIpzd9D/5JUFq0BIPXrV0Dts9zYFwY1PBCww+b6E9pwzZgeWGKKAq+BKqzeq16I5uQ1I+mNfoAZojj9K+J2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cGuDZn+5qdcbEHwWvwM4BMDtg0+BWDobM32yRaMn+jAyDsSqCozRRYmpqLGHx2K/D5pQIG5cXAPfWUz0fpmJDq9fIBmZJdVsx2RdBOqRDrQ53BTrjzfUjr9uL+7a4Cod7Mmx2d5uounCkhd0+yYmVp3BgVHIdHl9myYzfxFzxLp2+Bcvx1GYlKxphPoeG8YBv6oUADd/DobVyqlBM/63Wg/FeY7YGlKvSN+rRzw3VZc10tgIJUhnSY2v
Openpgp: preference=signencrypt

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

[Coq-Club] Rewriting in sort Type, Vincent Semeria, 08/09/2019
- Re: [Coq-Club] Rewriting in sort Type, Christian Doczkal, 08/09/2019
  - Re: [Coq-Club] Rewriting in sort Type, Vincent Semeria, 08/09/2019
    - Re: [Coq-Club] Rewriting in sort Type, Christian Doczkal, 08/09/2019
      - Re: [Coq-Club] Rewriting in sort Type, Vincent Semeria, 08/09/2019