[Merged by Bors] - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions

src/number_theory/padics/padic_norm.lean

@@ -51,6 +51,70 @@ open_locale rat
 
 open multiplicity
 
+def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
+if h : p ≠ 1 ∧ 0 < n
+then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h)
+else 0
+
+namespace padic_val_nat
+open multiplicity
+variables {p : ℕ}
+
+/--
+`padic_val_nat p 0` is 0 for any `p`.
+-/
+@[simp]
+protected lemma zero : padic_val_nat p 0 = 0 :=
+by simp [padic_val_nat]
+
+/--
+`padic_val_nat p 1` is 0 for any `p`.
+-/
+@[simp] protected lemma one : padic_val_nat p 1 = 0 :=
+by unfold padic_val_nat; split_ifs; simp *
+
+/--
+For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
+-/
+@[simp] lemma self (hp : 1 < p) : padic_val_nat p p = 1 :=
+begin
+  have neq_one : (¬ p = 1) ↔ true,
+  { exact iff_of_true ((ne_of_lt hp).symm) trivial, },
+  have eq_zero_false : (p = 0) ↔ false,
+  { exact iff_false_intro ((ne_of_lt (trans zero_lt_one hp)).symm) },
+  simp [padic_val_nat, neq_one, eq_zero_false],
+end
+
+end padic_val_nat
+
+def padic_val_int (p : ℕ) (z : ℤ) : ℕ :=
+padic_val_nat p (z.nat_abs)
+
+namespace padic_val_int
+open multiplicity
+variables {p : ℕ}
+
+/--
+`padic_val_int p 0` is 0 for any `p`.
+-/
+@[simp]
+protected lemma zero : padic_val_int p 0 = 0 :=
+by simp [padic_val_int]
+
+/--
+`padic_val_int p 1` is 0 for any `p`.
+-/
+@[simp] protected lemma one : padic_val_int p 1 = 0 :=
+by simp [padic_val_int]
+
+/--
+For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
+-/
+@[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
+by simp [padic_val_int, padic_val_nat.self hp]
+
+end padic_val_int
+
 /--
 For `p ≠ 1`, the p-adic valuation of an integer `z ≠ 0` is the largest natural number `n` such that
 p^n divides z.
@@ -60,21 +124,7 @@ valuation of `q.denom`.
 If `q = 0` or `p = 1`, then `padic_val_rat p q` defaults to 0.
 -/
 def padic_val_rat (p : ℕ) (q : ℚ) : ℤ :=
-if h : q ≠ 0 ∧ p ≠ 1
-then (multiplicity (p : ℤ) q.num).get
-    (multiplicity.finite_int_iff.2 ⟨h.2, rat.num_ne_zero_of_ne_zero h.1⟩) -
-  (multiplicity (p : ℤ) q.denom).get
-    (multiplicity.finite_int_iff.2 ⟨h.2, by exact_mod_cast rat.denom_ne_zero _⟩)
-else 0
-
-/--
-A simplification of the definition of `padic_val_rat p q` when `q ≠ 0` and `p` is prime.
--/
-lemma padic_val_rat_def (p : ℕ) [hp : fact p.prime] {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
-  (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp.1.ne_one, rat.num_ne_zero_of_ne_zero hq⟩) -
-  (multiplicity (p : ℤ) q.denom).get
-    (finite_int_iff.2 ⟨hp.1.ne_one, by exact_mod_cast rat.denom_ne_zero _⟩) :=
-dif_pos ⟨hq, hp.1.ne_one⟩
+padic_val_int p q.num - padic_val_nat p q.denom
 
 namespace padic_val_rat
 open multiplicity
@@ -84,49 +134,49 @@ variables {p : ℕ}
 `padic_val_rat p q` is symmetric in `q`.
 -/
 @[simp] protected lemma neg (q : ℚ) : padic_val_rat p (-q) = padic_val_rat p q :=
-begin
-  unfold padic_val_rat,
-  split_ifs,
-  { simp [-add_comm]; refl },
-  { exfalso, simp * at * },
-  { exfalso, simp * at * },
-  { refl }
-end
+by simp [padic_val_rat, padic_val_int]
 
 /--
 `padic_val_rat p 0` is 0 for any `p`.
 -/
 @[simp]
-protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := rfl
+protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat, padic_val_int]
 
 /--
 `padic_val_rat p 1` is 0 for any `p`.
 -/
-@[simp] protected lemma one : padic_val_rat p 1 = 0 :=
-by unfold padic_val_rat; split_ifs; simp *
+@[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
 /--
 For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
 -/
 @[simp] lemma padic_val_rat_self (hp : 1 < p) : padic_val_rat p p = 1 :=
-by unfold padic_val_rat; split_ifs; simp [*, nat.one_lt_iff_ne_zero_and_ne_one] at *
+begin
+  simp only [padic_val_rat, padic_val_int, rat.coe_nat_num, int.nat_abs_of_nat, rat.coe_nat_denom,
+    padic_val_nat.one, int.coe_nat_zero, sub_zero, padic_val_nat.self hp],
+  refl,
+end
 
 /--
 The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
 -/
 lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
-by rw [padic_val_rat, dif_pos]; simp *; refl
+begin
+  rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
+  simp_rw multiplicity.int.nat_abs,
+  simp only [rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num, int.coe_nat_inj',
+    sub_zero, multiplicity.get_one_right],
+  refl,
+  simp [hp],
+  simp [hp],
+  apply nat.pos_of_ne_zero,
+  simp [hz],
+end
 
 end padic_val_rat
 
-/--
-A convenience function for the case of `padic_val_rat` when both inputs are natural numbers.
--/
-def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
-int.to_nat (padic_val_rat p n)
-
 section padic_val_nat
 
 /--
@@ -135,48 +185,40 @@ this lemma ensures that the cast is well-behaved.
 -/
 lemma zero_le_padic_val_rat_of_nat (p n : ℕ) : 0 ≤ padic_val_rat p n :=
 begin
-  unfold padic_val_rat,
-  split_ifs,
-  { simp, },
-  { trivial, },
+  unfold padic_val_rat padic_val_int padic_val_nat,
+  split_ifs; simp,
 end
 
 /--
 `padic_val_rat` coincides with `padic_val_nat`.
 -/
 @[simp, norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :
   ↑(padic_val_nat p n) = padic_val_rat p n :=
-begin
-  unfold padic_val_nat,
-  rw int.to_nat_of_nonneg (zero_le_padic_val_rat_of_nat p n),
-end
+by simp [padic_val_rat, padic_val_int]
 
 /--
 A simplification of `padic_val_nat` when one input is prime, by analogy with `padic_val_rat_def`.
 -/
-lemma padic_val_nat_def {p : ℕ} [hp : fact p.prime] {n : ℕ} (hn : n ≠ 0) :
+lemma padic_val_nat_def {p : ℕ} [hp : fact p.prime] {n : ℕ} (hn : 0 < n) :
   padic_val_nat p n =
   (multiplicity p n).get
-    (multiplicity.finite_nat_iff.2 ⟨nat.prime.ne_one hp.1, bot_lt_iff_ne_bot.mpr hn⟩) :=
+    (multiplicity.finite_nat_iff.2 ⟨nat.prime.ne_one hp.1, hn⟩) :=
 begin
-  have n_nonzero : (n : ℚ) ≠ 0, by simpa only [cast_eq_zero, ne.def],
-  -- Infinite loop with @simp padic_val_rat_of_nat unless we restrict the available lemmas here,
-  -- hence the very long list
-  simpa only
-    [ int.coe_nat_multiplicity p n, rat.coe_nat_denom n, (padic_val_rat_of_nat p n).symm,
-      int.coe_nat_zero, int.coe_nat_inj', sub_zero, get_one_right, int.coe_nat_succ, zero_add,
-      rat.coe_nat_num ]
-    using padic_val_rat_def p n_nonzero,
+  simp [padic_val_nat],
+  split_ifs,
+  { refl, },
+  { exfalso,
+    apply h ⟨(hp.out).ne_one, hn⟩, }
 end
 
 @[simp] lemma padic_val_nat_self (p : ℕ) [fact p.prime] : padic_val_nat p p = 1 :=
-by simp [padic_val_nat_def (fact.out p.prime).ne_zero]
+by simp [padic_val_nat_def (fact.out p.prime).pos]
 
 lemma one_le_padic_val_nat_of_dvd
-  {n p : nat} [prime : fact p.prime] (nonzero : n ≠ 0) (div : p ∣ n) :
+  {n p : nat} [prime : fact p.prime] (n_pos : 0 < n) (div : p ∣ n) :
   1 ≤ padic_val_nat p n :=
 begin
-  rw @padic_val_nat_def _ prime _ nonzero,
+  rw @padic_val_nat_def _ prime _ n_pos,
   let one_le_mul : _ ≤ multiplicity p n :=
     @multiplicity.le_multiplicity_of_pow_dvd _ _ _ p n 1 (begin norm_num, exact div end),
   simp only [nat.cast_one] at one_le_mul,
@@ -185,12 +227,6 @@ begin
   solve_by_elim,
 end
 
-@[simp]
-lemma padic_val_nat_zero (m : nat) : padic_val_nat m 0 = 0 := rfl
-
-@[simp]
-lemma padic_val_nat_one (m : nat) : padic_val_nat m 1 = 0 := by simp [padic_val_nat]
-
 end padic_val_nat
 
 namespace padic_val_rat
@@ -215,9 +251,27 @@ protected lemma defn {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = n /. d) :
 have hn : n ≠ 0, from rat.mk_num_ne_zero_of_ne_zero hqz qdf,
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hn hd qdf in
-by rw [padic_val_rat, dif_pos];
+begin
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
-    (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz]
+    (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz],
+  rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
+  simp_rw [int.coe_nat_multiplicity p q.denom],
+  simp_rw multiplicity.int.nat_abs,
+  refl,
+  split,
+  { exact nat.prime.ne_one p_prime.out, },
+  { apply nat.pos_of_ne_zero,
+    intro hq,
+    simp [hq] at hc2,
+    exact hd hc2, },
+  split,
+  { exact nat.prime.ne_one p_prime.out, },
+  { apply nat.pos_of_ne_zero,
+    intro hq,
+    simp only [int.nat_abs_eq_zero] at hq,
+    simp [hq] at hc1,
+    exact hn hc1, },
+end
 
 /--
 A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`.
@@ -415,7 +469,7 @@ lemma padic_val_nat_of_not_dvd {p : ℕ} [fact p.prime] {n : ℕ} (not_dvd : ¬(
 begin
   by_cases hn : n = 0,
   { subst hn, simp at not_dvd, trivial, },
-  { rw padic_val_nat_def hn,
+  { rw padic_val_nat_def (nat.pos_of_ne_zero hn),
     exact (@multiplicity.unique' _ _ _ p n 0 (by simp) (by simpa using not_dvd)).symm,
     assumption, },
 end
@@ -434,7 +488,7 @@ begin
   { rw hn, exact dvd_zero (p ^ padic_val_nat p 0) },
   { rw multiplicity.pow_dvd_iff_le_multiplicity,
     apply le_of_eq,
-    rw padic_val_nat_def (ne_of_gt hn),
+    rw padic_val_nat_def hn,
     { apply enat.coe_get },
     { apply_instance } }
 end
@@ -443,10 +497,11 @@ lemma pow_succ_padic_val_nat_not_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn :
   ¬ p ^ (padic_val_nat p n + 1) ∣ n :=
 begin
   { rw multiplicity.pow_dvd_iff_le_multiplicity,
-    rw padic_val_nat_def (ne_of_gt hn),
+    rw padic_val_nat_def hn,
     { rw [nat.cast_add, enat.coe_get],
       simp only [nat.cast_one, not_le],
-      apply enat.lt_add_one (ne_top_iff_finite.2 (finite_nat_iff.2 ⟨hp.elim.ne_one, hn⟩)) },
+      exact enat.lt_add_one (ne_top_iff_finite.mpr
+        (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, hn⟩)), },
     { apply_instance } }
 end
 
@@ -477,7 +532,7 @@ lemma padic_val_nat_eq_factorization (p n : ℕ) [hp : fact p.prime] :
   padic_val_nat p n = n.factorization p :=
 begin
   by_cases hn : n = 0, { subst hn, simp },
-  rw @padic_val_nat_def p _ n hn,
+  rw @padic_val_nat_def p _ n (nat.pos_of_ne_zero hn),
   simp [@multiplicity_eq_factorization n p hp.elim hn],
 end
 

src/ring_theory/multiplicity.lean

@@ -57,6 +57,18 @@ begin
     apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
 end
 
+example (a b : ℤ) : a ∣ b ↔ a ∣ b.nat_abs := int.dvd_nat_abs.symm
+
+theorem nat_cast_nat_abs (a b : ℕ) :
+    multiplicity a (b : ℤ).nat_abs = multiplicity (a : ℤ) (b : ℤ) :=
+begin
+  apply part.ext',
+  { repeat { rw [← finite_iff_dom, finite_def] },
+    norm_cast },
+  { intros h1 h2,
+    apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
+end
+
 lemma not_finite_iff_forall {a b : α} : (¬ finite a b) ↔ ∀ n : ℕ, a ^ n ∣ b :=
 ⟨λ h n, nat.cases_on n (by { rw pow_zero, exact one_dvd _ }) (by simpa [finite, not_not] using h),
   by simp [finite, multiplicity, not_not]; tauto⟩
@@ -287,6 +299,19 @@ part.ext' (by simp only [multiplicity, enat.find, dvd_neg])
     eq.symm (unique ((dvd_neg _ _).2 (pow_multiplicity_dvd _))
       (mt (dvd_neg _ _).1 (is_greatest' _ (lt_succ_self _))))))
 
+theorem int.nat_abs (a : ℕ) (b : ℤ) :
+    multiplicity a b.nat_abs = multiplicity (a : ℤ) b :=
+begin
+  have h := @int.nat_abs_eq_iff b b.nat_abs,
+  simp only [true_iff, eq_self_iff_true] at h,
+  cases h,
+  { conv_rhs { rw h },
+   apply nat_cast_nat_abs, },
+  { conv_rhs { rw h },
+    rw multiplicity.neg,
+    apply nat_cast_nat_abs, },
+end
+
 lemma multiplicity_add_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) :
   multiplicity p (a + b) = multiplicity p b :=
 begin