chore(algebra, data/pnat): refactoring comm_semiring_has_dvd into comm_monoid_has_dvd (#3702)

changes the instance comm_semiring_has_dvd to apply to any comm_monoid
cleans up the pnat API to use this new definition

Author: awainverse

src/algebra/divisibility.lean

@@ -0,0 +1,92 @@
+import algebra.group_with_zero
+
+variables {α : Type*}
+
+section comm_monoid
+
+variables [comm_monoid α] {a b c : α}
+
+@[priority 100]
+instance comm_monoid_has_dvd : has_dvd α :=
+has_dvd.mk (λ a b, ∃ c, b = a * c)
+
+-- TODO: this used to not have c explicit, but that seems to be important
+--       for use with tactics, similar to exist.intro
+theorem dvd.intro (c : α) (h : a * c = b) : a ∣ b :=
+exists.intro c h^.symm
+
+alias dvd.intro ← dvd_of_mul_right_eq
+
+theorem dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
+dvd.intro _ (begin rewrite mul_comm at h, apply h end)
+
+alias dvd.intro_left ← dvd_of_mul_left_eq
+
+theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c := h
+
+theorem dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P :=
+exists.elim H₁ H₂
+
+theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
+dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
+
+theorem dvd.elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
+exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃)
+
+@[refl, simp] theorem dvd_refl (a : α) : a ∣ a :=
+dvd.intro 1 (by simp)
+
+local attribute [simp] mul_assoc mul_comm mul_left_comm
+
+@[trans] theorem dvd_trans (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
+match h₁, h₂ with
+| ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ :=
+  ⟨d * e, show c = a * (d * e), by simp [h₃, h₄]⟩
+end
+
+alias dvd_trans ← dvd.trans
+
+@[simp] theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (by simp)
+
+@[simp] theorem dvd_mul_right (a b : α) : a ∣ a * b := dvd.intro b rfl
+
+@[simp] theorem dvd_mul_left (a b : α) : a ∣ b * a := dvd.intro b (by simp)
+
+theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
+dvd.elim h (λ d h', begin rw [h', mul_assoc], apply dvd_mul_right end)
+
+theorem dvd_mul_of_dvd_right (h : a ∣ b) (c : α) : a ∣ c * b :=
+begin rw mul_comm, exact dvd_mul_of_dvd_left h _ end
+
+theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
+| a ._ c ._ ⟨e, rfl⟩ ⟨f, rfl⟩ := ⟨e * f, by simp⟩
+
+theorem mul_dvd_mul_left (a : α) {b c : α} (h : b ∣ c) : a * b ∣ a * c :=
+mul_dvd_mul (dvd_refl a) h
+
+theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
+mul_dvd_mul h (dvd_refl c)
+
+theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
+dvd.elim h (begin intros d h₁, rw [h₁, mul_assoc], apply dvd_mul_right end)
+
+theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
+dvd.elim h (λ d ceq, dvd.intro (a * d) (by simp [ceq]))
+
+end comm_monoid
+
+section comm_monoid_with_zero
+
+variables [comm_monoid_with_zero α] {a : α}
+
+theorem eq_zero_of_zero_dvd (h : 0 ∣ a) : a = 0 :=
+dvd.elim h (assume c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
+
+/-- Given an element a of a commutative monoid with zero, there exists another element whose product
+    with zero equals a iff a equals zero. -/
+@[simp] lemma zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
+⟨eq_zero_of_zero_dvd, λ h, by rw h⟩
+
+@[simp] theorem dvd_zero (a : α) : a ∣ 0 := dvd.intro 0 (by simp)
+
+end comm_monoid_with_zero

src/algebra/ring/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland
 -/
-import algebra.group_with_zero
+import algebra.divisibility
 import data.set.basic
 
 /-!
@@ -378,85 +378,9 @@ lemma add_mul_self_eq (a b : α) : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
 calc (a + b)*(a + b) = a*a + (1+1)*a*b + b*b : by simp [add_mul, mul_add, mul_comm, add_assoc]
               ...     = a*a + 2*a*b + b*b    : by rw one_add_one_eq_two
 
-instance comm_semiring_has_dvd : has_dvd α :=
-has_dvd.mk (λ a b, ∃ c, b = a * c)
-
--- TODO: this used to not have c explicit, but that seems to be important
---       for use with tactics, similar to exist.intro
-theorem dvd.intro (c : α) (h : a * c = b) : a ∣ b :=
-exists.intro c h^.symm
-
-alias dvd.intro ← dvd_of_mul_right_eq
-
-theorem dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
-dvd.intro _ (begin rewrite mul_comm at h, apply h end)
-
-alias dvd.intro_left ← dvd_of_mul_left_eq
-
-theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c := h
-
-theorem dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P :=
-exists.elim H₁ H₂
-
-theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
-dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
-
-theorem dvd.elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
-exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃)
-
-@[refl, simp] theorem dvd_refl (a : α) : a ∣ a :=
-dvd.intro 1 (by simp)
-
-local attribute [simp] mul_assoc mul_comm mul_left_comm
-
-@[trans] theorem dvd_trans (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
-match h₁, h₂ with
-| ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ :=
-  ⟨d * e, show c = a * (d * e), by simp [h₃, h₄]⟩
-end
-
-alias dvd_trans ← dvd.trans
-
-theorem eq_zero_of_zero_dvd (h : 0 ∣ a) : a = 0 :=
-dvd.elim h (assume c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
-
-/-- Given an element a of a commutative semiring, there exists another element whose product
-    with zero equals a iff a equals zero. -/
-@[simp] lemma zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
-⟨eq_zero_of_zero_dvd, λ h, by rw h⟩
-
-@[simp] theorem dvd_zero (a : α) : a ∣ 0 := dvd.intro 0 (by simp)
-
-@[simp] theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (by simp)
-
-@[simp] theorem dvd_mul_right (a b : α) : a ∣ a * b := dvd.intro b rfl
-
-@[simp] theorem dvd_mul_left (a b : α) : a ∣ b * a := dvd.intro b (by simp)
-
-theorem dvd_mul_of_dvd_left (h : a ∣ b) (c : α) : a ∣ b * c :=
-dvd.elim h (λ d h', begin rw [h', mul_assoc], apply dvd_mul_right end)
-
-theorem dvd_mul_of_dvd_right (h : a ∣ b) (c : α) : a ∣ c * b :=
-begin rw mul_comm, exact dvd_mul_of_dvd_left h _ end
-
-theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
-| a ._ c ._ ⟨e, rfl⟩ ⟨f, rfl⟩ := ⟨e * f, by simp⟩
-
-theorem mul_dvd_mul_left (a : α) {b c : α} (h : b ∣ c) : a * b ∣ a * c :=
-mul_dvd_mul (dvd_refl a) h
-
-theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
-mul_dvd_mul h (dvd_refl c)
-
 theorem dvd_add (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
 dvd.elim h₁ (λ d hd, dvd.elim h₂ (λ e he, dvd.intro (d + e) (by simp [left_distrib, hd, he])))
 
-theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
-dvd.elim h (begin intros d h₁, rw [h₁, mul_assoc], apply dvd_mul_right end)
-
-theorem dvd_of_mul_left_dvd (h : a * b ∣ c) : b ∣ c :=
-dvd.elim h (λ d ceq, dvd.intro (a * d) (by simp [ceq]))
-
 @[simp] theorem two_dvd_bit0 : 2 ∣ bit0 a := ⟨a, bit0_eq_two_mul _⟩
 
 lemma ring_hom.map_dvd (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=

src/data/pnat/basic.lean

@@ -286,13 +286,16 @@ begin
   { exact ⟨nat.mod_le (m : ℕ) (k : ℕ), le_of_lt (nat.mod_lt (m : ℕ) k.pos)⟩ }
 end
 
-instance : has_dvd ℕ+ := ⟨λ k m, (k : ℕ) ∣ (m : ℕ)⟩
-
-theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) := by {refl}
+theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) :=
+begin
+  split; intro h, rcases h with ⟨_, rfl⟩, apply dvd_mul_right,
+  rcases h with ⟨a, h⟩, cases a, { contrapose h, apply ne_zero, },
+  use a.succ, apply nat.succ_pos, rw [← coe_inj, h, mul_coe, mk_coe],
+end
 
 theorem dvd_iff' {k m : ℕ+} : k ∣ m ↔ mod m k = k :=
 begin
-  change (k : ℕ) ∣ (m : ℕ) ↔ mod m k = k,
+  rw dvd_iff,
   rw [nat.dvd_iff_mod_eq_zero], split,
   { intro h, apply eq, rw [mod_coe, if_pos h] },
   { intro h, by_cases h' : (m : ℕ) % (k : ℕ) = 0,
@@ -315,24 +318,8 @@ begin
  rw [mod_add_div m k, dvd_iff'.mp h, nat.mul_succ, add_comm],
 end
 
-theorem dvd_iff'' {k n : ℕ+} : k ∣ n ↔ ∃ m, k * m = n :=
-⟨λ h, ⟨div_exact h, mul_div_exact h⟩,
- λ ⟨m, h⟩, dvd.intro (m : ℕ)
-          ((mul_coe k m).symm.trans (congr_arg subtype.val h))⟩
-
-theorem dvd_intro {k n : ℕ+} (m : ℕ+) (h : k * m = n) : k ∣ n :=
- dvd_iff''.mpr ⟨m, h⟩
-
-@[simp]
-theorem dvd_refl (m : ℕ+) : m ∣ m := dvd_intro 1 (mul_one m)
-
 theorem dvd_antisymm {m n : ℕ+} : m ∣ n → n ∣ m → m = n :=
-λ hmn hnm, subtype.eq (nat.dvd_antisymm hmn hnm)
-
-protected theorem dvd_trans {k m n : ℕ+} : k ∣ m → m ∣ n → k ∣ n :=
-@dvd_trans ℕ _ (k : ℕ) (m : ℕ) (n : ℕ)
-
-theorem one_dvd (n : ℕ+) : 1 ∣ n := dvd_intro n (one_mul n)
+λ hmn hnm, le_antisymm (le_of_dvd hmn) (le_of_dvd hnm)
 
 theorem dvd_one_iff (n : ℕ+) : n ∣ 1 ↔ n = 1 :=
  ⟨λ h, dvd_antisymm h (one_dvd n), λ h, h.symm ▸ (dvd_refl 1)⟩
@@ -350,19 +337,19 @@ def lcm (n m : ℕ+) : ℕ+ :=
 
 @[simp] theorem lcm_coe (n m : ℕ+) : ((lcm n m) : ℕ) = nat.lcm n m := rfl
 
-theorem gcd_dvd_left (n m : ℕ+) : (gcd n m) ∣ n := nat.gcd_dvd_left (n : ℕ) (m : ℕ)
+theorem gcd_dvd_left (n m : ℕ+) : (gcd n m) ∣ n := dvd_iff.2 (nat.gcd_dvd_left (n : ℕ) (m : ℕ))
 
-theorem gcd_dvd_right (n m : ℕ+) : (gcd n m) ∣ m := nat.gcd_dvd_right (n : ℕ) (m : ℕ)
+theorem gcd_dvd_right (n m : ℕ+) : (gcd n m) ∣ m := dvd_iff.2 (nat.gcd_dvd_right (n : ℕ) (m : ℕ))
 
 theorem dvd_gcd {m n k : ℕ+} (hm : k ∣ m) (hn : k ∣ n) : k ∣ gcd m n :=
- @nat.dvd_gcd (m : ℕ) (n : ℕ) (k : ℕ) hm hn
+ dvd_iff.2 (@nat.dvd_gcd (m : ℕ) (n : ℕ) (k : ℕ) (dvd_iff.1 hm) (dvd_iff.1 hn))
 
-theorem dvd_lcm_left  (n m : ℕ+) : n ∣ lcm n m := nat.dvd_lcm_left  (n : ℕ) (m : ℕ)
+theorem dvd_lcm_left  (n m : ℕ+) : n ∣ lcm n m := dvd_iff.2 (nat.dvd_lcm_left  (n : ℕ) (m : ℕ))
 
-theorem dvd_lcm_right (n m : ℕ+) : m ∣ lcm n m := nat.dvd_lcm_right (n : ℕ) (m : ℕ)
+theorem dvd_lcm_right (n m : ℕ+) : m ∣ lcm n m := dvd_iff.2 (nat.dvd_lcm_right (n : ℕ) (m : ℕ))
 
 theorem lcm_dvd {m n k : ℕ+} (hm : m ∣ k) (hn : n ∣ k) : lcm m n ∣ k :=
- @nat.lcm_dvd (m : ℕ) (n : ℕ) (k : ℕ) hm hn
+  dvd_iff.2 (@nat.lcm_dvd (m : ℕ) (n : ℕ) (k : ℕ) (dvd_iff.1 hm) (dvd_iff.1 hn))
 
 theorem gcd_mul_lcm (n m : ℕ+) : (gcd n m) * (lcm n m) = n * m :=
  subtype.eq (nat.gcd_mul_lcm (n : ℕ) (m : ℕ))
@@ -393,12 +380,12 @@ by { intro pp, intro contra, apply nat.prime.ne_one pp, rw pnat.coe_eq_one_iff,
 lemma not_prime_one : ¬ (1: ℕ+).prime :=  nat.not_prime_one
 
 lemma prime.not_dvd_one {p : ℕ+} :
-p.prime →  ¬ p ∣ 1 := λ pp : p.prime, nat.prime.not_dvd_one pp
+p.prime →  ¬ p ∣ 1 := λ pp : p.prime, by {rw dvd_iff, apply nat.prime.not_dvd_one pp}
 
 lemma exists_prime_and_dvd {n : ℕ+} : 2 ≤ n → (∃ (p : ℕ+), p.prime ∧ p ∣ n) :=
 begin
   intro h, cases nat.exists_prime_and_dvd h with p hp,
-  existsi (⟨p, nat.prime.pos hp.left⟩ : ℕ+), apply hp
+  existsi (⟨p, nat.prime.pos hp.left⟩ : ℕ+), rw dvd_iff, apply hp
 end
 
 end prime

src/data/pnat/factors.lean

@@ -274,7 +274,7 @@ begin
   split,
   { intro h,
     rw [← prod_factor_multiset m, ← prod_factor_multiset m],
-    apply dvd_intro (n.factor_multiset - m.factor_multiset).prod,
+    apply dvd.intro (n.factor_multiset - m.factor_multiset).prod,
     rw [← prime_multiset.prod_add, prime_multiset.factor_multiset_prod,
         prime_multiset.add_sub_of_le h, prod_factor_multiset] },
   { intro  h,

src/data/pnat/xgcd.lean

@@ -323,16 +323,12 @@ begin
   rcases gcd_props a b with ⟨h₀, h₁, h₂, h₃, h₄, h₅, h₆⟩,
   apply dvd_antisymm,
   { apply dvd_gcd,
-    exact dvd_intro (gcd_a' a b) (h₁.trans (mul_comm _ _)).symm,
-    exact dvd_intro (gcd_b' a b) (h₂.trans (mul_comm _ _)).symm},
-  { have h₇ := calc
-     ((gcd a b) : ℕ) ∣ a : nat.gcd_dvd_left a b
-      ... ∣ (gcd_z a b) * a : dvd_mul_left _ _,
-    have h₈ := calc
-     ((gcd a b) : ℕ) ∣ b : nat.gcd_dvd_right a b
-      ... ∣ (gcd_x a b) * b : dvd_mul_left _ _,
-   rw[h₅] at h₇,
-   exact (nat.dvd_add_iff_right h₈).mpr h₇}
+    exact dvd.intro (gcd_a' a b) (h₁.trans (mul_comm _ _)).symm,
+    exact dvd.intro (gcd_b' a b) (h₂.trans (mul_comm _ _)).symm},
+  { have h₇ : (gcd a b : ℕ) ∣ (gcd_z a b) * a := dvd_trans (nat.gcd_dvd_left a b) (dvd_mul_left _ _),
+    have h₈ : (gcd a b : ℕ) ∣ (gcd_x a b) * b := dvd_trans (nat.gcd_dvd_right a b) (dvd_mul_left _ _),
+    rw[h₅] at h₇, rw dvd_iff,
+    exact (nat.dvd_add_iff_right h₈).mpr h₇,}
 end
 
 theorem gcd_det_eq :