refactor(data/int/gcd): move int gcd proofs to the GCD theory

Author: johoelzl

data/int/basic.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
 
 The integers, with addition, multiplication, and subtraction.
 -/
-import data.nat.prime algebra.char_zero algebra.order_functions
+import data.nat.basic algebra.char_zero algebra.order_functions
 open nat
 
 namespace int
@@ -125,23 +125,6 @@ by cases n; refl
 theorem nat_abs_mul (a b : ℤ) : nat_abs (a * b) = (nat_abs a) * (nat_abs b) :=
 by cases a; cases b; simp [(*), int.mul, nat_abs_neg_of_nat]
 
-theorem nat_abs_div (a b : ℤ) (H : b ∣ a) : nat_abs (a / b) = (nat_abs a) / (nat_abs b) :=
-begin
-  cases (nat.eq_zero_or_pos (nat_abs b)),
-  rw eq_zero_of_nat_abs_eq_zero h,
-  simp,
-  calc 
-  nat_abs (a / b) = nat_abs (a / b) * 1 : by rw mul_one
-    ... = nat_abs (a / b) * (nat_abs b / nat_abs b) : by rw nat.div_self h
-    ... = nat_abs (a / b) * nat_abs b / nat_abs b : by rw (nat.mul_div_assoc _ (dvd_refl _))
-    ... = nat_abs (a / b * b) / nat_abs b : by rw (nat_abs_mul (a / b) b)
-    ... = nat_abs a / nat_abs b : by rw int.div_mul_cancel H,
-end
-
-theorem nat_abs_dvd_abs_iff {i j : ℤ} : i.nat_abs ∣ j.nat_abs ↔ i ∣ j :=
-⟨assume (H : i.nat_abs ∣ j.nat_abs), dvd_nat_abs.mp (nat_abs_dvd.mp (coe_nat_dvd.mpr H)), 
-assume H : (i ∣ j), coe_nat_dvd.mp (dvd_nat_abs.mpr (nat_abs_dvd.mpr H))⟩
-
 theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=
 by simp [neg_succ_of_nat_eq]
 
@@ -613,18 +596,6 @@ begin
       exact hdiv }
 end
 
-lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n : ℤ} {k l : ℕ}
-      (hpm : ↑(p ^ k) ∣ m)
-      (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k+l+1)) ∣ m*n) : ↑(p ^ (k+1)) ∣ m ∨ ↑(p ^ (l+1)) ∣ n :=
-have hpm' : p ^ k ∣ m.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpm,
-have hpn' : p ^ l ∣ n.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpn,
-have hpmn' : (p ^ (k+l+1)) ∣ m.nat_abs*n.nat_abs,
-  by rw ←int.nat_abs_mul; apply (int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpmn),
-let hsd := nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn' in
-hsd.elim
-  (λ hsd1, or.inl begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd1 end)
-  (λ hsd2, or.inr begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd2 end)
-
 /- / and ordering -/
 
 protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a :=
@@ -1136,57 +1107,3 @@ by simp [abs]
 end cast
 
 end int
