Theory Abstract_Multivariate_Polynomials

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

  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 ‹Abstract Multivariate Polynomials›

theory Abstract_Multivariate_Polynomials
  imports
    Substitutions
    "HOL-Analysis.Finite_Cartesian_Product"
begin

text ‹Multivariate polynomials, abstractly›

locale multi_variate_polynomial = 
  fixes vars :: ‹'p :: comm_monoid_add ⇒ 'v set›
  and deg :: ‹'p ⇒ nat›
  and eval :: ‹'p ⇒ ('v, 'a::finite) subst ⇒ 'b :: comm_monoid_add›
  and inst :: ‹'p ⇒ ('v, 'a) subst ⇒ 'p›
assumes
  ― ‹vars›
  vars_finite: ‹finite (vars p)› and 
  vars_zero: ‹vars 0 = {}› and 
  vars_add: ‹vars (p + q) ⊆ vars p ∪ vars q› and
  vars_inst: ‹vars (inst p σ) ⊆ vars p - dom σ› and 

  ― ‹degree›
  deg_zero: ‹deg 0 = 0› and 
  deg_add: ‹deg (p + q) ≤ max (deg p) (deg q)› and 
  deg_inst: ‹deg (inst p ρ) ≤ deg p› and 

  ― ‹eval›
  eval_zero: ‹eval 0 σ = 0› and
  eval_add: ‹vars p ∪ vars q ⊆ dom σ ⟹ eval (p + q) σ = eval p σ + eval q σ› and
  eval_inst: ‹vars p ⊆ dom σ ∪ dom ρ ⟹ eval (inst p σ) ρ = eval p (ρ ++ σ)› and

  ― ‹small number of roots (variant for two polynomials)›
  roots: ‹card {r. deg p ≤ d ∧ vars p ⊆ {x} ∧ deg q ≤ d ∧ vars q ⊆ {x} ∧ 
                   p ≠ q ∧ eval p [x ↦ r] = eval q [x ↦ r]} ≤ d›
begin

lemmas vars_addD = vars_add[THEN subsetD]


subsection ‹Arity: definition and some lemmas›

definition arity :: ‹'p ⇒ nat› where
  ‹arity p = card (vars p)›

lemma arity_zero: ‹arity 0 = 0› 
  by (simp add: arity_def vars_zero)

lemma arity_add: ‹arity (p + q) ≤ arity p + arity q› 
proof - 
  have ‹card (vars (p + q)) ≤ card (vars p ∪ vars q)› 
    by (intro card_mono) (auto simp add: vars_add vars_finite) 
  also have ‹... ≤ card (vars p) + card (vars q)› by (simp add: card_Un_le)
  finally show ?thesis by (simp add: arity_def)
qed

lemma arity_inst: 
  assumes ‹dom σ ⊆ vars p› 
  shows ‹arity (inst p σ) ≤ arity p - card (dom σ)›
proof -
  have ‹card (vars (inst p σ)) ≤ card (vars p - dom σ)›
    by (auto simp add: vars_finite vars_inst card_mono)
  also have ‹… = card (vars p) - card (dom σ)› using assms 
    by (simp add: card_Diff_subset finite_subset vars_finite)
  finally show ?thesis by (simp add: arity_def)
qed

subsection ‹Lemmas about evaluation, degree, and variables of finite sums›

lemma eval_sum: 
  assumes ‹finite I› ‹⋀i. i ∈ I ⟹ vars (pp i) ⊆ dom σ›
  shows ‹eval (∑i∈I. pp i) σ = (∑i∈I. eval (pp i) σ)›
proof - 
  have ‹eval (∑i∈I. pp i) σ = (∑i∈I. eval (pp i) σ) ∧ vars (∑i∈I. pp i) ⊆ dom σ› using assms
  proof (induction rule: finite.induct)
    case emptyI
    then show ?case by (simp add: eval_zero vars_zero)
  next
    case (insertI A a)
    then show ?case 
      by (auto simp add: eval_add vars_add sum.insert_if dest!: vars_addD)
  qed
  then show ?thesis ..
qed

lemma vars_sum: 
  assumes ‹finite I›  
  shows ‹vars (∑i∈I. pp i) ⊆ (⋃i∈I. vars (pp i))›
  using assms
proof (induction rule: finite.induct)
  case emptyI
  then show ?case by(auto simp add: vars_zero)
next
  case (insertI A a)
  then show ?case using insertI by(auto simp add: sum.insert_if dest: vars_addD)
qed

lemma deg_sum:
  assumes ‹finite I›  and "I ≠ {}"
  shows ‹deg (∑i∈I. pp i) ≤ Max {deg (pp i) | i. i ∈ I}› 
  using assms 
