Theory Matrix_Equation_Construction

```theory Matrix_Equation_Construction

imports BKR_Algorithm
begin

section "Results with Sturm's Theorem"

lemma relprime:
fixes q::"real poly"
assumes "coprime p q"
assumes "p ≠ 0"
assumes "q ≠ 0"
shows "changes_R_smods p (pderiv p) = card {x. poly p x = 0 ∧ poly q x > 0} + card {x. poly p x = 0 ∧ poly q x < 0}"
proof -
have 1: "{x. poly p x = 0 ∧ poly q x = 0} = {}"
using assms(1) coprime_poly_0 by auto
have 2: "changes_R_smods p (pderiv p) = int (card {x . poly p x = 0})" using sturm_R by auto
have 3: "{x. poly p x = 0 ∧ poly q x > 0} ∩ {x. poly p x = 0 ∧ poly q x < 0} = {}" by auto
have "{x . poly p x = 0} =  {x. poly p x = 0 ∧ poly q x > 0} ∪{x. poly p x = 0 ∧ poly q x < 0} ∪ {x. poly p x = 0 ∧ poly q x = 0}" by force
then have "{x . poly p x = 0} = {x. poly p x = 0 ∧ poly q x > 0} ∪{x. poly p x = 0 ∧ poly q x < 0}" using 1 by auto
then have "(card {x . poly p x = 0}) = (card ({x. poly p x = 0 ∧ poly q x > 0} ∪{x. poly p x = 0 ∧ poly q x < 0}))" by presburger
then have 4: "(card {x . poly p x = 0}) =  card {x. poly p x = 0 ∧ poly q x > 0} + card {x. poly p x = 0 ∧ poly q x < 0}" using 3 by (simp add: card_Un_disjoint assms(2) poly_roots_finite)
show ?thesis  by (simp add: "2" "4")
qed

(* This is the same proof as card_eq_sum *)
lemma card_eq_const_sum:
fixes k:: real
assumes "finite A"
shows "k*card A = sum (λx. k) A"
proof -
have "plus ∘ (λ_. Suc 0) = (λ_. Suc)"
by (simp add: fun_eq_iff)
then have "Finite_Set.fold (plus ∘ (λ_. Suc 0)) = Finite_Set.fold (λ_. Suc)"
by (rule arg_cong)
then have "Finite_Set.fold (plus ∘ (λ_. Suc 0)) 0 A = Finite_Set.fold (λ_. Suc) 0 A"
by (blast intro: fun_cong)
then show ?thesis
by (simp add: card.eq_fold sum.eq_fold)
qed

lemma restate_tarski:
fixes q::"real poly"
assumes "coprime p q"
assumes "p ≠ 0"
assumes "q ≠ 0"
shows "changes_R_smods p ((pderiv p) * q) = card {x. poly p x = 0 ∧ poly q x > 0} -  int(card {x. poly p x = 0 ∧ poly q x < 0})"
proof -
have 3: "taq {x. poly p x=0} q ≡ ∑y∈{x. poly p x=0}. Sturm_Tarski.sign (poly q y)" by (simp add: taq_def)
have 4: "{x. poly p x=0} =  {x. poly p x = 0 ∧ poly q x > 0} ∪ {x. poly p x = 0 ∧ poly q x < 0} ∪ {x. poly p x = 0 ∧ poly q x = 0}" by force
then have 5: "{x. poly p x=0} =  {x. poly p x = 0 ∧ poly q x > 0} ∪ {x. poly p x = 0 ∧ poly q x < 0}" using assms(1) coprime_poly_0 by auto
then have 6: "∑y∈{x. poly p x=0}. Sturm_Tarski.sign (poly q y) ≡ ∑y∈{x. poly p x = 0 ∧ poly q x > 0} ∪ {x. poly p x = 0 ∧ poly q x < 0}. Sturm_Tarski.sign (poly q y)" by presburger
then have 12: "taq {x. poly p x=0} q ≡ ∑y∈{x. poly p x = 0 ∧ poly q x > 0} ∪ {x. poly p x = 0 ∧ poly q x < 0}. Sturm_Tarski.sign (poly q y)"
by (simp add: "3")
have 7: "{x. poly p x = 0 ∧ poly q x > 0} ∩ {x. poly p x = 0 ∧ poly q x < 0} = {}" by auto
then have 8: "∑y∈{x. poly p x = 0 ∧ poly q x > 0} ∪ {x. poly p x = 0 ∧ poly q x < 0}. Sturm_Tarski.sign (poly q y) ≡ (∑y∈{x. poly p x = 0 ∧ poly q x > 0}.Sturm_Tarski.sign (poly q y)) + (∑y∈{x. poly p x = 0 ∧ poly q x < 0}.Sturm_Tarski.sign(poly q y))" by (simp add: assms(2) poly_roots_finite sum.union_disjoint)
then have 13: "taq {x. poly p x=0} q ≡ (∑y∈{x. poly p x = 0 ∧ poly q x > 0}.Sturm_Tarski.sign (poly q y)) + (∑y∈{x. poly p x = 0 ∧ poly q x < 0}.Sturm_Tarski.sign(poly q y))"
by (simp add: "12")
then have 9: "taq {x. poly p x = 0} q ≡ (∑y∈{x. poly p x = 0 ∧ poly q x > 0}.1) + (∑y∈{x. poly p x = 0 ∧ poly q x < 0}.(-1))" by simp
have 10: "(∑y∈{x. poly p x = 0 ∧ poly q x > 0}.1) =  card {x. poly p x = 0 ∧ poly q x > 0}" using card_eq_sum by auto
have 11: " (∑y∈{x. poly p x = 0 ∧ poly q x < 0}.(-1)) = -1*card {x. poly p x = 0 ∧ poly q x < 0}" using card_eq_const_sum by simp
have 14: "taq {x. poly p x = 0} q ≡ card {x. poly p x = 0 ∧ poly q x > 0} + -1*card {x. poly p x = 0 ∧ poly q x < 0}" using 9 10 11 by simp
have 1: "changes_R_smods p (pderiv p * q) = taq {x. poly p x=0} q" using sturm_tarski_R by simp
then have 15: "changes_R_smods p (pderiv p * q) = card {x. poly p x = 0 ∧ poly q x > 0} + (-1*card {x. poly p x = 0 ∧ poly q x < 0})" using 14 by linarith
have 16: "(-1*card {x. poly p x = 0 ∧ poly q x < 0}) = - card {x. poly p x = 0 ∧ poly q x < 0}" by auto
then show ?thesis using 15 by linarith
qed

lemma restate_tarski2:
fixes q::"real poly"
assumes "p ≠ 0"
shows "changes_R_smods p ((pderiv p) * q) =
int(card {x. poly p x = 0 ∧ poly q x > 0}) -
int(card {x. poly p x = 0 ∧ poly q x < 0})"
unfolding sturm_tarski_R[symmetric] taq_def
proof -
let ?all = "{x. poly p x=0}"
let ?lt = "{x. poly p x=0 ∧ poly q x < 0}"
let ?gt = "{x. poly p x=0 ∧ poly q x > 0}"
let ?eq = "{x. poly p x=0 ∧ poly q x = 0}"
have eq: "?all = ?lt ∪ ?gt ∪ ?eq" by force
from poly_roots_finite[OF assms] have fin: "finite ?all" .
show  "(∑x | poly p x = 0. Sturm_Tarski.sign (poly q x)) = int (card ?gt) - int (card ?lt)"
unfolding eq
apply (subst sum_Un)
apply (auto simp add:fin)
apply (subst sum_Un)
by (auto simp add:fin)
qed

lemma coprime_set_prod:
fixes I:: "real poly set"
shows "finite I ⟹ ((∀ q ∈ I. (coprime p q)) ⟶ (coprime p (∏ I)))"
proof (induct rule: finite_induct)
case empty
then show ?case
by simp
next
case (insert x F)
then show ?case using coprime_mult_right_iff
by simp
qed

lemma finite_nonzero_set_prod:
fixes I:: "real poly set"
shows  nonzero_hyp: "finite I ⟹ ((∀ q ∈ I. q ≠ 0) ⟶ ∏ I ≠ 0)"
proof (induct rule: finite_induct)
case empty
then show ?case
by simp
next
case (insert x F)
have h: "∏ (insert x F) = x * (∏ F)"
by (simp add: insert.hyps(1) insert.hyps(2))
have h_xin: "x ∈ insert x F"
by simp
have hq: "(∀ q ∈ (insert x F). q ≠ 0) ⟶ x ≠ 0" using h_xin
by blast
show ?case using h hq
using insert.hyps(3) by auto
qed

section "Setting up the construction: Definitions"

definition characterize_root_list_p:: "real poly ⇒ real list"
where "characterize_root_list_p p ≡ sorted_list_of_set({x. poly p x = 0}::real set)"

(************** Renegar's N(I); towards defining the RHS of the matrix equation **************)

lemma construct_NofI_prop:
fixes p:: "real poly"
fixes I:: "real poly list"
assumes nonzero: "p≠0"
shows "construct_NofI p I =
rat_of_int (int (card {x. poly p x = 0 ∧ poly (prod_list I) x > 0}) -
int (card {x. poly p x = 0 ∧ poly (prod_list I) x < 0}))"
unfolding construct_NofI_def
using assms restate_tarski2 nonzero rsquarefree_def
by (simp add: rsquarefree_def)

definition construct_s_vector:: "real poly ⇒ real poly list list ⇒ rat vec"
where "construct_s_vector p Is = vec_of_list (map (λ I.(construct_NofI p I)) Is)"

(* Consistent Sturm_Tarski.sign asSturm_Tarski.signments *)
definition squash::"'a::linordered_field ⇒ rat"
where "squash x = (if x > 0 then 1
else if x < 0 then -1
else 0)"

definition signs_at::"real poly list ⇒ real ⇒ rat list"
where "signs_at qs x ≡
map (squash ∘ (λq. poly q x)) qs"

definition characterize_consistent_signs_at_roots:: "real poly ⇒ real poly list ⇒ rat list list"
where "characterize_consistent_signs_at_roots p qs =
(remdups (map (signs_at qs) (characterize_root_list_p p)))"

(* An alternate version designed to be used when every polynomial in qs is relatively prime to p*)
definition consistent_sign_vec_copr::"real poly list ⇒ real ⇒ rat list"
where "consistent_sign_vec_copr qs x ≡
map (λ q. if (poly q x > 0) then (1::rat) else (-1::rat)) qs"

definition characterize_consistent_signs_at_roots_copr:: "real poly ⇒ real poly list ⇒ rat list list"
where "characterize_consistent_signs_at_roots_copr p qss =
(remdups (map (consistent_sign_vec_copr qss) (characterize_root_list_p p)))"

lemma csa_list_copr_rel:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes nonzero: "p≠0"
assumes pairwise_rel_prime: "∀q. ((List.member qs q) ⟶ (coprime p q))"
shows "characterize_consistent_signs_at_roots p qs = characterize_consistent_signs_at_roots_copr p qs"
proof -
have "∀q ∈ set(qs). ∀ x ∈ set (characterize_root_list_p p).  poly q x ≠ 0"
using pairwise_rel_prime
using coprime_poly_0 in_set_member nonzero poly_roots_finite characterize_root_list_p_def by fastforce
then have h: "∀q ∈ set(qs). ∀ x ∈ set (characterize_root_list_p p). squash (poly q x) = (if (poly q x > 0) then (1::rat) else (-1::rat))"
by (simp add: squash_def)
have "map (λr. map (λp. if 0 < poly p r then 1 else - 1) qs) (characterize_root_list_p p) = map (λr. map (squash ∘ (λp. poly p r)) qs) (characterize_root_list_p p)"
by (simp add: h)
thus ?thesis unfolding characterize_consistent_signs_at_roots_def characterize_consistent_signs_at_roots_copr_def
signs_at_def consistent_sign_vec_copr_def
by presburger
qed

(************** Towards defining Renegar's polynomial function and the LHS of the matrix equation **************)

definition list_constr:: "nat list ⇒ nat ⇒ bool"
where "list_constr L n ≡ list_all (λx. x < n) L"

definition all_list_constr:: "nat list list ⇒ nat ⇒ bool"
where "all_list_constr L n ≡ (∀x. List.member L x ⟶ list_constr x n)"

(* The first input is the subset; the second input is the consistent Sturm_Tarski.sign asSturm_Tarski.signment.
We want to map over the first list and pull out all of the elements in the second list with
corresponding positions, and then multiply those together.
*)
definition z:: "nat list ⇒ rat list ⇒ rat"
where "z index_list sign_asg ≡ (prod_list (map (nth sign_asg) index_list))"

definition mtx_row:: "rat list list ⇒ nat list ⇒ rat list"
where "mtx_row sign_list index_list ≡ (map ( (z index_list)) sign_list)"

definition matrix_A:: "rat list list ⇒ nat list list ⇒ rat mat"
where "matrix_A sign_list subset_list =
(mat_of_rows_list (length sign_list) (map (λi .(mtx_row sign_list i)) subset_list))"

definition alt_matrix_A:: "rat list list ⇒ nat list list ⇒ rat mat"
where "alt_matrix_A signs subsets = (mat (length subsets) (length signs)
(λ(i, j). z (subsets ! i) (signs ! j)))"

lemma alt_matrix_char: "alt_matrix_A signs subsets = matrix_A signs subsets"
proof -
have h0: "(⋀i j. i < length subsets ⟹
j < length signs ⟹
map (λindex_list. map (z index_list) signs) subsets ! i ! j = z (subsets ! i) (signs ! j))"
proof -
fix i
fix j
assume i_lt: "i < length subsets"
assume j_lt: "j < length signs"
show "((map (λindex_list. map (z index_list) signs) subsets) ! i) ! j = z (subsets ! i) (signs ! j)"
proof -
have h0: "(map (λindex_list. map (z index_list) signs) subsets) ! i =  map (z (subsets ! i)) signs"
using nth_map i_lt
by blast
then show ?thesis using nth_map j_lt
by simp
qed
qed
have h: " mat (length subsets) (length signs) (λ(i, j). z (subsets ! i) (signs ! j)) =
mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z index_list) signs) subsets ! i ! y)"
using h0 eq_matI[where A = "mat (length subsets) (length signs) (λ(i, j). z (subsets ! i) (signs ! j))",
where B = "mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z index_list) signs) subsets ! i ! y)"]
by auto
show ?thesis unfolding alt_matrix_A_def matrix_A_def mat_of_rows_list_def apply (auto) unfolding mtx_row_def
using h   by blast
qed

lemma subsets_are_rows: "∀i < (length subsets). row (alt_matrix_A signs subsets) i  = vec (length signs) (λj. z (subsets ! i) (signs ! j))"
unfolding row_def unfolding alt_matrix_A_def by auto

lemma signs_are_cols: "∀i < (length signs). col (alt_matrix_A signs subsets) i  = vec (length subsets) (λj. z (subsets ! j) (signs ! i))"
unfolding col_def unfolding alt_matrix_A_def
by auto

(* ith entry of LHS vector is the number of (distinct) real zeros of p where the Sturm_Tarski.sign vector of the qs  is the ith entry of Sturm_Tarski.signs.*)
definition construct_lhs_vector:: "real poly ⇒ real poly list ⇒ rat list list  ⇒ rat vec"
where "construct_lhs_vector p qs signs ≡
vec_of_list (map (λw.  rat_of_int (int (length (filter (λv. v = w) (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)))))) signs)"

(* Putting all of the pieces of the construction together *)
definition satisfy_equation:: "real poly ⇒ real poly list ⇒ nat list list ⇒ rat list list ⇒ bool"
where "satisfy_equation p qs subset_list sign_list =
(mult_mat_vec (matrix_A sign_list subset_list) (construct_lhs_vector p qs sign_list) = (construct_rhs_vector p qs subset_list))"

section "Setting up the construction: Proofs"

(* Some matrix lemmas  *)
lemma row_mat_of_rows_list:
assumes "list_all (λr. length r = nc) rs"
assumes "i < length rs"
shows "row (mat_of_rows_list nc rs) i = vec_of_list (nth rs i)"
by (smt assms(1) assms(2) dim_col_mat(1) dim_vec_of_list eq_vecI index_row(2) index_vec list_all_length mat_of_rows_list_def row_mat split_conv vec_of_list_index)

lemma mult_mat_vec_of_list:
assumes "length ls = nc"
assumes "list_all (λr. length r = nc) rs"
shows "mat_of_rows_list nc rs *⇩v vec_of_list ls =
vec_of_list (map (λr. vec_of_list r ∙ vec_of_list ls) rs)"
unfolding mult_mat_vec_def
using row_mat_of_rows_list assms
apply auto
by (smt dim_row_mat(1) dim_vec dim_vec_of_list eq_vecI index_map_vec(1) index_map_vec(2) index_vec list_all_length mat_of_rows_list_def row_mat_of_rows_list vec_of_list_index)

lemma mtx_row_length:
"list_all (λr. length r = length signs) (map (mtx_row signs) ls)"
apply (induction ls)
by (auto simp add: mtx_row_def)

thm construct_lhs_vector_def
thm  poly_roots_finite

(* Recharacterize the LHS vector *)
lemma construct_lhs_vector_clean:
assumes "p ≠ 0"
assumes "i < length signs"
shows "(construct_lhs_vector p qs signs) \$ i =
card {x. poly p x = 0 ∧ ((consistent_sign_vec_copr qs x) = (nth signs i))}"
proof -
from poly_roots_finite[OF assms(1)] have "finite {x. poly p x = 0}" .
then have eq: "(Collect
((λv. v = signs ! i) ∘
consistent_sign_vec_copr qs) ∩
set (sorted_list_of_set
{x. poly p x = 0})) =
{x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = signs ! i}"
by auto
show ?thesis
unfolding construct_lhs_vector_def vec_of_list_index characterize_root_list_p_def
apply auto
apply (subst nth_map[OF assms(2)])
apply auto
apply (subst distinct_length_filter)
using eq by auto
qed

lemma construct_lhs_vector_cleaner:
assumes "p ≠ 0"
shows "(construct_lhs_vector p qs signs) =
vec_of_list (map (λs. rat_of_int (card {x. poly p x = 0 ∧ ((consistent_sign_vec_copr qs x) = s)})) signs)"
apply (rule eq_vecI)
apply (auto simp add:  construct_lhs_vector_clean[OF assms] )
apply (simp add: vec_of_list_index)
unfolding construct_lhs_vector_def
using assms construct_lhs_vector_clean construct_lhs_vector_def apply auto[1]
by simp

(* Show that because our consistent Sturm_Tarski.sign vectors consist of 1 and -1's, z returns 1 or -1
when applied to a consistent Sturm_Tarski.sign vector *)
lemma z_signs:
assumes "list_all (λi. i < length signs) I"
assumes "list_all (λs. s = 1 ∨ s = -1) signs"
shows "(z I signs = 1) ∨ (z I signs = -1)" using assms
proof (induction I)
case Nil
then show ?case
by (auto simp add:z_def)
next
case (Cons a I)
moreover have "signs ! a = 1 ∨ signs ! a = -1"
by (metis (mono_tags, lifting) add_Suc_right calculation(2) calculation(3) gr0_conv_Suc list.size(4) list_all_length nth_Cons_0)
ultimately show ?case
by (auto simp add:z_def)
qed

lemma z_lemma:
fixes I:: "nat list"
fixes sign:: "rat list"
assumes consistent: "sign ∈ set (characterize_consistent_signs_at_roots_copr p qs)"
assumes welldefined: "list_constr I (length qs)"
shows "(z I sign = 1) ∨ (z I sign = -1)"
proof (rule z_signs)
have "length sign = length qs" using consistent
by (auto simp add: characterize_consistent_signs_at_roots_copr_def consistent_sign_vec_copr_def)
thus "list_all (λi. i < length sign) I"
using welldefined
by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_copr_def consistent_sign_vec_copr_def)
show "list_all (λs. s = 1 ∨ s = - 1) sign" using consistent
apply (auto simp add: list.pred_map  characterize_consistent_signs_at_roots_copr_def  consistent_sign_vec_copr_def)
using Ball_set
by force
qed

(* Show that all consistent sign vectors on roots of polynomials are in characterize_consistent_signs_at_roots_copr  *)
lemma in_set:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec_copr qs x"
assumes welldefined: "list_constr I (length qs)"
shows "sign ∈ set (characterize_consistent_signs_at_roots_copr p qs)"
proof -
have h1: "consistent_sign_vec_copr qs x ∈
set (remdups (map (consistent_sign_vec_copr qs) (sorted_list_of_set {x. poly p x = 0})))"
using root_p apply auto apply (subst set_sorted_list_of_set)
using nonzero poly_roots_finite rsquarefree_def apply blast by auto
thus ?thesis unfolding characterize_consistent_signs_at_roots_copr_def characterize_root_list_p_def using sign_fix
by blast
qed

(* Since all of the polynomials in qs are relatively prime to p, products of subsets of these
polynomials are also relatively prime to p  *)
lemma nonzero_product:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
assumes pairwise_rel_prime_1: "∀q. ((List.member qs q) ⟶ (coprime p q))"
fixes I:: "nat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes welldefined: "list_constr I (length qs)"
shows "(poly (prod_list (retrieve_polys qs I)) x > 0) ∨ (poly (prod_list (retrieve_polys qs I)) x < 0)"
proof -
have "⋀x. x ∈ set (retrieve_polys qs I) ⟹ coprime p x"
unfolding retrieve_polys_def
by (smt in_set_conv_nth in_set_member length_map list_all_length list_constr_def nth_map pairwise_rel_prime_1 welldefined)
then have coprimeh: "coprime p (prod_list (retrieve_polys qs I))"
using prod_list_coprime_right by auto
thus ?thesis using root_p
using coprime_poly_0 linorder_neqE_linordered_idom by blast
qed

(* The next few lemmas relate z to the signs of the product of subsets of polynomials of qs *)
lemma horiz_vector_helper_pos_ind:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
assumes pairwise_rel_prime_1: "∀q. ((List.member qs q) ⟶ (coprime p q))"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec_copr qs x"
shows "(list_constr I (length qs)) ⟶ (poly (prod_list (retrieve_polys qs I)) x > 0) ⟷ (z I sign = 1)"
proof (induct I)
case Nil
then show ?case
by (simp add: retrieve_polys_def z_def)
next
case (Cons a I)
have welldef: "list_constr (a#I) (length qs) ⟶ (list_constr I (length qs))"
unfolding list_constr_def list_all_def by auto
have set_hyp: "list_constr I (length qs) ⟶ sign ∈ set (characterize_consistent_signs_at_roots_copr p qs)"
using in_set using nonzero root_p sign_fix by blast
have z_hyp: "list_constr I (length qs) ⟶ ((z I sign = 1) ∨ (z I sign = -1))"
using set_hyp z_lemma[where sign="sign", where I = "I", where p="p", where qs="qs"] by blast
have sign_hyp: "sign = map (λ q. if (poly q x > 0) then 1 else -1) qs"
using sign_fix unfolding consistent_sign_vec_copr_def by blast
have ind_hyp_1: "list_constr (a#I) (length qs) ⟶
((0 < poly (prod_list (retrieve_polys qs I)) x) = (z I sign = 1))"
using welldef Cons.hyps by auto
have ind_hyp_2: "list_constr (a#I) (length qs) ⟶
((0 > poly (prod_list (retrieve_polys qs I)) x) = (z I sign = -1))"
using welldef z_hyp Cons.hyps nonzero_product
using pairwise_rel_prime_1 nonzero root_p by auto
have h1: "prod_list (retrieve_polys qs (a # I)) = (nth qs a)*(prod_list (retrieve_polys qs I))"
by (simp add: retrieve_polys_def)
have h2: "(z (a # I) sign) = (nth sign a)*(z I sign)"
by (metis (mono_tags, opaque_lifting) list.simps(9) prod_list.Cons z_def)
have h3help: "list_constr (a#I) (length qs) ⟶ a < length qs" unfolding list_constr_def
by simp
then have h3: "list_constr (a#I) (length qs) ⟶
((nth sign a) = (if (poly (nth qs a) x > 0) then 1 else -1))"
using nth_map sign_hyp by auto
have h2: "(0 < poly ((nth qs a)*(prod_list (retrieve_polys qs I))) x) ⟷
((0 < poly (nth qs a) x ∧ (0 < poly (prod_list (retrieve_polys qs I)) x)) ∨
(0 > poly (nth qs a) x ∧ (0 > poly (prod_list (retrieve_polys qs I)) x)))"
by (simp add: zero_less_mult_iff)
have final_hyp_a: "list_constr (a#I) (length qs) ⟶ (((0 < poly (nth qs a) x ∧ (0 < poly (prod_list (retrieve_polys qs I)) x))
∨ (0 > poly (nth qs a) x ∧ (0 > poly (prod_list (retrieve_polys qs I)) x))) =
((nth sign a)*(z I sign) = 1))"
proof -
have extra_hyp_a: "list_constr (a#I) (length qs) ⟶ (0 < poly (nth qs a) x = ((nth sign a) = 1))" using h3
by simp
have extra_hyp_b: "list_constr (a#I) (length qs) ⟶  (0 > poly (nth qs a) x = ((nth sign a) = -1))"
using h3 apply (auto) using coprime_poly_0 h3help in_set_member nth_mem pairwise_rel_prime_1 root_p by fastforce
have ind_hyp_1: "list_constr (a#I) (length qs) ⟶ (((0 < poly (nth qs a) x ∧ (z I sign = 1)) ∨
(0 > poly (nth qs a) x ∧ (z I sign = -1)))
= ((nth sign a)*(z I sign) = 1))" using extra_hyp_a extra_hyp_b
using zmult_eq_1_iff
by (simp add: h3)
then show ?thesis
using ind_hyp_1 ind_hyp_2 by (simp add: Cons.hyps welldef)
qed
then show ?case
using h1 z_def by (simp add: zero_less_mult_iff)
qed

lemma horiz_vector_helper_pos:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
assumes pairwise_rel_prime_1: "∀q. ((List.member qs q) ⟶ (coprime p q))"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec_copr qs x"
assumes welldefined: "list_constr I (length qs)"
shows "(poly (prod_list (retrieve_polys qs I)) x > 0) ⟷ (z I sign = 1)"
using horiz_vector_helper_pos_ind
using pairwise_rel_prime_1 nonzero  root_p sign_fix welldefined by blast

lemma horiz_vector_helper_neg:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
assumes pairwise_rel_prime_1: "∀q. ((List.member qs q) ⟶ (coprime p q))"
fixes I:: "nat list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec_copr qs x"
assumes welldefined: "list_constr I (length qs)"
shows "(poly (prod_list (retrieve_polys qs I)) x < 0) ⟷ (z I sign = -1)"
proof -
have set_hyp: "list_constr I (length qs) ⟶ sign ∈ set (characterize_consistent_signs_at_roots_copr p qs)"
using in_set using nonzero root_p sign_fix by blast
have z_hyp: "list_constr I (length qs) ⟶ ((z I sign = 1) ∨ (z I sign = -1))"
using set_hyp  z_lemma[where sign="sign", where I = "I", where p="p", where qs="qs"] by blast
have poly_hyp: "(poly (prod_list (retrieve_polys qs I)) x > 0) ∨ (poly (prod_list (retrieve_polys qs I)) x < 0)"
using nonzero_product
using pairwise_rel_prime_1 nonzero root_p
using welldefined by blast
have pos_hyp: "(poly (prod_list (retrieve_polys qs I)) x > 0) ⟷ (z I sign = 1)" using horiz_vector_helper_pos
using pairwise_rel_prime_1 nonzero root_p sign_fix welldefined by blast
show ?thesis using z_hyp poly_hyp pos_hyp apply (auto)
using welldefined by blast
qed

(* Recharacterize the dot product *)
lemma vec_of_list_dot_rewrite:
assumes "length xs = length ys"
shows "vec_of_list xs ∙ vec_of_list ys =
sum_list (map2 (*) xs ys)"
using assms
proof (induction xs arbitrary:ys)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case apply auto
by (smt (verit, best) Suc_length_conv list.simps(9) old.prod.case scalar_prod_vCons sum_list.Cons vec_of_list_Cons zip_Cons_Cons)
qed

lemma lhs_dot_rewrite:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
shows
"(vec_of_list (mtx_row signs I) ∙ (construct_lhs_vector p qs signs)) =
sum_list (map (λs. (z I s)  *  rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) signs)"
proof -
have "p ≠ 0" using nonzero by auto
from construct_lhs_vector_cleaner[OF this]
have rhseq: "construct_lhs_vector p qs signs =
vec_of_list
(map (λs. rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) signs)" by auto
have "(vec_of_list (mtx_row signs I) ∙ (construct_lhs_vector p qs signs)) =
sum_list (map2 (*) (mtx_row signs I) (map (λs. rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) signs))"
unfolding rhseq
apply (intro vec_of_list_dot_rewrite)
by (auto simp add: mtx_row_def)
thus ?thesis unfolding mtx_row_def
using map2_map_map
by (auto simp add: map2_map_map)
qed

lemma sum_list_distinct_filter:
fixes f:: "'a ⇒ int"
assumes "distinct xs" "distinct ys"
assumes "set ys ⊆ set xs"
assumes "⋀x. x ∈ set xs - set ys ⟹ f x = 0"
shows "sum_list (map f xs) = sum_list (map f ys)"
by (metis List.finite_set assms(1) assms(2) assms(3) assms(4) sum.mono_neutral_cong_left sum_list_distinct_conv_sum_set)

(* If we have a superset of the signs, we can drop to just the consistent ones *)
lemma construct_lhs_vector_drop_consistent:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes welldefined: "list_constr I (length qs)"
shows
"(vec_of_list (mtx_row signs I) ∙ (construct_lhs_vector p qs signs)) =
(vec_of_list (mtx_row (characterize_consistent_signs_at_roots_copr p qs) I) ∙
(construct_lhs_vector p qs (characterize_consistent_signs_at_roots_copr p qs)))"
proof -
have h0: "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_nat (card
{xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = sgn}) ⟶ z I sgn = 0"
proof -
have "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_int (card
{xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = sgn}) ⟶ {xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = sgn} ≠ {}"
by fastforce
then show ?thesis
proof -
{ fix iis :: "rat list"
have ff1: "0 ≠ p"
using nonzero rsquarefree_def by blast
obtain rr :: "(real ⇒ bool) ⇒ real" where
ff2: "⋀p. p (rr p) ∨ Collect p = {}"
by moura
{ assume "∃is. is = iis ∧ {r. poly p r = 0 ∧ consistent_sign_vec_copr qs r = is} ≠ {}"
then have "∃is. consistent_sign_vec_copr qs (rr (λr. poly p r = 0 ∧ consistent_sign_vec_copr qs r = is)) = iis ∧ {r. poly p r = 0 ∧ consistent_sign_vec_copr qs r = is} ≠ {}"
using ff2
by (metis (mono_tags, lifting))
then have "∃r. poly p r = 0 ∧ consistent_sign_vec_copr qs r = iis"
using ff2 by smt
then have "iis ∈ consistent_sign_vec_copr qs ` set (sorted_list_of_set {r. poly p r = 0})"
using ff1 poly_roots_finite by fastforce }
then have "iis ∉ set signs ∨ iis ∈ consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ∨ ¬ 0 < rat_of_int (int (card {r. poly p r = 0 ∧ consistent_sign_vec_copr qs r = iis}))"
by (metis (no_types) ‹∀sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_int (int (card {xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = sgn})) ⟶ {xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = sgn} ≠ {}› characterize_root_list_p_def) }
then show ?thesis
by fastforce
qed
qed
then have "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ⟶ ((0 = rat_of_nat (card
{xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = sgn}) ∨ z I sgn = 0))"
by auto
then have hyp: "∀ s. s ∈ set signs ∧ s ∉ consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ⟶ (z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}) = 0)"
by auto
then have "(∑s∈ set(signs). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
(∑s∈(set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
proof -
have "set(signs) =(set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec_copr qs ` set (characterize_root_list_p p)))"
by blast
then have sum_rewrite: "(∑s∈ set(signs). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
(∑s∈ (set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
by auto
then have sum_split: "(∑s∈ (set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))
=
(∑s∈ (set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))
+ (∑s∈ (set(signs)-(consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
by (metis (no_types, lifting) List.finite_set sum.Int_Diff)
have sum_zero: "(∑s∈ (set(signs)-(consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) = 0"
using hyp
by (simp add: hyp)
show ?thesis using sum_rewrite sum_split sum_zero by linarith
qed
then have set_eq: "set (remdups
(map (consistent_sign_vec_copr qs)
(characterize_root_list_p p))) = set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))"
using all_info
by (simp add: characterize_consistent_signs_at_roots_copr_def subset_antisym)
have hyp1: "(∑s←signs. z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
(∑s∈set (signs). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
using distinct_signs sum_list_distinct_conv_sum_set by blast
have hyp2: "(∑s←remdups
(map (consistent_sign_vec_copr qs)
(characterize_root_list_p p)). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))
= (∑s∈ set (remdups
(map (consistent_sign_vec_copr qs)
(characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
using sum_list_distinct_conv_sum_set by blast
have set_sum_eq: "(∑s∈(set (signs) ∩ (consistent_sign_vec_copr qs ` set (characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
(∑s∈ set (remdups
(map (consistent_sign_vec_copr qs)
(characterize_root_list_p p))). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
using set_eq by auto
then have "(∑s←signs. z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
(∑s←remdups
(map (consistent_sign_vec_copr qs)
(characterize_root_list_p p)). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
using set_sum_eq hyp1 hyp2
using ‹(∑s∈set signs. z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) = (∑s∈set signs ∩ consistent_sign_vec_copr qs ` set (characterize_root_list_p p). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))› by linarith
then have "consistent_sign_vec_copr qs ` set (characterize_root_list_p p) ⊆ set signs ⟹
(⋀p qss.
characterize_consistent_signs_at_roots_copr p qss =
remdups (map (consistent_sign_vec_copr qss) (characterize_root_list_p p))) ⟹
(∑s←signs. z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
(∑s←remdups
(map (consistent_sign_vec_copr qs)
(characterize_root_list_p p)). z I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
by linarith
then show ?thesis  unfolding lhs_dot_rewrite[OF nonzero]
apply (auto intro!: sum_list_distinct_filter simp add: distinct_signs  characterize_consistent_signs_at_roots_copr_def)
using all_info characterize_consistent_signs_at_roots_copr_def by auto[1]
qed

(* Both matrix_equation_helper_step and matrix_equation_main_step relate the matrix construction
to the Tarski queries, i.e. relate the product of a row of the matrix and the LHS vector to a
Tarski query on the RHS *)
lemma matrix_equation_helper_step:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes welldefined: "list_constr I (length qs)"
assumes pairwise_rel_prime_1: "∀q. ((List.member qs q) ⟶ (coprime p q))"
shows "(vec_of_list (mtx_row signs I) ∙ (construct_lhs_vector p qs signs)) =
rat_of_int (card {x. poly p x = 0 ∧ poly (prod_list (retrieve_polys qs I)) x > 0}) -
rat_of_int (card {x. poly p x = 0 ∧ poly (prod_list (retrieve_polys qs I)) x < 0})"
proof -
have "finite (set (map (consistent_sign_vec_copr qs)  (characterize_root_list_p p)))" by auto
let ?gt = "(set (map (consistent_sign_vec_copr qs)  (characterize_root_list_p p)) ∩ {s. z I s = 1})"
let ?lt = "  (set (map (consistent_sign_vec_copr qs)  (characterize_root_list_p p)) ∩ {s. z I s = -1})"
have eq: "set (map (consistent_sign_vec_copr qs)  (characterize_root_list_p p)) = ?gt ∪ ?lt"
apply auto
by (metis characterize_root_list_p_def horiz_vector_helper_neg horiz_vector_helper_pos_ind nonzero nonzero_product pairwise_rel_prime_1 poly_roots_finite sorted_list_of_set(1) welldefined)
(* First, drop the signs that are irrelevant *)
from construct_lhs_vector_drop_consistent[OF assms(1-4)] have
"vec_of_list (mtx_row signs I) ∙ construct_lhs_vector p qs signs =
vec_of_list (mtx_row (characterize_consistent_signs_at_roots_copr p qs) I) ∙
construct_lhs_vector p qs (characterize_consistent_signs_at_roots_copr p qs)" .
(* Now we split the sum *)
from lhs_dot_rewrite[OF assms(1)]
moreover have "... =
(∑s←characterize_consistent_signs_at_roots_copr p qs.
z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))" .
moreover have "... =
(∑s∈set (map (consistent_sign_vec_copr qs)  (characterize_root_list_p p)).
z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))" unfolding characterize_consistent_signs_at_roots_copr_def sum_code[symmetric]
by (auto)
ultimately have "... =
(∑s∈?gt. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) +
(∑s∈?lt. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))"
apply (subst eq)
apply (rule sum.union_disjoint)
by auto
(* Now recharacterize lt, gt*)
have setroots: "set (characterize_root_list_p p) = {x. poly p x = 0}" unfolding characterize_root_list_p_def
using poly_roots_finite nonzero rsquarefree_def set_sorted_list_of_set by blast
have *: "⋀s. {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s} =
{x ∈{x. poly p x = 0}. consistent_sign_vec_copr qs x = s}"
by auto
have lem_e1: "⋀x. x ∈ {x. poly p x = 0} ⟹
card
{s ∈ consistent_sign_vec_copr  qs ` {x. poly p x = 0} ∩ {s. z I s = 1}.
consistent_sign_vec_copr qs x = s} =
(if 0 < poly (prod_list (retrieve_polys qs I)) x then 1 else 0)"
proof -
fix x
assume rt: "x ∈ {x. poly p x = 0}"
then have 1: "{s ∈ consistent_sign_vec_copr qs ` {x. poly p x = 0} ∩ {s. z I s = 1}. consistent_sign_vec_copr qs x = s} =
{s. z I s = 1 ∧ consistent_sign_vec_copr qs x = s}"
by auto
from horiz_vector_helper_pos[OF assms(1) assms(5) rt]
have 2: "... = {s. (0 < poly (prod_list (retrieve_polys qs I)) x)  ∧ consistent_sign_vec_copr qs x = s}"
using welldefined by blast
have 3: "... = (if (0 < poly (prod_list (retrieve_polys qs I)) x)  then {consistent_sign_vec_copr qs x} else {})"
by auto
thus "card {s ∈ consistent_sign_vec_copr qs ` {x. poly p x = 0} ∩ {s. z I s = 1}. consistent_sign_vec_copr qs x = s} =
(if 0 < poly (prod_list (retrieve_polys qs I)) x then 1 else 0) " using 1 2 3 by auto
qed
have e1: "(∑s∈consistent_sign_vec_copr qs ` {x. poly p x = 0} ∩ {s. z I s = 1}.
card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}) =
(sum (λx. if (poly (prod_list (retrieve_polys qs I)) x) > 0 then 1 else 0) {x. poly p x = 0})"
unfolding * apply (rule sum_multicount_gen)
using ‹finite (set (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)))› setroots apply auto[1]
apply (metis List.finite_set setroots)
using lem_e1 by auto
have gtchr: "(∑s∈?gt. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
rat_of_int (card {x. poly p x = 0 ∧ 0 < poly (prod_list (retrieve_polys qs I)) x})"
apply (auto simp add: setroots)
apply (subst of_nat_sum[symmetric])
apply (subst of_nat_eq_iff)
apply (subst e1)
apply (subst card_eq_sum)
apply (rule sum.mono_neutral_cong_right)
apply (metis List.finite_set setroots)
by auto
have lem_e2: "⋀x. x ∈ {x. poly p x = 0} ⟹
card
{s ∈ consistent_sign_vec_copr  qs ` {x. poly p x = 0} ∩ {s. z I s = -1}.
consistent_sign_vec_copr qs x = s} =
(if poly (prod_list (retrieve_polys qs I)) x < 0 then 1 else 0)"
proof -
fix x
assume rt: "x ∈ {x. poly p x = 0}"
then have 1: "{s ∈ consistent_sign_vec_copr qs ` {x. poly p x = 0} ∩ {s. z I s = -1}. consistent_sign_vec_copr qs x = s} =
{s. z I s = -1 ∧ consistent_sign_vec_copr qs x = s}"
by auto
from horiz_vector_helper_neg[OF assms(1) assms(5) rt]
have 2: "... = {s. (0 > poly (prod_list (retrieve_polys qs I)) x)  ∧ consistent_sign_vec_copr qs x = s}"
using welldefined by blast
have 3: "... = (if (0 > poly (prod_list (retrieve_polys qs I)) x)  then {consistent_sign_vec_copr qs x} else {})"
by auto
thus "card {s ∈ consistent_sign_vec_copr qs ` {x. poly p x = 0} ∩ {s. z I s = -1}. consistent_sign_vec_copr qs x = s} =
(if poly (prod_list (retrieve_polys qs I)) x < 0 then 1 else 0)" using 1 2 3 by auto
qed
have e2: " (∑s∈consistent_sign_vec_copr qs ` {x. poly p x = 0} ∩ {s. z I s = - 1}.
card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}) =
(sum (λx. if (poly (prod_list (retrieve_polys qs I)) x) < 0 then 1 else 0) {x. poly p x = 0})"
unfolding * apply (rule sum_multicount_gen)
using ‹finite (set (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)))› setroots apply auto[1]
apply (metis List.finite_set setroots)
using lem_e2 by auto
have ltchr: "(∑s∈?lt. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) =
- rat_of_int (card {x. poly p x = 0 ∧ 0 > poly (prod_list (retrieve_polys qs I)) x})"
apply (auto simp add: setroots sum_negf)
apply (subst of_nat_sum[symmetric])
apply (subst of_nat_eq_iff)
apply (subst e2)
apply (subst card_eq_sum)
apply (rule sum.mono_neutral_cong_right)
apply (metis List.finite_set setroots)
by auto
show ?thesis using gtchr ltchr
using ‹(∑s∈set (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)). z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) = (∑s∈set (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)) ∩ {s. z I s = 1}. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) + (∑s∈set (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)) ∩ {s. z I s = - 1}. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))› ‹(∑s←characterize_consistent_signs_at_roots_copr p qs. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s})) = (∑s∈set (map (consistent_sign_vec_copr qs) (characterize_root_list_p p)). z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))› ‹vec_of_list (mtx_row (characterize_consistent_signs_at_roots_copr p qs) I) ∙ construct_lhs_vector p qs (characterize_consistent_signs_at_roots_copr p qs) = (∑s←characterize_consistent_signs_at_roots_copr p qs. z I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}))› ‹vec_of_list (mtx_row signs I) ∙ construct_lhs_vector p qs signs = vec_of_list (mtx_row (characterize_consistent_signs_at_roots_copr p qs) I) ∙ construct_lhs_vector p qs (characterize_consistent_signs_at_roots_copr p qs)›
by linarith
qed

