refactor(library/theories/number_theory/primes): add some minor theorems, and rename some theorems

library/theories/number_theory/primes.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Jeremy Avigad
 
-Prime numbers
+Prime numbers.
 -/
 import data.nat logic.identities
 open bool
@@ -33,6 +33,12 @@ decidable_of_decidable_of_iff _ (prime_ext_iff_prime p)
 lemma ge_two_of_prime {p : nat} : prime p → p ≥ 2 :=
 assume h, obtain h₁ h₂, from h, h₁
 
+theorem gt_one_of_prime {p : ℕ} (primep : prime p) : p > 1 :=
+lt_of_succ_le (ge_two_of_prime primep)
+
+theorem pos_of_prime {p : ℕ} (primep : prime p) : p > 0 :=
+lt.trans zero_lt_one (gt_one_of_prime primep)
+
 lemma not_prime_zero : ¬ prime 0 :=
 λ h, absurd (ge_two_of_prime h) dec_trivial
 
@@ -51,9 +57,9 @@ have h₁ : p ≥ 2, from ge_two_of_prime h,
 lt_of_succ_le (pred_le_pred h₁)
 
 lemma succ_pred_prime {p : nat} : prime p → succ (pred p) = p :=
-assume h, succ_pred_of_pos (lt_of_succ_le (le_of_succ_le (ge_two_of_prime h)))
+assume h, succ_pred_of_pos (pos_of_prime h)
 
-lemma divisor_of_prime {p m : nat} : prime p → m ∣ p → m = 1 ∨ m = p :=
+lemma eq_one_or_eq_self_of_prime_of_dvd {p m : nat} : prime p → m ∣ p → m = 1 ∨ m = p :=
 assume h d, obtain h₁ h₂, from h, h₂ m d
 
 lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i :=
@@ -63,7 +69,7 @@ have h₂ : p ≥ 2, from ge_two_of_prime ipp,
 have h₃ : p ≤ i, from le_of_dvd pos h₁,
 lt_of_succ_le (le.trans h₂ h₃)
 
-theorem has_divisor_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
+theorem ex_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
 assume h₁ h₂,
 have h₃ : ¬ prime_ext n, from iff.mp' (not_iff_not_of_iff !prime_ext_iff_prime) h₂,
 have h₄ : ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not h₃,
@@ -76,10 +82,10 @@ obtain (h₈ : m ∣ n) (h₉ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_
 have h₁₀ : ¬ m = 1 ∧ ¬ m = n, from iff.mp !not_or_iff_not_and_not h₉,
 exists.intro m (and.intro h₈ h₁₀)
 
-theorem has_divisor_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
+theorem ex_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≥ 2 ∧ m < n :=
 assume h₁ h₂,
 have n_ne_0 : n ≠ 0, from assume h, begin subst n, exact absurd h₁ dec_trivial end,
-obtain m m_dvd_n m_ne_1 m_ne_n, from has_divisor_of_not_prime h₁ h₂,
+obtain m m_dvd_n m_ne_1 m_ne_n, from ex_dvd_of_not_prime h₁ h₂,
 assert m_ne_0 : m ≠ 0, from assume h, begin subst m, exact absurd (eq_zero_of_zero_dvd m_dvd_n) n_ne_0 end,
 begin
   existsi m, split, assumption,
@@ -89,7 +95,7 @@ begin
      exact lt_of_le_and_ne m_le_n m_ne_n}
 end
 
-theorem has_prime_divisor {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
+theorem ex_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
 nat.strong_induction_on n
   (take n,
    assume ih : ∀ m, m < n → m ≥ 2 → ∃ p, prime p ∧ p ∣ m,
@@ -97,7 +103,7 @@ nat.strong_induction_on n
    by_cases
     (λ h : prime n, exists.intro n (and.intro h (dvd.refl n)))
     (λ h : ¬ prime n,
-      obtain m m_dvd_n m_ge_2 m_lt_n, from has_divisor_of_not_prime2 n_ge_2 h,
+      obtain m m_dvd_n m_ge_2 m_lt_n, from ex_dvd_of_not_prime2 n_ge_2 h,
       obtain p (hp : prime p) (p_dvd_m : p ∣ m), from ih m m_lt_n m_ge_2,
       have p_dvd_n : p ∣ n, from dvd.trans p_dvd_m m_dvd_n,
       exists.intro p (and.intro hp p_dvd_n)))
@@ -109,7 +115,7 @@ let m := fact (n + 1) in
 have Hn1 : n + 1 ≥ 1, from succ_le_succ (zero_le _),
 have m_ge_1 : m ≥ 1,  from le_of_lt_succ (succ_lt_succ (fact_gt_0 _)),
 have m1_ge_2 : m + 1 ≥ 2, from succ_le_succ m_ge_1,
-obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from has_prime_divisor m1_ge_2,
+obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from ex_prime_and_dvd m1_ge_2,
 have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p,
 have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2),
 have p_ge_n : p ≥ n, from by_contradiction
@@ -127,26 +133,47 @@ lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=
   have even_p : even p, from even_of_not_odd hn,
   obtain k (hk : p = 2*k), from exists_of_even even_p,
   assert two_div_p : 2 ∣ p, by rewrite [hk]; apply dvd_mul_right,
-  or.elim (divisor_of_prime pp two_div_p)
+  or.elim (eq_one_or_eq_self_of_prime_of_dvd pp two_div_p)
     (λ h : 2 = 1, absurd h dec_trivial)
     (λ h : 2 = p, by subst h; exact absurd p_gt_2 !lt.irrefl))
 
