The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Richard Dapoigny wrote:
> Le 01/07/2012 02:34, Adam Chlipala a écrit :
> > Richard Dapoigny wrote:
> > > Le 30/06/2012 00:52, Adam Chlipala a écrit :
> > > > Richard Dapoigny wrote:
> > > > > I have some basic question about the hierarchy of universes in 
> > > > > Coq. Suppose that we have the following code fragment:
> > > > > Definition PT  := Type.
> > > > > Definition ED : PT := Type.
> > > > > Definition PD : PT := Type.
> > > > > Print Universes.
> > > > > Variable Test : ED->Prop.
> > > > > Variable x : ED.
> > > > > Variable y : PD.
> > > > > Check Test x.
> > > > > Check Test y.
> > > > > We expect that the universes ED and PD are different, however, the 
> > > > > test works for both.
> > > >
> > > > Why do we expect that?  The act of calling [Test] on both asserts a 
> > > > relationship between them.
> > > The point here was to check with the test whether ED and PD 
> > > correspond to distinct universes which means that the universe 
> > > hierarchy is a partial order (as in ECC) . If it is not the case 
> > > then the hierarchy simply correspond to a total order (linear).
> >
> > I'm not sure what you mean by the above.  Coq maintains a partial 
> > order (the universe constraint graph) that must always be 
> > concretizable to some total order, though Coq never materializes that 
> > order, to my knowledge.  The [Check Test y] line just has the effect 
> > of asserting [PD <= ED] in either of these kinds of order, which 
> > leads to a constraint system that is consistent.
> Yes. What is important for us is to control (at least to be aware of) 
> the ordering between universes. Now suppose that we remove the [Check 
> Test x] and [Check Test y]. Normally we expect that ED and PD are not 
> ordered (if it is a partial order). If this assumption is true, are we 
> able to prove it?

No, I don't think you can prove unrelatedness of two universe 
variables.  Any theorem statement that could be interpreted in this way 
would itself have the side effect of creating a relationship!