(* A clean restatement of the helper lemma *)
lemma matrix_equation_main_step:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes welldefined: "list_constr I (length qs)"
assumes pairwise_rel_prime_1: "∀q. ((List.member qs q) ⟶ (coprime p q))"
shows "(vec_of_list (mtx_row signs I) ∙ (construct_lhs_vector p qs signs)) =
construct_NofI p (retrieve_polys qs I)"
unfolding construct_NofI_prop[OF nonzero]
using matrix_equation_helper_step[OF assms]
by linarith

lemma map_vec_vec_of_list_eq_intro:
assumes "map f xs = map g ys"
shows "map_vec f (vec_of_list xs) = map_vec g (vec_of_list ys)"
by (metis assms vec_of_list_map)

(* Shows that as long as we have a "basis" of sign assignments (see assumptions all_info, welldefined),
and some other mild assumptions on our inputs (given in nonzero, distinct_signs, pairwise_rel_prime),
the construction will be satisfied *)
theorem matrix_equation:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes subsets:: "nat list list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes pairwise_rel_prime: "∀q. ((List.member qs q) ⟶ (coprime p q))"
assumes welldefined: "all_list_constr (subsets) (length qs)"
shows "satisfy_equation p qs subsets signs"
unfolding satisfy_equation_def matrix_A_def
construct_lhs_vector_def construct_rhs_vector_def all_list_constr_def
apply (subst mult_mat_vec_of_list)
apply (auto simp add: mtx_row_length intro!: map_vec_vec_of_list_eq_intro)
using matrix_equation_main_step[OF assms(1-3) _ assms(4), unfolded construct_lhs_vector_def]
using all_list_constr_def in_set_member welldefined by fastforce

