exactly_divides.lean

import data.nat.prime

open nat

-- local attribute [trans] dvd_trans

-- Definition
def exactly_divides (p : ℕ) (r : ℕ) (n : ℕ) := p^r ∣ n ∧ ¬(p^(succ r) ∣ n)

notation p`^`r `∣∣`:50 n:50 := exactly_divides p r n

section
variable {p : ℕ}

-- Equivalent definitions
lemma exactly_divides' {r : ℕ} {n : ℕ} : p^r ∣∣ n ↔ (∀ i, p^i ∣ n ↔ i ≤ r) :=
begin
  apply iff.intro,
  { intros prn i, apply iff.intro,
    { intro pin,
      apply (le_or_gt _ _).resolve_right, intro i_gt_r,
      exact absurd (dvd_trans (pow_dvd_pow p i_gt_r) pin) prn.right },
    { intro i_le_r,
      exact dvd.trans (pow_dvd_pow p i_le_r) (and.left prn) }
    },
  { intro h, split,
    { exact (h r).mpr (refl r) },
    { exact mt (h (succ r)).mp (not_succ_le_self r) }
  }
end

lemma exactly_divides'' {r : ℕ} {n : ℕ} (p_pos : p > 0) :
  p^r ∣∣ n ↔ ∃ k, n = p^r * k ∧ ¬(p ∣ k) :=
