Theory Univariate_Roots_Bound

(*******************************************************************************

  Project: Sumcheck Protocol

  Authors: Azucena Garvia Bosshard <zucegb@gmail.com>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
           Jonathan Bootle, IBM Research Europe <jbt@zurich.ibm.com>

*******************************************************************************)

section ‹Roots Bound for Univariate Polynomials›

theory Univariate_Roots_Bound
  imports 
    "HOL-Computational_Algebra.Polynomial"  
begin

text ‹
\textbf{NOTE:} if considered to be useful enough, the lemmas in this theory could be moved to 
the theory @{theory "HOL-Computational_Algebra.Polynomial"}.
›

subsection ‹Basic lemmas›

lemma finite_non_zero_coeffs: ‹finite {n. poly.coeff p n ≠ 0}›
  using MOST_coeff_eq_0 eventually_cofinite 
  by fastforce

text ‹Univariate degree in terms of @{term Max}›

lemma poly_degree_eq_Max_non_zero_coeffs: 
  "degree p = Max (insert 0 {n. poly.coeff p n ≠ 0})"
  by (intro le_antisym degree_le) (auto simp add: finite_non_zero_coeffs le_degree)


subsection ‹Univariate roots bound›

text ‹The number of roots of a product of polynomials is bounded by 
the sum of the number of roots of each.›

lemma card_poly_mult_roots:
  fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" 
    and q :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" 
  assumes "p ≠ 0" and "q ≠ 0" 
  shows "card {x. poly p x * poly q x = 0} ≤ card {x. poly p x = 0} + card {x. poly q x = 0}"
proof -
  have "card {x . poly p x * poly q x = 0} ≤ card ({x . poly p x = 0} ∪ {x . poly q x = 0})"
    by (auto simp add: poly_roots_finite assms intro!: card_mono)
  also have "… ≤ card {x . poly p x = 0} + card {x . poly q x = 0}" 
    by(auto simp add: Finite_Set.card_Un_le)
  finally show ?thesis .
qed

text ‹A univariate polynomial p has at most deg p roots.›

lemma univariate_roots_bound:
  fixes p :: ‹'a::idom poly›
  assumes ‹p ≠ 0› 
  shows ‹card {x. poly p x = 0} ≤ degree p›
  using assms
proof (induction "degree p" arbitrary: p rule: nat_less_induct)
  case 1
  then show ?case
  proof(cases "∃r. poly p r = 0")
    case True ― ‹A root exists›

    ― ‹Get root r of polynomial and write @{text "p = [:- r, 1:] ^ order r p * q"} for some @{text q}.›
    then obtain r where "poly p r = 0" by(auto)
    let ?xr = "[:- r, 1:] ^ order r p"
    obtain q where "p = ?xr * q" using order_decomp ‹p ≠ 0› by(auto)

    ― ‹Useful facts about q and @{term "[:- r, 1:] ^ order r p"}›
    have "q ≠ 0" using ‹p = ?xr * q› ‹p ≠ 0› by(auto)
    have "?xr ≠ 0" by(simp)
    have "degree ?xr > 0" using ‹?xr ≠ 0› ‹p ≠ 0› ‹poly p r = 0› 
      by (simp add: degree_power_eq order_root) 
    have "degree q < degree p" 
      using ‹?xr ≠ 0› ‹q ≠ 0› ‹p = ?xr * q› ‹degree ?xr > 0› 
            degree_mult_eq[where p = "?xr" and q = "q"] 
      by (simp)
    have x_roots: "card {r. poly ?xr r = 0} = 1" using ‹p ≠ 0› ‹poly p r = 0› 
      by(simp add: order_root)
    have q_roots: "card {r. poly q r = 0} ≤ degree q" using ‹q ≠ 0› ‹degree q < degree p› 1 
      by (simp)

    ― ‹Final bound›
    have "card {r . poly p r = 0} ≤ degree p" 
      using ‹p = ?xr * q› ‹q ≠ 0› ‹?xr ≠ 0› ‹degree q < degree p›
            poly_mult[where p = "?xr" and q = "q"] 
            card_poly_mult_roots[where p = "?xr" and q = "q"] 
            x_roots q_roots  
      by (simp) 
    then show ?thesis .    
  next
    case False ― ‹No root exists›
    then show ?thesis by simp
  qed
qed


end