feat(data/nat/modeq): Generalised version of the Chinese remainder theorem (#5683)

That allows the moduli to not be coprime, assuming the necessary condition. Old crt is now in terms of this one

Author: alexjbest

src/algebra/euclidean_domain.lean

@@ -230,6 +230,12 @@ def gcd_a (x y : R) : R := (xgcd x y).1
 /-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
 def gcd_b (x y : R) : R := (xgcd x y).2
 
+@[simp] theorem gcd_a_zero_left {s : R} : gcd_a 0 s = 0 :=
+by { unfold gcd_a, rw [xgcd, xgcd_zero_left] }
+
+@[simp] theorem gcd_b_zero_left {s : R} : gcd_b 0 s = 1 :=
+by { unfold gcd_b, rw [xgcd, xgcd_zero_left] }
+
 @[simp] theorem xgcd_aux_fst (x y : R) : ∀ s t s' t',
   (xgcd_aux x s t y s' t').1 = gcd x y :=
 gcd.induction x y (by intros; rw [xgcd_zero_left, gcd_zero_left])

src/data/int/basic.lean

@@ -699,6 +699,9 @@ protected theorem mul_div_assoc (a : ℤ) : ∀ {b c : ℤ}, c ∣ b → (a * b)
 | ._ c ⟨d, rfl⟩ := if cz : c = 0 then by simp [cz] else
   by rw [mul_left_comm, int.mul_div_cancel_left _ cz, int.mul_div_cancel_left _ cz]
 
+protected theorem mul_div_assoc' (b : ℤ) {a c : ℤ} (h : c ∣ a) : a * b / c = a / c * b :=
+by rw [mul_comm, int.mul_div_assoc _ h, mul_comm]
+
 theorem div_dvd_div : ∀ {a b c : ℤ} (H1 : a ∣ b) (H2 : b ∣ c), b / a ∣ c / a
 | a ._ ._ ⟨b, rfl⟩ ⟨c, rfl⟩ := if az : a = 0 then by simp [az] else
   by rw [int.mul_div_cancel_left _ az, mul_assoc, int.mul_div_cancel_left _ az];
@@ -736,6 +739,16 @@ theorem neg_div_of_dvd : ∀ {a b : ℤ} (H : b ∣ a), -a / b = -(a / b)
 | ._ b ⟨c, rfl⟩ := if bz : b = 0 then by simp [bz] else
   by rw [neg_mul_eq_mul_neg, int.mul_div_cancel_left _ bz, int.mul_div_cancel_left _ bz]
 
+lemma sub_div_of_dvd {a b c : ℤ} (hcb : c ∣ b) : (a - b) / c = a / c - b / c :=
+begin
+  rw [sub_eq_add_neg, sub_eq_add_neg, int.add_div_of_dvd_right ((dvd_neg c b).mpr hcb)],
+  congr,
+  exact neg_div_of_dvd hcb,
+end
+
+lemma sub_div_of_dvd_sub {a b c : ℤ} (hcab : c ∣ (a - b)) : (a - b) / c = a / c - b / c :=
+by rw [eq_sub_iff_add_eq, ← int.add_div_of_dvd_left hcab, sub_add_cancel]
+
 theorem div_sign : ∀ a b, a / sign b = a * sign b
 | a (n+1:ℕ) := by unfold sign; simp
 | a 0       := by simp [sign]

src/data/int/gcd.lean

@@ -46,6 +46,28 @@ def gcd_a (x y : ℕ) : ℤ := (xgcd x y).1
 /-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
 def gcd_b (x y : ℕ) : ℤ := (xgcd x y).2
 
+@[simp] theorem gcd_a_zero_left {s : ℕ} : gcd_a 0 s = 0 :=
+by { unfold gcd_a, rw [xgcd, xgcd_zero_left] }
+
+@[simp] theorem gcd_b_zero_left {s : ℕ} : gcd_b 0 s = 1 :=
+by { unfold gcd_b, rw [xgcd, xgcd_zero_left] }
+
+@[simp] theorem gcd_a_zero_right {s : ℕ} (h : s ≠ 0) : gcd_a s 0 = 1 :=
+begin
+  unfold gcd_a xgcd,
+  induction s,
+  { exact absurd rfl h, },
+  { simp [xgcd_aux], }
+end
+
+@[simp] theorem gcd_b_zero_right {s : ℕ} (h : s ≠ 0) : gcd_b s 0 = 0 :=
+begin
+  unfold gcd_b xgcd,
+  induction s,
+  { exact absurd rfl h, },
+  { simp [xgcd_aux], }
+end
+
 @[simp] theorem xgcd_aux_fst (x y) : ∀ s t s' t',
   (xgcd_aux x s t y s' t').1 = gcd x y :=
 gcd.induction x y (by simp) (λ x y h IH s t s' t', by simp [xgcd_aux_rec, h, IH]; rw ← gcd_rec)

src/data/nat/gcd.lean

@@ -139,21 +139,36 @@ by rw [gcd_comm m n, gcd_gcd_self_left_right]
 lemma gcd_add_mul_self (m n k : ℕ) : gcd m (n + k * m) = gcd m n :=
 by simp [gcd_rec m (n + k * m), gcd_rec m n]
 
+theorem gcd_eq_zero_iff {i j : ℕ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
+begin
+  split,
+  { intro h,
+    exact ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩, },
+  { intro h,
+    rw [h.1, h.2],
+    exact nat.gcd_zero_right _ }
+end
+
 /-! ### `lcm` -/
 
 theorem lcm_comm (m n : ℕ) : lcm m n = lcm n m :=
 by delta lcm; rw [mul_comm, gcd_comm]
 
+@[simp]
 theorem lcm_zero_left (m : ℕ) : lcm 0 m = 0 :=
 by delta lcm; rw [zero_mul, nat.zero_div]
 
+@[simp]
 theorem lcm_zero_right (m : ℕ) : lcm m 0 = 0 := lcm_comm 0 m ▸ lcm_zero_left m
 
+@[simp]
 theorem lcm_one_left (m : ℕ) : lcm 1 m = m :=
 by delta lcm; rw [one_mul, gcd_one_left, nat.div_one]
 
+@[simp]
 theorem lcm_one_right (m : ℕ) : lcm m 1 = m := lcm_comm 1 m ▸ lcm_one_left m
 
+@[simp]
 theorem lcm_self (m : ℕ) : lcm m m = m :=
 or.elim (eq_zero_or_pos m)
   (λh, by rw [h, lcm_zero_left])
@@ -184,6 +199,9 @@ dvd_antisymm
     (dvd.trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
     (lcm_dvd (dvd.trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k)) (dvd_lcm_right (lcm m n) k)))
 
+theorem lcm_ne_zero {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 :=
+by { intro h, simpa [h, hm, hn] using gcd_mul_lcm m n, }
+
 /-!
 ### `coprime`
 

src/data/nat/modeq.lean

@@ -105,31 +105,45 @@ by rw [modeq_iff_dvd] at *; exact dvd.trans (dvd_mul_left (n : ℤ) (m : ℤ)) h
 theorem modeq_of_modeq_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] :=
 mul_comm m n ▸ modeq_of_modeq_mul_left _
 
+theorem modeq_one : a ≡ b [MOD 1] := modeq_of_dvd $ one_dvd _
+
 local attribute [semireducible] int.nonneg
 
+/-- The natural number less than `lcm n m` congruent to `a` mod `n` and `b` mod `m` -/
+def chinese_remainder' (h : a ≡ b [MOD gcd n m]) : {k // k ≡ a [MOD n] ∧ k ≡ b [MOD m]} :=
+if hn : n = 0 then ⟨a, begin rw [hn, gcd_zero_left] at h, split, refl, exact h end⟩ else
+if hm : m = 0 then ⟨b, begin rw [hm, gcd_zero_right] at h, split, exact h.symm, refl end⟩ else
+⟨let (c, d) := xgcd n m in int.to_nat (((n * c * b + m * d * a) / gcd n m) % lcm n m), begin
+  rw xgcd_val,
+  dsimp [chinese_remainder'._match_1],
+  rw [modeq_iff_dvd, modeq_iff_dvd,
+    int.to_nat_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero.2 (lcm_ne_zero hn hm)))],
+  have hnonzero : (gcd n m : ℤ) ≠ 0 := begin
+    norm_cast,
+    rw [nat.gcd_eq_zero_iff, not_and],
+    exact λ _, hm,
+  end,
+  have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := λ t, dvd_mul_of_dvd_right h.dvd_of_modeq _,
+  have := gcd_eq_gcd_ab n m,
+  split; rw [int.mod_def, ← sub_add]; refine dvd_add _ (dvd_mul_of_dvd_left _ _); try {norm_cast},
+  { rw ← sub_eq_iff_eq_add' at this,
+    rw [← this, sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← mul_sub,
+      int.add_div_of_dvd_left, int.mul_div_cancel_left _ hnonzero, int.mul_div_assoc _ h.dvd_of_modeq,
+      ← sub_sub, sub_self, zero_sub, dvd_neg, mul_assoc],
+    exact dvd_mul_right _ _,
+    norm_cast, exact dvd_mul_right _ _, },
+  { exact dvd_lcm_left n m, },
+  { rw ← sub_eq_iff_eq_add at this,
+    rw [← this, sub_mul, sub_add, ← mul_sub, int.sub_div_of_dvd, int.mul_div_cancel_left _ hnonzero,
+      int.mul_div_assoc _ h.dvd_of_modeq, ← sub_add, sub_self, zero_add, mul_assoc],
+    exact dvd_mul_right _ _,
+    exact hcoedvd _ },
+  { exact dvd_lcm_right n m, },
+end⟩
+
 /-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m` -/
 def chinese_remainder (co : coprime n m) (a b : ℕ) : {k // k ≡ a [MOD n] ∧ k ≡ b [MOD m]} :=
-⟨let (c, d) := xgcd n m in int.to_nat ((b * c * n + a * d * m) % (n * m)), begin
-  rw xgcd_val, dsimp [chinese_remainder._match_1],
-  rw [modeq_iff_dvd, modeq_iff_dvd],
-  rw [int.to_nat_of_nonneg], swap,
-  { by_cases h₁ : n = 0, {simp [coprime, h₁] at co, substs m n, simp},
-    by_cases h₂ : m = 0, {simp [coprime, h₂] at co, substs m n, simp},
-    exact int.mod_nonneg _
-      (mul_ne_zero (int.coe_nat_ne_zero.2 h₁) (int.coe_nat_ne_zero.2 h₂)) },
-  have := gcd_eq_gcd_ab n m, simp [co.gcd_eq_one, mul_comm] at this,
-  rw [int.mod_def, ← sub_add, ← sub_add]; split,
-  { refine dvd_add _ (dvd_trans (dvd_mul_right _ _) (dvd_mul_right _ _)),
-    rw [add_comm, ← sub_sub], refine _root_.dvd_sub _ (dvd_mul_left _ _),
-    have := congr_arg ((*) ↑a) this,
-    exact ⟨_, by rwa [mul_add, ← mul_assoc, ← mul_assoc, mul_one, mul_comm,
-        ← sub_eq_iff_eq_add] at this⟩ },
-  { refine dvd_add _ (dvd_trans (dvd_mul_left _ _) (dvd_mul_right _ _)),
-    rw [← sub_sub], refine _root_.dvd_sub _ (dvd_mul_left _ _),
-    have := congr_arg ((*) ↑b) this,
-    exact ⟨_, by rwa [mul_add, ← mul_assoc, ← mul_assoc, mul_one, mul_comm _ ↑m,
-        ← sub_eq_iff_eq_add'] at this⟩ }
-end⟩
+chinese_remainder' (by convert modeq_one)
 
 lemma modeq_and_modeq_iff_modeq_mul {a b m n : ℕ} (hmn : coprime m n) :
   a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ (a ≡ b [MOD m * n]) :=