[Merged by Bors] - feat(Data/UInt, Data/Fin/Basic) declarations

Mathlib/Data/Fin/Basic.lean

@@ -1,148 +1,115 @@
 import Mathlib.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Algebra.Group.Defs
-
-section Fin
-
-variable {n : Nat}
-
-instance : Zero (Fin n.succ) where
-  zero := Fin.ofNat 0
-
-@[simp]
-lemma Fin.val_zero : (0 : Fin n.succ).val = (0 : Nat) :=
-  show (Fin.ofNat 0).val = 0 by simp [Fin.ofNat]
-
-instance : One (Fin n.succ) where
-  one := ⟨1 % n.succ, Nat.mod_lt 1 (Nat.zero_lt_succ n)⟩
-
-@[simp]
-lemma Fin.of_nat_zero : (Fin.ofNat 0 : Fin n.succ) = (0 : Fin n.succ) := by
-  apply Fin.eq_of_val_eq; simp only [Fin.ofNat, Nat.zero_mod, Fin.val_zero]
-
-@[simp]
-lemma Fin.val_one : (1 : Fin n.succ).val = (1 % n.succ : Nat) := by
-  have h0 : ∀ x, (OfNat.ofNat x : Fin n.succ) = Fin.ofNat x := by simp [OfNat.ofNat]
-  simp only [h0, Fin.ofNat]
+import Mathlib.Algebra.GroupWithZero.Defs
+import Mathlib.Algebra.Ring.Basic
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
-lemma Fin.positive_size : ∀ (x : Fin n), 0 < n
+lemma Fin.size_positive : ∀ (x : Fin n), 0 < n
 | ⟨x, h⟩ =>
   match Nat.eq_or_lt_of_le (Nat.zero_le x) with
   | Or.inl h_eq => h_eq ▸ h
   | Or.inr h_lt => Nat.lt_trans h_lt h
 
-lemma Fin.modn_def : ∀ (a : Fin n) (m : Nat), a % m = Fin.mk ((a.val % m) % n) (Nat.mod_lt (a.val % m) (Fin.positive_size a))
-| ⟨a, pa⟩, m => by simp only [HMod.hMod, Fin.modn]
-
-lemma Fin.add_def : ∀ (a b : Fin n), a + b = (Fin.mk ((a.val + b.val) % n) (Nat.mod_lt _ (Fin.positive_size a)))
-| ⟨a, pa⟩, ⟨b, pb⟩ => by simp only [HAdd.hAdd, Add.add, Fin.add]
+lemma Fin.size_positive' [Inhabited (Fin n)] : 0 < n := Fin.size_positive (Inhabited.default)
 
-lemma Fin.mul_def : ∀ (a b : Fin n), a * b = (Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ (Fin.positive_size a)))
-| ⟨a, pa⟩, ⟨b, pb⟩ => by simp only [HMul.hMul, Mul.mul, Fin.mul]
+lemma zero_lt_of_lt {a : Nat} : ∀ {x : Nat}, x < a -> 0 < a
+| 0, h   => h
+| x+1, h => Nat.lt_trans (Nat.zero_lt_succ x) h
 
