feat(data/polynomial): rec_on_horner

Author: ChrisHughes24

src/data/polynomial.lean

@@ -45,6 +45,8 @@ def X : polynomial α := single 1 1
 /-- coeff p n is the coefficient of X^n in p -/
 def coeff (p : polynomial α) := p.to_fun
 
+@[simp] lemma coeff_mk (s) (f) (h) : coeff (finsupp.mk s f h : polynomial α) = f := rfl
+
 instance [has_repr α] : has_repr (polynomial α) :=
 ⟨λ p, if p = 0 then "0"
   else (p.support.sort (≤)).foldr
@@ -67,6 +69,8 @@ def degree (p : polynomial α) : with_bot ℕ := p.support.sup some
 def degree_lt_wf : well_founded (λp q : polynomial α, degree p < degree q) :=
 inv_image.wf degree (with_bot.well_founded_lt nat.lt_wf)
 
+instance : has_well_founded (polynomial α) := ⟨_, degree_lt_wf⟩
+
 /-- `nat_degree p` forces `degree p` to ℕ, by defining nat_degree 0 = 0. -/
 def nat_degree (p : polynomial α) : ℕ := (degree p).get_or_else 0
 
@@ -80,7 +84,6 @@ lemma single_eq_C_mul_X : ∀{n}, single n a = C a * X^n
 lemma sum_C_mul_X_eq (p : polynomial α) : p.sum (λn a, C a * X^n) = p :=
 eq.trans (sum_congr rfl $ assume n hn, single_eq_C_mul_X.symm) (finsupp.sum_single _)
 
-
 @[elab_as_eliminator] protected lemma induction_on {M : polynomial α → Prop} (p : polynomial α)
   (h_C : ∀a, M (C a))
   (h_add : ∀p q, M p → M q → M (p + q))
@@ -542,6 +545,9 @@ end
 lemma eq_C_of_degree_eq_zero (h : degree p = 0) : p = C (coeff p 0) :=
 eq_C_of_degree_le_zero (h ▸ le_refl _)
 
+lemma degree_le_zero_iff : degree p ≤ 0 ↔ p = C (coeff p 0) :=
+⟨eq_C_of_degree_le_zero, λ h, h.symm ▸ degree_C_le⟩
+
 lemma degree_add_le (p q : polynomial α) : degree (p + q) ≤ max (degree p) (degree q) :=
 calc degree (p + q) = ((p + q).support).sup some : rfl
   ... ≤ (p.support ∪ q.support).sup some : sup_mono support_add
@@ -971,6 +977,128 @@ lemma ne_zero_of_monic (h : monic p) : p ≠ 0 :=
 
 end nonzero_comm_semiring
 
