Merge pull request #1805 from jdchristensen/universe-vars

Reduce universe variables and other clean-ups

theories/Algebra/AbGroups/Z.v

@@ -8,7 +8,11 @@ Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Open Scope int_scope.
 
-Definition abgroup_Z : AbGroup.
+Section MinimizationToSet.
+
+Local Set Universe Minimization ToSet.
+
+Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
   - refine (Build_Group Int int_add 0 int_negation _); repeat split.
@@ -20,6 +24,8 @@ Proof.
   - exact int_add_comm.
 Defined.
 
+End MinimizationToSet.
+
 (** We can multiply by [n : Int] in any abelian group. *)
 Definition ab_mul (n : Int) {A : AbGroup} : GroupHomomorphism A A.
 Proof.

theories/Algebra/Groups/Group.v

@@ -252,6 +252,7 @@ Definition pequiv_groupisomorphism {A B : Group}
   := fun f => Build_pEquiv _ _ f _.
 
 Coercion equiv_groupisomorphism : GroupIsomorphism >-> Equiv.
+Coercion pequiv_groupisomorphism : GroupIsomorphism >-> pEquiv.
 
 Definition equiv_path_groupisomorphism `{F : Funext} {G H : Group}
   (f g : GroupIsomorphism G H)

theories/Basics/Tactics.v

@@ -6,13 +6,17 @@ Require Import Basics.Overture.
 
 (** This module implements various tactics used in the library. *)
 
-(** The following tactic is designed to be more or less interchangeable with [induction n as [ | n' IH ]] whenever [n] is a [nat] or a [trunc_index].  The difference is that it produces proof terms involving [fix] explicitly rather than [nat_ind] or [trunc_index_ind], and therefore does not introduce higher universe parameters. *)
+(** The following tactic is designed to be more or less interchangeable with [induction n as [ | n' IH ]] whenever [n] is a [nat] or a [trunc_index].  The difference is that it produces proof terms involving [fix] explicitly rather than [nat_ind] or [trunc_index_ind], and therefore does not introduce higher universe parameters. It works if [n] is in the context or in the goal. *)
 Ltac simple_induction n n' IH :=
-  generalize dependent n;
+  try generalize dependent n;
   fix IH 1;
   intros [| n'];
   [ clear IH | specialize (IH n') ].
 
+Ltac simple_induction' n :=
+  let IH := fresh "IH" in
+  simple_induction n n IH.
+
 (** Debugging tactics to show the goal during evaluation. *)
 
 Ltac show_goal := match goal with [ |- ?T ] => idtac T end.

theories/Classes/implementations/natpair_integers.v

@@ -1049,10 +1049,7 @@ Global Instance Z_abs@{} : IntAbs@{UN UN UN UN UN
   UN UN UN UN UN
   UN UN UN UN UN
   UN UN} Z N
-  := ltac:(first [exact Z_abs'@{Ularge Ularge Ularge Ularge Ularge
-                                Ularge Ularge}|
-                  exact Z_abs'@{Ularge Ularge Ularge Ularge Ularge
-                                Ularge}]).
+  := Z_abs'.
 
 Notation n_to_z := (naturals_to_semiring N Z).
 

theories/Classes/implementations/peano_naturals.v

@@ -15,6 +15,7 @@ Local Set Universe Minimization ToSet.
 Section nat_lift.
 
 Universe N.
+(* It's important that the universe [N] be free.  Occasionally, Coq will choose universe variables in proofs that force [N] to be [Set].  To pinpoint where this happens, you can add the line [Constraint Set < N.] here, and see what fails below. *)
 
 Let natpaths := @paths@{N} nat.
 Infix "=N=" := natpaths.
@@ -425,7 +426,7 @@ Qed.
 
 Instance decidable_nat_apart x y : Decidable (nat_apart x y).
 Proof.
-  rapply decidable_sum; apply Nat.Core.decidable_lt.
+  rapply decidable_sum@{N N N}; apply Nat.Core.decidable_lt.
 Defined.
 
 Global Instance nat_trivial_apart : TrivialApart nat.

theories/Homotopy/SuccessorStructure.v

@@ -1,8 +1,11 @@
 Require Import Basics.
+Require Import Nat.Core.
 Require Import Spaces.Int.
 Require Import Spaces.Finite.Fin.
 Require Import WildCat.
 
+Local Set Universe Minimization ToSet.
+
 (** * Successor Structures. *)
 
 (** A successor structure is just a type with a endofunctor on it, called 'successor'. Typical examples include either the integers or natural numbers with the successor (or predecessor) operation. *)
@@ -15,6 +18,7 @@ Record SuccStr : Type := {
 Declare Scope succ_scope.
 
 Local Open Scope nat_scope.
+Local Open Scope type_scope.
 Local Open Scope succ_scope.
 
 Delimit Scope succ_scope with succ.
@@ -33,14 +37,16 @@ Notation "'+Z'" := IntSucc : succ_scope.
 
 (** Stratified successor structures *)
 
-Definition StratifiedType (N : SuccStr) (n : nat) : Type := N * Fin n.
+(** If [N] has a successor structure, then so does the product [N * Fin n].  The successor operation increases the second factor, and if it wraps around, it also increases the first factor. *)
+
+Definition StratifiedType (N : SuccStr) (n : nat) := N * Fin n.
 
 Definition stratified_succ (N : SuccStr) (n : nat) (x : StratifiedType N n)
   : StratifiedType N n.
 Proof.
   constructor.
-  + induction n.
-    - induction (snd x).
+  + destruct n.
+    - exact (Empty_rec _ (snd x)).
     - destruct (dec (snd x = inr tt)).
       * exact (ss_succ (fst x)).
       * exact (fst x).
@@ -51,21 +57,17 @@ Definition Stratified (N : SuccStr) (n : nat) : SuccStr
   := Build_SuccStr (StratifiedType N n) (stratified_succ N n).
 
 (** Addition in successor structures *)
-Fixpoint ss_add {N : SuccStr} (n : N) (k : nat) : N :=
-  match k with
-  | O   => n
-  | S k => (ss_add n k).+1
-  end.
+Definition ss_add {N : SuccStr} (n : N) (k : nat) : N := nat_iter k ss_succ n.
 
 Infix "+" := ss_add : succ_scope.
 
 Definition ss_add_succ {N : SuccStr} (n : N) (k : nat)
-  : (n + k.+1) = n.+1 + k.
-Proof.
-  induction k.
-  + reflexivity.
-  + exact (ap ss_succ IHk).
-Defined.
+  : n + k.+1 = n.+1 + k
+  := nat_iter_succ_r k ss_succ n.
+
+Definition ss_add_sum {N : SuccStr} (n : N) (k l : nat)
+  : n + (k + l) = (n + l) + k
+  := nat_iter_add k l ss_succ n.
 
 (** Nat and Int segmented by triples *)
 Notation "'N3'" := (Stratified (+N) 3) : succ_scope.