-lemma Fin.sub_def : ∀ (a b : Fin n), a - b = (Fin.mk ((a + (n - b)) % n) (Nat.mod_lt _ (Fin.positive_size a)))
-| ⟨a, pa⟩, ⟨b, pb⟩ => by simp only [HSub.hSub, Sub.sub, Fin.sub]
+lemma Fin.val_eq_of_lt {n a : Nat} (h : a < n) : (Fin.ofNat' a (zero_lt_of_lt h)).val = a := by
+  simp only [Fin.ofNat', Nat.mod_eq_of_lt h]
 
-@[simp] lemma Fin.mod_eq (a : Fin n) : a % n = a := by
-  apply Fin.eq_of_val_eq
-  simp only [Fin.modn_def, Nat.mod_mod]
-  exact Nat.mod_eq_of_lt a.isLt
-
-lemma Fin.add_comm (a b : Fin n) : a + b = b + a := by
-apply Fin.eq_of_val_eq
-simp only [Fin.add_def, Nat.add_comm]
+lemma Fin.modn_def : ∀ (a : Fin n) (m : Nat), a % m = Fin.mk ((a.val % m) % n) (Nat.mod_lt (a.val % m) (a.size_positive))
+| ⟨a, pa⟩, m => rfl
 
-@[simp] lemma Fin.add_zero (a : Fin n.succ) : a + 0 = a := by
-apply Fin.eq_of_val_eq
-simp only [Fin.add_def, Fin.val_zero, Nat.add_zero]
-exact Nat.mod_eq_of_lt a.isLt
+lemma Fin.mod_def : ∀ (a m : Fin n), a % m = Fin.mk ((a.val % m.val) % n) (Nat.mod_lt (a.val % m.val) (a.size_positive))
+| ⟨a, pa⟩, ⟨m, pm⟩ => rfl
 
-@[simp] lemma Fin.zero_add (a : Fin n.succ) : 0 + a = a := by
-rw [Fin.add_comm]
-exact Fin.add_zero a
+lemma Fin.add_def : ∀ (a b : Fin n), a + b = (Fin.mk ((a.val + b.val) % n) (Nat.mod_lt _ (a.size_positive)))
+| ⟨a, pa⟩, ⟨b, pb⟩ => rfl
 
-@[simp] lemma Fin.zero_mul (a : Fin n.succ) : 0 * a = 0 := by
-apply Fin.eq_of_val_eq
-simp only [Fin.mul_def, Fin.val_zero, Nat.zero_mul]
-simp [Nat.zero_mod]
+lemma Fin.mul_def : ∀ (a b : Fin n), a * b = (Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ (a.size_positive)))
+| ⟨a, pa⟩, ⟨b, pb⟩ => rfl
 
-lemma Fin.mul_comm (a b : Fin n) : a * b = b * a := by
-apply Fin.eq_of_val_eq
-simp only [Fin.mul_def, Nat.mul_comm]
+lemma Fin.sub_def : ∀ (a b : Fin n), a - b = (Fin.mk ((a + (n - b)) % n) (Nat.mod_lt _ (a.size_positive)))
+| ⟨a, pa⟩, ⟨b, pb⟩ => rfl
 
-lemma Fin.add_assoc (a b c : Fin n) : (a + b) + c = a + (b + c) := by
-apply Fin.eq_of_val_eq
-simp only [Fin.mul_def, Fin.add_def, Nat.mod_add_mod, Nat.add_mod_mod, Nat.add_assoc]
+@[simp] lemma Fin.mod_eq (a : Fin n) : a % n = a := by
+  apply Fin.eq_of_val_eq
+  simp only [Fin.modn_def, Nat.mod_mod]
+  exact Nat.mod_eq_of_lt a.isLt
 
-instance : Neg (Fin n) where
-  neg a := ⟨(n - a) % n, Nat.mod_lt _ (lt_of_le_of_lt (Nat.zero_le _) a.isLt)⟩
+@[simp] lemma Fin.mod_eq_val (a : Fin n) : a.val % n = a.val := by
+  simp only [Fin.modn_def, Nat.mod_mod]
+  exact Nat.mod_eq_of_lt a.isLt
 
-@[simp] lemma Fin.add_left_neg : ∀ (a : Fin n.succ), -a + a = 0
-| ⟨a, isLt⟩ => by
+theorem Fin.mod_eq_of_lt {a b : Fin n} (h : a < b) : a % b = a := by
   apply Fin.eq_of_val_eq
-  simp only [Neg.neg, Fin.add_def, Fin.val_zero]
-  cases a with
-  | zero => rw [Nat.sub_zero, Nat.add_zero, Nat.mod_mod, Nat.mod_self]
-  | succ a =>
-    have h1 : (n.succ - a.succ) % n.succ = (n.succ - a.succ) :=
-      Nat.mod_eq_of_lt (Nat.sub_lt (Nat.succ_pos _) (Nat.succ_pos _))
-    have h_aux : (Nat.succ n - Nat.succ a + Nat.succ a) = Nat.succ n := by
-      rw [Nat.add_comm]
-      exact Nat.add_sub_of_le (Nat.le_of_lt isLt)
-    rw [h1, h_aux, Nat.mod_self]
-
-def Fin.nsmul (x : Nat) (a : Fin n.succ) : Fin n.succ := (Fin.ofNat x) * a
-
-def Fin.gsmul (x : Int) (a : Fin n.succ) : Fin n.succ :=
-  match x with
-  | Int.ofNat x' => Fin.nsmul x' a
-  | Int.negSucc x' => -(Fin.nsmul x'.succ a)
+  simp only [Fin.mod_def]
+  rw [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt a.isLt]
+
+/- The basic structures on `Fin` are predicated on `Fin n` being inhabited.
+The Inhabited bound is there so that we can implement `Zero` in a way that satisfies
+the requirements of the relevant typeclasses (for example, AddMonoid). If we were to
+use `Fin n+1` for the `Zero` implementation, we would be shutting out some irreducible
+definitions (notably USize.size) that are known to be inhabited, but not defined in terms
+of `Nat.succ`. Since there's a blanket implementation of `∀ n, Inhabited (Fin n+1)` in
+the prelude, this hopefully won't be a significant impediment. -/
+section Fin
+
+variable {n : Nat} [Inhabited (Fin n)]
+
+instance : Numeric (Fin n) where
+  ofNat a := Fin.ofNat' a Fin.size_positive'
+
+instance : AddSemigroup (Fin n) where
+  add_assoc := fun _ _ _ => by
+    apply Fin.eq_of_val_eq
+    simp only [Fin.add_def, Nat.mod_add_mod, Nat.add_mod_mod, Nat.add_assoc]
+
+instance : AddCommSemigroup (Fin n) where
+  add_comm := fun _ _ => by
+    apply Fin.eq_of_val_eq
+    simp only [Fin.add_def, Nat.add_comm]
+
+instance : Semigroup (Fin n) where
+  mul_assoc := fun a b c => by
+    apply Fin.eq_of_val_eq
+    simp only [Fin.mul_def]
+    generalize lhs : ((a.val * b.val) % n * c.val) % n = l
+    generalize rhs : a.val * (b.val * c.val % n) % n = r
+    rw [<- Nat.mod_eq_of_lt c.isLt, (Nat.mul_mod (a.val * b.val) c.val n).symm] at lhs
+    rw [<- Nat.mod_eq_of_lt a.isLt, (Nat.mul_mod a.val (b.val * c.val) n).symm, <- Nat.mul_assoc] at rhs
+    rw [<- lhs, <- rhs]
+
+@[simp] lemma Fin.zero_def : (0 : Fin n).val = (0 : Nat) :=
+  show (Fin.ofNat' 0 Fin.size_positive').val = (0 : Nat) by simp only [Fin.ofNat', Nat.zero_mod]
+
+theorem Fin.mod_lt : ∀ (i : Fin n) {m : Fin n}, (0 : Fin n) < m → (i % m) < m
+| ⟨a, aLt⟩, ⟨m, mLt⟩, hp =>  by
+    have zero_lt : (0 : Nat) < m := Fin.zero_def ▸ hp
+    have a_mod_lt : a % m < m := Nat.mod_lt _ zero_lt
+    simp only [Fin.mod_def, LT.lt]
+    rw [(Nat.mod_eq_of_lt (Nat.lt_trans a_mod_lt mLt) : a % m % n = a % m)]
+    exact Nat.mod_lt _ zero_lt
 
 /- Aux lemma that makes nsmul_succ' easier -/
-lemma Fin.nsmuls_eq (x : Nat) : ∀ (a : Fin n.succ), Fin.nsmul x a = Fin.ofNat (x * a.val)
+protected lemma Fin.nsmuls_eq (x : Nat) : ∀ (a : Fin n), ((Fin.ofNat' x Fin.size_positive') * a) = Fin.ofNat' (x * a.val) Fin.size_positive'
 | ⟨a, isLt⟩ => by
   apply Fin.eq_of_val_eq
-  simp only [Fin.nsmul, Fin.ofNat, Fin.mul_def]
-  have hh : a % n.succ = a := Nat.mod_eq_of_lt isLt
-  generalize hq : x * a % Nat.succ n = q
-  rw [<- hh, <- Nat.mul_mod, hq]
-
-lemma Fin.nsmul_succ' (x : Nat) (a : Fin n.succ) : Fin.nsmul x.succ a = a + (Fin.nsmul x a) := by
-  simp only [Fin.nsmuls_eq]
-  simp [nsmul, Fin.ofNat, Fin.add_def]
-  exact congrArg (fun x => x % n.succ) (Nat.add_comm (x * a.val) (a.val) ▸ Nat.succ_mul x a.val)
-
-lemma Fin.sub_eq_add_neg (a b : Fin n) : a - b = a + -b := by
-  simp [Fin.add_def, Fin.sub_def, Neg.neg]
+  simp only [Fin.ofNat', Fin.mul_def]
+  generalize hy : x * a % n = y
+  rw [<- Nat.mod_eq_of_lt isLt, <- Nat.mul_mod, hy]
 
-@[simp] lemma Fin.gsmul_zero' (a : Fin n.succ) : Fin.gsmul 0 a = (0 : Fin n.succ) := by
-  simp only [Fin.gsmul, Fin.nsmul, Fin.of_nat_zero, Fin.zero_mul]
+@[simp] lemma Fin.one_def: (1 : Fin n).val = (1 % n : Nat) :=
+  show (Fin.ofNat' 1 Fin.size_positive').val = 1 % n by simp [Fin.ofNat']
 
-lemma Fin.gsmul_succ' (m : ℕ) (a : Fin n.succ) : Fin.gsmul (Int.ofNat m.succ) a = a + Fin.gsmul (Int.ofNat m) a := by
-  simp only [Fin.gsmul, Fin.nsmul_succ']
+def Fin.addOverflows? (a b : Fin n) : Bool := n <= a.val + b.val
 
-lemma Fin.gsmul_neg' (m : ℕ) (a : Fin n.succ) : gsmul (Int.negSucc m) a = -(gsmul (m.succ) a) := by
-  simp only [Fin.gsmul, Fin.nsmul]
+def Fin.mulOverflows? (a b : Fin n) : Bool := n <= a.val * b.val
 
-instance : AddSemigroup (Fin n.succ) where
-  add_assoc := Fin.add_assoc
-
-instance : AddMonoid (Fin n.succ) where
-  add_zero := Fin.add_zero
-  zero_add := Fin.zero_add
-  nsmul := Fin.nsmul
-  nsmul_zero' := Fin.zero_mul
-  nsmul_succ' := Fin.nsmul_succ'
-
-instance : SubNegMonoid (Fin n.succ) where
-  sub_eq_add_neg := Fin.sub_eq_add_neg
-  gsmul := Fin.gsmul
-  gsmul_zero' := Fin.gsmul_zero'
-  gsmul_succ' := Fin.gsmul_succ'
-  gsmul_neg' := Fin.gsmul_neg'
-
-instance : AddGroup (Fin n.succ) where
-  add_left_neg := Fin.add_left_neg
+def Fin.subUnderflows? (a b : Fin n) : Bool := a.val < b.val
 
 def Fin.overflowingAdd (a b : Fin n) : (Bool × Fin n) := (n <= a.val + b.val, a + b)
 
@@ -187,4 +154,86 @@ lemma Fin.checked_sub_spec (a b : Fin n) : (Fin.checkedSub a b).isSome = true <-
     case neg => exact Nat.le_of_not_lt hx
   case mpr => simp only [decide_eq_false (Nat.not_lt_of_le h : ¬a.val < b.val)]
 
+instance : Semiring (Fin n) :=
+  let add_zero_ : ∀ (a : Fin n), a + 0 = a := fun a => by
+    apply Fin.eq_of_val_eq
+    simp only [Fin.add_def, Fin.zero_def, Nat.add_zero]
+    exact Nat.mod_eq_of_lt a.isLt
+  let zero_mul_ : ∀ (x : Fin n), 0 * x = 0 := fun _ => by
+    apply Fin.eq_of_val_eq
+    simp only [Fin.mul_def, Fin.zero_def, Nat.zero_mul, Nat.zero_mod]
+  let mul_add_ : ∀ (a b c : Fin n), a * (b + c) = a * b + a * c := fun a b c => by
+    apply Fin.eq_of_val_eq
+    simp [Fin.mul_def, Fin.add_def]
+    generalize lhs : a.val * ((b.val + c.val) % n) % n = l
+    rw [(Nat.mod_eq_of_lt a.isLt).symm, <- Nat.mul_mod] at lhs
+    rw [<- lhs, Semiring.mul_add]
+  let mul_comm : ∀ (a b : Fin n), a * b = b * a := fun _ _ => by apply Fin.eq_of_val_eq; simp only [Fin.mul_def, Nat.mul_comm]
+
+  let mul_one_ : ∀ (a : Fin n), a * 1 = a := fun a => by
+    apply Fin.eq_of_val_eq
+    simp only [Fin.mul_def, Fin.one_def]
+    cases n with
+    | zero => exact (False.elim a.elim0)
+    | succ n =>
+      match Nat.lt_or_eq_of_le (Nat.mod_le 1 n.succ) with
+      | Or.inl h_lt =>
+        have h_eq : 1 % n.succ = 0 := Nat.eq_zero_of_le_zero (Nat.le_of_lt_succ h_lt)
+        have hnz : n = 0 := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ (Nat.le_of_mod_lt h_lt))
+        have haz : a.val = 0 := Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ (hnz ▸ a.isLt))
+        rw [h_eq, haz]
+        simp only [Nat.zero_mul, Nat.zero_mod]
+      | Or.inr h_eq => simp only [h_eq, Nat.mul_one, Nat.mod_eq_of_lt (a.isLt)]
+  {
+    ofNat_succ := fun _ => by simp [Numeric.ofNat, Fin.ofNat', Fin.add_def]
+    add_zero := add_zero_
+    zero_add := fun _ => by rw [add_comm]; exact add_zero_ _
+    nsmul := fun x a => (Fin.ofNat' x a.size_positive) * a
+    nsmul_zero' := fun _ => by
+      apply Fin.eq_of_val_eq
+      simp [Numeric.ofNat, Fin.mul_def, Fin.ofNat', Fin.zero_def, Nat.zero_mul, Nat.zero_mod]
+    nsmul_succ' := fun x a => by
+      simp only [Fin.nsmuls_eq]
+      simp [Fin.ofNat', Fin.add_def]
+      exact congrArg (fun x => x % n) (Nat.add_comm (x * a.val) (a.val) ▸ Nat.succ_mul x a.val)
+    zero_mul := zero_mul_
+    mul_zero := fun _ => by rw [mul_comm]; exact zero_mul_ _
+    mul_one := mul_one_
+    one_mul := fun _ => by rw [mul_comm]; exact mul_one_ _
+    npow_zero' := fun _ => rfl
+    npow_succ' := fun _ _ => rfl
+    mul_add := mul_add_
+    add_mul := fun a b c => by
+      have h0 := mul_add_ c a b
+      have h1 : (a + b) * c = c * (a + b) := mul_comm (a + b) c
+      have h2 : a * c = c * a := mul_comm a _
+      have h3 : b * c = c * b := mul_comm b _
+      rw [h1, h2, h3, h0]
+  }
+
+instance : Neg (Fin n) where
+  neg a := ⟨(n - a) % n, Nat.mod_lt _ (lt_of_le_of_lt (Nat.zero_le _) a.isLt)⟩
+
+instance : Ring (Fin n) :=
+  let sub_eq_add_neg_ : ∀ (a b : Fin n), a - b = a + -b := fun _ _ => by simp [Fin.add_def, Fin.sub_def, Neg.neg]
+  {
+    sub_eq_add_neg := sub_eq_add_neg_
+    gsmul := fun x a =>
+      match x with
+      | Int.ofNat x' => Semiring.nsmul x' a
+      | Int.negSucc x' => -(Semiring.nsmul x'.succ a)
+    gsmul_zero' := fun _ => by
+      apply Fin.eq_of_val_eq
+      simp only [Semiring.nsmul, Fin.ofNat', Fin.mul_def, Nat.zero_mod, Nat.zero_mul, Fin.zero_def]
+    gsmul_succ' := by simp [Semiring.nsmul_succ']
+    gsmul_neg' := by simp [Semiring.nsmul]
+    add_left_neg := fun a => by
+      rw [add_comm, <- sub_eq_add_neg_]
+      apply Fin.eq_of_val_eq
+      simp [Fin.sub_def, (Nat.add_sub_cancel' (Nat.le_of_lt a.isLt)), Nat.mod_self]
+  }
+
+instance : CommRing (Fin n) where
+  mul_comm := fun _ _ => by apply Fin.eq_of_val_eq; simp only [Fin.mul_def, Nat.mul_comm]
+
 end Fin

Mathlib/Data/Nat/Basic.lean

@@ -17,6 +17,9 @@ protected lemma not_lt_of_le {n m : ℕ} (h₁ : m ≤ n) : ¬ n < m
 
 protected lemma not_le_of_lt {n m : ℕ} : m < n → ¬ n ≤ m  := Nat.not_le_of_gt
 
+protected lemma ne_of_lt {a b : Nat} : a < b -> a ≠ b :=
+  fun h_lt h_eq => (Nat.not_le_of_lt h_lt : ¬b <= a) (h_eq ▸ Nat.le_refl b : b <= a)
+
 protected lemma lt_of_not_le {a b : ℕ} : ¬ a ≤ b → b < a := (Nat.lt_or_ge b a).resolve_right
 
 protected lemma le_of_not_lt {a b : ℕ} : ¬ a < b → b ≤ a := (Nat.lt_or_ge a b).resolve_left