The Coq mailing list

[Ben Sherman <sherman AT csail.mit.edu>]

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.