Theory Roots_Bounds

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

  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 Multivariate Polynomials of Arity at Most One›

theory Roots_Bounds
  imports 
    "Polynomials.MPoly_Type_Univariate"
    Univariate_Roots_Bound
begin

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

subsection ‹Lemmas connecting univariate and multivariate polynomials›

subsubsection ‹Basic lemmas›

lemma mpoly_to_poly_zero_iff:
  fixes p::"'a::comm_monoid_add mpoly"
  assumes ‹vars p ⊆ {v}›  
  shows "mpoly_to_poly v p = 0 ⟷ p = 0"
  by (metis assms mpoly_to_poly_inverse poly_to_mpoly0 poly_to_mpoly_inverse)

lemma keys_monom_subset_vars:
  fixes p::"'a::zero mpoly"
  assumes ‹m ∈ keys (mapping_of p)› 
  shows "keys m ⊆ vars p" 
  using assms 
  by (auto simp add: vars_def)

lemma sum_lookup_keys_eq_lookup:
  fixes p::"'a::zero mpoly"
  assumes ‹m ∈ keys (mapping_of p)› and ‹vars p ⊆ {v}› 
  shows "sum (lookup m) (keys m) = lookup m v"
  using assms
  by (auto simp add: subset_singleton_iff dest!: keys_monom_subset_vars)


subsubsection ‹Total degree corresponds to degree for polynomials of arity at most one›

lemma poly_degree_eq_mpoly_degree:
  fixes p::"'a::comm_monoid_add mpoly"
  assumes ‹vars p ⊆ {v}›
  shows "degree (mpoly_to_poly v p) = MPoly_Type.degree p v"
  using assms
proof - 
  have *: "⋀n. MPoly_Type.coeff p (Poly_Mapping.single v n) ≠ 0 
               ⟷ (∃m∈keys (mapping_of p). n = lookup m v)"  
    by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_insert add_0 keys_eq_empty 
              keys_monom_subset_vars lookup_single_eq remove_key_keys remove_key_sum 
              singleton_insert_inj_eq' coeff_keys[symmetric] assms)

  have "degree (mpoly_to_poly v p) 
      = Max (insert 0 {n. MPoly_Type.coeff p (Poly_Mapping.single v n) ≠ 0})" 
    by (simp add: poly_degree_eq_Max_non_zero_coeffs) 
  also have "… = MPoly_Type.degree p v"
    by (simp add: degree.rep_eq image_def *)
  finally show ?thesis .
qed

lemma mpoly_degree_eq_total_degree:
  fixes p::"'a::zero mpoly"
  assumes ‹vars p ⊆ {v}›
  shows "MPoly_Type.degree p v = total_degree p"
  using assms
  by (auto simp add: MPoly_Type.degree_def total_degree_def sum_lookup_keys_eq_lookup)

corollary poly_degree_eq_total_degree:
  fixes p::"'a::comm_monoid_add mpoly"
  assumes ‹vars p ⊆ {v}›
  shows "degree (mpoly_to_poly v p) = total_degree p"
  using assms
  by (simp add: poly_degree_eq_mpoly_degree mpoly_degree_eq_total_degree)  


subsection ‹Roots bound for univariate polynomials of type @{typ "'a mpoly"}›

lemma univariate_mpoly_roots_bound: 
  fixes p::"'a::idom mpoly"
  assumes ‹vars p ⊆ {v}› ‹p ≠ 0› 
  shows ‹card {x. insertion (λv. x) p = 0} ≤ total_degree p›
  using assms univariate_roots_bound[of "mpoly_to_poly v p", unfolded poly_eq_insertion[OF ‹vars p ⊆ {v}›]] 
  by (auto simp add: poly_degree_eq_total_degree mpoly_to_poly_zero_iff)

end