begin
  apply iff.intro,
  { intro prn,
    existsi n / (p^r), split,
    { exact (nat.mul_div_cancel' prn.left).symm },
    { intro d,
      have :=
      calc p^(succ r) = p^r * p            : rfl
           ...        ∣ p^r * (n / (p^r))  : mul_dvd_mul_left (p^r) d
           ...        = n                  : nat.mul_div_cancel' prn.left,
      have := prn.right, contradiction
    }
  },
  { intro h, rcases h with ⟨k, h1, h2⟩, split,
    { exact ⟨k,h1⟩ },
    { intro d,
      rw h1 at d,
      have : p ∣ k := dvd_of_mul_dvd_mul_left (pos_pow_of_pos r p_pos) d,
      contradiction
    }
  }
end

-- Uniqueness
lemma exactly_divides_unique {r s : ℕ} {n : ℕ} : p^r ∣∣ n → p^s ∣∣ n → r = s :=
λ prn psn,
have ri : ∀ i, p^i ∣ n ↔ i ≤ r := exactly_divides'.mp prn,
have si : ∀ i, p^i ∣ n ↔ i ≤ s := exactly_divides'.mp psn,
have this : ∀ i, i ≤ r ↔ i ≤ s := λ i, (ri i).symm.trans (si i),
le_antisymm ((this r).mp (le_refl r)) ((this s).mpr (le_refl s))

-- Recursion relations
lemma exactly_divides_zero {n : ℕ} (p_pos : p > 0) : ¬(p ∣ n) ↔ p^0 ∣∣ n :=
begin
  rw exactly_divides'' p_pos,
  apply iff.intro,
  { intro h, exact ⟨n, by simp, h⟩ },
  { intro h, rcases h with ⟨k, e, nd⟩, simp [e, nd] }
end

lemma exactly_divides_succ {r n : ℕ} (p_pos : p > 0) : p^r ∣∣ n ↔ p^(succ r) ∣∣ (p * n) :=
begin
  rw [exactly_divides'' p_pos, exactly_divides'' p_pos],
  apply iff.intro,
  {
    intro prn,
    rcases prn with ⟨k, h1, h2⟩,
    have h1' : p * n = p^(succ r) * k :=
    calc p * n = p * (p^r * k)  : by rw h1
         ...   = (p^r * p) * k  : by ac_refl,
    exact ⟨k, h1', h2⟩,
  },
  {
    intro psrpn,
    rcases psrpn with ⟨k, h1, h2⟩,
    have h1' : p * n = p * (p^r * k) :=
    calc p * n = p^(succ r) * k  : h1
         ...   = p * (p^r * k)   : by unfold nat.pow; ac_refl,
    exact ⟨k, eq_of_mul_eq_mul_left p_pos h1', h2⟩
  }
end


-- Multiplicative
lemma exactly_divides_one (hp : prime p) : p^0 ∣∣ 1 :=
(exactly_divides_zero (hp.gt_one.trans dec_trivial)).mp (prime.not_dvd_one hp)

lemma exactly_divides_mul {r s a b : ℕ} (hp : prime p) : p^r ∣∣ a → p^s ∣∣ b → p^(r+s) ∣∣ a*b :=
begin
  intros pra psb,
  rw exactly_divides'' (hp.gt_one.trans dec_trivial) at ⊢ pra psb,
  rcases pra with ⟨ka, ha1, ha2⟩,
  rcases psb with ⟨kb, hb1, hb2⟩,
  existsi ka * kb, split,
  { exact calc a * b = (p^r * ka) * (p^s * kb)  : by rw [ha1, hb1]
               ...   = (p^r * p^s) * (ka * kb)  : by ac_refl
               ...   = p^(r+s) * (ka * kb)      : by rw pow_add },
  { exact prime.not_dvd_mul hp ha2 hb2 }
end

lemma exactly_divides_pow {r k a : ℕ} (hp : prime p) : p^r ∣∣ a → p^(k * r) ∣∣ a^k :=
mul_comm r k ▸
  λ pra, nat.rec_on k
           (exactly_divides_one hp)
           (λ k' ih, (exactly_divides_mul hp ih pra))

-- Gcd
lemma dvd_gcd_iff {a b k : ℕ} : k ∣ gcd a b ↔ k ∣ a ∧ k ∣ b :=
iff.intro (λ d, ⟨dvd_trans d (gcd_dvd a b).left,
                 dvd_trans d (gcd_dvd a b).right⟩)
          (λ p, and.elim p dvd_gcd)

lemma exactly_divides_gcd {r s a b : ℕ} : p^r ∣∣ a → p^s ∣∣ b → p^(min r s) ∣∣ gcd a b :=
begin
  intros pra psb,
  rw exactly_divides' at ⊢ pra psb,
  intro i,
  exact calc p^i ∣ gcd a b ↔ p^i ∣ a ∧ p^i ∣ b  : dvd_gcd_iff
             ...           ↔ i ≤ r ∧ i ≤ s      : and_congr (pra i) (psb i)
             ...           ↔ i ≤ min r s        : le_min_iff.symm
end

end

order.lean

import data.nat.prime
import data.pnat

import data.nat.exactly_divides

open nat

namespace order

section raw_order

variables (p : ℕ) (hp : p > 1)

protected def order_core : Π (n : ℕ), n > 0 → {r // p^r ∣∣ n}
| 0       := λ n_pos, absurd n_pos dec_trivial
| n@(k+1) := λ n_pos,
  have n / p < n, from div_lt_self n_pos hp,
  if h : p ∣ n
  then
    have p * (n / p) = n, from nat.mul_div_cancel' h,
    let ⟨s, hs⟩ :=
      order_core (n / p)
        (pos_of_mul_pos_left (this.symm ▸ n_pos : 0 < p * (n / p)) dec_trivial)
    in ⟨succ s, this ▸ (exactly_divides_succ (hp.trans dec_trivial)).mp hs⟩
  else ⟨0, (exactly_divides_zero (hp.trans dec_trivial)).mp h⟩

def order (n : ℕ) (n_pos : n > 0) : ℕ := (order.order_core p hp n n_pos).val

lemma exactly_divides_order (n : ℕ) (n_pos : n > 0) :
  p^(order p hp n n_pos) ∣∣ n :=
(order.order_core p hp n n_pos).property


end raw_order

/- XXX comments -/

instance : has_dvd ℕ+ := ⟨λ a b, a.val ∣ b.val⟩

def 𝓟 := {p : ℕ // prime p}
notation `PP` := 𝓟

def 𝓟.gt_one (p : 𝓟) : p.val > 1 := p.property.gt_one
def 𝓟.pos (p : 𝓟) : p.val > 0 := p.property.pos

instance : has_coe 𝓟 ℕ+ := ⟨λ p, ⟨p.val, p.pos⟩⟩

def ord (p : 𝓟) (n : ℕ+) : ℕ := order p p.gt_one n n.property
def exactly_divides_ord {p : 𝓟} {n : ℕ+} : p^(ord p n) ∣∣ n :=
exactly_divides_order p p.gt_one n n.property
def exactly_divides_iff_ord {p : 𝓟} {r : ℕ} {n : ℕ+} : ord p n = r ↔ p^r ∣∣ n :=
iff.intro
  (λ e, e ▸ exactly_divides_ord)
  (exactly_divides_unique exactly_divides_ord)

variable {p : 𝓟}

-- Recursion (though we prove them in a round-about fashion)

lemma ord_not_div {n : ℕ+} : ¬(↑p ∣ n) ↔ ord p n = 0 :=
(exactly_divides_zero p.pos).trans exactly_divides_iff_ord.symm

lemma ord_div {n : ℕ+} : ord p (p * n) = succ (ord p n) :=
exactly_divides_iff_ord.mpr
((exactly_divides_succ p.pos).mp exactly_divides_ord)

-- Multiplicative

lemma ord_one : ord p 1 = 0 :=
exactly_divides_iff_ord.mpr (exactly_divides_one p.property)

lemma ord_mul (a b : ℕ+) : ord p (a * b) = ord p a + ord p b :=
exactly_divides_iff_ord.mpr
(exactly_divides_mul p.property
  exactly_divides_ord exactly_divides_ord)

lemma ord_ppow {k : ℕ} {a : ℕ+} : ord p (pnat.pow a k) = k * ord p a :=
exactly_divides_iff_ord.mpr
(exactly_divides_pow p.property exactly_divides_ord)

lemma ord_pow {k : ℕ} {a : ℕ+} : ord p (a^k) = k * ord p a :=
have pnat.pow a k = a^k, from (pnat.coe_nat_coe _).symm, this ▸ ord_ppow

-- Gcd

def pgcd (a b : ℕ+) : ℕ+ := ⟨gcd a b, gcd_pos_of_pos_left b a.pos⟩

lemma ord_pgcd {a b : ℕ+} : ord p (pgcd a b) = min (ord p a) (ord p b) :=
exactly_divides_iff_ord.mpr
(exactly_divides_gcd
  exactly_divides_ord exactly_divides_ord)

lemma ord_gcd {a b : ℕ+} : ord p (gcd a b) = min (ord p a) (ord p b) :=
have pgcd a b = gcd a b, from (pnat.coe_nat_coe _).symm, this ▸ ord_pgcd

end order