-lemma coprime_of_prime_of_not_dvd {p n : nat} : prime p → ¬ p ∣ n → coprime p n :=
+theorem dvd_of_prime_of_not_coprime {p n : ℕ} (primep : prime p) (nc : ¬ coprime p n) : p ∣ n :=
-λ pp h₂,
+have H : gcd p n = 1 ∨ gcd p n = p, from eq_one_or_eq_self_of_prime_of_dvd primep !gcd_dvd_left,
-  assert d₁ : gcd p n ∣ p, from !gcd_dvd_left,
+or_resolve_right H nc ▸ !gcd_dvd_right
-  assert d₂ : gcd p n ∣ n, from !gcd_dvd_right,
+
-  or.elim (divisor_of_prime pp d₁)
+theorem coprime_of_prime_of_not_dvd {p n : ℕ} (primep : prime p) (npdvdn : ¬ p ∣ n) :
-    (λ h : gcd p n = 1, h)
+  coprime p n :=
-    (λ h : gcd p n = p,
+by_contradiction (assume nc : ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprime primep nc))
-      assert d₃ : p ∣ n, by rewrite -h; exact d₂,
+
-      by contradiction)
+theorem not_dvd_of_prime_of_coprime {p n : ℕ} (primep : prime p) (cop : coprime p n) : ¬ p ∣ n :=
+assume pdvdn : p ∣ n,
+have H1 : p ∣ gcd p n, from dvd_gcd !dvd.refl pdvdn,
+have H2 : p ≤ gcd p n, from le_of_dvd (!gcd_pos_of_pos_left (pos_of_prime primep)) H1,
+have H3 : 2 ≤ 1, from le.trans (ge_two_of_prime primep) (cop ▸ H2),
+show false, from !not_succ_le_self H3
+
+theorem not_coprime_of_prime_dvd {p n : ℕ} (primep : prime p) (pdvdn : p ∣ n) : ¬ coprime p n :=
+assume cop, not_dvd_of_prime_of_coprime primep cop pdvdn
+
+theorem dvd_of_prime_of_dvd_mul_left {p m n : ℕ} (primep : prime p)
+    (Hmn : p ∣ m * n) (Hm : ¬ p ∣ m) :
+  p ∣ n :=
+have copm : coprime p m, from coprime_of_prime_of_not_dvd primep Hm,
+show p ∣ n, from dvd_of_coprime_of_dvd_mul_left copm Hmn
+
+theorem dvd_of_prime_of_dvd_mul_right {p m n : ℕ} (primep : prime p)
+    (Hmn : p ∣ m * n) (Hn : ¬ p ∣ n) :
+  p ∣ m :=
+dvd_of_prime_of_dvd_mul_left primep (!mul.comm ▸ Hmn) Hn
+
+theorem not_dvd_mul_of_prime {p m n : ℕ} (primep : prime p) (Hm : ¬ p ∣ m) (Hn : ¬ p ∣ n) :
+  ¬ p ∣ m * n :=
+assume Hmn, Hm (dvd_of_prime_of_dvd_mul_right primep Hmn Hn)
 
 lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n → p ∣ m ∨ p ∣ n :=
-λ h₁ h₂, by_contradiction (λ h,
+λ h₁ h₂, by_cases
-  obtain (n₁ : ¬ p ∣ m) (n₂ : ¬ p ∣ n), from iff.mp !not_or_iff_not_and_not h,
+  (assume h : p ∣ m, or.inl h)
-  assert c₁ : coprime p m, from coprime_of_prime_of_not_dvd h₁ n₁,
+  (assume h : ¬ p ∣ m, or.inr (dvd_of_prime_of_dvd_mul_left h₁ h₂ h))
-  assert n₃ : p ∣ n, from dvd_of_coprime_of_dvd_mul_left c₁ h₂,
-  by contradiction)
 
 lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m
 | 0 hp hd :=
@@ -166,11 +193,11 @@ lemma coprime_primes {p q : nat} : prime p → prime q → p ≠ q → coprime p
 λ hp hq hn,
   assert d₁ : gcd p q ∣ p, from !gcd_dvd_left,
   assert d₂ : gcd p q ∣ q, from !gcd_dvd_right,
-  or.elim (divisor_of_prime hp d₁)
+  or.elim (eq_one_or_eq_self_of_prime_of_dvd hp d₁)
     (λ h : gcd p q = 1, h)
     (λ h : gcd p q = p,
       have d₃ : p ∣ q, by rewrite -h; exact d₂,
-      or.elim (divisor_of_prime hq d₃)
+      or.elim (eq_one_or_eq_self_of_prime_of_dvd hq d₃)
         (λ h₁ : p = 1, by subst p; exact absurd hp not_prime_one)
         (λ he : p = q, by contradiction))
 
@@ -182,12 +209,12 @@ by_cases
  (λ h : p ∣ i, or.inr h)
  (λ h : ¬ p ∣ i, or.inl (coprime_of_prime_of_not_dvd Pp h))
 
-lemma divisor_of_prime_pow {p : nat} : ∀ {m i : nat}, prime p → i ∣ (p^m) → i = 1 ∨ p ∣ i
+lemma eq_one_or_dvd_of_dvd_prime_pow {p : nat} : ∀ {m i : nat}, prime p → i ∣ (p^m) → i = 1 ∨ p ∣ i
 | 0        := take i, assume Pp, begin rewrite [pow_zero], intro Pdvd, apply or.inl (eq_one_of_dvd_one Pdvd) end
 | (succ m) := take i, assume Pp, or.elim (coprime_or_dvd_of_prime Pp i)
   (λ Pcp, begin
     rewrite [pow_succ], intro Pdvd,
-    apply divisor_of_prime_pow Pp,
+    apply eq_one_or_dvd_of_dvd_prime_pow Pp,
     apply dvd_of_coprime_of_dvd_mul_right,
       apply coprime_swap Pcp, exact Pdvd
   end)