feat(data/fin): add some lemmas about coercions (leanprover-community…

…#2522)

Two of these lemmas allow norm_cast to work with inequalities
involving fin values converted to ℕ.  The rest are for simplifying
expressions where coercions are used to convert from ℕ to fin, in
cases where an inequality means those coercions do not in fact change
the value.

There are very few lemmas relating to coercions from ℕ to fin in
mathlib at present; the lemma of_nat_eq_coe (and val_add on which it
depends, and a few similarly trivial lemmas alongside val_add) is
moved from data.zmod.basic to fin.basic for use in proving the other
lemmas, while the nat lemma add_mod is moved to data.nat.basic for use
in the proof of of_nat_eq_coe, and mul_mod is moved alongside it as
suggested in review.  These lemmas were found useful in formalising
solutions to an olympiad problem, see
<https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations>,
and seem more generally relevant than to just that particular problem.

src/data/fin.lean

@@ -98,6 +98,61 @@ attribute [simp] val_zero
 @[simp] lemma coe_one  {n : ℕ} : ((1 : fin (n+2)) : ℕ) = 1 := rfl
 @[simp] lemma coe_two  {n : ℕ} : ((2 : fin (n+3)) : ℕ) = 2 := rfl
 
+/-- `a < b` as natural numbers if and only if `a < b` in `fin n`. -/
+@[norm_cast, simp] lemma coe_fin_lt {n : ℕ} {a b : fin n} : (a : ℕ) < (b : ℕ) ↔ a < b :=
+iff.rfl
+
+/-- `a ≤ b` as natural numbers if and only if `a ≤ b` in `fin n`. -/
+@[norm_cast, simp] lemma coe_fin_le {n : ℕ} {a b : fin n} : (a : ℕ) ≤ (b : ℕ) ↔ a ≤ b :=
+iff.rfl
+
+lemma val_add {n : ℕ} : ∀ a b : fin n, (a + b).val = (a.val + b.val) % n
+| ⟨_, _⟩ ⟨_, _⟩ := rfl
+
+lemma val_mul {n : ℕ} :  ∀ a b : fin n, (a * b).val = (a.val * b.val) % n
+| ⟨_, _⟩ ⟨_, _⟩ := rfl
+
+lemma one_val {n : ℕ} : (1 : fin (n+1)).val = 1 % (n+1) := rfl
+
+@[simp] lemma zero_val (n : ℕ) : (0 : fin (n+1)).val = 0 := rfl
+
+@[simp]
+lemma of_nat_eq_coe (n : ℕ) (a : ℕ) : (of_nat a : fin (n+1)) = a :=
+begin
+  induction a with a ih, { refl },
+  ext, show (a+1) % (n+1) = fin.val (a+1 : fin (n+1)),
+  { rw [val_add, ← ih, of_nat],
+    exact add_mod _ _ _ }
+end
+
+/-- Converting an in-range number to `fin (n + 1)` produces a result
+whose value is the original number.  -/
+lemma coe_val_of_lt {n : ℕ} {a : ℕ} (h : a < n + 1) :
+  (a : fin (n + 1)).val = a :=
+begin
+  rw ←of_nat_eq_coe,
+  exact nat.mod_eq_of_lt h
+end
+
+/-- Converting the value of a `fin (n + 1)` to `fin (n + 1)` results
+in the same value.  -/
+@[simp] lemma coe_val_eq_self {n : ℕ} (a : fin (n + 1)) : (a.val : fin (n + 1)) = a :=
+begin
+  rw fin.eq_iff_veq,
+  exact coe_val_of_lt a.is_lt
+end
+
+/-- Coercing an in-range number to `fin (n + 1)`, and converting back
+to `ℕ`, results in that number. -/
+lemma coe_coe_of_lt {n : ℕ} {a : ℕ} (h : a < n + 1) :
+  ((a : fin (n + 1)) : ℕ) = a :=
+coe_val_of_lt h
+
+/-- Converting a `fin (n + 1)` to `ℕ` and back results in the same
+value. -/
+@[simp] lemma coe_coe_eq_self {n : ℕ} (a : fin (n + 1)) : ((a : ℕ) : fin (n + 1)) = a :=
+coe_val_eq_self a
+
 /-- Assume `k = l`. If two functions defined on `fin k` and `fin l` are equal on each element,
 then they coincide (in the heq sense). -/
 protected lemma heq_fun_iff {α : Type*} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :

src/data/nat/basic.lean

@@ -606,6 +606,21 @@ by rw [←nat.mod_add_div a c, ←nat.mod_add_div b c, ←h, ←nat.sub_sub, nat
 lemma dvd_sub_mod (k : ℕ) : n ∣ (k - (k % n)) :=
 ⟨k / n, nat.sub_eq_of_eq_add (nat.mod_add_div k n).symm⟩
 
+lemma add_mod (a b n : ℕ) : (a + b) % n = ((a % n) + (b % n)) % n :=
+begin
+  conv_lhs {
+    rw [←mod_add_div a n, ←mod_add_div b n, ←add_assoc, add_mul_mod_self_left,
+        add_assoc, add_comm _ (b % n), ←add_assoc, add_mul_mod_self_left] }
+end
+
+lemma mul_mod (a b n : ℕ) : (a * b) % n = ((a % n) * (b % n)) % n :=
+begin
+  conv_lhs {
+    rw [←mod_add_div a n, ←mod_add_div b n, right_distrib, left_distrib, left_distrib,
+        mul_assoc, mul_assoc, ←left_distrib n _ _, add_mul_mod_self_left,
+        mul_comm _ (n * (b / n)), mul_assoc, add_mul_mod_self_left] }
+end
+
 theorem add_pos_left {m : ℕ} (h : 0 < m) (n : ℕ) : 0 < m + n :=
 calc
   m + n > 0 + n : nat.add_lt_add_right h n

src/data/nat/modeq.lean

@@ -141,12 +141,6 @@ end)
 
 end modeq
 
-lemma add_mod (a b n : ℕ) : (a + b) % n = ((a % n) + (b % n)) % n :=
-(nat.modeq.modeq_add (nat.modeq.mod_modeq a n) (nat.modeq.mod_modeq b n)).symm
-
-lemma mul_mod (a b n : ℕ) : (a * b) % n = ((a % n) * (b % n)) % n :=
-(nat.modeq.modeq_mul (nat.modeq.mod_modeq a n) (nat.modeq.mod_modeq b n)).symm
-
 @[simp] lemma mod_mul_right_mod (a b c : ℕ) : a % (b * c) % b = a % b :=
 modeq.modeq_of_modeq_mul_right _ (modeq.mod_modeq _ _)
 

src/data/zmod/basic.lean

@@ -73,16 +73,6 @@ def comm_semigroup (n : ℕ) : comm_semigroup (fin (n+1)) :=
 
 local attribute [instance] fin.add_comm_semigroup fin.comm_semigroup
 
-lemma val_add {n : ℕ} : ∀ a b : fin n, (a + b).val = (a.val + b.val) % n
-| ⟨_, _⟩ ⟨_, _⟩ := rfl
-
-lemma val_mul {n : ℕ} :  ∀ a b : fin n, (a * b).val = (a.val * b.val) % n
-| ⟨_, _⟩ ⟨_, _⟩ := rfl
-
-lemma one_val {n : ℕ} : (1 : fin (n+1)).val = 1 % (n+1) := rfl
-
-@[simp] lemma zero_val (n : ℕ) : (0 : fin (n+1)).val = 0 := rfl
-
 private lemma one_mul_aux (n : ℕ) (a : fin (n+1)) : (1 : fin (n+1)) * a = a :=
 begin
   cases n with n,
@@ -124,17 +114,6 @@ def comm_ring (n : ℕ) : comm_ring (fin (n+1)) :=
   ..fin.add_comm_semigroup n,
   ..fin.comm_semigroup n }
 
-local attribute [instance] fin.add_comm_semigroup
-
-@[simp]
-lemma of_nat_eq_coe (n : ℕ) (a : ℕ) : (of_nat a : fin (n+1)) = a :=
-begin
-  induction a with a ih, { refl },
-  ext, show (a+1) % (n+1) = fin.val (a+1 : fin (n+1)),
-  { rw [fin.val_add, ← ih, of_nat],
-    exact nat.add_mod _ _ _ }
-end
-
 end fin
 
 /-- The integers modulo `n : ℕ`. -/