-
-/- extended euclidean algorithm -/
-namespace nat
-
-def xgcd_aux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
-| 0          s t r' s' t' := (r', s', t')
-| r@(succ _) s t r' s' t' :=
-  have r' % r < r, from mod_lt _ $ succ_pos _,
-  let q := r' / r in xgcd_aux (r' % r) (s' - q * s) (t' - q * t) r s t
-
-@[simp] theorem xgcd_zero_left {s t r' s' t'} : xgcd_aux 0 s t r' s' t' = (r', s', t') :=
-by simp [xgcd_aux]
-
-@[simp] theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) : xgcd_aux r s t r' s' t' = xgcd_aux (r' % r) (s' - (r' / r) * s) (t' - (r' / r) * t) r s t :=
-by cases r; [exact absurd h (lt_irrefl _), {simp only [xgcd_aux], refl}]
-
-/-- Use the extended GCD algorithm to generate the `a` and `b` values
-  satisfying `gcd x y = x * a + y * b`. -/
-def xgcd (x y : ℕ) : ℤ × ℤ := (xgcd_aux x 1 0 y 0 1).2
-
-/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
-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 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 [h, IH]; rw ← gcd_rec)
-
-theorem xgcd_aux_val (x y) : xgcd_aux x 1 0 y 0 1 = (gcd x y, xgcd x y) :=
-by rw [xgcd, ← xgcd_aux_fst x y 1 0 0 1]; cases xgcd_aux x 1 0 y 0 1; refl
-
-theorem xgcd_val (x y) : xgcd x y = (gcd_a x y, gcd_b x y) :=
-by unfold gcd_a gcd_b; cases xgcd x y; refl
-
-section
-parameters (a b : ℕ)
-
-private def P : ℕ × ℤ × ℤ → Prop | (r, s, t) := (r : ℤ) = a * s + b * t
-
-theorem xgcd_aux_P {r r'} : ∀ {s t s' t'}, P (r, s, t) → P (r', s', t') → P (xgcd_aux r s t r' s' t') :=
-gcd.induction r r' (by simp) $ λ x y h IH s t s' t' p p', begin
-  rw [xgcd_aux_rec h], refine IH _ p, dsimp [P] at *,
-  rw [int.mod_def], generalize : (y / x : ℤ) = k,
-  rw [p, p'], simp [mul_add, mul_comm, mul_left_comm]
-end
-
-theorem gcd_eq_gcd_ab : (gcd a b : ℤ) = a * gcd_a a b + b * gcd_b a b :=
-by have := @xgcd_aux_P a b a b 1 0 0 1 (by simp [P]) (by simp [P]);
-   rwa [xgcd_aux_val, xgcd_val] at this
-end
-
-end nat

data/int/gcd.lean

@@ -3,13 +3,101 @@ Copyright (c) 2018 Guy Leroy. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sangwoo Jo (aka Jason), Guy Leroy
 
-Lemmas and extended definitions and properties of gcd and lcm for integers.
+Greatest common divisor (gcd) and least common multiple (lcm) for integers.
 -/
+import data.int.basic data.nat.prime
 
-import data.int.basic data.nat.basic data.nat.gcd
+/- extended euclidean algorithm -/
+namespace nat
+
+def xgcd_aux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
+| 0          s t r' s' t' := (r', s', t')
+| r@(succ _) s t r' s' t' :=
+  have r' % r < r, from mod_lt _ $ succ_pos _,
+  let q := r' / r in xgcd_aux (r' % r) (s' - q * s) (t' - q * t) r s t
+
+@[simp] theorem xgcd_zero_left {s t r' s' t'} : xgcd_aux 0 s t r' s' t' = (r', s', t') :=
+by simp [xgcd_aux]
+
+@[simp] theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) : xgcd_aux r s t r' s' t' = xgcd_aux (r' % r) (s' - (r' / r) * s) (t' - (r' / r) * t) r s t :=
+by cases r; [exact absurd h (lt_irrefl _), {simp only [xgcd_aux], refl}]
+
+/-- Use the extended GCD algorithm to generate the `a` and `b` values
+  satisfying `gcd x y = x * a + y * b`. -/
+def xgcd (x y : ℕ) : ℤ × ℤ := (xgcd_aux x 1 0 y 0 1).2
+
+/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
+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 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 [h, IH]; rw ← gcd_rec)
+
+theorem xgcd_aux_val (x y) : xgcd_aux x 1 0 y 0 1 = (gcd x y, xgcd x y) :=
+by rw [xgcd, ← xgcd_aux_fst x y 1 0 0 1]; cases xgcd_aux x 1 0 y 0 1; refl
+
+theorem xgcd_val (x y) : xgcd x y = (gcd_a x y, gcd_b x y) :=
+by unfold gcd_a gcd_b; cases xgcd x y; refl
+
+section
+parameters (a b : ℕ)
+
+private def P : ℕ × ℤ × ℤ → Prop | (r, s, t) := (r : ℤ) = a * s + b * t
+
+theorem xgcd_aux_P {r r'} : ∀ {s t s' t'}, P (r, s, t) → P (r', s', t') → P (xgcd_aux r s t r' s' t') :=
+gcd.induction r r' (by simp) $ λ x y h IH s t s' t' p p', begin
+  rw [xgcd_aux_rec h], refine IH _ p, dsimp [P] at *,
+  rw [int.mod_def], generalize : (y / x : ℤ) = k,
+  rw [p, p'], simp [mul_add, mul_comm, mul_left_comm]
+end
+
+theorem gcd_eq_gcd_ab : (gcd a b : ℤ) = a * gcd_a a b + b * gcd_b a b :=
+by have := @xgcd_aux_P a b a b 1 0 0 1 (by simp [P]) (by simp [P]);
+   rwa [xgcd_aux_val, xgcd_val] at this
+end
+
+end nat
 
 namespace int
 
+theorem nat_abs_div (a b : ℤ) (H : b ∣ a) : nat_abs (a / b) = (nat_abs a) / (nat_abs b) :=
+begin
+  cases (nat.eq_zero_or_pos (nat_abs b)),
+  rw eq_zero_of_nat_abs_eq_zero h,
+  simp,
+  calc
+  nat_abs (a / b) = nat_abs (a / b) * 1 : by rw mul_one
+    ... = nat_abs (a / b) * (nat_abs b / nat_abs b) : by rw nat.div_self h
+    ... = nat_abs (a / b) * nat_abs b / nat_abs b : by rw (nat.mul_div_assoc _ (dvd_refl _))
+    ... = nat_abs (a / b * b) / nat_abs b : by rw (nat_abs_mul (a / b) b)
+    ... = nat_abs a / nat_abs b : by rw int.div_mul_cancel H,
+end
+
+theorem nat_abs_dvd_abs_iff {i j : ℤ} : i.nat_abs ∣ j.nat_abs ↔ i ∣ j :=
+⟨assume (H : i.nat_abs ∣ j.nat_abs), dvd_nat_abs.mp (nat_abs_dvd.mp (coe_nat_dvd.mpr H)),
+assume H : (i ∣ j), coe_nat_dvd.mp (dvd_nat_abs.mpr (nat_abs_dvd.mpr H))⟩
+
+lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n : ℤ} {k l : ℕ}
+      (hpm : ↑(p ^ k) ∣ m)
+      (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k+l+1)) ∣ m*n) : ↑(p ^ (k+1)) ∣ m ∨ ↑(p ^ (l+1)) ∣ n :=
+have hpm' : p ^ k ∣ m.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpm,
+have hpn' : p ^ l ∣ n.nat_abs, from int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpn,
+have hpmn' : (p ^ (k+l+1)) ∣ m.nat_abs*n.nat_abs,
+  by rw ←int.nat_abs_mul; apply (int.coe_nat_dvd.1 $ int.dvd_nat_abs.2 hpmn),
+let hsd := nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn' in
+hsd.elim
+  (λ hsd1, or.inl begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd1 end)
+  (λ hsd2, or.inr begin apply int.dvd_nat_abs.1, apply int.coe_nat_dvd.2 hsd2 end)
+
+theorem dvd_of_mul_dvd_mul_left {i j k : ℤ} (k_non_zero : k ≠ 0) (H : k * i ∣ k * j) : i ∣ j :=
+dvd.elim H (λl H1, by rw mul_assoc at H1; exact ⟨_, eq_of_mul_eq_mul_left k_non_zero H1⟩)
+
+theorem dvd_of_mul_dvd_mul_right {i j k : ℤ} (k_non_zero : k ≠ 0) (H : i * k ∣ j * k) : i ∣ j :=
+by rw [mul_comm i k, mul_comm j k] at H; exact dvd_of_mul_dvd_mul_left k_non_zero H
+
 /- gcd -/
 
 @[simp] theorem gcd_self (i : ℤ) : gcd i i = nat_abs i :=