+section comm_semiring
+variables [comm_semiring α] [decidable_eq α] {p q : polynomial α}
+
+/-- `dix_X p` return a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
+  It can be used in a semiring where the usual division algorithm is not possible -/
+def div_X (p : polynomial α) : polynomial α :=
+{ to_fun := λ n, p.coeff (n + 1),
+  support := ⟨(p.support.filter (> 0)).1.map (λ n, n - 1),
+    multiset.nodup_map_on begin
+        simp only [finset.mem_def.symm, finset.mem_erase, finset.mem_filter],
+        assume x hx y hy hxy,
+        rwa [← @add_right_cancel_iff _ _ 1, nat.sub_add_cancel hx.2,
+          nat.sub_add_cancel hy.2] at hxy
+      end
+      (p.support.filter (> 0)).2⟩,
+  mem_support_to_fun := λ n,
+    suffices (∃ (a : ℕ), (¬coeff p a = 0 ∧ a > 0) ∧ a - 1 = n) ↔
+      ¬coeff p (n + 1) = 0,
+    by simpa [finset.mem_def.symm, apply_eq_coeff],
+    ⟨λ ⟨a, ha⟩, by rw [← ha.2, nat.sub_add_cancel ha.1.2]; exact ha.1.1,
+      λ h, ⟨n + 1, ⟨h, nat.succ_pos _⟩, nat.succ_sub_one _⟩⟩ }
+
+lemma div_X_mul_X_add (p : polynomial α) : div_X p * X + C (p.coeff 0) = p :=
+polynomial.ext.2 $ λ n,
+  nat.cases_on n
+   (by simp)
+   (by simp [coeff_C, nat.succ_ne_zero, coeff_mul_X, div_X])
+
+@[simp] lemma div_X_C (a : α) : div_X (C a) = 0 :=
+polynomial.ext.2 $ λ n, by cases n; simp [div_X, coeff_C]; simp [coeff]
+
+lemma div_X_eq_zero_iff : div_X p = 0 ↔ p = C (p.coeff 0) :=
+⟨λ h, by simpa [eq_comm, h] using div_X_mul_X_add p,
+  λ h, by rw [h, div_X_C]⟩
+
+lemma div_X_add : div_X (p + q) = div_X p + div_X q :=
+polynomial.ext.2 $ by simp [div_X]
+
+def nonzero_comm_semiring.of_polynomial_ne (h : p ≠ q) : nonzero_comm_semiring α :=
+{ zero_ne_one := λ h01 : 0 = 1, h $
+    by rw [← mul_one p, ← mul_one q, ← C_1, ← h01, C_0, mul_zero, mul_zero],
+  ..show comm_semiring α, by apply_instance }
+
+lemma degree_lt_degree_mul_X (hp : p ≠ 0) : p.degree < (p * X).degree :=
+by letI := nonzero_comm_semiring.of_polynomial_ne hp; exact
+have leading_coeff p * leading_coeff X ≠ 0, by simpa,
+by erw [degree_mul_eq' this, degree_eq_nat_degree hp,
+    degree_X, ← with_bot.coe_one, ← with_bot.coe_add, with_bot.coe_lt_coe];
+  exact nat.lt_succ_self _
+
+lemma degree_div_X_lt (hp0 : p ≠ 0) : (div_X p).degree < p.degree :=
+by letI := nonzero_comm_semiring.of_polynomial_ne hp0; exact
+calc (div_X p).degree < (div_X p * X + C (p.coeff 0)).degree :
+  if h : degree p ≤ 0
+  then begin
+      have h' : C (p.coeff 0) ≠ 0, by rwa [← eq_C_of_degree_le_zero h],
+      rw [eq_C_of_degree_le_zero h, div_X_C, degree_zero, zero_mul, zero_add],
+      exact lt_of_le_of_ne lattice.bot_le (ne.symm (mt degree_eq_bot.1 $
+        by simp [h'])),
+    end
+  else
+    have hXp0 : div_X p ≠ 0,
+      by simpa [div_X_eq_zero_iff, -not_le, degree_le_zero_iff] using h,
+    have leading_coeff (div_X p) * leading_coeff X ≠ 0, by simpa,
+    have degree (C (p.coeff 0)) < degree (div_X p * X),
+      from calc degree (C (p.coeff 0)) ≤ 0 : degree_C_le
+         ... < 1 : dec_trivial
+         ... = degree (X : polynomial α) : degree_X.symm
+         ... ≤ degree (div_X p * X) :
+          by rw [← zero_add (degree X), degree_mul_eq' this];
+            exact add_le_add'
+              (by rw [zero_le_degree_iff, ne.def, div_X_eq_zero_iff];
+                exact λ h0, h (h0.symm ▸ degree_C_le))
+              (le_refl _),
+    by rw [add_comm, degree_add_eq_of_degree_lt this];
+      exact degree_lt_degree_mul_X hXp0
+... = p.degree : by rw div_X_mul_X_add
+
+@[elab_as_eliminator] def rec_on_horner
+  {M : polynomial α → Sort*} : Π (p : polynomial α),
+  M 0 →
+  (Π p a, coeff p 0 = 0 → a ≠ 0 → M p → M (p + C a)) →
+  (Π p, p ≠ 0 → M p → M (p * X)) →
+  M p
+| p := λ M0 MC MX,
+if hp : p = 0 then eq.rec_on hp.symm M0
+else
+have wf : degree (div_X p) < degree p,
+  from degree_div_X_lt hp,
+by rw [← div_X_mul_X_add p] at *;
+  exact
+  if hcp0 : coeff p 0 = 0
+  then by rw [hcp0, C_0, add_zero];
+    exact MX _ (λ h : div_X p = 0, by simpa [h, hcp0] using hp)
+      (rec_on_horner _ M0 MC MX)
+  else MC _ _ (coeff_mul_X_zero _) hcp0 (if hpX0 : div_X p = 0
+    then show M (div_X p * X), by rw [hpX0, zero_mul]; exact M0
+    else MX (div_X p) hpX0 (rec_on_horner _ M0 MC MX))
+using_well_founded {dec_tac := tactic.assumption}
+
+@[elab_as_eliminator] lemma degree_pos_induction_on
+  {P : polynomial α → Prop} (p : polynomial α) (h0 : 0 < degree p)
+  (hC : ∀ {a}, a ≠ 0 → P (C a * X))
+  (hX : ∀ {p}, 0 < degree p → P p → P (p * X))
+  (hadd : ∀ {p} {a}, 0 < degree p → P p → P (p + C a)) : P p :=
+rec_on_horner p
+  (λ h, by rw degree_zero at h; exact absurd h dec_trivial)
+  (λ p a _ _ ih h0,
+    have 0 < degree p,
+      from lt_of_not_ge (λ h, (not_lt_of_ge degree_C_le) $
+        by rwa [eq_C_of_degree_le_zero h, ← C_add] at h0),
+    hadd this (ih this))
+  (λ p _ ih h0',
+    if h0 : 0 < degree p
+    then hX h0 (ih h0)
+    else by rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at *;
+      exact hC (λ h : coeff p 0 = 0,
+        by simpa [h, not_lt.2 (@lattice.bot_le (  ℕ) _ _)] using h0'))
+  h0
+
+end comm_semiring
+
 section comm_ring
 variables [comm_ring α] [decidable_eq α] {p q : polynomial α}
 instance : comm_ring (polynomial α) := finsupp.to_comm_ring
@@ -1045,8 +1173,6 @@ calc degree (p - q) = degree (erase (nat_degree q) p + -erase (nat_degree q) q)
   : degree_neg (erase (nat_degree q) q) ▸ degree_add_le _ _
 ... < degree p : max_lt_iff.2 ⟨hd' ▸ degree_erase_lt hp0, hd.symm ▸ degree_erase_lt hq0⟩
 
-instance : has_well_founded (polynomial α) := ⟨_, degree_lt_wf⟩
-
 lemma ne_zero_of_ne_zero_of_monic (hp : p ≠ 0) (hq : monic q) : q ≠ 0
 | h := begin
   rw [h, monic.def, leading_coeff_zero] at hq,