The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You may be interested in https://coq.inria.fr/bugs/show_bug.cgi?id=5200, https://coq.inria.fr/bugs/show_bug.cgi?id=4870, https://coq.inria.fr/bugs/show_bug.cgi?id=4868.

You can reduce the number of used universes by doing some hackery like this:

Global Instance reflexive_proper_proxy

  : forall (A : Type)

           (R : crelation A),

    Reflexive R ->

    forall x : A,

      ProperProxy R x

  := fun (A : Type)

         (R : crelation A)

         (H : Reflexive R)

         (x : A) => (fun X : R x x => X) (H x).

Hint Extern 0 (ProperProxy ?R ?x)

=> unfold ProperProxy;

     let v := (eval unfold reflexivity in (@reflexivity _ R _ x)) in

     exact v

     : typeclass_instances.

Instance trans_co_eq_inv_arrow_morphism

  : forall (A : Type) (R : crelation A),

    Transitive R -> Proper (R ==> eq ==> flip arrow) R.

Proof. compute; intros; subst; eauto with nocore. Defined.

Hint Extern 0 (Proper ?P ?R)

=> let val := constr:(@trans_co_eq_inv_arrow_morphism _ R _ : Proper P R) in

   let val := (eval cbv [trans_co_eq_inv_arrow_morphism] in val) in

   let val := uconstr:(val) in

   exact val : typeclass_instances.

Then the body is:

test1@{Top.2685 Top.2753 Top.2754 Top.2760 Top.2788 Top.2854 Top.2860

Top.2905} = 

fun (a b a' b' : U) (X : a == a') (X0 : b == b') =>

(fun lemma : a == a' =>

 (fun (x y : U) (X1 : x == y) (x0 y0 : U) (H : x0 = y0) (X2 : y == y0) =>

  eq_rect_r (fun x1 : U => x == x1)

    (Equivalence_Transitive@{I P} x y y0 X1 X2) H) 

   (a * b) (a' * b)

   (star_Proper a a' lemma b b (Equivalence_Reflexive@{I P} b)) 

   (a' * b') (a' * b') (eq_Reflexive@{I Top.2788} (a' * b'))) X

  ((fun lemma : b == b' =>

    (fun (x y : U) (X1 : x == y) (x0 y0 : U) (H : x0 = y0) (X2 : y == y0) =>

     eq_rect_r (fun x1 : U => x == x1)

       (Equivalence_Transitive@{I P} x y y0 X1 X2) H) 

      (a' * b) (a' * b')

      (Reflexive_partial_app_morphism@{I I I IP P IP} star_Proper

         (Equivalence_Reflexive@{I P} a') b b' lemma) 

      (a' * b') (a' * b') (eq_Reflexive@{I Top.2905} (a' * b'))) X0

     (reflexivity@{I P} (a' * b')))

     : goal

(* Top.2685 Top.2753 Top.2754 Top.2760 Top.2788 Top.2854 Top.2860 Top.2905 |= 

   P < Top.2685

   I <= IP

   I <= Top.2753

   I <= Top.2754

   I <= Top.2854

   I <= Coq.Init.Logic.8

   I <= Coq.Init.Logic.13

   P <= IP

   P <= Top.2754

   P <= Top.2854

   P <= Coq.Init.Logic.14

   Top.2685 <= Top.2753

   Top.2760 <= Top.2754

   Top.2860 <= Top.2854

    *)

Note how only two universes are mentioned.  Hopefully a better minimization algorithm would fix this.

As a work-around, you can do something like this:

Theorem test1' : goal.

Proof.

unfold goal. intros.

rewrite X, X0. reflexivity.

Defined.

(* for the one with my modifications: *)

Definition test1@{a} := Eval hnf in test1'@{a a a a Set a a Set}. (* feel free to replace [a] with [I] or [IP] if you're okay with the constraint [P < I] or [P < IP], respectively *)

(* for your version: *)

Definition test1@{a} := Eval hnf in test1'@{a a a a a a}. (* feel free to replace [a] with [I] or [IP] if you're okay with the constraint [P < I] or [P < IP], respectively *)

By carefully managing your universes at key points, you can avoid universe blow-up without introducing too much pain.

On Wed, Jan 18, 2017 at 9:53 PM Ben Sherman <sherman AT csail.mit.edu> wrote:

Hi all,

Coq 8.5 allows rewriting with Type-valued relations. This is useful, but I've found that using rewriting in Type to define a term often adds many unnecessary universe variables and constraints. If I'm not careful, these add up and soon enough a definition in my library has thousands of universe variables. Does anyone have ideas on how to avoid this, other than avoiding using rewriting in Type altogether? What follows is a short code example illustrating how unnecessary universe variables are added.

Thanks,
Ben
-----------------

Set Universe Polymorphism.

Require Coq.Setoids.Setoid.
Require Import CRelationClasses CMorphisms.

Section Test.
Universes I P IP.
Variable U : Type@{I}.
Variable eqU : U -> U -> Type@{P}.
Variable star : U -> U -> U.

Local Infix "==" := eqU (at level 70, no associativity).
Local Infix "*" := star (at level 40, left associativity).

Axiom eqU_Equivalence : Equivalence eqU.
Axiom star_proper : forall (x x' y y' : U), x == x' -> y == y'
  -> x * y == x' * y'.

Instance star_Proper@{} : Proper@{I IP}
  (respectful@{I P I IP I IP} eqU (eqU ==> eqU)) star.
Proof.
repeat intro. apply star_proper; assumption.
Qed.

Set Printing Universes.

Definition goal@{} := forall a b a' b',
  a == a' -> b == b' -> a * b == a' * b'.

Theorem test1 : goal.
Proof.
unfold goal. intros.
rewrite X, X0. reflexivity.
Qed.
Print test1.
(* 9 extraneous universe variables, and 26 constraints. *)

Theorem test2@{} : goal.
Proof.
unfold goal. intros.
apply star_proper; assumption.
Qed.
Print test2.
(* No extraneous universe variables or constraints.*)

End Test.