The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

It may not be as pretty but you can do "Fail Fail Constraint U <= V." 
for the first and "Fail Constraint V <= U." for the second.

Gaëtan Gilbert

On 17/10/2018 22:15, Christian Doczkal wrote:
> If someone is touching the naming of universes it would be nice if the automatically 
> generated names were actually Coq-identifiers. This would allow using them with the 
> "Constraint" command.
>
> In the same vein, it would be nice if there were also commands like "Consistent Constraint U <= V" that checks 
> whether "U <= V" is consistent but does not add it and "Implied Constraint U < V" that checks whether 
> "U < V" is implied by the current universe constraint.
>
> Best,
> Christian
>
> On 10/17/2018 06:18 PM, Gaëtan Gilbert wrote:
> > > Also, do you think it would make sense to name the universes of the most
> > > important template polymorphic inductive types (e.g., eq, list, etc.).
> > > That is, replace the definition of eq with:
> >
> > In https://github.com/coq/coq/issues/2829#issuecomment-350265818 I talk about 
> > a branch of mine which tries to do this automatically, such that for instance 
> > the universe on eq is called eq.0
> > In it I mention some issues but the universe naming system has changed some 
> > since so maybe it can be made to work reliably (also those issues were not 
> > that bad in the first place).
> >
> > I'll look into updating it and getting it into Coq.
> >
> > Gaëtan Gilbert
> >
> > On 17/10/2018 17:41, Christian Doczkal wrote:
> > > Hi Matthieu,
> > >
> > > Thank you very much for your explanation, this seems to be pretty much
> > > exactly what is happening. I don't yet know whether that will allow me
> > > to achieve what I was trying to do last month, but at least I now have
> > > small example exhibiting exactly the behavior you describe.
> > >
> > > Naturally, this leads to the question whether there are other
> > > circumstances where the universe constraints inferred for a particular
> > > definition are stronger than what could be inferred or can be inferred
> > > for a convertible definition (or a slight variation).
> > >
> > > Also, do you think it would make sense to name the universes of the most
> > > important template polymorphic inductive types (e.g., eq, list, etc.).
> > > That is, replace the definition of eq with:
> > >
> > > Universe eq.
> > > Inductive eq (A : Type@{eq}) (x : A) : A -> Prop :=  eq_refl : eq A x x.
> > >
> > > If I understand the mechanisms correctly, this by itself should not
> > > introduce any compatibility issues and might help understand the output
> > > of "Print Universes".
> > >
> > > Similarly, reusing this universe for basic lemmas might be a way to
> > > avoid introducing unnecessary universes without introducing too many
> > > compatibility issues, but I'm less sure about that.
> > >
> > > Best,
> > > Christian
> > >
> > >
> > > On 17/10/18 12:00, Matthieu Sozeau wrote:
> > > > Hi Christian,
> > > >
> > > >     this is a bit surprising but I don't think it is a bug. I guess what
> > > > happens is that your use
> > > > of @eq partially applied in foo, results in a cumulativity test of the form
> > > > Type@{Coq.Init.Logic.8} -> ? <= Type@{U} -> ?
> > > >
> > > > Which by default forces U = Coq.Init.Logic.8. If you enforce your
> > > > constraint, it might force
> > > > that assignment U = Coq.Init.Logic.8 to fail, and in that case the Coq
> > > > typechecker will backtrack
> > > > and eta-expand @eq to (fun A : U => @eq A) and only enforce U <=
> > > > Coq.Init.Logic.8. You can
> > > > confirm this by looking at the definition of foo in the first case, it
> > > > should have this eta expansion.
> > > > The conclusion is that you should avoid partial applications of
> > > > "template" polymorphic constants
> > > > like eq, that's one of the quirks of the feature.
> > > >
> > > > Best regards,
> > > > -- Matthieu
> > > >
> > > > On Tue, Sep 11, 2018 at 4:04 PM Christian Doczkal
> > > > <christian.doczkal AT ens-lyon.fr
> > > >  
> > > > <mailto:christian.doczkal AT ens-lyon.fr>>
> > > > wrote:
> > > >
> > > >       Hello,
> > > >
> > > >       I stumbled across another universe behavior where I am not sure whether
> > > >       this is a bug or not.
> > > >
> > > >       I have declared a bunch of Universes, say L,S,M and U and used them in a
> > > >       bunch of definitions. This ensures that U,S <= L as can be witnessed by:
> > > >
> > > >       Fail Constraint L < S.
> > > >       Fail Constraint L < U.
> > > >
> > > >       Now I can enforce S = L before some definition:
> > > >
> > > >       Constraint S = L.
> > > >       Definition foo := Foo Type@{U} ... (@eq)
> > > >       Constraint S = L.
> > > >
> > > >       In this case, everything typechecks. However, if I remove the first
> > > >       line, then the universe constraints imposed by foo change (become
> > > >       stronger) and the third line yields a universe inconsisteny.
> > > >
> > > >       In the first case, the constraints imposed by foo are:
> > > >         U < M and U <= Coq.Init.Logic.8 (the argument of eq)
> > > >
> > > >       Without the constraint "S = L", I get
> > > >         U < M and U = Coq.Init.Logic.8
> > > >
> > > >       So S = L is consistent with foo, but ruled out by it unless enforced
> > > >       before.
> > > >
> > > >       The concrete example is again too large, but having discovered the
> > > >       "Constraint" command, coming up with a reasonably sized example may be
> > > >       feasible.
> > > >
> > > >       Best,
> > > >       Christian
> > > >
> > > >       PS. It would be nice if the automatically generated universe names were
> > > >       actually names in the Coq sense, so that one could use them with the
> > > >       Constraint command.
> > > >
> > > >       On 10/09/18 14:53, Matthieu Sozeau wrote:
> > > >       > Dear Christian,
> > > >       >
> > > >       > There is documentation in dev/doc/universes about the changes
> > > >       necessary.
> > > >       > The main idea is that if your tactic produces a term with polymorphic
> > > >       > constants in it, it must produce one fresh instance of the constant at
> > > >       > each use. Before giving the final proof term containing those fresh
> > > >       > instances, you can call a type inference function to gather the
> > > >       universe
> > > >       > constraints necessary for the whole term to typecheck automatically.
> > > >       > Maybe a look at the OCaml code you use could help us fix this.
> > > >       > The « cannot ensure that i <= j » error could also be because that
> > > >       > constraint is not present in the graph you produce in a tactic I
> > > >       believe.
> > > >       >
> > > >       > The order-of-Imports issue is a bug for sure. Note that if you have a
> > > >       > module A with everything polymorphic then importing it incurs no
> > > >       global
> > > >       > constraints so the bug couldn’t happen in that case.
> > > >       >
> > > >       > Best,
> > > >       > — Matthieu
> > > >       > Le lun. 10 sept. 2018 à 14:28, Christian Doczkal
> > > >       > 
> > > > <christian.doczkal AT ens-lyon.fr
> > > >       
> > > > <mailto:christian.doczkal AT ens-lyon.fr>
> > > >       
> > > > <mailto:christian.doczkal AT ens-lyon.fr
> > > >       
> > > > <mailto:christian.doczkal AT ens-lyon.fr>>>
> > > >  a
> > > >       > écrit :
> > > >       >
> > > >       >     Hi,
> > > >       >     >> - Require Import A B. succeeds
> > > >       >     >> - Require Import B A. fails
> > > >       >     >
> > > >       >     > That sounds like a bug, you can open an issue on github with
> > > >       >     > reproduction instructions and we will look into it.
> > > >       >
> > > >       >     Unfortunately, that's an internal repository with well over
> > > >       10K lines,
> > > >       >     and the problem occurs at the end. Should I manage to find a small
> > > >       >     example, I will open an issue.
> > > >       >
> > > >       >     >> globalization of polymorphic reference <ID> would forget
> > > >       universes.
> > > >       >     >
> > > >       >     > Unfortunately various tactics and commands do not support or
> > > >       badly
> > > >       >     > support universe polymorphism. This error means some
> > > >       function hasn't
> > > >       >     > been adapted. It should probably be an anomaly.
> > > >       >     > Depending on what exactly is failing it may be possible for
> > > >       us to fix
> > > >       >     > it, or it could be beyond our current manpower.
> > > >       >
> > > >       >     This happens when calling one of our own tactics written in
> > > >       OCaml. So
> > > >       >     how does one have to adapt tactics in order to properly
> > > >       support universe
> > > >       >     polymorphism? (The error occurred while trying to see what
> > > >       happens if I
> > > >       >     make just about everything universe polymorphic, so it may or
> > > >       may not be
> > > >       >     necessary to fix this)
> > > >       >
> > > >       >     Thanks for the pointers,
> > > >       >     Christian
> > > >       >