proof (induction rule: finite.induct)
  case emptyI
  then show ?case by(auto simp add: deg_zero)
next
  case (insertI A a)
  show ?case 
  proof(cases "A = {}")
    assume ‹A = {}›
    then show ?thesis by(simp)
  next
    assume ‹A ≠ {}›
    then have *: ‹Max {deg (pp i) |i. i ∈ A} ≤ Max {deg (pp i) |i. i = a ∨ i ∈ A}› using ‹finite A›
      by (intro Max_mono) auto
    show ?thesis using insertI ‹A ≠ {}› 
      by (auto 4 4 simp add: sum.insert_if intro: Max_ge *[THEN [2] le_trans] deg_add[THEN le_trans])
  qed
qed
     
subsection ‹Lemmas combining eval, sum, and inst›

lemma eval_sum_inst: 
  assumes ‹vars p ⊆ V ∪ dom ρ› ‹finite V›
  shows ‹eval (∑σ ∈ substs V H. inst p σ) ρ = (∑σ ∈ substs V H. eval p (ρ ++ σ))› 
proof - 
  have A1: ‹⋀σ. σ ∈ substs V H ⟹ vars (inst p σ) ⊆ dom ρ› using assms(1) vars_inst by blast
  have A2: ‹⋀σ. σ ∈ substs V H ⟹ vars p ⊆ dom σ ∪ dom ρ› using assms(1) by (auto)

  have ‹eval (∑σ ∈ substs V H. inst p σ) ρ = (∑σ∈substs V H. eval (inst p σ) ρ)› using A1 assms(2)
    by (simp add: eval_sum substs_finite)    ― ‹requires @{term "finite H"}›
  also have ‹... = (∑σ ∈ substs V H. eval p (ρ ++ σ))› using A2 
    by (simp add: eval_inst)
  finally show ?thesis .
qed

lemma  eval_sum_inst_commute:
  assumes ‹vars p ⊆ insert x V› ‹x ∉ V› ‹finite V›
  shows ‹eval (∑σ∈substs V H. inst p σ) [x ↦ r]
         = (∑σ∈substs V H. eval (inst p [x ↦ r]) σ)›
proof -
  have ‹eval (sum (inst p) (substs V H)) [x ↦ r] = 
        (∑σ∈substs V H. eval p ([x ↦ r] ++ σ))› using ‹vars p ⊆ insert x V› ‹finite V›
    by (simp add: eval_sum_inst)
  also have ‹... = (∑σ∈substs V H. eval p (σ(x ↦ r)))› using ‹x ∉ V›
    by (intro Finite_Cartesian_Product.sum_cong_aux) 
       (auto simp add: map_add_comm subst_dom)
  also have ‹... = (∑σ∈substs V H. eval (inst p [x ↦ r]) σ)› using ‹vars p ⊆ insert x V›
    by (intro Finite_Cartesian_Product.sum_cong_aux)
       (auto simp add: eval_inst)
  finally show ?thesis .
qed

subsection ‹Merging sums over substitutions›

lemma sum_merge:
  assumes ‹x ∉ V›   
  shows "(∑h∈H. (∑σ ∈ substs V H. eval p ([x ↦ h] ++ σ)))
          = (∑σ∈substs (insert x V) H. eval p σ)"
proof -
  have  "⋀h σ. (h,σ) ∈ H × substs V H ⟹ dom [x ↦ h] ∩ dom σ = {}" using ‹x ∉ V› 
    by(auto simp add: substs_def)
  then have *: "⋀h σ. (h,σ) ∈ H × substs V H ⟹ [x ↦ h] ++ σ = σ(x ↦ h)" 
    by(auto simp add: map_add_comm)

  have "(∑h∈H. (∑σ ∈ substs V H. eval p ([x ↦ h] ++ σ))) =
        (∑(h,σ) ∈ H × substs V H. eval p ([x ↦ h] ++ σ))"
    by(auto simp add: sum.cartesian_product)
  also have "… = (∑(h,σ) ∈ H × substs V H. eval p (σ(x ↦ h)))" using *  
    by (intro Finite_Cartesian_Product.sum_cong_aux) (auto)
  also have "… =  (∑σ∈substs (insert x V) H. eval p σ)" using ‹x ∉ V› 
    by(auto simp add: sum.reindex_bij_betw[OF bij_betw_set_substs, 
              where V1 = "insert x V" and x1 = "x" and H1 = "H" and g = "λσ. eval p σ", symmetric]
            intro: Finite_Cartesian_Product.sum_cong_aux)
  finally show ?thesis .
qed

end

end