The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

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?


--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard