coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nathanaël Courant <nathanael.courant AT ens.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Debugging universe inconsistencies
- Date: Wed, 20 Jun 2018 13:24:50 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nathanael.courant AT ens.fr; spf=Pass smtp.mailfrom=nathanael.courant AT ens.fr; spf=None smtp.helo=postmaster AT nef2.ens.fr
- Ironport-phdr: 9a23:hNow2h0UDmERwIPhsmDT+DRfVm0co7zxezQtwd8Zse0RKPad9pjvdHbS+e9qxAeQG9mDtrQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYwhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlTkJNzA5/m/UhMJ/gq1UrxC9qBJw2IPUfIKYOeBicq/Bc94XR2xMVdtRWSxbBYO8apMCAfIbMuZEr4nyvV0OogGiAgmoHOzi1DhIhmLs3aIg1eQhDRzN0QsmH90UrHTUrM/6NKEIXu+ryKnE1ynMb/RL2Tfn8ofIdAwhrOqSUrJ2asrd00cvFxncg1iWtIfrMTSV1uEXvGia6eptTe2vi287qwFxvzig3d0ghZXOhoIQzF3P6CZ3wJ4tKNGlVkJ2ZcSoHIZUuiyeLYd7RsIvT3tntSom0rEKpIC3cSsQxJkjyRPTcf2KfoiS7h/gSuqcJypzimh/d7KlnRmy9FCtyu3iWcmw11ZHtixFncfCtnwTzRDc9M6HSuBn8kevwzaDzwHT6udaLkAojafXNoAtz7oqmpYOtUnOGjX6lUH3gaOMeUgo5vCk6+H9bbXnop+cOZV0igb7Mqk2nMywG/g4MggUUGid4+uzyrnj8VflT7VNk/02iLPWsJbGJckAuKG5BRRV3pwt6xalFzumysgXnWEbLFJZfxKKl5TmO1bXIPzhEfi/h0msnyxwyvDdPrzhB43NIWLZnLfge7Z98U9cxxApwdBR/ZIHQo0Gdfn0Qwr6sMHSJh4/KQ29hej9W/tn0YZLf2uTAqafOSDWhnSP+/gmJfXEMIkcpDb0LfEo47jlimIjkFkBVaSvxt0ZcibrTbxdP0yFbC+00Z86GmAQs19mFb24uBi5STdWIk2Kcec57zA/BpihCNeRS4a2xrKbjn7iQs9mI1teA1XJKk/GMp2eUqdeZSSJZMF7wGRdCOqRDrQ53BTrjzfUjrpqKu2NoX8euJy5ktVz/Kvdj0Nq+A==
Looking through the code, it looks like the problem is caused by the use of setoid_rewrite in multiple places. For instance, trying to put the snippet below at the end of Map_poly.v produces an universe inconsistency.
Require Import ImpureConfig.
Require Import List.
Definition f (x : unit) : imp unit := pure x.
Definition g l := map f l
However, changing the proof of mapsto_add_compat in the same file to avoid using "rewrite ... at 1", which does a setoid_rewrite with the equality relation, is enough to make the inconsistency error disappear. I am a bit clueless as to why setoid_rewrite poses such problems though, and why map is specifically affected.
Thanks,
Nathanaël
On 20/06/2018 10:59, Sylvain Boulmé wrote:
Hi Nathanaël,
I am not an expert on universe issues. But this is very strange, because it seems somehow specific to "map". I do not understand why.
Here is a little variant of your code that is accepted by Coq: it uses "fold_right" instead of "map".
Require Import Vpl.ImpureConfig.
Require Import Vpl.PedraQ.
Require Import List.
Definition f (x : unit) : imp unit := pure x.
Definition g := fold_right (fun x l => (f x)::l).
A variant with "fold_left" also works !
Moreover, the VPL already uses some higher-order iterator, see "swithAll" in
https://github.com/VERIMAG-Polyhedra/VPL/blob/master/coq/AssignD.v
So, I do not understand where this issue comes from. I am also interested in any hint about this...
Thanks,
Sylvain.
Le 20/06/2018 à 10:09, Nathanaël Courant a écrit :
Require Import ImpureConfig.
Require Import PedraQ.
Require Import List.
Definition f (x : unit) : imp unit := pure x.
Definition g l := map f l.
- [Coq-Club] Debugging universe inconsistencies, Nathanaël Courant, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Sylvain Boulmé, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Nathanaël Courant, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Matthieu Sozeau, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Nathanaël Courant, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Matthieu Sozeau, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Nathanaël Courant, 06/20/2018
- Re: [Coq-Club] Debugging universe inconsistencies, Sylvain Boulmé, 06/20/2018
Archive powered by MHonArc 2.6.18.