coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewriting in sort Type

From: Vincent Semeria <vincent.semeria AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Rewriting in sort Type
Date: Fri, 9 Aug 2019 12:04:04 +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-f44.google.com
Ironport-phdr: 9a23:BwXsIh+S+kVs3v9uRHKM819IXTAuvvDOBiVQ1KB41eMcTK2v8tzYMVDF4r011RmVBN+dsqsbwLCM+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhWiDanfL9+MRe7oQrPusUInIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahcNwgqxVoxyvugJxzJLPbY6PKPZzZLnQcc8GSWdDWMtaSixPApm7b4sKF+cOMudYr4/hqFQQqxu+GRSnCv7xxT9NmHD2x6w63P48GgzBwgwgHtQOv2jKo9XzKKceS/u1w7fNzTrddfNW2C3y5ZPHchAku/6MXLZwfdDNxkkoEgPIl1OdopHrMTOS0+QCqWmb7+x4WOKujW4nsQBxrSK1yscikInEgJ8exFPc9Shh3oo5Odm1RFR4bNOkCpdcqTyWO5dsTs4tTGxlvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+hfjW/yQITd8nX5lf66/iwur/UiuxeDxWdO40FlNripCndnMsm4C2wbP5ciAT/tx5kah2TCR2ADP8uxIP1w4mK7BJ5MiwrM8jIQfvVnfEiPsl0j7g7eadkA+9eip7+TnbK/mppiZN4JslAH+M6IuldChDuQ+LggCRXOb9vq51LL95035Qa9Fg+Y5kqncqp/aJMAbqrSlDA9S14Yv8wy/ACu+0NQEgXkHK0pIdw6Aj4jwIl3BPPT4DeqkjFm3izdqx/XGPqX7DZnXL3jDlq3hfbdn5EJGxgoz14MX25UBAbYYZfn3R0XZtdrCDxZ/PRbn7fzgDYBD14UVVGSTSpSUNa7IsFbAsvwuJeKBYpNTozv4JuIk7tbhiHY4nRkWeqz/jshfU2yxAvkzexbRWnHrmNpUST5W7Dp7d/TjjRi5aRAWf2y7Bvtu6TQyCYbgBoDGFNj03e6xmRyjF5gTXVhoT1CBFXCyKteBUvYILSWOe4pvzmBCWr+mRIsskxqpsV2ikus1Hq/v4iQd8Knb+p1w7uzXmws18GUtXcuY2mCJCWpzmzFRSg==

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

[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