# Theory Multiv_Pseudo_Remainder_Sequence

```(* This uses insights from Wenda Li's Pseudo_Remainder_Sequence.thy,
but it specializes pseudo-remainder sequences to our type of polynomials.
*)

theory Multiv_Pseudo_Remainder_Sequence
imports
Multiv_Consistent_Sign_Assignments

begin

section "Functions"

definition mul_pseudo_mod:: "'a::{comm_ring_1,semiring_1_no_zero_divisors} Polynomial.poly ⇒ 'a Polynomial.poly ⇒ 'a Polynomial.poly" where
"mul_pseudo_mod p q = (
let m =
(if even(Polynomial.degree p+1-Polynomial.degree q)
then -1
Polynomial.smult m (pseudo_mod p q))"

(* This is only ever called when LC p != 0 *)
(* Key helper function for spmods_multiv *)
function spmods_multiv_aux::
"real mpoly Polynomial.poly ⇒
real mpoly Polynomial.poly ⇒
(real mpoly × rat) list ⇒
((real mpoly × rat) list × real mpoly Polynomial.poly list) list" where
"spmods_multiv_aux p q assumps = (
if q = 0 then [(assumps, [p])] else
(case (lookup_assump_aux (Polynomial.lead_coeff q) assumps) of
None ⇒
let left = spmods_multiv_aux p (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # assumps) in
let res_one  = spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (1::rat)) # assumps) in
let res_minus_one  = spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (-1::rat)) # assumps) in
let right_one = map (λx. (fst x, Cons p (snd x))) res_one in
let right_minus_one = map (λx. (fst x, Cons p (snd x))) res_minus_one in
append left (append right_one right_minus_one)
| (Some i) ⇒
(if i = 0 then  spmods_multiv_aux p (one_less_degree q) assumps
else
let res = spmods_multiv_aux q (mul_pseudo_mod p q) assumps in
map (λx. (fst x, Cons p (snd x))) res
)
))" using prod_cases3
apply blast
by fastforce
termination
apply (relation "measure (λ(p,q,r). if q = [:0:] then 1 else 2 + Polynomial.degree q)")
apply blast
apply (auto)
using one_less_degree_degree
apply (metis one_less_degree_def cancel_comm_monoid_add_class.diff_cancel degree_0_id gr0I monom_0)
unfolding mul_pseudo_mod_def
using pseudo_mod(2)
apply auto[1]
apply (metis Multiv_Poly_Props.one_less_degree_def cancel_comm_monoid_add_class.diff_cancel degree_0_id monom_0 not_gr_zero one_less_degree_degree)
by (metis degree_pseudo_mod_less degree_smult_eq smult_eq_0_iff)

(* The top-level function to generate multivariate pseudo-remainder sequences
specialized to real mpoly Polynomial.poly *)
function spmods_multiv::
"real mpoly Polynomial.poly ⇒
real mpoly Polynomial.poly ⇒
(real mpoly × rat) list ⇒
((real mpoly × rat) list × (real mpoly Polynomial.poly list)) list"
where "spmods_multiv p q assumps = (
if p = 0 then [(assumps,[])] else
(case (lookup_assump_aux (Polynomial.lead_coeff p) assumps) of
None ⇒
let left = spmods_multiv (one_less_degree p) q ((Polynomial.lead_coeff p, (0::rat)) # assumps) in
let right_one  = spmods_multiv_aux p q ((Polynomial.lead_coeff p, (1::rat)) # assumps) in
let right_minus_one  = spmods_multiv_aux p q ((Polynomial.lead_coeff p, (-1::rat)) # assumps) in
left @ (right_one @ right_minus_one)
| (Some i) ⇒
(if i = 0 then  spmods_multiv (one_less_degree p) q assumps
else
spmods_multiv_aux p q assumps
)
))"
using spmods_multiv_aux.cases apply blast
by force
termination
apply (relation "measure (λ(p,q). if p = [:0:] then 1 else 2 + Polynomial.degree p)")
apply blast
apply (auto)
using one_less_degree_degree
apply (metis Multiv_Poly_Props.one_less_degree_def cancel_comm_monoid_add_class.diff_cancel degree_0_id monom_0 not_gr_zero)
by (metis Multiv_Poly_Props.one_less_degree_def cancel_comm_monoid_add_class.diff_cancel degree_0_id monom_0 not_gr_zero one_less_degree_degree)

declare spmods_multiv_aux.simps[simp del]
declare spmods_multiv.simps[simp del]

section "Proofs"

lemma mul_pseudo_mod_valuation:
assumes "satisfies_evaluation val (Polynomial.lead_coeff p) n"
assumes "n ≠ 0"
assumes "satisfies_evaluation val (Polynomial.lead_coeff q) m"
assumes "m ≠ 0"
shows "mul_pseudo_mod (eval_mpoly_poly val p) (eval_mpoly_poly val q) =
eval_mpoly_poly val (mul_pseudo_mod p q)"
proof -
from degree_valuation[OF assms(1-2)] have
1: "Polynomial.degree p = Polynomial.degree (eval_mpoly_poly val p)" .
from degree_valuation[OF assms(3-4)] have
2: "Polynomial.degree q = Polynomial.degree (eval_mpoly_poly val q)" .
show ?thesis
using assms
by (smt (verit, ccfv_SIG) "1" "2" "4" eval_mpoly_map_poly_comm_ring_hom.base.hom_one eval_mpoly_map_poly_comm_ring_hom.base.hom_uminus eval_mpoly_poly_pseudo_mod eval_mpoly_poly_smult mul_pseudo_mod_def of_int_hom.hom_one of_int_hom.hom_uminus)
(* apply (auto simp add: mul_pseudo_mod_def 1 2 3 4 eval_mpoly_poly_comm_ring_hom.hom_uminus eval_mpoly_poly_pseudo_mod eval_mpoly_poly_smult)
apply (metis "2" "4" eval_mpoly_poly_smult)
by (metis 2 4 eval_mpoly_poly_smult) *)
qed

lemma spmods_multiv_aux_induct[case_names Base Rec Lookup0 LookupN0]:
fixes p q :: "real mpoly Polynomial.poly"
fixes assumps ::"(real mpoly × rat) list"
assumes base: "⋀p q assumps. q = 0 ⟹ P p q assumps"
and rec: "⋀p q assumps.
⟦q ≠ 0;
lookup_assump_aux (Polynomial.lead_coeff q) assumps = None;
P p (one_less_degree q) ((Polynomial.lead_coeff q, 0) # assumps);
P q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, 1) # assumps);
P q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, -1) # assumps)⟧ ⟹
P p q assumps"
and lookup0: "⋀p q assumps.
⟦q ≠ 0;
lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some 0;
P p (one_less_degree q) assumps⟧ ⟹ P p q assumps"
and lookupN0: "⋀p q assumps r.
⟦q ≠ 0;
lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some r;
r ≠ 0;
P q (mul_pseudo_mod p q) assumps⟧ ⟹ P p q assumps"
shows "P p q assumps"
apply(induct p q assumps rule: spmods_multiv_aux.induct)
by (metis base rec lookup0 lookupN0 not_None_eq)

lemma spmods_multiv_induct[case_names Base Rec Lookup0 LookupN0]:
fixes p q :: "real mpoly Polynomial.poly"
fixes assumps ::"(real mpoly × rat) list"
assumes base: "⋀p q assumps. p = 0 ⟹ P p q assumps"
and rec: "⋀p q assumps.
⟦p ≠ 0;
lookup_assump_aux (Polynomial.lead_coeff p) assumps = None;
P (one_less_degree p) q ((Polynomial.lead_coeff p, 0) # assumps)⟧ ⟹
P p q assumps"
and lookup0: "⋀p q assumps.
⟦p ≠ 0;
lookup_assump_aux (Polynomial.lead_coeff p) assumps = Some 0;
P (one_less_degree p) q assumps⟧ ⟹ P p q assumps"
and lookupN0: "⋀p q assumps r.
⟦p ≠ 0;
lookup_assump_aux (Polynomial.lead_coeff p) assumps = Some r;
r ≠ 0⟧ ⟹ P p q assumps"
shows "P p q assumps"
apply(induct p q assumps rule: spmods_multiv.induct)
by (metis base rec lookup0 lookupN0 not_None_eq)

lemma spmods_multiv_aux_assum_acc:
assumes "(acc',seq') ∈ set (spmods_multiv_aux p q acc)"
shows "set acc ⊆ set acc'"
using assms
proof (induct p q acc arbitrary:acc' seq' rule: spmods_multiv_aux_induct)
case (Base p q assumps)
then show ?case by (auto simp add: spmods_multiv_aux.simps)
next
case (Rec p q assumps)
then show ?case using spmods_multiv_aux.simps[of p q assumps]
by (smt (z3) Un_iff imageE insert_subset list.set(2) list.set_map old.prod.inject option.simps(4) prod.collapse set_append)
(* apply (auto simp add: spmods_multiv_aux.simps[of p q assumps])
apply blast
by blast *)
next
case (Lookup0 p q assumps)
then show ?case
by (auto simp add: spmods_multiv_aux.simps[of p q assumps])
next
case (LookupN0 p q assumps r)
then show ?case using spmods_multiv_aux.simps[of p q assumps]
using option.simps(5) prod.collapse by fastforce
qed

lemma spmods_multiv_assum_acc:
assumes "(acc',seq') ∈ set (spmods_multiv p q acc)"
shows "set acc ⊆ set acc'"
using assms
proof (induct p q acc arbitrary:acc' seq' rule: spmods_multiv_induct)
case (Base p q assumps)
then show ?case by (auto simp add: spmods_multiv.simps)
next
case (Rec p q assumps)
then show ?case
using spmods_multiv_aux_assum_acc spmods_multiv.simps[of p q assumps]
by (metis Un_iff insert_subset list.set(2) option.simps(4) set_append)
next
case (Lookup0 p q assumps)
then show ?case
by (auto simp add: spmods_multiv.simps[of p q assumps])
next
case (LookupN0 p q assumps r)
then show ?case
using spmods_multiv_aux_assum_acc
by (auto simp add: spmods_multiv.simps[of p q assumps])
qed

lemma lookup_assum_aux_mem:
assumes "lookup_assump_aux x ls = Some i"
shows "(x,i) ∈ set ls"
using assms
apply (induction ls)
apply force
by (metis fst_conv list.set_intros(1) list.set_intros(2) lookup_assump_aux.simps(2) old.prod.exhaust option.inject prod.sel(2))

lemma matches_ss:
assumes "(Polynomial.lead_coeff p,m) ∈ set assumps" "m ≠ 0"
assumes "(assumps, sturm_seq) ∈ set (spmods_multiv_aux p q acc)"
assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
shows "map (eval_mpoly_poly val) sturm_seq =
spmods (eval_mpoly_poly val p) (eval_mpoly_poly val q)"
using assms
proof (induct p q acc arbitrary:assumps sturm_seq m rule: spmods_multiv_aux_induct)
case (Base p q assumps)
then show ?case
using lead_coeff_valuation satisfies_evaluation_nonzero spmods_multiv_aux.simps by fastforce
next
case ih: (Rec p q acc)
let ?left = "spmods_multiv_aux p (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # acc)"
let ?res_one = "spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (1::rat)) # acc)"
let ?res_minus_one = "spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (-1::rat)) # acc)"
have rec: "(assumps, sturm_seq) ∈ set ?left ∨
(assumps, sturm_seq) ∈ set (map (λx. (fst x, Cons p (snd x))) ?res_one) ∨
(assumps, sturm_seq) ∈ set (map (λx. (fst x, Cons p (snd x))) ?res_minus_one)"
using ih by (auto simp add:  spmods_multiv_aux.simps[of p q acc])
moreover {
assume "(assumps, sturm_seq) ∈ set ?left"
then have "map (eval_mpoly_poly val) sturm_seq = spmods (eval_mpoly_poly val p) (eval_mpoly_poly val q)"
by (metis eval_mpoly_poly_one_less_degree ih.hyps(3) ih.prems(1) ih.prems(2) ih.prems(4) insert_subset list.set(2) spmods_multiv_aux_assum_acc)
}
moreover {
assume **:"
(assumps, sturm_seq) ∈ set (map (λx. (fst x, Cons p (snd x))) ?res_one) ∨
(assumps, sturm_seq) ∈ set (map (λx. (fst x, Cons p (snd x))) ?res_minus_one)"
then obtain s ss where ss:"sturm_seq = s#ss"
and rec:"(assumps,ss) ∈ set ?res_one ∨ (assumps,ss) ∈ set ?res_minus_one"
by auto
using ** spmods_multiv_aux_assum_acc by fastforce
then have A:"map (eval_mpoly_poly val) ss =
spmods (eval_mpoly_poly val q) (eval_mpoly_poly val (mul_pseudo_mod p q))"
by (metis ih.hyps(4) ih.hyps(5) ih.prems(4) local.rec zero_neq_neg_one zero_neq_one)
have B:"spmods (eval_mpoly_poly val p) (eval_mpoly_poly val q) =
((eval_mpoly_poly val p) # (spmods (eval_mpoly_poly val q) (mul_pseudo_mod  (eval_mpoly_poly val p) (eval_mpoly_poly val q))))"
have C: "mul_pseudo_mod (eval_mpoly_poly val p) (eval_mpoly_poly val q) = eval_mpoly_poly val (mul_pseudo_mod p q)"
by (metis lead_coeff_inset ih.prems(1) ih.prems(2) ih.prems(4) mul_pseudo_mod_valuation zero_neq_neg_one zero_neq_one)
have "map (eval_mpoly_poly val) sturm_seq = spmods (eval_mpoly_poly val p) (eval_mpoly_poly val q)"
using A B C rec ss ** by auto
}
ultimately show ?case
using local.rec by blast
next
case (Lookup0 p q acc)
then have rec: "(assumps, sturm_seq) ∈ set (spmods_multiv_aux p (one_less_degree q) acc)"
by (auto simp add:  spmods_multiv_aux.simps[of p q acc])
have "(Polynomial.lead_coeff q,0) ∈ set acc"
then have "satisfies_evaluation val (Polynomial.lead_coeff q) 0"
using Lookup0.prems(3) Lookup0.prems(4) spmods_multiv_aux_assum_acc by blast
then have "eval_mpoly_poly val (one_less_degree q) = (eval_mpoly_poly val q)"
then show ?case
using Lookup0.hyps(3) Lookup0.prems(1) Lookup0.prems(2) Lookup0.prems(4) local.rec by presburger
next
case ih:(LookupN0 p q acc r)
then have asm:"(assumps, sturm_seq) ∈ set (
map (λx. (fst x, Cons p (snd x)))
(spmods_multiv_aux q (mul_pseudo_mod p q) acc))"
by (auto simp add:  spmods_multiv_aux.simps[of p q acc])
then obtain s ss where ss:"sturm_seq = s#ss"
and rec:"(assumps,ss) ∈ set (spmods_multiv_aux q (mul_pseudo_mod p q) acc)"
by auto
have A:"map (eval_mpoly_poly val) ss = spmods (eval_mpoly_poly val q) (eval_mpoly_poly val (mul_pseudo_mod p q))"
using ih(4)[OF _ _ rec]
by (meson ih.hyps(2) ih.hyps(3) ih.prems(4) in_mono local.rec lookup_assump_means_inset spmods_multiv_aux_assum_acc)
have B:"spmods (eval_mpoly_poly val p) (eval_mpoly_poly val q) =
((eval_mpoly_poly val p) # (spmods (eval_mpoly_poly val q) (mul_pseudo_mod  (eval_mpoly_poly val p) (eval_mpoly_poly val q))))"
have C: "mul_pseudo_mod (eval_mpoly_poly val p)  (eval_mpoly_poly val q) = eval_mpoly_poly val (mul_pseudo_mod p q)"
by (meson ih.hyps(2) ih.hyps(3) ih.prems(1) ih.prems(2) ih.prems(4) local.rec lookup_assum_aux_mem mul_pseudo_mod_valuation spmods_multiv_aux_assum_acc subsetD)
show ?case
using A B C rec ss asm by force
qed

lemma spmods_multiv_aux_sturm_lc:
assumes "(Polynomial.lead_coeff p,m) ∈ set acc" "m ≠ 0"
assumes "(acc',seq') ∈ set (spmods_multiv_aux p q acc)"
assumes "el ∈ set seq'"
shows "∃r. (Polynomial.lead_coeff el,r) ∈ set acc' ∧ r ≠ 0"
using assms
proof (induct p q acc arbitrary:acc' seq' el m rule: spmods_multiv_aux_induct)
case (Base p q acc)
then show ?case
using empty_iff fst_conv list.set(1) prod.sel(2) set_ConsD spmods_multiv_aux.simps by auto
next
case (Rec p q acc)
then show ?case
apply (auto simp add: spmods_multiv_aux.simps[of p q acc])
apply (meson Rec.prems(3) spmods_multiv_aux_assum_acc subset_eq)
apply (metis zero_neq_one)
apply (meson Rec.prems(3) spmods_multiv_aux_assum_acc subset_iff)
by (metis zero_neq_neg_one)

next
case (Lookup0 p q acc)
then show ?case
by (auto simp add: spmods_multiv_aux.simps[of p q acc])
next
case (LookupN0 p q acc r)
then show ?case
apply (auto simp add: spmods_multiv_aux.simps[of p q acc])
using spmods_multiv_aux_assum_acc apply blast
by (meson lookup_assum_aux_mem)
qed

lemma spmods_multiv_sturm_lc:
assumes "(acc',seq') ∈ set (spmods_multiv p q acc)"
assumes "el ∈ set seq'"
shows "∃r. (Polynomial.lead_coeff el,r) ∈ set acc' ∧ r ≠ 0"
using assms
proof (induct p q acc arbitrary:acc' seq' rule: spmods_multiv_induct)
case (Base p q assumps)
then show ?case
using spmods_multiv.simps
by simp
next
case (Rec p q assumps)
then show ?case
apply (auto simp add: spmods_multiv.simps[of p q assumps])
using spmods_multiv_aux_sturm_lc
apply (metis list.set_intros(1) zero_neq_one)
by (metis list.set_intros(1) spmods_multiv_aux_sturm_lc zero_neq_neg_one)
next
case (Lookup0 p q assumps)
then show ?case
by (auto simp add: spmods_multiv.simps[of p q assumps])
next
case (LookupN0 p q assumps r)
then show ?case using spmods_multiv.simps[of p q assumps]
spmods_multiv_aux_sturm_lc lookup_assum_aux_mem
by (smt (verit, ccfv_threshold) option.simps(5))
(* apply (auto simp add: spmods_multiv.simps[of p q assumps])
using spmods_multiv_aux_sturm_lc
by (meson lookup_assum_aux_mem) *)
qed

lemma matches_len_complete:
assumes "⋀p n. (p,n) ∈ set acc ⟹ satisfies_evaluation val p n"
obtains assumps sturm_seq where
"(assumps, sturm_seq) ∈ set (spmods_multiv_aux p q acc)"
"⋀ p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
using assms
proof (induct p q acc arbitrary: thesis rule: spmods_multiv_aux_induct)
case (Base p q acc)
then show ?case
next
case ih: (Rec p q acc)
let ?left = "spmods_multiv_aux p (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # acc)"
let ?res_one = "spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (1::rat)) # acc)"
let ?res_minus_one = "spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (-1::rat)) # acc)"
have "satisfies_evaluation val (Polynomial.lead_coeff q) 0 ∨
satisfies_evaluation val (Polynomial.lead_coeff q) 1 ∨
unfolding satisfies_evaluation_def
apply auto
using Sturm_Tarski.sign_cases
by (metis of_int_hom.hom_one of_int_minus)
then have q:"
(∀p n. (p,n) ∈ set ((Polynomial.lead_coeff q, 0) # acc) ⟶ satisfies_evaluation val p n) ∨
(∀p n. (p,n) ∈ set ((Polynomial.lead_coeff q, 1) # acc) ⟶ satisfies_evaluation val p n) ∨
(∀p n. (p,n) ∈ set ((Polynomial.lead_coeff q, -1) # acc) ⟶ satisfies_evaluation val p n)"
moreover {
assume *:"(∀p n. (p,n) ∈ set ((Polynomial.lead_coeff q, 0) # acc) ⟶ satisfies_evaluation val p n)"
then have ?case using * ih(3)
by (metis (no_types, lifting) Un_iff ih.hyps(1) ih.hyps(2) ih.prems(1) option.case(1) set_append spmods_multiv_aux.simps)
}
moreover {
assume *:"(∀p n. (p,n) ∈ set ((Polynomial.lead_coeff q, 1) # acc) ⟶ satisfies_evaluation val p n)"
then have ?case using * ih(4)
by (smt (z3) Un_iff fst_conv ih.hyps(1) ih.hyps(2) ih.prems(1) in_set_conv_decomp list.simps(9) map_append option.case(1) set_append spmods_multiv_aux.simps)
}
moreover {
assume *:"(∀p n. (p,n) ∈ set ((Polynomial.lead_coeff q, -1) # acc) ⟶ satisfies_evaluation val p n)"
then have ?case using * ih(5)
by (smt (z3) Un_iff fst_conv ih.hyps(1) ih.hyps(2) ih.prems(1) in_set_conv_decomp list.simps(9) map_append option.case(1) set_append spmods_multiv_aux.simps)
}
ultimately show ?case
by fastforce
next
case (Lookup0 p q acc)
then show ?case
by (auto simp add: spmods_multiv_aux.simps[of p q acc])
next
case ih: (LookupN0 p q assumps r)
then obtain assumps' sturm_seq' where
"(assumps', sturm_seq') ∈ set (spmods_multiv_aux q (mul_pseudo_mod p q) assumps)"
"(⋀p n. (p, n) ∈ set assumps' ⟹ satisfies_evaluation val p n)"
by blast
then show ?case using ih spmods_multiv_aux.simps[of p q assumps] fst_conv image_eqI
by (smt (verit) list.set_map option.simps(5))
(* apply (auto simp add: spmods_multiv_aux.simps[of p q assumps])
by (metis (mono_tags, lifting) fst_conv image_eqI) *)
qed

lemma spmods_multiv_nonz_some:
fixes p:: "real mpoly Polynomial.poly"
fixes q:: "real mpoly Polynomial.poly"
assumes inset: "(assumps, sturm_seq) ∈ set (spmods_multiv p q acc)"
shows "p ≠ 0 ⟹ ∃i. lookup_assump_aux (Polynomial.lead_coeff p) assumps = Some i"
using assms
proof (induct p q acc rule: spmods_multiv_induct)
case (Base p q acc)
then show ?case by auto
next
case (Rec p q acc)
then have "(lookup_assump_aux (Polynomial.lead_coeff p) acc) = None"
by meson
then have "set (spmods_multiv p q acc) =
set (spmods_multiv (one_less_degree p) q ((Polynomial.lead_coeff p, (0::rat)) # acc))
∪ set (spmods_multiv_aux p q ((Polynomial.lead_coeff p, (1::rat)) # acc))
∪ set (spmods_multiv_aux p q ((Polynomial.lead_coeff p, (-1::rat)) # acc))"
by (simp add: Rec.prems(1) spmods_multiv.simps sup_assoc)
then have "(assumps, sturm_seq) ∈ set (spmods_multiv (one_less_degree p) q ((Polynomial.lead_coeff p, (0::rat)) # acc))
∨ (assumps, sturm_seq) ∈ set (spmods_multiv_aux p q ((Polynomial.lead_coeff p, (1::rat)) # acc))
∨ (assumps, sturm_seq) ∈ set (spmods_multiv_aux p q ((Polynomial.lead_coeff p, (-1::rat)) # acc))"
using Rec.prems(2) by blast
then show ?case
using spmods_multiv_assum_acc spmods_multiv_aux_assum_acc
by (metis insert_subset inset_means_lookup_assump_some list.set(2))
next
case (Lookup0 p q acc)
then show ?case
by (meson inset_means_lookup_assump_some lookup_assum_aux_mem spmods_multiv_assum_acc subset_eq)
next
case (LookupN0 p q acc r)
then show ?case
by (meson in_set_member inset_means_lookup_assump_some lookup_assump_means_inset spmods_multiv_assum_acc subsetD)
qed

lemma spmods_multiv_aux_nonz_some:
fixes p:: "real mpoly Polynomial.poly"
fixes q:: "real mpoly Polynomial.poly"
assumes inset: "(assumps, sturm_seq) ∈ set (spmods_multiv_aux p q acc)"
shows "q ≠ 0 ⟹ ∃i. lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some i"
using assms
proof (induct p q acc rule: spmods_multiv_aux_induct)
case (Base p q acc)
then show ?case by auto
next
case (Rec p q acc)
then have "(lookup_assump_aux (Polynomial.lead_coeff q) acc) = None"
by meson
then have "set (spmods_multiv_aux p q acc) =
set (spmods_multiv_aux p (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # acc))
∪ set ( map (λx. (fst x, Cons p (snd x))) (spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (1::rat)) # acc)))
∪ set ( map (λx. (fst x, Cons p (snd x)))  (spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (-1::rat)) # acc)))"
using Rec.prems(1) spmods_multiv_aux.simps
by (simp add: Rec.prems(1) spmods_multiv_aux.simps sup_assoc)
then have bigh: "(assumps, sturm_seq) ∈ set (spmods_multiv_aux p (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # acc))
∨ (assumps, sturm_seq) ∈ set ( map (λx. (fst x, Cons p (snd x))) (spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (1::rat)) # acc)))
∨ (assumps, sturm_seq) ∈ set ( map (λx. (fst x, Cons p (snd x)))  (spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, (-1::rat)) # acc)))"
using Rec.prems(2)
by blast
have h1: "(⋀acc' seq' p q acc. (acc', seq') ∈ set (spmods_multiv_aux p q acc) ⟹ set acc ⊆ set acc') ⟹
(assumps, sturm_seq)
∈ set (spmods_multiv_aux p (Multiv_Poly_Props.one_less_degree q)
((Polynomial.lead_coeff q, 0) # acc)) ⟹
∃i. lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some i"
by (meson in_set_member inset_means_lookup_assump_some list.set_intros(1) subsetD)
have h2: "⋀b. (⋀acc' seq' p q acc. (acc', seq') ∈ set (spmods_multiv_aux p q acc) ⟹ set acc ⊆ set acc') ⟹
(assumps, b)
∈ set (spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, 1) # acc)) ⟹
sturm_seq = p # b ⟹ ∃i. lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some i"
by (meson in_set_member inset_means_lookup_assump_some list.set_intros(1) subsetD)
have h3: "⋀b. (⋀acc' seq' p q acc. (acc', seq') ∈ set (spmods_multiv_aux p q acc) ⟹ set acc ⊆ set acc') ⟹
(assumps, b)
∈ set (spmods_multiv_aux q (mul_pseudo_mod p q) ((Polynomial.lead_coeff q, - 1) # acc)) ⟹
sturm_seq = p # b ⟹ ∃i. lookup_assump_aux (Polynomial.lead_coeff q) assumps = Some i"
by (meson in_set_member inset_means_lookup_assump_some list.set_intros(1) subsetD)
show ?case
using bigh spmods_multiv_aux_assum_acc h1 h2 h3
by auto
next
case (Lookup0 p q acc)
then show ?case
by (meson inset_means_lookup_assump_some lookup_assum_aux_mem spmods_multiv_aux_assum_acc subsetD)
next
case (LookupN0 p q acc r)
then show ?case
by (meson in_set_member inset_means_lookup_assump_some lookup_assump_means_inset spmods_multiv_aux_assum_acc subsetD)
qed

lemma spmods_multiv_sound:
assumes "(assumps, sturm_seq) ∈ set (spmods_multiv p q acc)"
assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
shows "map (eval_mpoly_poly val) sturm_seq =
spmods (eval_mpoly_poly val p) (eval_mpoly_poly val q)"
using assms
proof (induct p q acc arbitrary:assumps sturm_seq rule: spmods_multiv_induct)
case (Base p q assumps)
then show ?case
next
case (Rec p q assumps)
then show ?case
by (smt (verit, best) UnE eval_mpoly_poly_one_less_degree list.set_intros(1) matches_ss option.simps(4) set_append spmods_multiv.simps spmods_multiv_assum_acc spmods_multiv_aux_assum_acc subsetD zero_neq_neg_one zero_neq_one)
next
case (Lookup0 p q assumps)
define pval where pval:"pval = eval_mpoly_poly val p"
define qval where qval:"qval = eval_mpoly_poly val q"
have "(Polynomial.lead_coeff p,0) ∈ set assumps"
using Lookup0.hyps Lookup0.prems
by (meson lookup_assum_aux_mem spmods_multiv_assum_acc subset_code(1))
then have "satisfies_evaluation val (Polynomial.lead_coeff p) 0"
using Lookup0.hyps Lookup0.prems by blast
from eval_mpoly_poly_one_less_degree[OF this] have
eval_prop: "eval_mpoly_poly val (one_less_degree p) = pval" using pval qval
by auto
have "map (eval_mpoly_poly val) sturm_seq = spmods pval qval"
using Lookup0.hyps Lookup0.prems pval qval
then show ?case
using pval qval by blast
next
case (LookupN0 p q assumps r)
define pval where pval:"pval = eval_mpoly_poly val p"
define qval where qval:"qval = eval_mpoly_poly val q"
{
assume right: "∃k. lookup_assump_aux (Polynomial.lead_coeff p) assumps = Some k ∧k ≠ 0"
then obtain k where k_prop: "lookup_assump_aux (Polynomial.lead_coeff p) assumps = Some k ∧k ≠ 0"
by auto
then have "(Polynomial.lead_coeff p,k) ∈ set assumps"
using spmods_multiv_aux_assum_acc
have "k ≠ 0"
using k_prop by auto
then have
"map (eval_mpoly_poly val) sturm_seq = spmods pval qval"
using matches_ss[of p k assumps sturm_seq q _ val] right LookupN0.prems(2)  LookupN0.prems LookupN0.hyps
using ‹(Polynomial.lead_coeff p, k) ∈ set assumps› pval qval