[Merged by Bors] - refactor(data/nat/factorization): Change definition of factorization to be computable

src/data/nat/factorization.lean

@@ -6,6 +6,7 @@ Authors: Stuart Presnell
 import data.nat.prime
 import data.finsupp.multiset
 import algebra.big_operators.finsupp
+import number_theory.padics.padic_norm
 import tactic.linarith
 
 /-!
@@ -42,7 +43,30 @@ namespace nat
 
 /-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
  mapping each prime factor of `n` to its multiplicity in `n`. -/
-noncomputable def factorization (n : ℕ) : ℕ →₀ ℕ := (n.factors : multiset ℕ).to_finsupp
+def factorization (n : ℕ) : ℕ →₀ ℕ :=
+{ support := n.factors.to_finset,
+  to_fun := λ p, if p.prime then padic_val_nat p n else 0,
+  mem_support_to_fun :=
+    begin
+      intro a,
+      rw list.mem_to_finset,
+      by_cases hn0 : n = 0,
+      { sorry, },
+      rw mem_factors hn0,
+      simp only [ne.def, ite_eq_right_iff, exists_prop],
+      sorry,
+    end }
+
+
+lemma multiplicity_eq_factorization {n p : ℕ} (pp : p.prime) (hn : n ≠ 0) :
+  multiplicity p n = n.factorization p :=
+begin
+  have hdom : (multiplicity p n).dom,
+  { rw multiplicity.nat.multiplicity_dom_iff, split, exact hn, sorry, },
+  simp [factorization, pp],
+  rw part.get_or_else_of_dom (multiplicity p n) hdom,
+  simp,
+end
 
 /-! ### Basic facts about factorization -/
 

src/data/part.lean

@@ -193,13 +193,23 @@ otherwise. -/
 def get_or_else (a : part α) [decidable a.dom] (d : α) :=
 if ha : a.dom then a.get ha else d
 
+
+
 @[simp] lemma get_or_else_none (d : α) [decidable (none : part α).dom] : get_or_else none d = d :=
 dif_neg id
 
 @[simp] lemma get_or_else_some (a : α) (d : α) [decidable (some a).dom] :
   get_or_else (some a) d = a :=
 dif_pos trivial
 
+lemma get_or_else_of_dom (a : part α) (h : a.dom) [decidable a.dom] (d : α) :
+  get_or_else a d = a.get h :=
+begin
+  rw ←get_or_else_some (a.get h) d,
+  congr,
+  simp,
+end
+
 @[simp] theorem mem_to_option {o : part α} [decidable o.dom] {a : α} :
   a ∈ to_option o ↔ a ∈ o :=
 begin

src/number_theory/padics/padic_norm.lean

@@ -9,7 +9,7 @@ import ring_theory.int.basic
 import tactic.basic
 import tactic.ring_exp
 import number_theory.divisors
-import data.nat.factorization
+-- import data.nat.factorization
 
 /-!
 # p-adic norm
@@ -473,34 +473,34 @@ protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
       { exact hc } },
   end
 
-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,
-  simp [@multiplicity_eq_factorization n p hp.elim hn],
-end
+-- 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,
+--   simp [@multiplicity_eq_factorization n p hp.elim hn],
+-- end
 
 open_locale big_operators
 
-lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :
-  ∏ p in finset.filter nat.prime (finset.range m), p ^ (padic_val_nat p n) = n :=
-begin
-  nth_rewrite_rhs 0 ←factorization_prod_pow_eq_self hn,
-  rw eq_comm,
-  apply finset.prod_subset_one_on_sdiff,
-  { exact λ p hp, finset.mem_filter.mpr
-      ⟨finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
-       prime_of_mem_factorization hp⟩ },
-  { intros p hp,
-    cases finset.mem_sdiff.mp hp with hp1 hp2,
-    haveI := fact_iff.mpr (finset.mem_filter.mp hp1).2,
-    rw padic_val_nat_eq_factorization p n,
-    simp [finsupp.not_mem_support_iff.mp hp2] },
-  { intros p hp,
-    haveI := fact_iff.mpr (prime_of_mem_factorization hp),
-    simp [padic_val_nat_eq_factorization] }
-end
+-- lemma prod_pow_prime_padic_val_nat (n : nat) (hn : n ≠ 0) (m : nat) (pr : n < m) :
+--   ∏ p in finset.filter nat.prime (finset.range m), p ^ (padic_val_nat p n) = n :=
+-- begin
+--   nth_rewrite_rhs 0 ←factorization_prod_pow_eq_self hn,
+--   rw eq_comm,
+--   apply finset.prod_subset_one_on_sdiff,
+--   { exact λ p hp, finset.mem_filter.mpr
+--       ⟨finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
+--        prime_of_mem_factorization hp⟩ },
+--   { intros p hp,
+--     cases finset.mem_sdiff.mp hp with hp1 hp2,
+--     haveI := fact_iff.mpr (finset.mem_filter.mp hp1).2,
+--     rw padic_val_nat_eq_factorization p n,
+--     simp [finsupp.not_mem_support_iff.mp hp2] },
+--   { intros p hp,
+--     haveI := fact_iff.mpr (prime_of_mem_factorization hp),
+--     simp [padic_val_nat_eq_factorization] }
+-- end
 
 lemma range_pow_padic_val_nat_subset_divisors {n : ℕ} (p : ℕ) [fact p.prime] (hn : n ≠ 0) :
   (finset.range (padic_val_nat p n + 1)).image (pow p) ⊆ n.divisors :=

src/ring_theory/multiplicity.lean

@@ -6,7 +6,8 @@ Authors: Robert Y. Lewis, Chris Hughes
 import algebra.associated
 import algebra.big_operators.basic
 import ring_theory.valuation.basic
-import data.nat.factorization
+-- import data.nat.factorization
+import data.nat.log
 
 /-!
 # Multiplicity of a divisor
@@ -486,8 +487,4 @@ begin
   exact hp this
 end
 
-lemma multiplicity_eq_factorization {n p : ℕ} (pp : p.prime) (hn : n ≠ 0) :
-  multiplicity p n = n.factorization p :=
-multiplicity.eq_coe_iff.mpr ⟨pow_factorization_dvd n p, pow_succ_factorization_not_dvd hn pp⟩
-
 end nat