@@ -20,21 +108,21 @@ by cases i; simp [gcd, mod_self]
 @[simp] theorem gcd_zero_right (i : ℤ) : gcd i 0 = nat_abs i :=
 by cases i; simp [gcd]
 
-theorem gcd_dvd_left (i j : ℤ) : (gcd i j : ℤ) ∣ i := 
+theorem gcd_dvd_left (i j : ℤ) : (gcd i j : ℤ) ∣ i :=
 dvd_nat_abs.mp (coe_nat_dvd.mpr (nat.gcd_dvd_left (nat_abs i) (nat_abs j)))
 
 theorem gcd_dvd_right (i j : ℤ) : (gcd i j : ℤ) ∣ j :=
 dvd_nat_abs.mp (coe_nat_dvd.mpr (nat.gcd_dvd_right (nat_abs i) (nat_abs j)))
 
-theorem gcd_dvd (i j : ℤ) : ((gcd i j : ℤ) ∣ i) ∧ ((gcd i j : ℤ) ∣ j) := 
+theorem gcd_dvd (i j : ℤ) : ((gcd i j : ℤ) ∣ i) ∧ ((gcd i j : ℤ) ∣ j) :=
 ⟨gcd_dvd_left i j, gcd_dvd_right i j⟩
 
 theorem dvd_gcd {i j k : ℤ} : k ∣ i → k ∣ j → k ∣ gcd i j :=
