The Coq mailing list

[Amin Timany <amin.timany AT cs.kuleuven.be>]

Hi,

In trunk version we have universe polymorphism but this universe polymorphic types are not *cumulative*: see the following example

Set Universe Polymorphism.

Set Primitive Projections.

Class C : Type := {t : Type}.

Fail Definition Clift (c : C@{i}) : $( let h := constr:(Type@{i}:Type@{j}) in exact (C@{j}) )$ := c.

This definition fails due to universe inconsistency. The problem is that c : C@{i} but it is expected to be of type C@{j} where i < j. The following alternative definition works though.

Definition Clift (c : C@{i}) : $( let h := constr:(Type@{i}:Type@{j}) in exact (C@{j}) )$ := Build_C (@t c).

Of course, we cant prove c = Clift c as the types of lhs and rhs of equality are different (they differ in universe levels). But we can prove the following weaker theorem:

Definition Clift_idempotent (c : C) : Clift c = Clift (Clift c).

Proof.

  unfold Clift.

  reflexivity.

Defined.

Proving this theorem needs case analysis on c (as projections are primitive, unfolding Clift does this case analysis). This means that even this simple equality is definitional and therefore hidden from type checker. Which in turn means working with this alternative definition would not be easy in practice.

Is it simply a feature that is not implemented or is there a fundamental problem with having it in CIC? In the first case, is there a plan to have it implemented in the near future?

Regards,

Amin

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm for more information.