refactor(fin+nat): move is_succ to nat

hott/algebra/group.hlean

@@ -22,7 +22,7 @@ structure semigroup [class] (A : Type) extends has_mul A :=
 (is_set_carrier : is_set A)
 (mul_assoc : Πa b c, mul (mul a b) c = mul a (mul b c))
 
-attribute semigroup.is_set_carrier [instance]
+attribute semigroup.is_set_carrier [instance] [priority 950]
 
 definition mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
 !semigroup.mul_assoc
@@ -63,7 +63,7 @@ structure add_semigroup [class] (A : Type) extends has_add A :=
 (is_set_carrier : is_set A)
 (add_assoc : Πa b c, add (add a b) c = add a (add b c))
 
-attribute add_semigroup.is_set_carrier [instance]
+attribute add_semigroup.is_set_carrier [instance] [priority 900]
 
 definition add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
 !add_semigroup.add_assoc

hott/types/fin.hlean

@@ -5,8 +5,8 @@ Authors: Haitao Zhang, Leonardo de Moura, Jakob von Raumer, Floris van Doorn
 
 Finite ordinal types.
 -/
-import types.list algebra.group function logic types.prod types.sum types.nat.div
-open eq nat function list equiv is_trunc algebra sigma sum
+import types.list algebra.bundled function logic types.prod types.sum types.nat.div
+open eq function list equiv is_trunc algebra sigma sum nat
 
 structure fin (n : nat) := (val : nat) (is_lt : val < n)
 
@@ -19,7 +19,7 @@ attribute fin.val [coercion]
 section def_equal
 variable {n : nat}
 
-definition sigma_char : fin n ≃ Σ (val : nat), val < n :=
+protected definition sigma_char : fin n ≃ Σ (val : nat), val < n :=
 begin
   fapply equiv.MK,
     intro i, cases i with i ilt, apply dpair i ilt,
@@ -30,7 +30,8 @@ end
 
 definition is_set_fin [instance] : is_set (fin n) :=
 begin
-  apply is_trunc_equiv_closed, apply equiv.symm, apply sigma_char,
+  assert H : Πa, is_set (a < n), exact _, -- I don't know why this is necessary
+  apply is_trunc_equiv_closed_rev, apply fin.sigma_char,
 end
 
 definition eq_of_veq : Π {i j : fin n}, (val i) = j → i = j :=
@@ -301,6 +302,9 @@ lemma madd_left_inv : Π i : fin (succ n), madd (minv i) i = fin.zero n
 definition madd_is_comm_group [instance] : add_comm_group (fin (succ n)) :=
 add_comm_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm
 
+definition gfin (n : ℕ) [H : is_succ n] : AddCommGroup.{0} :=
+by induction H with n; exact AddCommGroup.mk (fin (succ n)) _
+
 end madd
 
 definition pred [constructor] : fin n → fin n
@@ -602,20 +606,6 @@ end
     successor.
   -/
 
-  inductive is_succ [class] : ℕ → Type :=
-  | mk : Π(n : ℕ), is_succ (nat.succ n)
-
-  attribute is_succ.mk [instance]
-
-  definition is_succ_add_right [instance] (n m : ℕ) [H : is_succ m] : is_succ (n+m) :=
-  by induction H with m; constructor
-
-  definition is_succ_add_left [instance] (n m : ℕ) [H : is_succ n] : is_succ (n+m) :=
-  by induction H with n; cases m with m: constructor
-
-  definition is_succ_bit0 [instance] (n : ℕ) [H : is_succ n] : is_succ (bit0 n) :=
-  by induction H with n; constructor
-
   /- this is a version of `madd` which might compute better -/
   protected definition add {n : ℕ} (x y : fin n) : fin n :=
   iterate cyclic_succ (val y) x

hott/types/nat/hott.hlean

@@ -144,4 +144,55 @@ namespace nat
       ... = (succ m) * n + (succ m) * k : by rewrite -succ_mul
       ... = (succ m) * (n + k) : !left_distrib⁻¹
 
+  /-
+    Some operations work only for successors. For example fin (succ n) has a 0 and a 1, but fin 0
+    doesn't. However, we want a bit more, because sometimes we want a zero of (fin a)
+    where a is either
+    - equal to a successor, but not definitionally a successor (e.g. (0 : fin (3 + n)))
+    - definitionally equal to a successor, but not in a way that type class inference can infer.
+      (e.g. (0 : fin 4). Note that 4 is bit0 (bit0 one), but (bit0 x) (defined as x + x),
+        is not always a successor)
+    To solve this we use an auxillary class `is_succ` which can solve whether a number is a
+    successor.
+  -/
+
+  inductive is_succ [class] : ℕ → Type :=
+  | mk : Π(n : ℕ), is_succ (succ n)
+
+  attribute is_succ.mk [instance]
+
+  definition is_succ_add_right [instance] (n m : ℕ) [H : is_succ m] : is_succ (n+m) :=
+  by induction H with m; constructor
+
+  definition is_succ_add_left [instance] (n m : ℕ) [H : is_succ n] : is_succ (n+m) :=
+  by induction H with n; cases m with m: constructor
+
+  definition is_succ_bit0 (n : ℕ) [H : is_succ n] : is_succ (bit0 n) :=
+  by exact _
+
+  -- level 2 is useful for abelian homotopy groups, which only exist at level 2 and higher
+  inductive is_at_least_two [class] : ℕ → Type :=
+  | mk : Π(n : ℕ), is_at_least_two (succ (succ n))
+
+  attribute is_at_least_two.mk [instance]
+
+  definition is_at_least_two_add_right [instance] (n m : ℕ) [H : is_at_least_two m] :
+    is_at_least_two (n+m) :=
+  by induction H with m; constructor
+
+  definition is_at_least_two_add_left [instance] (n m : ℕ) [H : is_at_least_two n] :
+    is_at_least_two (n+m) :=
+  by induction H with n; cases m with m: try cases m with m: constructor
+
+  definition is_at_least_two_add_both [instance] [priority 900] (n m : ℕ)
+    [H : is_succ n] [K : is_succ m] : is_at_least_two (n+m) :=
+  by induction H with n; induction K with m; cases m with m: constructor
+
+  definition is_at_least_two_bit0 (n : ℕ) [H : is_succ n] : is_at_least_two (bit0 n) :=
+  by exact _
+
+  definition is_at_least_two_bit1 (n : ℕ) [H : is_succ n] : is_at_least_two (bit1 n) :=
+  by exact _
+
+
 end nat