# Theory Hybrid_Multiv_Algorithm_Proofs

```(* This file includes proofs (soundness and completeness) for our
top-level hybrid QE algorithm defined in Hybrid_Multiv_Algorithm.thy.
*)

theory Hybrid_Multiv_Algorithm_Proofs

imports Hybrid_Multiv_Algorithm
Hybrid_Multiv_Matrix_Proofs
Virtual_Substitution.ExportProofs

begin

subsection "Lemmas about branching (lc assump generation)"

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

lemma lc_assump_generation_subset:
assumes "(branch_assms, branch_poly_list) ∈ set(lc_assump_generation q assumps)"
shows "set assumps ⊆ set branch_assms"
using assms
proof (induct q assumps rule: lc_assump_generation_induct)
case (Base q assumps)
then show ?case
next
case (Rec q assumps)
let ?zero = "lc_assump_generation (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # assumps)"
let ?one  = "((Polynomial.lead_coeff q, (1::rat)) # assumps, q)"
let ?minus_one  = "((Polynomial.lead_coeff q, (-1::rat)) # assumps, q)"
have "(branch_assms, branch_poly_list) ∈ set (?one#?minus_one#?zero)"
using Rec.hyps Rec(4) lc_assump_generation.simps by auto
then show ?case
using Rec(3) by force
next
case (Lookup0 q assumps)
then show ?case
using lc_assump_generation.simps
by simp
next
case (LookupN0 q assumps r)
then show ?case
qed

lemma branch_init_assms_subset:
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
shows "set init_assumps ⊆ set branch_assms"
using assms
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps)
case Nil
then show ?case
next
case (Cons a bpl)
then show ?case
using lc_assump_generation_subset
by blast
qed

lemma prod_list_var_gen_nonzero:
shows "prod_list_var_gen qs ≠ 0"
proof (induct qs)
case Nil
then show ?case by auto
next
case (Cons a qs)
then show ?case by auto
qed

(* Invariant: For all (a, q) in the output, either
q is 0 or the leading coefficient of q is assumed nonzero in a *)
lemma lc_assump_generation_inv:
assumes "(a, q) ∈ set (lc_assump_generation init_q assumps)"
shows "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
using assms
proof (induct init_q assumps arbitrary: q a rule: lc_assump_generation_induct )
case (Base init_q assumps)
then show ?case
using lc_assump_generation.simps by auto
next
case (Rec init_q assumps)
let ?zero = "lc_assump_generation (one_less_degree init_q) ((Polynomial.lead_coeff init_q, (0::rat)) # assumps)"
let ?one  = "((Polynomial.lead_coeff init_q, (1::rat)) # assumps, init_q)"
let ?minus_one = "((Polynomial.lead_coeff init_q, (-1::rat)) # assumps, init_q)"
have "(a, q) ∈ set (?one # ?minus_one # ?zero)"
using Rec.prems Rec.hyps(1) Rec.hyps(2) lc_assump_generation.simps
by auto
then have eo: "(a, q) = ?one ∨ (a, q) = ?minus_one ∨ (a, q) ∈ set(?zero)"
by auto
{assume *: "(a, q) = ?one"
then have "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
by auto
}
moreover {assume *: "(a, q) = ?minus_one"
then have "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
by auto
}
moreover   {assume *: "(a, q)  ∈ set(?zero)"
then have "q = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff q) a = Some i ∧ i ≠ 0))"
using Rec.hyps Rec.prems by auto
}
ultimately show ?case
using lc_assump_generation.simps
using eo by fastforce
next
case (Lookup0 init_q assumps)
then show ?case using lc_assump_generation.simps by auto
next
case (LookupN0 init_q assumps r)
then show ?case using lc_assump_generation.simps by auto
qed

lemma lc_assump_generation_list_inv:
assumes val: "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
shows "q ∈ set branch_poly_list ⟹ q = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff q) branch_assms = Some i ∧ i ≠ 0)"
using assms
proof (induct qs arbitrary: q init_assumps branch_poly_list branch_assms)
case Nil
then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
using lc_assump_generation_list.simps by auto
then have "branch_poly_list = []"
using in_set_member
by simp
then show ?case
using Nil.prems(1)
by simp
next
case (Cons a qs)
let ?rec = "lc_assump_generation a init_assumps"
have inset: "(branch_assms,branch_poly_list) ∈ set (
concat (map (
λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
using Cons.prems lc_assump_generation_list.simps
by auto
then obtain new_assumps r where deconstruct_prop:
"(new_assumps, r) ∈ set ?rec"
"(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec)"
using inset
by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
then obtain elem list_rec where list_rec_prop:
"list_rec = lc_assump_generation_list qs new_assumps"
"elem ∈ set list_rec"
"(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))"
by auto
then have pair_in_set: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
using deconstruct_prop by auto
then have snd_elem_is: "⋀q. q ∈ set (snd elem) ⟹
q = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff q) branch_assms = Some i ∧ i ≠ 0)"
using Cons.hyps
have ris_var: "r = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff r)new_assumps = Some i ∧ i ≠ 0) "
using lc_assump_generation_inv[of new_assumps r a init_assumps] deconstruct_prop(1)
by auto
have "set new_assumps ⊆ set branch_assms"
using deconstruct_prop list_rec_prop
using pair_in_set branch_init_assms_subset by presburger
then have "(∃i. lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i ∧ i ≠ 0) ⟹
(∃i. lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i ∧ i ≠ 0)"
using val lookup_assump_aux_subset_consistency
using local.Cons(3) by blast
then have ris: "r = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i ∧ i ≠ 0) "
using ris_var by auto
then show ?case
using ris snd_elem_is list_rec_prop(3)
using Cons.prems(1) by auto
qed

subsection "Correctness of sign determination inner"

lemma q_dvd_prod_list_var_prop:
assumes "q ∈ set qs"
assumes "q ≠ 0"
shows "q dvd prod_list_var_gen qs" using assms
proof (induct qs)
case Nil
then show ?case by auto
next
case (Cons a qs)
then have eo: "q = a ∨q ∈ set qs" by auto
have c1: "q = a ⟹ q dvd prod_list_var_gen (a#qs)"
proof -
assume "q = a"
then have "prod_list_var_gen (a#qs) = q*(prod_list_var_gen qs)" using Cons.prems
unfolding prod_list_var_gen_def by auto
then show ?thesis using prod_list_var_gen_nonzero[of qs] by auto
qed
have c2: "q ∈ set qs ⟶ q dvd prod_list_var_gen qs"
using Cons.prems Cons.hyps unfolding prod_list_var_gen_def by auto
show ?case using eo c1 c2 by auto
qed

lemma poly_p_nonzero_on_branch:
assumes assms: "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
assumes "p = poly_p_in_branch (branch_assms, branch_poly_list)"
shows "eval_mpoly_poly val p ≠ 0"
proof -
(* Some intuition: the assumps on the qs are contained in branch_assms,
then because branch_assms contains the proper assumps,
the poly_p_in_branch definition correctly handles things *)
{assume *: "(check_all_const_deg_gen branch_poly_list = True)"
then have p_is: "p = [:0, 1:]"
using assms
using poly_p_in_branch.simps by presburger
then have "eval_mpoly_poly val p ≠ 0"
by (metis Polynomial.lead_coeff_monom degree_0 dvd_refl eval_commutes eval_mpoly_map_poly_comm_ring_hom.base.hom_one not_is_unit_0 poly_dvd_1 x_as_monom)
}
moreover {assume *: "(check_all_const_deg_gen branch_poly_list = False)"
then have p_is: "p = (pderiv (prod_list_var_gen branch_poly_list)) * (prod_list_var_gen branch_poly_list)"
using assms
using poly_p_in_branch.simps by presburger
then have assms_inv: "⋀q. q ∈ set branch_poly_list ⟹ q = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff q) branch_assms = Some i ∧ i ≠ 0)"
using lc_assump_generation_list_inv assms
by (meson assms(2))
have q_inv: "⋀q. q ∈ set branch_poly_list ⟹ q ≠ 0 ⟹ eval_mpoly_poly val q ≠ 0"
using assms_inv assms
by (metis eval_commutes leading_coeff_0_iff lookup_assum_aux_mem satisfies_evaluation_nonzero)
then have "⋀q. q ∈ set branch_poly_list ⟹ (q ≠ 0 ⟷ eval_mpoly_poly val q ≠ 0)"
by auto
then have prod_list_eval: "(eval_mpoly_poly val (prod_list_var_gen branch_poly_list)) = (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list))"
proof (induct branch_poly_list)
case Nil
then show ?case by auto
next
case (Cons a branch_poly_list)
{ assume *: "a = 0"
then have h1: "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) =
eval_mpoly_poly val (prod_list_var_gen branch_poly_list)"
by simp
have "eval_mpoly_poly val a = 0"
using * by auto
then have h2: "prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))
= prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
by auto
then have "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) =
prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))"
using Cons.hyps Cons.prems h1 h2
}
moreover { assume *: "a ≠ 0"
then have h1: "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) =
(eval_mpoly_poly val a)*(eval_mpoly_poly val (prod_list_var_gen branch_poly_list))"
have "eval_mpoly_poly val a ≠ 0"
using * assms Cons.prems
by (meson list.set_intros(1))
then have h2: "prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))
= (eval_mpoly_poly val a)* prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
by auto
have "eval_mpoly_poly val (prod_list_var_gen (a # branch_poly_list)) =
prod_list_var_gen (map (eval_mpoly_poly val) (a # branch_poly_list))"
using Cons.hyps Cons.prems h1 h2
}
ultimately show ?case
by auto
qed
have degree_q_inv: "⋀q. q ∈ set branch_poly_list ⟹ q ≠ 0 ⟹ Polynomial.degree (eval_mpoly_poly val q) = Polynomial.degree q"
using assms_inv assms q_inv
by (metis degree_valuation lookup_assum_aux_mem)
have prod_nonz: "eval_mpoly_poly val (prod_list_var_gen branch_poly_list) ≠ 0"
using q_inv prod_list_eval
have ex_q: "∃q ∈ set branch_poly_list. (q ≠ 0 ∧ Polynomial.degree q > 0)"
using * proof (induct branch_poly_list)
case Nil
then show ?case by auto
next
case (Cons a branch_poly_list)
then show ?case
by (metis bot_nat_0.not_eq_extremum check_all_const_deg_gen.simps(2) degree_0 list.set_intros(1) list.set_intros(2))
qed
obtain pos_deg_poly where pos_deg_poly: "pos_deg_poly∈set branch_poly_list ∧ pos_deg_poly ≠ 0 ∧ 0 < Polynomial.degree pos_deg_poly"
using ex_q by blast
have "pos_deg_poly dvd (prod_list_var_gen branch_poly_list)"
then have nonc_dvd: "(eval_mpoly_poly val pos_deg_poly) dvd (eval_mpoly_poly val (prod_list_var_gen branch_poly_list))"
by blast
have "Polynomial.degree (eval_mpoly_poly val pos_deg_poly) > 0"
using pos_deg_poly degree_q_inv
by metis
then have prod_nonc:"Polynomial.degree (eval_mpoly_poly val (prod_list_var_gen branch_poly_list)) ≠ 0"
using  nonc_dvd prod_nonz
by (metis bot_nat_0.extremum_strict dvd_const)
then have "eval_mpoly_poly val p ≠ 0"
using prod_nonz prod_nonc
by (metis eval_mpoly_poly_comm_ring_hom.hom_mult no_zero_divisors p_is pderiv_commutes pderiv_eq_0_iff)
}
ultimately show ?thesis by auto
qed

lemma calc_data_to_signs_and_extract_signs:
shows "(calculate_data_to_signs ell) = extract_signs ell"
by auto

lemma branch_poly_eval:
assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "(eval_mpoly_poly val) q = (eval_mpoly_poly val) init_q"
using assms
proof (induct init_q init_assumps arbitrary: q a rule: lc_assump_generation_induct )
case (Base init_q init_assumps)
then show ?case
next
case (Rec init_q init_assumps)
then show ?case using lc_assump_generation.simps
basic_trans_rules(31) eval_mpoly_poly_one_less_degree in_set_member lc_assump_generation_subset member_rec(1) option.case(1) prod.inject
by (smt (verit, best))
next
case (Lookup0 init_q init_assumps)
then show ?case
using lc_assump_generation.simps
by (smt (z3) eval_mpoly_poly_one_less_degree lc_assump_generation_subset lookup_assum_aux_mem option.simps(5) subset_eq)
(* Takes a second to load *)
next
case (LookupN0 init_q init_assumps r)
then show ?case
qed

lemma eval_prod_list_var_gen_match:
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
shows "eval_mpoly_poly val (prod_list_var_gen branch_poly_list) =
prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
using assms
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps val)
case Nil
then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
using lc_assump_generation_list.simps by auto
then have "branch_poly_list = []"
using in_set_member
by simp
then show ?case
by simp
next
case (Cons a qs)
let ?rec = "lc_assump_generation a init_assumps"
have inset: "(branch_assms,branch_poly_list) ∈ set (
concat (map (
λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
using Cons.prems lc_assump_generation_list.simps
by auto
then obtain new_assumps r where deconstruct_prop:
"(new_assumps, r) ∈ set ?rec"
"(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec)"
using inset
by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
then obtain elem list_rec where list_rec_prop:
"list_rec = lc_assump_generation_list qs new_assumps"
"elem ∈ set list_rec"
"(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))"
by auto
then have branch_assms_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
using deconstruct_prop by auto
then have "set new_assumps ⊆ set branch_assms"
using deconstruct_prop list_rec_prop branch_init_assms_subset
by presburger
have ris_var: "r = 0 ∨ (∃i. lookup_assump_aux (Polynomial.lead_coeff r)new_assumps = Some i ∧ i ≠ 0) "
using lc_assump_generation_inv[of new_assumps r a init_assumps] deconstruct_prop(1)
by auto
then have r_prop: "r = 0 ⟷ eval_mpoly_poly val r = 0"
by (metis ‹set new_assumps ⊆ set branch_assms› basic_trans_rules(31) eval_commutes eval_mpoly_poly_comm_ring_hom.hom_zero leading_coeff_0_iff local.Cons(3) lookup_assum_aux_mem satisfies_evaluation_nonzero)
have "eval_mpoly_poly val (prod_list_var_gen (snd elem)) =
prod_list_var_gen (map (eval_mpoly_poly val) (snd elem))"
using Cons.hyps list_rec_prop
using branch_assms_inset local.Cons(3) by blast
then show ?case using r_prop list_rec_prop(3)
qed

lemma map_branch_poly_list:
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
shows "(map (eval_mpoly_poly val) qs) = (map (eval_mpoly_poly val) branch_poly_list)"
using assms
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps)
case Nil
then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
using lc_assump_generation_list.simps by auto
then have "branch_poly_list = []"
using in_set_member
by simp
then show ?case
using Nil.prems(1)
by meson
next
case (Cons a qs)
let ?rec = "lc_assump_generation a init_assumps"
have inset: "(branch_assms,branch_poly_list) ∈ set (
concat (map (
λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
using Cons.prems lc_assump_generation_list.simps
by auto
then obtain new_assumps r where deconstruct_prop:
"(new_assumps, r) ∈ set ?rec"
"(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec)"
using inset
by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
then obtain elem list_rec where list_rec_prop:
"list_rec = lc_assump_generation_list qs new_assumps"
"elem ∈ set list_rec"
"(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))"
by auto
then have branch_assms_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
using deconstruct_prop by auto
then have map_prop: "map (eval_mpoly_poly val) (qs) =
map (eval_mpoly_poly val) (snd elem)" using Cons.hyps Cons.prems
by blast
have "set new_assumps ⊆ set branch_assms"
using deconstruct_prop list_rec_prop branch_assms_inset branch_init_assms_subset
by presburger
then have "eval_mpoly_poly val r = eval_mpoly_poly val a"
using branch_poly_eval
by (meson basic_trans_rules(31) deconstruct_prop(1) local.Cons(3))
then show ?case
using map_prop list_rec_prop(3)
by simp
qed

lemma check_constant_degree_match:
assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "Polynomial.degree q = Polynomial.degree (eval_mpoly_poly val init_q)"
using assms
proof (induct init_q init_assumps arbitrary: q a rule: lc_assump_generation_induct )
case (Base init_q init_assumps)
then show ?case
using lc_assump_generation.simps
by simp
next
case (Rec init_q init_assumps)
then show ?case using lc_assump_generation.simps
by (metis branch_poly_eval degree_0 degree_valuation eval_mpoly_poly_comm_ring_hom.hom_zero lc_assump_generation_inv lookup_assum_aux_mem)
next
case (Lookup0 init_q init_assumps)
then show ?case  using lc_assump_generation.simps
by (metis branch_poly_eval degree_0 degree_valuation eval_mpoly_poly_comm_ring_hom.hom_zero lc_assump_generation_inv lookup_assum_aux_mem)
next
case (LookupN0 init_q init_assumps r)
then show ?case
using lc_assump_generation.simps
by (metis branch_poly_eval degree_0 degree_valuation eval_mpoly_poly_comm_ring_hom.hom_zero lc_assump_generation_inv lookup_assum_aux_mem)
qed

lemma check_constant_degree_match_list:
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
shows "(check_all_const_deg_gen branch_poly_list) = (check_all_const_deg_gen (map (eval_mpoly_poly val) qs))"
using assms
proof (induct qs arbitrary: branch_assms branch_poly_list init_assumps)
case Nil
then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
using lc_assump_generation_list.simps
by auto
then have "branch_poly_list = []"
using in_set_member
by simp
then show ?case
by simp
next
case (Cons a qs)
let ?rec = "lc_assump_generation a init_assumps"
have inset: "(branch_assms,branch_poly_list) ∈ set (
concat (map (
λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
using Cons.prems lc_assump_generation_list.simps
by auto
then obtain new_assumps r where deconstruct_prop:
"(new_assumps, r) ∈ set ?rec"
"(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec)"
using inset
by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
then obtain elem list_rec where list_rec_prop:
"list_rec = lc_assump_generation_list qs new_assumps"
"elem ∈ set list_rec"
"(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))"
by auto
then have branch_assms_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
using deconstruct_prop by auto
then have ind_prop: "(check_all_const_deg_gen (snd elem)) = (check_all_const_deg_gen (map (eval_mpoly_poly val) qs))" using Cons.hyps Cons.prems
by blast
have "set new_assumps ⊆ set branch_assms"
using deconstruct_prop list_rec_prop branch_assms_inset branch_init_assms_subset
by presburger
then have "Polynomial.degree r = Polynomial.degree (eval_mpoly_poly val a)"
using check_constant_degree_match
by (meson basic_trans_rules(31) deconstruct_prop(1) local.Cons(3))
then show ?case
using ind_prop list_rec_prop(3)
by simp
qed

lemma check_all_const_deg_match:
shows "check_all_const_deg qs = check_all_const_deg_gen qs"
proof (induct qs)
case Nil
then show ?case by auto
next
case (Cons a qs)
then show ?case by auto
qed

lemma prod_list_var_match:
shows "prod_list_var_gen qs = prod_list_var qs"
proof (induct qs)
case Nil
then show ?case by auto
next
case (Cons a qs)
then show ?case by auto
qed

assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "q ≠ 0"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "((Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))) =
using assms
proof (induct init_q init_assumps arbitrary: q a rule: lc_assump_generation_induct )
case (Base init_q init_assumps)
then show ?case using lc_assump_generation.simps
by simp
next
case (Rec init_q init_assumps)
let ?zero = "lc_assump_generation (one_less_degree init_q) ((Polynomial.lead_coeff init_q, (0::rat)) # init_assumps)"
let ?one  = "((Polynomial.lead_coeff init_q, (1::rat)) # init_assumps, init_q)"
let ?minus_one  = "((Polynomial.lead_coeff init_q, (-1::rat)) # init_assumps, init_q)"
have inset: "(a, q) ∈ set (?one#?minus_one#?zero)"
using Rec.hyps lc_assump_generation.simps Rec(4)
by auto
{ assume * : "(a, q) = ?one"
then have h1: "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = (1::rat)"
by auto
have h2: "satisfies_evaluation val (Polynomial.lead_coeff q) (1)"
using Rec.hyps
by (metis "*" Pair_inject Rec.prems(3) list.set_intros(1))
then have h3: "Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q)) = (1::int)"
unfolding satisfies_evaluation_def eval_mpoly_def
by (metis Sturm_Tarski.sign_def h2 lead_coeff_valuation of_int_hom.injectivity one_neq_zero satisfies_evaluation_def verit_comp_simplify(28))
(* may take a second to load *)
have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) =
using h1 h3
by auto
} moreover {
assume * : "(a, q) = ?minus_one"
then have h1: "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) = (-1::rat)"
by auto
have h2: "satisfies_evaluation val (Polynomial.lead_coeff q) (-1)"
using Rec.hyps
by (metis "*" Pair_inject Rec.prems(3) list.set_intros(1))
then have h3: "rat_of_int (Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q))) = (-1::rat)"
unfolding satisfies_evaluation_def eval_mpoly_def
by (metis Sturm_Tarski.sign_def degree_valuation eval_mpoly_def eval_mpoly_map_poly_comm_ring_hom.base.coeff_map_poly_hom eval_mpoly_poly_def h2 of_int_hom.hom_one of_int_hom.injectivity of_int_minus rel_simps(88) sign_uminus verit_comp_simplify(28))
(* May take a second to load *)
have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) =
using h1 h3
by (metis of_int_eq_iff of_rat_of_int_eq)
}
moreover {
assume * : "(a, q) ∈ set ?zero"
then have "(a, q)
∈ set (lc_assump_generation (Multiv_Poly_Props.one_less_degree init_q)
by auto
then have "set ((Polynomial.lead_coeff init_q, 0) # init_assumps) ⊆ set a "
using lc_assump_generation_subset by presburger
then have "⋀p n. (p, n) ∈ set ((Polynomial.lead_coeff init_q, 0) # init_assumps) ⟹ satisfies_evaluation val p n"
using Rec.prems by auto
then have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) =
using Rec.hyps Rec.prems
by (smt (verit, ccfv_SIG) "*" Sturm_Tarski.sign_cases more_arith_simps(10) neg_one_neq_one sign_uminus)
(* Takes a couple seconds to load *)
}
ultimately show ?case using lc_assump_generation.simps
inset
by (smt (verit, del_insts) set_ConsD) (* Takes a second *)
next
case (Lookup0 init_q init_assumps)
then show ?case using lc_assump_generation.simps
by auto

next
case (LookupN0 init_q init_assumps r)
then have match: "(a, q) = (init_assumps, init_q)"
using lc_assump_generation.simps in_set_member by auto
then obtain i where i_prop: "i ≠ 0"
"lookup_assump_aux (Polynomial.lead_coeff init_q) init_assumps = Some i"
"(Polynomial.lead_coeff init_q, i) ∈ set init_assumps"
using LookupN0.prems LookupN0.hyps
by (meson lookup_assum_aux_mem)
then have "(Polynomial.lead_coeff init_q, i) ∈ set a"
using match by auto
then have sat_eval: "satisfies_evaluation val (Polynomial.lead_coeff init_q) i"
using LookupN0(6) by blast
have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a)
= Sturm_Tarski.sign i"
using i_prop match lookup_assump_aux_subset_consistent_sign
by simp
then show ?case
by (smt (verit, del_insts) LookupN0(6) LookupN0.prems(1) sat_eval branch_poly_eval i_prop(1) lead_coeff_valuation of_int_hom.injectivity satisfies_evaluation_def)
qed

assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "q ≠ 0"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a) =
by (metis assms(1) assms(2) assms(3))

lemma pos_limit_point_on_branch:
assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val q))) =
(if q = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))"
using assms
proof -
have "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val q))) =
Sturm_Tarski.sign (Polynomial.lead_coeff (eval_mpoly_poly val q)) "
unfolding sgn_pos_inf_def
by auto
then show ?thesis using sign_lead_coeff_on_branch assms
by (smt (verit, del_insts) eval_mpoly_poly_comm_ring_hom.hom_zero leading_coeff_0_iff sign_simps(2))
(* May take a few seconds to load *)
qed

lemma pos_limit_point_on_branch_init:
assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val init_q))) =
(if q = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))"
using branch_poly_eval by force

lemma pos_limit_point_on_branch_list:
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
assumes "(pos_limit_branch, neg_limit_branch) = limit_points_on_branch (branch_assms, branch_poly_list)"
shows "map rat_of_int (sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs)) = pos_limit_branch"
using assms
proof (induct qs arbitrary: pos_limit_branch neg_limit_branch branch_assms branch_poly_list init_assumps)
case Nil
then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
using lc_assump_generation_list.simps
by auto
then have "branch_poly_list = []"
using in_set_member
by simp
then show ?case using Nil.prems
unfolding eval_mpoly_poly_def sgn_pos_inf_rat_list_def
by auto
next
case (Cons a qs)
let ?rec = "lc_assump_generation a init_assumps"
have inset: "(branch_assms,branch_poly_list) ∈ set (
concat (map (
λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
using Cons.prems lc_assump_generation_list.simps
by auto
then obtain new_assumps r where deconstruct_prop:
"(new_assumps, r) ∈ set ?rec"
"(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec)"
using inset
by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
then obtain elem list_rec where list_rec_prop:
"list_rec = lc_assump_generation_list qs new_assumps"
"elem ∈ set list_rec"
"(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))"
by auto
then have snd_elem_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
using deconstruct_prop by auto
obtain pos_limit_sublist neg_limit_sublist where sublist_prop:
"(pos_limit_sublist, neg_limit_sublist) = limit_points_on_branch (branch_assms, snd elem)"
by auto
then have ind_prop: "pos_limit_sublist = map rat_of_int (sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))"
using snd_elem_inset Cons.hyps Cons.prems
by blast
have sublist_connection: "pos_limit_branch = (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))#pos_limit_sublist"
using Cons.prems(3) sublist_prop list_rec_prop(3)
by simp
have list_prop: "map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
(map (eval_mpoly_poly val) (a#qs)) =
(rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a)))) # map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
(map (eval_mpoly_poly val) qs)"
by simp
have tail_prop: "pos_limit_branch =
(if r = 0 then 0
else Sturm_Tarski.sign
map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
(map (eval_mpoly_poly val) qs)"
using sublist_connection ind_prop  unfolding sgn_pos_inf_rat_list_def
by auto
have subs: "set new_assumps ⊆ set branch_assms"
using deconstruct_prop list_rec_prop snd_elem_inset branch_init_assms_subset
by presburger
then have r_sign: "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a))) =
(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))"
using pos_limit_point_on_branch_init deconstruct_prop(1) local.Cons(3) subsetD
by (smt (verit, ccfv_threshold))
have r_inv: "r = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i ∧ i ≠ 0))"
using lc_assump_generation_inv
by (meson deconstruct_prop(1))
have r_match: " (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
proof -
{assume *: "r = 0"
then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
by auto
} moreover {assume *: "r ≠ 0"
then obtain i1 where i1_prop: "lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i1 ∧ i1 ≠ 0"
using r_inv by auto
then obtain i2 where i2_prop: "lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i2 ∧ i2 ≠ 0"
using lookup_assump_aux_subset_consistency subs
using Cons.prems(2) by blast
then have " Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps) =
using lookup_assump_aux_subset_consistent_sign subs
i1_prop i2_prop Cons.prems(2)
proof -
obtain mm :: "real list ⇒ (real mpoly × rat) list ⇒ real mpoly" and rr :: "real list ⇒ (real mpoly × rat) list ⇒ rat" where
"∀x4 x5. (∃v6 v7. (v6, v7) ∈ set x5 ∧ ¬ satisfies_evaluation x4 v6 v7) = ((mm x4 x5, rr x4 x5) ∈ set x5 ∧ ¬ satisfies_evaluation x4 (mm x4 x5) (rr x4 x5))"
by moura
then have "∀ps rs psa p r ra. ((mm rs ps, rr rs ps) ∈ set ps ∧ ¬ satisfies_evaluation rs (mm rs ps) (rr rs ps) ∨ ¬ set psa ⊆ set ps ∨ lookup_assump_aux (Polynomial.lead_coeff p) psa ≠ Some r ∨ lookup_assump_aux (Polynomial.lead_coeff p) ps ≠ Some ra) ∨ (Sturm_Tarski.sign r) = Sturm_Tarski.sign ra"
by (meson lookup_assump_aux_subset_consistent_sign)
then have "(Sturm_Tarski.sign i1) = Sturm_Tarski.sign i2"
using i1_prop i2_prop local.Cons(3) subs by blast
then show ?thesis
qed
(*  by (smt (verit, del_insts) lookup_assump.simps option.case(2)) *)
then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
by auto
}
ultimately show ?thesis
by auto
qed
then have "rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a))) =
(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
using r_sign r_match
by fastforce
then have "pos_limit_branch = (rat_of_int (Sturm_Tarski.sign (sgn_pos_inf (eval_mpoly_poly val a)))) #
(map (λx. rat_of_int (Sturm_Tarski.sign (sgn_pos_inf x)))
(map (eval_mpoly_poly val) qs)) "
using tail_prop
by (smt (verit, ccfv_threshold) list.inj_map_strong list.map(2) of_rat_hom.eq_iff)
then show ?case using  list_prop
using sgn_pos_inf_rat_list_def
by (auto)
qed

lemma neg_limit_point_on_branch_init:
assumes "(a, q) ∈ set (lc_assump_generation init_q init_assumps)"
assumes "⋀p n. (p,n) ∈ set a ⟹ satisfies_evaluation val p n"
shows "rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val init_q))) =
(if q = 0 then 0 else (Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))*(-1)^(Polynomial.degree q))"
proof -
have at_inf: "rat_of_int
(Sturm_Tarski.sign  (sgn_class.sgn (Polynomial.lead_coeff (eval_mpoly_poly val init_q)))) =
(if q = 0 then 0
else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff q) a))"
using assms  pos_limit_point_on_branch_init
unfolding sgn_pos_inf_def
by auto
have "Polynomial.degree q = Polynomial.degree (eval_mpoly_poly val init_q)"
using check_constant_degree_match assms by auto
then show ?thesis using at_inf
unfolding sgn_neg_inf_def
using Sturm_Tarski_casting degree_0 even_zero more_arith_simps(6) more_arith_simps(8) ring_1_class.minus_one_power_iff by auto
(* Takes a couple seconds to load *)
qed

lemma neg_limit_point_on_branch_list:
assumes "(branch_assms, branch_poly_list) ∈ set (lc_assump_generation_list qs init_assumps)"
assumes "⋀p n. (p,n) ∈ set branch_assms ⟹ satisfies_evaluation val p n"
assumes "(pos_limit_branch, neg_limit_branch) = limit_points_on_branch (branch_assms, branch_poly_list)"
shows "map rat_of_int (sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs)) = neg_limit_branch"
using assms
proof (induct qs arbitrary: pos_limit_branch neg_limit_branch branch_assms branch_poly_list init_assumps)
case Nil
then have "(branch_assms, branch_poly_list) ∈ set [(init_assumps, [])]"
using lc_assump_generation_list.simps
by auto
then have "branch_poly_list = []"
using in_set_member
by simp
then show ?case using Nil.prems
unfolding eval_mpoly_poly_def sgn_neg_inf_rat_list_def
by auto
next
case (Cons a qs)
let ?rec = "lc_assump_generation a init_assumps"
have inset: "(branch_assms,branch_poly_list) ∈ set (
concat (map (
λ(new_assumps, r). (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec) ) ?rec ))"
using Cons.prems lc_assump_generation_list.simps
by auto
then obtain new_assumps r where deconstruct_prop:
"(new_assumps, r) ∈ set ?rec"
"(branch_assms,branch_poly_list) ∈ set (let list_rec = lc_assump_generation_list qs new_assumps in
map (λelem. (fst elem, r#(snd elem))) list_rec)"
using inset
by (metis (no_types, lifting) concat_map_in_set nth_mem prod.collapse split_def)
then obtain elem list_rec where list_rec_prop:
"list_rec = lc_assump_generation_list qs new_assumps"
"elem ∈ set list_rec"
"(branch_assms,branch_poly_list) = (fst elem, r#(snd elem))"
by auto
then have snd_elem_inset: "(branch_assms, snd elem) ∈ set (lc_assump_generation_list qs new_assumps)"
using deconstruct_prop by auto
obtain pos_limit_sublist neg_limit_sublist where sublist_prop:
"(pos_limit_sublist, neg_limit_sublist) = limit_points_on_branch (branch_assms, snd elem)"
by auto
then have ind_prop_var: "neg_limit_sublist = map rat_of_int (sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs))"
using snd_elem_inset Cons.hyps Cons.prems by blast
then have ind_prop: "neg_limit_sublist = sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs)"
by auto
have sublist_connection: "pos_limit_branch = (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))#pos_limit_sublist"
using Cons.prems(3) sublist_prop list_rec_prop(3)
by simp
then have sublist_connection_var: "pos_limit_branch = (if r = 0 then 0 else (rat_of_int ∘ Sturm_Tarski.sign) (lookup_assump (Polynomial.lead_coeff r) branch_assms))#pos_limit_sublist"
using Cons.prems(3) sublist_prop list_rec_prop(3)
by simp
have list_prop: "map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
(map (eval_mpoly_poly val) (a#qs)) =
(rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a)))) # map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
(map (eval_mpoly_poly val) qs)"
by simp
have ind_prop_var2: "neg_limit_sublist =
(map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))
(map (eval_mpoly_poly val) qs))"
using ind_prop_var unfolding sgn_neg_inf_rat_list_def
by auto
have "neg_limit_branch =
(if r = 0 then (0::rat)
else ((rat_of_int ∘ Sturm_Tarski.sign)
(lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))) #
map (λx. ((rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x)))
(map (eval_mpoly_poly val) qs)"
using  sublist_connection_var ind_prop_var2 local.Cons(4)  unfolding sgn_neg_inf_rat_list_def
unfolding limit_points_on_branch.simps
by (metis (no_types, lifting) limit_points_on_branch.simps list.simps(9) list_rec_prop(3) prod.simps(1) sublist_prop)
then have tail_prop_helper: "neg_limit_branch =
(if r = 0 then 0
else rat_of_int (Sturm_Tarski.sign
(lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))) #
map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
(map (eval_mpoly_poly val) qs)"
by auto
then have tail_prop: "neg_limit_branch =
(if r = 0 then 0
else Sturm_Tarski.sign
(lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r)) #
map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
(map (eval_mpoly_poly val) qs)"
by (smt (verit, ccfv_threshold) list.map(2) of_int_hom.hom_zero of_rat_of_int_eq)
have subs: "set new_assumps ⊆ set branch_assms"
using deconstruct_prop list_rec_prop snd_elem_inset branch_init_assms_subset
by presburger
then have r_sign: "rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a))) =
(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps)*(-1)^(Polynomial.degree r))"
using neg_limit_point_on_branch_init deconstruct_prop(1) local.Cons(3) subsetD
by (smt (verit, ccfv_threshold))
have r_inv: "r = (0::rmpoly) ∨ (∃i. (lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i ∧ i ≠ 0))"
using lc_assump_generation_inv
by (meson deconstruct_prop(1))
have r_match_pre: " (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
proof -
{assume *: "r = 0"
then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
by auto
} moreover {assume *: "r ≠ 0"
then obtain i1 where i1_prop: "lookup_assump_aux (Polynomial.lead_coeff r) new_assumps = Some i1 ∧ i1 ≠ 0"
using r_inv by auto
then obtain i2 where i2_prop: "lookup_assump_aux (Polynomial.lead_coeff r) branch_assms = Some i2 ∧ i2 ≠ 0"
using lookup_assump_aux_subset_consistency subs
using Cons.prems(2) by blast
then have "Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps) =
using lookup_assump_aux_subset_consistent_sign subs
i1_prop i2_prop Cons.prems(2)
proof -
obtain mm :: "real list ⇒ (real mpoly × rat) list ⇒ real mpoly" and rr :: "real list ⇒ (real mpoly × rat) list ⇒ rat" where
"∀x4 x5. (∃v6 v7. (v6, v7) ∈ set x5 ∧ ¬ satisfies_evaluation x4 v6 v7) = ((mm x4 x5, rr x4 x5) ∈ set x5 ∧ ¬ satisfies_evaluation x4 (mm x4 x5) (rr x4 x5))"
by moura
then have "∀ps rs psa p r ra. ((mm rs ps, rr rs ps) ∈ set ps ∧ ¬ satisfies_evaluation rs (mm rs ps) (rr rs ps) ∨ ¬ set psa ⊆ set ps ∨ lookup_assump_aux (Polynomial.lead_coeff p) psa ≠ Some r ∨ lookup_assump_aux (Polynomial.lead_coeff p) ps ≠ Some ra) ∨ (Sturm_Tarski.sign r) = Sturm_Tarski.sign ra"
by (meson lookup_assump_aux_subset_consistent_sign)
then have "(Sturm_Tarski.sign i1) = Sturm_Tarski.sign i2"
using i1_prop i2_prop local.Cons(3) subs by blast
then show ?thesis
qed
(*  by (smt (verit, del_insts) lookup_assump.simps option.case(2)) *)
then have "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms))"
by auto
}
ultimately show ?thesis
by auto
qed
then have r_match: "(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) new_assumps)*(-1)^(Polynomial.degree r))
=  (if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))"
by metis
then have "rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a))) =
(if r = 0 then 0 else Sturm_Tarski.sign (lookup_assump (Polynomial.lead_coeff r) branch_assms)*(-1)^(Polynomial.degree r))"
using r_sign r_match
by fastforce
then have "neg_limit_branch = (rat_of_int (Sturm_Tarski.sign (sgn_neg_inf (eval_mpoly_poly val a)))) #
(map (λx. rat_of_int (Sturm_Tarski.sign (sgn_neg_inf x)))
(map (eval_mpoly_poly val) qs)) "
using tail_prop tail_prop_helper
then show ?case using  list_prop
using sgn_neg_inf_rat_list_def
by auto
qed

lemma complex_rat_casting_lemma:
fixes a:: "int list"
fixes b:: "rat list"
shows "map complex_of_int a = map of_rat b ⟹ map rat_of_int a = b"
by (metis (no_types, lifting) list.inj_map_strong list.map_comp of_rat_hom.injectivity of_rat_of_int)

lemma complex_rat_casting_lemma_sets:
fixes a:: "rat list list"
fixes b1:: "int list"
fixes b2:: "int list"
fixes c:: "rat list list"
assumes "set (map (map of_rat) a) ∪ {map complex_of_int b1, map complex_of_int b2}
= set (map (map of_rat) c)"
shows "set a ∪ {map rat_of_int b1, map rat_of_int b2} = set c"
proof -
have "map complex_of_int b1 ∈ set (map (map of_rat) c)"
using assms by auto
then have h1: "map rat_of_int b1 ∈ set c"
using complex_rat_casting_lemma by auto
have "map complex_of_int b2 ∈ set (map (map of_rat) c)"
using assms by auto
then have h2: "map rat_of_int b2 ∈ set c"
using complex_rat_casting_lemma by auto
have set_lem: "⋀ a b c . a ∪ b = c ⟹ a ⊆ c"
by blast
have "set (map (map of_rat) a) ⊆ set (map (map of_rat) c)"
using assms set_lem[of "set (map (map of_rat) a)" "{map complex_of_int b1, map complex_of_int b2}" "set (map (map of_rat) c)"]
by auto
then have "⋀x. x ∈ set (map (map of_rat) a) ⟹ x ∈ set (map (map of_rat) c)"
by auto
then have h3: "⋀x. x ∈ set a ⟹ x ∈ set c"
using complex_rat_casting_lemma
by fastforce
have h4_a: "⋀x. x ∈ set (map (map of_rat) c) ⟹
x ≠ map complex_of_int b1 ⟹ x ∉ set (map (map of_rat) a) ⟹ x = map complex_of_int b2"
using assms
by blast
have h4: "⋀x. x ∈ set c ⟹
x ≠ map rat_of_int b1 ⟹ x ∉ set a ⟹ x = map rat_of_int b2"
proof -
fix x
assume a1: "x ∈ set c"
assume a2: "x ≠ map rat_of_int b1"
assume a3: "x ∉ set a"
have "((map of_rat x)::complex list) ∈ set (map (map of_rat) c)"
using a1 by auto
then have impl: "((map of_rat x)::complex list) ≠ map complex_of_int b1 ⟹ (map of_rat x) ∉ set (map (map of_rat) a) ⟹ (map of_rat x) = map complex_of_int b2"
using h4_a[of "((map of_rat x)::complex list)"]
using a3 imageE inj_map_eq_map list.set_map of_rat_hom.inj_f by fastforce
have impl_h1: "((map of_rat x)::complex list) ≠ map complex_of_int b1"
using a2 complex_rat_casting_lemma
by metis
have impl_h2: "(map of_rat x) ∉ set (map (map of_rat) a)"
using a3 complex_rat_casting_lemma by (auto)
then have "(map of_rat x) = map complex_of_int b2"
using impl impl_h1 impl_h2 by auto
then show "x = map rat_of_int b2"
using complex_rat_casting_lemma by metis
qed
show ?thesis using h1 h2 h3 h4 by auto
qed

lemma complex_rat_casting_lemma_sets2:
shows "{map rat_of_int
(map (λx. Sturm_Tarski.sign (sgn_neg_inf x))
(map (eval_mpoly_poly val) qs)),
map rat_of_int
(map (λx. Sturm_Tarski.sign (sgn_pos_inf x))
(map (eval_mpoly_poly val) qs))} = {map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))
(map (eval_mpoly_poly val) qs),
map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_pos_inf x))
(map (eval_mpoly_poly val) qs)}"
proof -
have h1: "map rat_of_int
(map (λx. Sturm_Tarski.sign (sgn_neg_inf x))
(map (eval_mpoly_poly val) qs)) = map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_neg_inf x))
(map (eval_mpoly_poly val) qs)"
by auto
have h2: "map rat_of_int
(map (λx. Sturm_Tarski.sign (sgn_pos_inf x))
(map (eval_mpoly_poly val) qs)) = map (λx. (rat_of_int ∘ Sturm_Tarski.sign) (sgn_pos_inf x))
(map (eval_mpoly_poly val) qs)"
by auto
show ?thesis using h1 h2
by auto
qed

lemma sign_determination_inner_gives_noncomp_signs_at_roots:
assumes "(assumps, signs) ∈ set (sign_determination_inner qs init_assumps)"
assumes "⋀p n. (p,n) ∈ set assumps ⟹ satisfies_evaluation val p n"
shows "set signs = (consistent_sign_vectors_R (map (eval_mpoly_poly val) qs) UNIV)"
proof -
have elem_in_set: "(assumps, signs) ∈ set (let branches = lc_assump_generation_list qs init_assumps  in
concat (map (λbranch.
let poly_p_branch = poly_p_in_branch branch;
(pos_limit_branch, neg_limit_branch) = limit_points_on_branch branch;
calculate_data_branch = extract_signs (calculate_data_assumps_M poly_p_branch (snd branch) (fst branch))
in map (λ(a, signs). (a, pos_limit_branch#neg_limit_branch#signs)) calculate_data_branch
) branches))"
using assms
by auto
obtain branch where branch_prop: "branch ∈ set (lc_assump_generation_list qs init_assumps)"
"(assumps, signs) ∈ set (
let poly_p_branch = poly_p_in_branch branch;
(pos_limit_branch, neg_limit_branch) = limit_points_on_branch branch;
calculate_data_branch = extract_signs (calculate_data_assumps_M poly_p_branch (snd branch) (fst branch))
in map (λ(a, signs). (a, pos_limit_branch#neg_limit_branch#signs)) calculate_data_branch)"
using elem_in_set
by auto
then obtain branch_assms branch_poly_list where branch_is:
"branch = (branch_assms, branch_poly_list)"
using poly_p_in_branch.cases by blast
then obtain calculate_data_branch poly_p_branch pos_limit_branch neg_limit_branch
where branch_prop_expanded:
"poly_p_branch = poly_p_in_branch branch"
"(pos_limit_branch, neg_limit_branch) = limit_points_on_branch branch"
"calculate_data_branch = extract_signs (calculate_data_assumps_M poly_p_branch branch_poly_list branch_assms)"
"branch ∈ set (lc_assump_generation_list qs init_assumps)"
"(assumps, signs) ∈ set (
map (λ(a, signs). (a, pos_limit_branch#neg_limit_branch#signs)) calculate_data_branch)"
using branch_prop
by (metis (no_types, lifting) case_prod_beta fst_conv prod.exhaust_sel snd_conv)
obtain calc_a calc_signs where calc_prop:
"(calc_a, calc_signs) ∈ set calculate_data_branch"
"(assumps, signs) = (calc_a, pos_limit_branch#neg_limit_branch#calc_signs)"
using in_set_member branch_prop_expanded(5)
by auto
then have branch_assms_subset: "set branch_assms ⊆ set assumps"
using branch_prop_expanded(3) extract_signs_M_subset
by blast
have "set init_assumps ⊆ set branch_assms"
using branch_is branch_prop(1) branch_init_assms_subset
by blast
have assumps_calc_a: "assumps = calc_a"
using calc_prop by auto
let ?poly_p_branch = "poly_p_in_branch (branch_assms, branch_poly_list)"
have nonz_poly_p: "eval_mpoly_poly val ?poly_p_branch ≠ 0"
using poly_p_nonzero_on_branch
using ‹set branch_assms ⊆ set assumps› assms(2) branch_is branch_prop(1) by blast
have map_branch_poly_list: "(map (eval_mpoly_poly val) qs) = (map (eval_mpoly_poly val) branch_poly_list)"
using map_branch_poly_list
using assms(2) branch_assms_subset branch_is branch_prop(1) by blast
have "(calc_a, calc_signs)
∈ set (calculate_data_to_signs (calculate_data_assumps_M poly_p_branch branch_poly_list branch_assms))"
using calc_prop branch_prop_expanded calc_data_to_signs_and_extract_signs
by metis
then have "(assumps, calc_signs)
∈ set (calculate_data_to_signs (calculate_data_assumps_M poly_p_branch branch_poly_list branch_assms))"
using assumps_calc_a by auto
then have "set calc_signs = set(characterize_consistent_signs_at_roots (eval_mpoly_poly val ?poly_p_branch) (map (eval_mpoly_poly val) branch_poly_list))"
using nonz_poly_p calculate_data_assumps_gives_noncomp_signs_at_roots[of assumps signs poly_p_branch branch_poly_list branch_assms val ]
using assms(2) branch_is branch_prop_expanded(1) calculate_data_assumps_gives_noncomp_signs_at_roots by blast
then have calc_signs_is: "set calc_signs = set(characterize_consistent_signs_at_roots (eval_mpoly_poly val ?poly_p_branch) (map (eval_mpoly_poly val) qs))"
using map_branch_poly_list by auto
have poly_p_is: "poly_p_in_branch (branch_assms, branch_poly_list) = (if (check_all_const_deg_gen branch_poly_list = True) then  [:0, 1:] else
(pderiv (prod_list_var_gen branch_poly_list)) * (prod_list_var_gen branch_poly_list))"
by auto
have const_match: "(check_all_const_deg_gen branch_poly_list) = (check_all_const_deg_gen (map (eval_mpoly_poly val) qs))"
using check_constant_degree_match_list
using assms(2) branch_assms_subset branch_is branch_prop(1) by blast
have "eval_mpoly_poly val (prod_list_var_gen branch_poly_list) =
prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)"
using eval_prod_list_var_gen_match
using assms(2) branch_assms_subset branch_is branch_prop(1) by blast
then have same_prod:  "eval_mpoly_poly val ((pderiv (prod_list_var_gen branch_poly_list)) * (prod_list_var_gen branch_poly_list))
= pderiv (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)) * (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list))"
by (metis eval_mpoly_poly_comm_ring_hom.hom_mult pderiv_commutes)
{assume *: "check_all_const_deg_gen branch_poly_list = True"
then have "?poly_p_branch = [: 0, 1 :]"
using poly_p_is by presburger
then have "(eval_mpoly_poly val ?poly_p_branch) = [:0, 1:]"
unfolding eval_mpoly_poly_def
by auto
then have "(eval_mpoly_poly val ?poly_p_branch) =  (poly_f_nocrb (map (eval_mpoly_poly val) qs))"
unfolding poly_f_nocrb_def using const_match check_all_const_deg_match "*"
by presburger
}
moreover {assume *: "check_all_const_deg_gen branch_poly_list = False"
then have "(eval_mpoly_poly val ?poly_p_branch)  = pderiv (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list)) * (prod_list_var_gen (map (eval_mpoly_poly val) branch_poly_list))"
using poly_p_is same_prod by auto
then have h1: "(eval_mpoly_poly val ?poly_p_branch)  = pderiv (prod_list_var_gen (map (eval_mpoly_poly val) qs)) * (prod_list_var_gen (map (eval_mpoly_poly val) qs))"
using map_branch_poly_list
by presburger
have "(check_all_const_deg (map (eval_mpoly_poly val) qs) = False) "
using * const_match check_all_const_deg_match by auto
then have "(eval_mpoly_poly val ?poly_p_branch) =  (poly_f_nocrb (map (eval_mpoly_poly val) qs))"
using h1 prod_list_var_match
unfolding poly_f_nocrb_def
by metis
}
ultimately have poly_branch_no_crb_connect: "(eval_mpoly_poly val ?poly_p_branch) =  (poly_f_nocrb (map (eval_mpoly_poly val) qs))"
by auto
let ?eval_qs = "(map (eval_mpoly_poly val) qs)"
have "set calc_signs =
set (characterize_consistent_signs_at_roots (poly_f_nocrb ?eval_qs) ?eval_qs)"
using poly_branch_no_crb_connect calc_signs_is
by presburger
(* Use Renegar_Modified *)
then have calc_signs_relation: "(set calc_signs) ∪ {sgn_neg_inf_rat_list ?eval_qs, sgn_pos_inf_rat_list ?eval_qs} =
set (characterize_consistent_signs_at_roots (poly_f ?eval_qs) ?eval_qs)"
using poly_f_ncrb_connection[of ?eval_qs]
by auto
(* Some minor casting details *)
then have "set calc_signs ∪
{map rat_of_int
(sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs)),
map rat_of_int
(sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))} =
set (characterize_consistent_signs_at_roots
(poly_f (map (eval_mpoly_poly val) qs))
(map (eval_mpoly_poly val) qs))"
unfolding sgn_neg_inf_rat_list2_def sgn_pos_inf_rat_list2_def
using complex_rat_casting_lemma_sets[of calc_signs "(sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs))" "(sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))"
"(characterize_consistent_signs_at_roots (poly_f (map (eval_mpoly_poly val) qs)) (map (eval_mpoly_poly val) qs))"]
by (auto)
then have calc_signs_relation_var: "(set calc_signs) ∪ ({sgn_neg_inf_rat_list2 ?eval_qs, sgn_pos_inf_rat_list2 ?eval_qs}::rat list set) =
set (characterize_consistent_signs_at_roots (poly_f ?eval_qs) ?eval_qs)"
unfolding sgn_neg_inf_rat_list2_def sgn_pos_inf_rat_list2_def sgn_neg_inf_rat_list_def sgn_pos_inf_rat_list_def
using complex_rat_casting_lemma_sets2
by auto
have pos_inf: "sgn_pos_inf_rat_list ?eval_qs = pos_limit_branch"
using branch_prop_expanded(2) pos_limit_point_on_branch_list
using assms(2) branch_assms_subset branch_is branch_prop(1)
by (smt (verit, ccfv_threshold) basic_trans_rules(31) list.map_comp of_rat_of_int)
then have pos_inf_var: "sgn_pos_inf_rat_list2 ?eval_qs = pos_limit_branch"
unfolding sgn_pos_inf_rat_list2_def
using complex_rat_casting_lemma[of "(sgn_pos_inf_rat_list (map (eval_mpoly_poly val) qs))" pos_limit_branch]
unfolding sgn_pos_inf_rat_list_def by auto
have neg_inf: "sgn_neg_inf_rat_list ?eval_qs = neg_limit_branch"
using branch_prop_expanded(2) neg_limit_point_on_branch_init
using assms(2) branch_assms_subset branch_is branch_prop(1)
by (smt (verit, ccfv_SIG) basic_trans_rules(31) list.map_comp neg_limit_point_on_branch_list of_rat_of_int)
then have neg_inf_var: "sgn_neg_inf_rat_list2 ?eval_qs = neg_limit_branch"
unfolding sgn_neg_inf_rat_list2_def
using complex_rat_casting_lemma[of "(sgn_neg_inf_rat_list (map (eval_mpoly_poly val) qs))" neg_limit_branch]
unfolding sgn_neg_inf_rat_list_def
by auto
have "set signs = set (characterize_consistent_signs_at_roots (poly_f ?eval_qs) ?eval_qs)"
using calc_signs_relation_var pos_inf_var neg_inf_var calc_prop(2)
unfolding sgn_neg_inf_rat_list2_def sgn_pos_inf_rat_list2_def
by auto
then show "set signs = (consistent_sign_vectors_R (map (eval_mpoly_poly val) qs) UNIV)"
using find_consistent_signs_at_roots_R poly_f_ncrb_connection calc_signs_is
main_step_R
by (metis find_consistent_signs_R_def poly_f_nonzero)
qed

subsection "Completeness"

(* This is the branch where all of the leading coefficients satisfy
the given sign conditions.  *)
lemma lc_assump_generation_valuation:
assumes "⋀p n. (p,n) ∈ set init_assumps ⟹ satisfies_evaluation val p n"
shows "∃branch ∈ set (lc_assump_generation q init_assumps).
set (fst branch) ⊆ set (init_assumps) ∪ set
(map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using assms
proof (induct q init_assumps rule: lc_assump_generation_induct )
case (Base q assumps)
then show ?case
using lc_assump_generation.simps by auto
next
case (Rec q assumps)
let ?zero = "lc_assump_generation (one_less_degree q) ((Polynomial.lead_coeff q, (0::rat)) # assumps)"
let ?one  = "((Polynomial.lead_coeff q, (1::rat)) # assumps, q)"
let ?minus_one  = "((Polynomial.lead_coeff q, (-1::rat)) # assumps, q)"
have set_is: "set (lc_assump_generation q assumps) = set (?one#?minus_one#?zero)"
using Rec.hyps Rec(4) lc_assump_generation.simps by auto
have eo: "satisfies_evaluation val ?lc (0::rat) ∨ satisfies_evaluation val ?lc (1::rat) ∨ satisfies_evaluation val ?lc (-1::rat)"
unfolding satisfies_evaluation_def eval_mpoly_def Sturm_Tarski.sign_def by auto
{assume *: "satisfies_evaluation val ?lc (1::rat) "
then have "1 = mpoly_sign val (Polynomial.lead_coeff q)"
unfolding satisfies_evaluation_def eval_mpoly_def mpoly_sign_def Sturm_Tarski.sign_def
by simp
then have "(Polynomial.lead_coeff q, 1)  ∈ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
then have "set (fst ?one) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
by auto
then have " ∃branch∈set (lc_assump_generation q assumps).
set (fst branch) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using set_is by auto
} moreover
{assume *: "satisfies_evaluation val ?lc (-1::rat) "
then have "-1 = mpoly_sign val (Polynomial.lead_coeff q)"
unfolding satisfies_evaluation_def eval_mpoly_def mpoly_sign_def Sturm_Tarski.sign_def
by (smt (z3) of_int_1 of_int_minus rel_simps(66) zero_neq_neg_one)
then have "(Polynomial.lead_coeff q, -1)  ∈ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
then have "set (fst ?minus_one) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
by auto
then have " ∃branch∈set (lc_assump_generation q assumps).
set (fst branch) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using set_is by auto
} moreover {assume *: "satisfies_evaluation val ?lc (0::rat) "
then have "∃branch∈set (lc_assump_generation (Multiv_Poly_Props.one_less_degree q) ((Polynomial.lead_coeff q, 0) # assumps)).
set (fst branch)
⊆ set ((Polynomial.lead_coeff q, 0) # assumps) ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)))"
using lc_assump_generation.simps
using Rec(3) Rec(4) by fastforce
then obtain branch where branch_prop: "branch∈set (lc_assump_generation (Multiv_Poly_Props.one_less_degree q) ((Polynomial.lead_coeff q, 0) # assumps))"
"set (fst branch)
⊆ set ((Polynomial.lead_coeff q, 0) # assumps) ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)))"
by auto
then have branch_prop_2: "branch∈set ?zero"
by auto
have "0 = mpoly_sign val (Polynomial.lead_coeff q)" using *
unfolding satisfies_evaluation_def eval_mpoly_def mpoly_sign_def Sturm_Tarski.sign_def
by simp
then have lc_sign: "(Polynomial.lead_coeff q, 0) ∈ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
{assume **: "Multiv_Poly_Props.one_less_degree q ≠ 0"
then have "set (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)) ⊆ set (Polynomial.coeffs q)"
using coeff_one_less_degree_subset unfolding Polynomial.coeffs_def
by blast
then have "set (fst branch) ⊆ set assumps ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using branch_prop
by (smt (verit, del_insts) UnCI UnE lc_sign imageE image_eqI list.set_map set_ConsD subset_code(1))
then have "∃branch∈set (lc_assump_generation q assumps).
set (fst branch)
⊆ set assumps ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using  branch_prop_2
using set_is by force
}
moreover {assume **: "Multiv_Poly_Props.one_less_degree q = 0"
then have "∃branch∈set (lc_assump_generation q assumps).
set (fst branch) ⊆ set assumps ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
by (metis (no_types, lifting))
}
ultimately have " ∃branch∈set (lc_assump_generation q assumps).
set (fst branch) ⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
by auto
}
ultimately show ?case using eo by auto
next
case (Lookup0 q assumps)
then obtain branch where branch_prop:"branch∈set (lc_assump_generation (Multiv_Poly_Props.one_less_degree q) assumps)"
"set (fst branch)
⊆ set assumps ∪ set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)))"
by auto
have same_gen: "lc_assump_generation (one_less_degree q) assumps = lc_assump_generation q assumps"
using Lookup0.hyps lc_assump_generation.simps by auto
then have branch_prop_2 :"branch∈set (lc_assump_generation q assumps)"
using branch_prop(1) by auto
{assume *: "Multiv_Poly_Props.one_less_degree q ≠ 0"
then have "set (Polynomial.coeffs (Multiv_Poly_Props.one_less_degree q)) ⊆ set (Polynomial.coeffs q)"
using coeff_one_less_degree_subset unfolding Polynomial.coeffs_def
by blast
then have "set (fst branch)
⊆ set assumps ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using branch_prop_2 branch_prop(2) by auto
then have "∃branch∈set (lc_assump_generation q assumps).
set (fst branch)
⊆ set assumps ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
using branch_prop_2
by auto
}
moreover {assume *: "Multiv_Poly_Props.one_less_degree q = 0"
then have "∃branch∈set (lc_assump_generation q assumps).
set (fst branch)
⊆ set assumps ∪
set (map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs q))"
}
ultimately show ?case
by force
next
case (LookupN0 q assumps r)
then show ?case using lc_assump_generation.simps
by simp
qed

lemma lc_assump_generation_valuation_satisfies_eval:
fixes q:: "rmpoly"
assumes "(p,n) ∈ set (map (λx. (x, mpoly_sign val x)) ell)"
shows "satisfies_evaluation val p n"
proof -
obtain c where c_prop: "c ∈ set ell"
"(p, n) = (c, mpoly_sign val c)"
using assms by auto
have "satisfies_evaluation val c (mpoly_sign val c)"
unfolding satisfies_evaluation_def mpoly_sign_def eval_mpoly_def
Sturm_Tarski.sign_def by auto
then show ?thesis
using c_prop by auto
qed

(* relate lc_assump_generation_list to lc_assump_generation *)
lemma lc_assump_generation_list_valuation:
assumes "⋀p n. (p,n) ∈ set init_assumps ⟹ satisfies_evaluation val p n"
shows "∃branch ∈ set (lc_assump_generation_list qs init_assumps).
set (fst branch) ⊆ set (init_assumps) ∪ set
(map (λx. (x, mpoly_sign val x)) (coeffs_list qs))"
using assms
proof (induct qs arbitrary: init_assumps)
case Nil
then show ?case
using lc_assump_generation_list.simps
by simp
next
case (Cons a qs)
then obtain branch_a where branch_a_prop: "branch_a ∈ set (lc_assump_generation a init_assumps)"
"set (fst branch_a) ⊆ set (init_assumps) ∪ set
(map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))"
using lc_assump_generation_valuation
by blast
then obtain branch_a_assms branch_a_poly where branch_a_is: "branch_a = (branch_a_assms, branch_a_poly)"
"set (branch_a_assms) ⊆ set (init_assumps) ∪ set
(map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))"
by (meson prod.exhaust_sel)
have inset: "set (map (λelem. (fst elem, branch_a_poly#(snd elem))) (lc_assump_generation_list qs branch_a_assms))
⊆ set (lc_assump_generation_list (a#qs) init_assumps)"
using lc_assump_generation_list.simps branch_a_is(1) branch_a_prop(1)
by auto
have "⋀p n. (p,n) ∈ set branch_a_assms ⟹ satisfies_evaluation val p n"
using lc_assump_generation_valuation_satisfies_eval branch_a_is(1) fst_conv local.Cons(2) Set.basic_monos(7) UnE
proof -
fix p :: "real mpoly" and n :: rat
assume "(p, n) ∈ set branch_a_assms"
then show "satisfies_evaluation val p n"
by (meson UnE lc_assump_generation_valuation_satisfies_eval Set.basic_monos(7) branch_a_is(2) local.Cons(2))
qed
then obtain branch where branch_props:
"branch∈set (lc_assump_generation_list qs branch_a_assms)"
"set (fst branch)
⊆ set branch_a_assms ∪
set (map (λx. (x, mpoly_sign val x)) (coeffs_list qs))"
using Cons.hyps[of branch_a_assms] by auto
then have branch_inset:
"(fst branch, branch_a_poly#(snd branch))
∈ set (lc_assump_generation_list (a#qs) init_assumps)"
using inset
by auto
then have subset_h: "set (fst branch) ⊆ set (init_assumps) ∪ (set
(map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))
∪ set (map (λx. (x, mpoly_sign val x)) (coeffs_list qs)))"
using branch_props(2) branch_a_is(2) by auto
have "coeffs_list (a # qs) = (Polynomial.coeffs a) @ (coeffs_list qs)"
unfolding coeffs_list_def by auto
then have same_set:
"set (map (λx. (x, mpoly_sign val x)) (coeffs_list (a#qs))) = (set
(map (λx. (x, mpoly_sign val x)) (Polynomial.coeffs a))
∪ set (map (λx. (x, mpoly_sign val x)) (coeffs_list qs)))"
by auto
then have "set (fst branch) ⊆ set (init_assumps) ∪ set
(map (λx. (x, mpoly_sign val x)) (coeffs_list (a#qs)))"
using subset_h by auto
then show ?case
using branch_inset
by (metis (no_types, lifting) prod.sel(1))
qed

lemma base_case_info_M_assumps_complete:
assumes "⋀p n. (p,n) ∈ set init_assumps ⟹ satisfies_evaluation val p n"
shows  "∃ (assumps, mat_eq) ∈ set (base_case_info_M_assumps init_assumps).
(∀ (p,n) ∈ set assumps. satisfies_evaluation val p n)"
using assms unfolding base_case_info_M_assumps_def by auto

lemma matches_len_complete_spmods_ex:
assumes "⋀p' n'. (p',n') ∈ set acc ⟹ satisfies_evaluation val p' n'"
shows  "∃(assumps, sturm_seq) ∈ set (spmods_multiv p q acc).
(∀ (p,n) ∈ set assumps. satisfies_evaluation val p n)"
using assms
proof (induct p q acc rule: spmods_multiv_induct)
case (Base p q acc)
then show ?case
next
case (Rec p q acc)
let ?left = "spmods_multiv (one_less_degree p) q ((Polynomial.lead_coeff p, (0::rat)) # acc)"
let ?res_one = "spmods_multiv_aux p q ((Polynomial.lead_coeff p, (1::rat)) # acc)"
let ?res_minus_one = "spmods_multiv_aux p q ((Polynomial.lead_coeff p, (-1::rat)) # acc)"
have spmods_is: "spmods_multiv p q acc = ?left @ (?res_one @ ?res_minus_one)"
using spmods_multiv.simps Rec(1-2) by auto
have "satisfies_evaluation val (Polynomial.lead_coeff p) 0 ∨
satisfies_evaluation val (Polynomial.lead_coeff p) 1 ∨
unfolding satisfies_evaluation_def
apply auto
using Sturm_Tarski.sign_cases
by (metis of_int_1 of_int_minus)
then have q:"
(∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, 0) # acc) ⟶ satisfies_evaluation val p' n') ∨
(∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, 1) # acc) ⟶ satisfies_evaluation val p' n') ∨
(∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, -1) # acc) ⟶ satisfies_evaluation val p' n')"
using Rec
by simp
moreover {
assume *:"(∀p' n'. (p',n') ∈ set ((Polynomial.lead_coeff p, 0) # acc) ⟶ satisfies_evaluation val p' n')"
then have "∃a∈set (spmods_multiv (Multiv_Poly_Props.one_less_degree p) q