(* Prettifying some theorems*)
definition roots:: "real poly ⇒ real set"
where "roots p = {x. poly p x = 0}"

definition sgn::"'a::linordered_field ⇒ rat"
where "sgn x = (if x > 0 then 1
else if x < 0 then -1
else 0)"

definition sgn_vec::"real poly list ⇒ real ⇒ rat list"
where "sgn_vec qs x ≡  map (sgn ∘ (λq. poly q x)) qs"

definition consistent_signs_at_roots:: "real poly ⇒ real poly list ⇒ rat list set"
where "consistent_signs_at_roots p qs =
(sgn_vec qs) ` (roots p)"

lemma consistent_signs_at_roots_eq:
assumes "p ≠ 0"
shows "consistent_signs_at_roots p qs =
set (characterize_consistent_signs_at_roots p qs)"
unfolding consistent_signs_at_roots_def characterize_consistent_signs_at_roots_def
characterize_root_list_p_def
apply auto
apply (subst set_sorted_list_of_set)
using assms poly_roots_finite apply blast
unfolding sgn_vec_def sgn_def signs_at_def squash_def o_def
using roots_def apply auto[1]
by (smt Collect_cong assms image_iff poly_roots_finite roots_def sorted_list_of_set(1))

abbreviation w_vec:: "real poly ⇒ real poly list ⇒ rat list list  ⇒ rat vec"
where "w_vec ≡ construct_lhs_vector"

abbreviation v_vec:: "real poly ⇒ real poly list ⇒ nat list list ⇒ rat vec"
where "v_vec ≡ construct_rhs_vector"

abbreviation M_mat:: "rat list list ⇒ nat list list ⇒ rat mat"
where "M_mat ≡ matrix_A"

theorem matrix_equation_pretty:
assumes "p≠0"
assumes "⋀q. q ∈ set qs ⟹ coprime p q"
assumes "distinct signs"
assumes "consistent_signs_at_roots p qs ⊆ set signs"
assumes "⋀l i. l ∈ set subsets ⟹ i ∈ set l ⟹ i < length qs"
shows "M_mat signs subsets *⇩v w_vec p qs signs = v_vec p qs subsets"
unfolding satisfy_equation_def[symmetric]
apply (rule matrix_equation[OF assms(1) assms(3)])
apply (metis assms(1) assms(2) assms(4) consistent_signs_at_roots_eq csa_list_copr_rel member_def)
apply (simp add: assms(2) in_set_member)
using Ball_set all_list_constr_def assms(5) list_constr_def member_def by fastforce

end```