The Coq mailing list

[Nathanaël Courant <nathanael.courant AT ens.fr>]

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.