-by intros H1 H2; 
-exact nat_abs_dvd.mp (coe_nat_dvd.mpr (nat.dvd_gcd (nat_abs_dvd_abs_iff.mpr H1) 
+by intros H1 H2;
+exact nat_abs_dvd.mp (coe_nat_dvd.mpr (nat.dvd_gcd (nat_abs_dvd_abs_iff.mpr H1)
                                                    (nat_abs_dvd_abs_iff.mpr H2)))
 
-theorem gcd_comm (i j : ℤ) : gcd i j = gcd j i := 
+theorem gcd_comm (i j : ℤ) : gcd i j = gcd j i :=
 nat.gcd_comm (nat_abs i) (nat_abs j)
 
 theorem gcd_assoc (i j k : ℤ) : gcd (gcd i j) k = gcd i (gcd j k) :=
@@ -46,11 +134,11 @@ nat.gcd_assoc (nat_abs i) (nat_abs j) (nat_abs k)
 eq.trans (gcd_comm i 1) $ gcd_one_left i
 
 theorem gcd_mul_left (i j k : ℤ) : gcd (i * j) (i * k) = nat_abs i * gcd j k :=
-by rw [gcd, nat_abs_mul, nat_abs_mul]; 
+by rw [gcd, nat_abs_mul, nat_abs_mul];
 exact nat.gcd_mul_left (nat_abs i) (nat_abs j) (nat_abs k)
 
-theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * nat_abs j := 
-by rw [gcd, nat_abs_mul, nat_abs_mul]; 
+theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * nat_abs j :=
+by rw [gcd, nat_abs_mul, nat_abs_mul];
 exact nat.gcd_mul_right (nat_abs i) (nat_abs j) (nat_abs k)
 
 theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : gcd i j > 0 :=
@@ -113,15 +201,15 @@ theorem lcm_zero_right (i : ℤ) : lcm i 0 = 0 := lcm_comm 0 i ▸ lcm_zero_left
 theorem lcm_one_left (i : ℤ) : lcm 1 i = nat_abs i :=
 by rw [lcm, one_mul, gcd_one_left, nat.div_one]
 
-theorem lcm_one_right (i : ℤ) : lcm i 1 = nat_abs i := 
+theorem lcm_one_right (i : ℤ) : lcm i 1 = nat_abs i :=
 by unfold lcm; simp
 
 theorem lcm_self (i : ℤ) : lcm i i = nat_abs i :=
-by rw [lcm, gcd_self, nat_abs_mul, nat.mul_div_assoc, mul_comm, nat.div_mul_cancel]; 
+by rw [lcm, gcd_self, nat_abs_mul, nat.mul_div_assoc, mul_comm, nat.div_mul_cancel];
 simp; simp
 
 theorem dvd_lcm_left (i j : ℤ) : i ∣ lcm i j :=
-nat_abs_dvd.mp (coe_nat_dvd.mpr (eq.subst (eq.symm (lcm_def i j)) 
+nat_abs_dvd.mp (coe_nat_dvd.mpr (eq.subst (eq.symm (lcm_def i j))
                                           (nat.dvd_lcm_left (nat_abs i) (nat_abs j))))
 
 theorem dvd_lcm_right (i j : ℤ) : j ∣ lcm i j :=
@@ -130,26 +218,17 @@ lcm_comm j i ▸ dvd_lcm_left j i
 theorem gcd_mul_lcm (i j : ℤ) : gcd i j * lcm i j = nat_abs (i * j) :=
 begin
   rw [lcm, mul_comm, nat.div_mul_cancel],
-  exact eq.subst (eq.symm (nat_abs_mul i j)) 
+  exact eq.subst (eq.symm (nat_abs_mul i j))
                  (dvd_mul_of_dvd_left (coe_nat_dvd.mp (dvd_nat_abs.mpr (gcd_dvd_left i j))) _),
 end
 
 theorem lcm_dvd {i j k : ℤ} (H1 : i ∣ k) (H2 : j ∣ k) : (lcm i j : ℤ) ∣ k :=
-dvd_nat_abs.mp (coe_nat_dvd.mpr (eq.subst (eq.symm (lcm_def i j)) 
+dvd_nat_abs.mp (coe_nat_dvd.mpr (eq.subst (eq.symm (lcm_def i j))
                                           (nat.lcm_dvd (nat_abs_dvd_abs_iff.mpr H1)
                                                        (nat_abs_dvd_abs_iff.mpr H2))))
 
 theorem lcm_assoc (i j k : ℤ) : lcm (lcm i j) k = lcm i (lcm j k) :=
 by rw [lcm_def, lcm_def, lcm_def, lcm_def];
 exact nat.lcm_assoc (nat_abs i) (nat_abs j) (nat_abs k)
 
-/- lemmas -/
-
-theorem dvd_of_mul_dvd_mul_left {i j k : ℤ} (k_non_zero : k ≠ 0) (H : k * i ∣ k * j) : i ∣ j :=
-dvd.elim H (λl H1, by rw mul_assoc at H1; exact ⟨_, eq_of_mul_eq_mul_left k_non_zero H1⟩)
-
-theorem dvd_of_mul_dvd_mul_right {i j k : ℤ} (k_non_zero : k ≠ 0) (H : i * k ∣ j * k) : i ∣ j :=
-by rw [mul_comm i k, mul_comm j k] at H; exact dvd_of_mul_dvd_mul_left k_non_zero H
-
-
 end int

data/nat/modeq.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 
 Modular equality relation.
 -/
-import data.int.basic data.nat.gcd
+import data.int.gcd
 
 namespace nat
 

data/padics/padic_norm.lean

@@ -6,7 +6,7 @@ Authors: Robert Y. Lewis
 Define the p-adic valuation on ℤ and ℚ, and the p-adic norm on ℚ
 -/
 
-import data.rat data.int.basic algebra.field_power
+import data.rat data.int.gcd algebra.field_power
 import tactic.wlog tactic.ring
 
 universe u

data/zmod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Chris Hughes
 -/
-import data.int.modeq data.fintype data.nat.prime data.nat.gcd data.pnat
+import data.int.modeq data.int.gcd data.fintype data.pnat
 
 open nat nat.modeq int