coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0

From: Pierre-Evariste Dagand <pierre-evariste.dagand AT ens-cachan.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0
Date: Tue, 26 Mar 2019 10:02:07 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre-evariste.dagand AT ens-cachan.org; spf=Pass smtp.mailfrom=pedagand AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f52.google.com
Ironport-phdr: 9a23:zb+yVBWAZsj7bsKZFQx5ycrXKNjV8LGtZVwlr6E/grcLSJyIuqrYbBaDt8tkgFKBZ4jH8fUM07OQ7/m4HzNRqs/b7DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsQndrMsbjI9tJqos1BfErWZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNwzY7bYoGbOvR9cK3AY90VWXFMXtpNWyFbHo+wc5cDAugHMO1Fr4f9vVwOrR6mCAe2BePg1CVIhmXo0qEj3OohDxvJ3BYhH9IVrHTbssj+OqkIXuC61qbIyyjMZO5R1Dfl6YjHbAohoeuSUr5pb8XR11MgFxnEjlWLtYzqISmZ2fkXvGiU9eVgU/+ghnU5pAF3uTij39sjhZPViYIV0F/E8z91wIEvJd23UUN2Z8OvHpVXtyGfLYR2Q8UiTnl1uCY8y70KoIK7fDILyJs53R7TceGIfJaO7xn+V+iROS91iGx5dL+7nRq/8kitxvfhWsS1zVpGtCpInsfKu3sQzRLc8NKHReF4/kq52TaAyQTT6uZcLEAxj6XbKpohzqcwl5sdrEjPByH2lUXogKOMeUUk/e+o6+vjYrr4vJOTK4h0igTmPqQvnMywH/g4PxAQU2SH/emwzr7u8E3jTLlXj/A6j7PVvZDEKcgDo662GQ5V0oIt6xalCDem1cwVnWEZI11YYh2HgJLmO1fTL/3jAve/hk6jkDZvx/zcIrLhBZDNImDZkLj9ZbZ991JcyA0rwN9D4JJUE6gNL+73Wk/sr9PVFQQ5Mgyxw+b/EtpxzIIeWWSVAq+YKqzeq1GI5vh8a9WLMYQSoXP2L+Uvz//ol34w31EHLoez2p5CUHG1BO5rZmiHaGDtmcsMWUsDsQM4QKS+kFyPSyReInusVrg9/S02To6vAo7FSqighqfE1y6wHpRQIGdcBQbfQj/Ta4yYVqJUO2qpKch7n2lcDOnze8oazRir8TTC5f9iJ+vQ9DcfsMu6htdw7uzX0xo18G4tVpjP4yS2V2hx21gwaXouxqkm/x5wzEzG2qFzg/VeU9tJ6KERC1poBdvn1+V/TuvKdEfBc9OOEgv0R9ynBXQgUYt0zYJUJUl6HNqmg1bI2C/4W7I=

> I think using this for optimization by memoization is feasible, since by
> moving a fold into the index of a type itself, you are storing the result,
> and retrieval should be
> constant time. If you have a specific use case you are thinking of, I would
> love to see it. It's a use case I had entertained, but I hadn't fleshed it
> out with a particular
> example.

You may find this interesting:

https://dblp.uni-trier.de/rec/bibtex/conf/ifl/LeatherLJ09

Best regards,

--
Pierre

[Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Talia Ringer, 03/23/2019
- Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Siddharth Bhat, 03/23/2019
  - Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Talia Ringer, 03/25/2019
    - Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Siddharth Bhat, 03/25/2019
    - Re: [Coq-Club] Plugin for proof reuse with indexed types for Coq 8.8.0, Pierre-Evariste Dagand, 03/26/2019