Theory Renegar_Proofs
theory Renegar_Proofs
imports Renegar_Algorithm
BKR_Proofs
begin
section "Tarski Queries Changed"
lemma construct_NofI_R_relation:
fixes p:: "real poly"
fixes I1:: "real poly list"
fixes I2:: "real poly list"
shows "construct_NofI_R p I1 I2 =
construct_NofI (sum_list (map power2 (p # I1))) I2"
unfolding construct_NofI_R_def construct_NofI_def
by metis
lemma sum_list_map_power2:
shows "sum_list (map power2 ls) ≥ (0::real poly)"
apply (induct ls)
by auto
lemma sum_list_map_power2_poly:
shows "poly (sum_list (map power2 (ls::real poly list))) x ≥ (0::real)"
apply (induct ls)
by auto
lemma construct_NofI_R_prop_helper:
fixes p:: "real poly"
fixes I1:: "real poly list"
fixes I2:: "real poly list"
assumes nonzero: "p≠0"
shows "construct_NofI_R p I1 I2 =
rat_of_int (int (card {x. poly (sum_list (map (λx. x^2) (p # I1))) x = 0 ∧ poly (prod_list I2) x > 0}) -
int (card {x. poly (sum_list (map (λx. x^2) (p # I1))) x = 0 ∧ poly (prod_list I2) x < 0}))"
proof -
show ?thesis unfolding construct_NofI_R_relation[of p I1 I2]
apply (subst construct_NofI_prop[of _ I2])
apply auto
using assms sum_list_map_power2
by (metis le_add_same_cancel1 power2_less_eq_zero_iff)
qed
lemma zer_iff:
fixes p:: "real poly"
fixes ls:: "real poly list"
shows "poly (sum_list (map (λx. x^2) ls)) x = 0 ⟷ (∀i ∈ set ls. poly i x = 0)"
proof (induct ls)
case Nil
then show ?case by auto
next
case (Cons a I1)
then show ?case
apply simp
apply (subst add_nonneg_eq_0_iff)
using zero_le_power2 apply blast
using sum_list_map_power2_poly apply presburger
by simp
qed
lemma construct_NofI_prop_R:
fixes p:: "real poly"
fixes I1:: "real poly list"
fixes I2:: "real poly list"
assumes nonzero: "p≠0"
shows "construct_NofI_R p I1 I2 =
rat_of_int (int (card {x. poly p x = 0 ∧ (∀q ∈ set I1. poly q x = 0) ∧ poly (prod_list I2) x > 0}) -
int (card {x. poly p x = 0 ∧ (∀q ∈ set I1. poly q x = 0) ∧ poly (prod_list I2) x < 0}))"
unfolding construct_NofI_R_prop_helper[OF nonzero]
using zer_iff
apply auto
by (smt (verit, del_insts) Collect_cong sum_list_map_power2_poly zero_le_power2 zero_less_power2)
section "Matrix Equation"
definition map_sgas:: "rat list ⇒ rat list"
where "map_sgas l = map (λr. (1 - r^2)) l"
definition z_R:: "(nat list*nat list) ⇒ rat list ⇒ rat"
where "z_R index_list sign_asg ≡ (prod_list (map (nth (map_sgas sign_asg)) (fst(index_list))))*(prod_list (map (nth sign_asg) (snd(index_list))))"
definition mtx_row_R:: "rat list list ⇒ (nat list * nat list) ⇒ rat list"
where "mtx_row_R sign_list index_list ≡ (map ((z_R index_list)) sign_list)"
definition matrix_A_R:: "rat list list ⇒ (nat list * nat list) list ⇒ rat mat"
where "matrix_A_R sign_list subset_list =
(mat_of_rows_list (length sign_list) (map (λi .(mtx_row_R sign_list i)) subset_list))"
definition all_list_constr_R:: "(nat list*nat list) list ⇒ nat ⇒ bool"
where "all_list_constr_R L n ≡ (∀x. List.member L x ⟶ (list_constr (fst x) n ∧ list_constr (snd x) n))"
definition alt_matrix_A_R:: "rat list list ⇒ (nat list*nat list) list ⇒ rat mat"
where "alt_matrix_A_R signs subsets = (mat (length subsets) (length signs)
(λ(i, j). z_R (subsets ! i) (signs ! j)))"
lemma alt_matrix_char_R: "alt_matrix_A_R signs subsets = matrix_A_R signs subsets"
proof -
have h0: "(⋀i j. i < length subsets ⟹
j < length signs ⟹
map (λindex_list. map (z_R index_list) signs) subsets ! i ! j = z_R (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_R index_list) signs) subsets) ! i) ! j = z_R (subsets ! i) (signs ! j)"
proof -
have h0: "(map (λindex_list. map (z_R index_list) signs) subsets) ! i = map (z_R (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_R (subsets ! i) (signs ! j)) =
mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z_R index_list) signs) subsets ! i ! y)"
using h0 eq_matI[where A = "mat (length subsets) (length signs) (λ(i, j). z_R (subsets ! i) (signs ! j))",
where B = "mat (length subsets) (length signs) (λ(i, y). map (λindex_list. map (z_R index_list) signs) subsets ! i ! y)"]
by auto
show ?thesis unfolding alt_matrix_A_R_def matrix_A_R_def mat_of_rows_list_def apply (auto) unfolding mtx_row_R_def
using h by blast
qed
lemma subsets_are_rows_R: "∀i < (length subsets). row (alt_matrix_A_R signs subsets) i = vec (length signs) (λj. z_R (subsets ! i) (signs ! j))"
unfolding row_def unfolding alt_matrix_A_R_def by auto
lemma signs_are_cols_R: "∀i < (length signs). col (alt_matrix_A_R signs subsets) i = vec (length subsets) (λj. z_R (subsets ! j) (signs ! i))"
unfolding col_def unfolding alt_matrix_A_R_def by auto
definition consistent_sign_vec::"real poly list ⇒ real ⇒ rat list"
where "consistent_sign_vec qs x ≡
map (λ q. if (poly q x > 0) then (1::rat) else (if (poly q x = 0) then (0::rat) else (-1::rat))) qs"
definition construct_lhs_vector_R:: "real poly ⇒ real poly list ⇒ rat list list ⇒ rat vec"
where "construct_lhs_vector_R p qs signs ≡
vec_of_list (map (λw. rat_of_int (int (length (filter (λv. v = w) (map (consistent_sign_vec qs) (characterize_root_list_p p)))))) signs)"
definition satisfy_equation_R:: "real poly ⇒ real poly list ⇒ (nat list*nat list) list ⇒ rat list list ⇒ bool"
where "satisfy_equation_R p qs subset_list sign_list =
(mult_mat_vec (matrix_A_R sign_list subset_list) (construct_lhs_vector_R p qs sign_list) = (construct_rhs_vector_R p qs subset_list))"
lemma construct_lhs_vector_clean_R:
assumes "p ≠ 0"
assumes "i < length signs"
shows "(construct_lhs_vector_R p qs signs) $ i =
card {x. poly p x = 0 ∧ ((consistent_sign_vec 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 qs) ∩
set (sorted_list_of_set
{x. poly p x = 0})) =
{x. poly p x = 0 ∧ consistent_sign_vec qs x = signs ! i}"
by auto
show ?thesis
unfolding construct_lhs_vector_R_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)
apply (auto)
using eq
by auto
qed
lemma construct_lhs_vector_cleaner_R:
assumes "p ≠ 0"
shows "(construct_lhs_vector_R p qs signs) =
vec_of_list (map (λs. rat_of_int (card {x. poly p x = 0 ∧ ((consistent_sign_vec qs x) = s)})) signs)"
apply (rule eq_vecI)
apply (auto simp add: construct_lhs_vector_clean_R[OF assms] )
apply (simp add: vec_of_list_index)
unfolding construct_lhs_vector_R_def
using assms construct_lhs_vector_clean_R construct_lhs_vector_def apply auto[1]
apply (simp add: construct_lhs_vector_R_def)
by auto
lemma z_signs_R2:
fixes I:: "nat list"
fixes signs:: "rat list"
assumes lf: "list_all (λi. i < length signs) I"
assumes la: "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) signs"
shows "(prod_list (map (nth signs) I)) = 1 ∨
(prod_list (map (nth signs) I)) = 0 ∨
(prod_list (map (nth signs) I)) = -1" using assms
proof (induct I)
case Nil
then show ?case by auto
next
case (Cons a I)
moreover have eo: "signs ! a = 1 ∨ signs ! a = 0 ∨ signs ! a = -1"
using assms
by (smt (verit, del_insts) calculation(2) list_all_length list_all_simps(1))
have "prod_list (map ((!) (map_sgas signs)) (a # I)) = (1 - (signs ! a)^2)*prod_list (map ((!) (map_sgas signs)) (I))"
unfolding map_sgas_def apply (auto)
using calculation(2) by auto
then show ?case using eo
using Cons.hyps calculation(2) la by auto
qed
lemma z_signs_R1:
fixes I:: "nat list"
fixes signs:: "rat list"
assumes lf: "list_all (λi. i < length signs) I"
assumes la: "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) signs"
shows "(prod_list (map (nth (map_sgas signs)) I)) = 1 ∨
(prod_list (map (nth (map_sgas signs)) I)) = 0" using assms
proof (induct I)
case Nil
then show ?case by auto
next
case (Cons a I)
moreover have "signs ! a = 1 ∨ signs ! a = 0 ∨ signs ! a = -1"
using assms
by (smt (verit, best) calculation(2) list_all_length list_all_simps(1))
then have eo: "1 - (signs ! a)^2 = 1 ∨ 1 - (signs !a)^2 = 0"
using cancel_comm_monoid_add_class.diff_cancel diff_zero by fastforce
have "prod_list (map ((!) (map_sgas signs)) (a # I)) = (1 - (signs ! a)^2)*prod_list (map ((!) (map_sgas signs)) (I))"
unfolding map_sgas_def apply (auto)
using calculation(2) by auto
then show ?case using eo
using Cons.hyps calculation(2) la by auto
qed
lemma z_signs_R:
fixes I:: "(nat list * nat list)"
fixes signs:: "rat list"
assumes lf: "list_all (λi. i < length signs) (fst(I))"
assumes ls: "list_all (λi. i < length signs) (snd(I))"
assumes la: "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) signs"
shows "(z_R I signs = 1) ∨ (z_R I signs = 0) ∨ (z_R I signs = -1)"
using assms z_signs_R2 z_signs_R1 unfolding z_R_def apply (auto)
by (metis (no_types, lifting) mult_cancel_left1 mult_minus1_right)
lemma z_lemma_R:
fixes I:: "nat list * nat list"
fixes sign:: "rat list"
assumes consistent: "sign ∈ set (characterize_consistent_signs_at_roots p qs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "(z_R I sign = 1) ∨ (z_R I sign = 0) ∨ (z_R I sign = -1)"
proof (rule z_signs_R)
have same: "length sign = length qs" using consistent
using characterize_consistent_signs_at_roots_def signs_at_def by fastforce
thus "(list_all (λi. i < length sign) (fst I))"
using welldefined1
by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_def consistent_sign_vec_copr_def)
thus "(list_all (λi. i < length sign) (snd I))"
using same welldefined2
by (auto simp add: list_constr_def characterize_consistent_signs_at_roots_def consistent_sign_vec_copr_def)
show "list_all (λs. s = 1 ∨ s = 0 ∨ s = - 1) sign" using consistent
apply (auto simp add: list.pred_map characterize_consistent_signs_at_roots_def consistent_sign_vec_def)
using Ball_set
by (simp add: list_all_length signs_at_def squash_def)
qed
lemma in_set_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
shows "sign ∈ set (characterize_consistent_signs_at_roots p qs)"
proof -
have h1: "consistent_sign_vec qs x ∈
set (remdups (map (signs_at qs) (sorted_list_of_set {x. poly p x = 0})))"
unfolding consistent_sign_vec_def signs_at_def squash_def
using root_p nonzero poly_roots_finite set_sorted_list_of_set apply (auto)
by (smt (verit, ccfv_SIG) Collect_cong comp_def image_eqI map_eq_conv mem_Collect_eq poly_roots_finite set_sorted_list_of_set)
thus ?thesis unfolding characterize_consistent_signs_at_roots_def characterize_root_list_p_def using sign_fix
by blast
qed
lemma consistent_signs_prop_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
shows "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) sign"
using assms unfolding consistent_sign_vec_def squash_def apply (auto)
by (smt (z3) length_map list_all_length nth_map)
lemma horiz_vector_helper_pos_ind_R1:
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 qs x"
assumes asm: "list_constr I (length qs)"
shows "(prod_list (map (nth (map_sgas sign)) I)) = 1 ⟷
(∀p ∈ set (retrieve_polys qs I). poly p x = 0)"
using asm
proof (induction "I")
case Nil
then show ?case unfolding map_sgas_def apply (auto)
by (simp add: retrieve_polys_def)
next
case (Cons a xa)
then have same0: "(prod_list (map (nth (map_sgas sign)) xa)) = 1 ⟷
(∀p ∈ set (retrieve_polys qs xa). poly p x = 0)" unfolding list_constr_def by auto
have welldef: "a < length qs" using Cons.prems assms unfolding list_constr_def by auto
then have h: "prod_list (map ((!) (map_sgas sign)) (a#xa)) = (1 - (sign ! a)^2)*(prod_list (map ((!) (map_sgas sign)) (xa)))"
unfolding map_sgas_def using assms apply (auto)
by (metis (no_types, lifting) consistent_sign_vec_def length_map nth_map)
have "list_all (λs. s = 1 ∨ s = 0 ∨ s = -1) sign" using sign_fix unfolding consistent_sign_vec_def squash_def
apply (auto)
by (smt (z3) length_map list_all_length nth_map)
then have eo: "(prod_list (map ((!) (map_sgas sign)) (xa))) = 0 ∨ (prod_list (map ((!) (map_sgas sign)) (xa))) = 1"
using z_signs_R1 assms Cons.prems consistent_sign_vec_def length_map list_all_simps(1) length_map list_all_length list_constr_def
by (smt (verit, best))
have "(sign ! a)^2 = 1 ∨ (sign ! a)^2 = 0" using sign_fix welldef unfolding consistent_sign_vec_def
by auto
then have s1: "(prod_list (map (nth (map_sgas sign)) (a#xa))) = 1 ⟷
((sign ! a)^2 = 0 ∧ (prod_list (map ((!) (map_sgas sign)) (xa))) = 1)"
using eo h
by (metis (mono_tags, opaque_lifting) cancel_comm_monoid_add_class.diff_cancel diff_zero mult.left_neutral mult_zero_left)
have "(sign ! a)^2 = 0 ⟷ (poly (qs ! a) x = 0)"
using sign_fix unfolding consistent_sign_vec_def welldef apply (auto)
apply (smt (z3) class_field.neg_1_not_0 class_field.zero_not_one nth_map welldef)
by (smt (z3) nth_map welldef)
then have same1:"(prod_list (map (nth (map_sgas sign)) (a#xa))) = 1 ⟷
((poly (qs ! a) x = 0) ∧ (prod_list (map ((!) (map_sgas sign)) (xa))) = 1)" using s1 by auto
have "set (retrieve_polys qs (a#xa)) = {(qs ! a)} ∪ set (retrieve_polys qs xa)"
by (metis (no_types, lifting) insert_is_Un list.simps(15) list.simps(9) retrieve_polys_def)
then have same2:"(∀p ∈ set (retrieve_polys qs (a#xa)). poly p x = 0) = ((poly (qs ! a) x = 0)
∧ (∀p ∈ set (retrieve_polys qs (xa)). poly p x = 0))"
by auto
then show ?case using same0 same1 same2
assms by auto
qed
lemma csv_length_same_as_qlist:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes sign:: "rat list"
fixes x:: "real"
assumes root_p: "x ∈ {x. poly p x = 0}"
assumes sign_fix: "sign = consistent_sign_vec qs x"
shows "length sign = length qs"
using assms unfolding consistent_sign_vec_def by auto
lemma horiz_vector_helper_zer_ind_R2:
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 qs x"
assumes asm: "list_constr I (length qs)"
shows "(prod_list (map (nth sign) I)) = 0 ⟷
(poly (prod_list (retrieve_polys qs I)) x = 0)"
using asm
proof (induction "I")
case Nil
then show ?case unfolding map_sgas_def apply (auto) unfolding retrieve_polys_def
by auto next
case (Cons a xa)
have "poly (prod_list (retrieve_polys qs (a # xa))) x = (poly (qs ! a) x)*poly (prod_list (retrieve_polys qs (xa))) x"
by (simp add: retrieve_polys_def)
then show ?case using Cons.prems
by (smt (z3) Cons.IH class_field.neg_1_not_0 class_field.zero_not_one consistent_sign_vec_def list.simps(9) list_all_simps(1) list_constr_def mult_eq_0_iff nth_map prod_list.Cons sign_fix)
qed
lemma horiz_vector_helper_pos_ind_R2:
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 qs x"
assumes asm: "list_constr I (length qs)"
shows "(prod_list (map (nth sign) I)) = 1 ⟷
(poly (prod_list (retrieve_polys qs I)) x > 0)"
using asm
proof (induction "I")
case Nil
then show ?case unfolding map_sgas_def apply (auto) unfolding retrieve_polys_def
by auto next
case (Cons a xa)
then have ih: "(prod_list (map ((!) sign) xa) = 1) = (0 < poly (prod_list (retrieve_polys qs xa)) x)"
unfolding list_constr_def by auto
have lensame: "length sign = length qs" using sign_fix csv_length_same_as_qlist[of p x sign qs]
nonzero root_p by auto
have "poly (prod_list (retrieve_polys qs (a # xa))) x = (poly (qs ! a) x)*poly (prod_list (retrieve_polys qs (xa))) x"
by (simp add: retrieve_polys_def)
then have iff1: "(poly (prod_list (retrieve_polys qs (a#xa))) x > 0) ⟷
(((poly (qs ! a) x) > 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x > 0) ∨
((poly (qs ! a) x) < 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x < 0))"
by (metis zero_less_mult_iff)
have prodsame: "(prod_list (map (nth sign) (a#xa))) = (sign ! a)* (prod_list (map (nth sign) (xa)))"
using lensame Cons.prems unfolding list_constr_def by auto
have sagt: "sign ! a = 1 ⟷ (poly (qs ! a) x) > 0" using assms unfolding consistent_sign_vec_def
apply (auto)
apply (smt (verit, best) Cons.prems list_all_simps(1) list_constr_def neg_equal_zero nth_map zero_neq_one)
by (smt (verit, ccfv_threshold) Cons.prems list_all_simps(1) list_constr_def nth_map)
have salt: "sign ! a = -1 ⟷ (poly (qs ! a) x) < 0" using assms unfolding consistent_sign_vec_def
apply (auto)
apply (smt (verit, ccfv_SIG) Cons.prems less_minus_one_simps(1) less_minus_one_simps(3) list_all_simps(1) list_constr_def neg_0_less_iff_less nth_map)
by (smt (verit, best) Cons.prems list_all_simps(1) list_constr_def nth_map)
have h1: "((poly (qs ! a) x) > 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x > 0) ⟶
(prod_list (map (nth sign) (a#xa))) = 1"
using prodsame sagt ih by auto
have eo: "(prod_list (map ((!) sign) xa) = 1) ∨ (prod_list (map ((!) sign) xa) = 0) ∨
(prod_list (map ((!) sign) xa) = -1)"
using Cons.prems consistent_signs_prop_R lensame list_constr_def nonzero root_p sign_fix z_signs_R2 by auto
have d1:"(prod_list (map ((!) sign) xa) = -1) ⟹ (0 > poly (prod_list (retrieve_polys qs xa)) x)"
proof -
assume "(prod_list (map ((!) sign) xa) = -1) "
then show "(0 > poly (prod_list (retrieve_polys qs xa)) x)"
using prodsame salt ih assms Cons.prems class_field.neg_1_not_0 equal_neg_zero horiz_vector_helper_zer_ind_R2 linorder_neqE_linordered_idom list_all_simps(1) list_constr_def
apply (auto)
apply (smt (verit, ccfv_threshold) class_field.neg_1_not_0 list.set_map list_all_length semidom_class.prod_list_zero_iff)
by (smt (verit, ccfv_threshold) class_field.neg_1_not_0 list.set_map list_all_length semidom_class.prod_list_zero_iff)
qed
have d2: "(0 > poly (prod_list (retrieve_polys qs xa)) x) ⟶ (prod_list (map ((!) sign) xa) = -1)"
using eo assms horiz_vector_helper_zer_ind_R2[where p = "p", where x = "x", where sign = "sign", where I ="I"]
apply (auto)
using ih apply force
by (metis (full_types, lifting) Cons.prems class_field.neg_1_not_0 horiz_vector_helper_zer_ind_R2 ih imageI list.set_map list_all_simps(1) list_constr_def mem_Collect_eq neg_equal_0_iff_equal semidom_class.prod_list_zero_iff)
have "(prod_list (map ((!) sign) xa) = -1) = (0 > poly (prod_list (retrieve_polys qs xa)) x)"
using d1 d2
by blast
then have h2: "((poly (qs ! a) x) < 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x < 0) ⟶
(prod_list (map (nth sign) (a#xa))) = 1"
using prodsame salt ih by auto
have h3: "(prod_list (map (nth sign) (a#xa))) = 1 ⟶ (((poly (qs ! a) x) > 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x > 0) ∨
((poly (qs ! a) x) < 0 ∧ poly (prod_list (retrieve_polys qs (xa))) x < 0))"
using prodsame salt ih assms horiz_vector_helper_zer_ind_R2[where p = "p", where x = "x", where sign = "sign", where I ="I"]
by (smt (verit, ccfv_threshold) Cons.prems ‹poly (prod_list (retrieve_polys qs (a # xa))) x = poly (qs ! a) x * poly (prod_list (retrieve_polys qs xa)) x› horiz_vector_helper_zer_ind_R2 mem_Collect_eq mult_cancel_left1 mult_not_zero sagt)
then show ?case using h1 h2 h3 iff1 Cons.prems by auto
qed
lemma horiz_vector_helper_pos_ind_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list * 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 qs x"
assumes asm1: "list_constr (fst I) (length qs)"
assumes asm2: "list_constr (snd I) (length qs)"
shows "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)) ⟷ (z_R I sign = 1)"
proof -
have len: "length sign = length qs" using sign_fix csv_length_same_as_qlist[of p x sign qs]
nonzero root_p by auto
have d1: "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)) ⟶ (z_R I sign = 1)"
using assms horiz_vector_helper_pos_ind_R1[where p = "p", where qs = "qs", where sign = "sign", where x = "x", where I = "fst I"]
horiz_vector_helper_pos_ind_R2[where p = "p", where qs = "qs", where sign = "sign", where x = "x", where I = "snd I"] unfolding z_R_def
by auto
have d2: "(z_R I sign = 1) ⟶ ((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0))"
proof -
have h1: "(z_R I sign = 1) ⟶ (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0)"
proof -
have "(prod_list (map (nth (map_sgas sign)) (fst I))) = 1 ∨ (prod_list (map (nth (map_sgas sign)) (fst I))) = 0"
using len consistent_signs_prop_R[where p = "p", where qs = "qs", where x = "x", where sign = "sign"] z_signs_R1[where signs = "sign", where I = "fst I"] assms
unfolding list_constr_def
by auto
then show ?thesis
using z_signs_R1[where signs = "sign", where I = "fst I"] horiz_vector_helper_pos_ind_R1[where sign = "sign", where I = "fst I", where p = "p", where x = "x"] assms
apply (auto)
by (metis (mono_tags, opaque_lifting) ‹prod_list (map ((!) (map_sgas sign)) (fst I)) = 1 ∨ prod_list (map ((!) (map_sgas sign)) (fst I)) = 0› mult_zero_left z_R_def)
qed
then have h2: "(z_R I sign = 1) ⟶ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)"
unfolding z_R_def using assms horiz_vector_helper_pos_ind_R2[where p = "p", where x = "x", where sign = "sign", where qs = "qs", where I ="snd I"]
by (metis horiz_vector_helper_pos_ind_R1 mult.left_neutral)
show ?thesis using h1 h2 by auto
qed
show ?thesis using d1 d2 by blast
qed
lemma horiz_vector_helper_pos_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list*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 qs x"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x > 0)) ⟷ (z_R I sign = 1)"
using horiz_vector_helper_pos_ind_R
using nonzero root_p sign_fix welldefined1 welldefined2 by blast
lemma horiz_vector_helper_neg_R:
fixes p:: "real poly"
assumes nonzero: "p≠0"
fixes qs:: "real poly list"
fixes I:: "nat list*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 qs x"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x < 0)) ⟷ (z_R I sign = -1)"
proof -
have set_hyp: "sign ∈ set (characterize_consistent_signs_at_roots p qs)"
using in_set_R[of p x sign qs] nonzero root_p sign_fix by blast
have z_hyp: "((z_R I sign = 1) ∨ (z_R I sign = 0) ∨ (z_R I sign = -1))"
using welldefined1 welldefined2 set_hyp z_lemma_R[where sign="sign", where I = "I", where p="p", where qs="qs"] by blast
have d1: "((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x < 0)) ⟹ (z_R I sign = -1)"
using horiz_vector_helper_pos_R
using nonzero root_p sign_fix welldefined1 welldefined2
by (smt (verit, ccfv_threshold) horiz_vector_helper_pos_ind_R1 horiz_vector_helper_zer_ind_R2 mem_Collect_eq mult_eq_0_iff z_R_def z_hyp)
have d2: "(z_R I sign = -1) ⟹ ((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd I))) x < 0))"
using horiz_vector_helper_pos_ind_R1 horiz_vector_helper_zer_ind_R2 nonzero root_p sign_fix welldefined1 welldefined2
by (smt (verit, ccfv_threshold) class_field.neg_1_not_0 consistent_sign_vec_def consistent_signs_prop_R equal_neg_zero horiz_vector_helper_pos_ind_R2 length_map list_all_length list_constr_def mem_Collect_eq mem_Collect_eq mult_cancel_left1 mult_not_zero retrieve_polys_def z_R_def z_signs_R1 zero_neq_one)
then show ?thesis using d1 d2
by linarith
qed
lemma lhs_dot_rewrite:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*nat list"
fixes signs:: "rat list list"
assumes nonzero: "p≠0"
shows
"(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
sum_list (map (λs. (z_R I s) * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) signs)"
proof -
have "p ≠ 0" using nonzero by auto
from construct_lhs_vector_cleaner[OF this]
have rhseq: "construct_lhs_vector_R p qs signs =
vec_of_list
(map (λs. rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) signs)"
using construct_lhs_vector_cleaner_R nonzero by presburger
have "(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
sum_list (map2 (*) (mtx_row_R signs I) (map (λs. rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) signs))"
unfolding rhseq
apply (intro vec_of_list_dot_rewrite)
by (auto simp add: mtx_row_R_def)
thus ?thesis unfolding mtx_row_R_def
using map2_map_map
by (auto simp add: map2_map_map)
qed
lemma construct_lhs_vector_drop_consistent_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*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 p qs) ⊆ set(signs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows
"(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
(vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙
(construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)))"
proof -
have h0: "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ∧
0 < rat_of_nat (card {xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn}) ⟶ z_R I sgn = 0"
proof -
have "∀ sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_int (card
{xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn}) ⟶ {xa. poly p xa = 0 ∧ consistent_sign_vec 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 (metis Collect_empty_eq)
{ assume "∃is. is = iis ∧ {r. poly p r = 0 ∧ consistent_sign_vec qs r = is} ≠ {}"
then have "∃is. consistent_sign_vec qs (rr (λr. poly p r = 0 ∧ consistent_sign_vec qs r = is)) = iis ∧ {r. poly p r = 0 ∧ consistent_sign_vec qs r = is} ≠ {}"
using ff2
by (metis (mono_tags, lifting))
then have "∃r. poly p r = 0 ∧ consistent_sign_vec qs r = iis"
using ff2
by smt
then have "iis ∈ consistent_sign_vec qs ` set (sorted_list_of_set {r. poly p r = 0})"
using ff1 poly_roots_finite
by (metis (mono_tags) imageI mem_Collect_eq set_sorted_list_of_set) }
then have "iis ∉ set signs ∨ iis ∈ consistent_sign_vec qs ` set (characterize_root_list_p p) ∨ ¬ 0 < rat_of_int (int (card {r. poly p r = 0 ∧ consistent_sign_vec qs r = iis}))"
by (metis (no_types) ‹∀sgn. sgn ∈ set signs ∧ sgn ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ∧ 0 < rat_of_int (int (card {xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn})) ⟶ {xa. poly p xa = 0 ∧ consistent_sign_vec 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 qs ` set (characterize_root_list_p p) ⟶ ((0 = rat_of_nat (card
{xa. poly p xa = 0 ∧ consistent_sign_vec qs xa = sgn}) ∨ z_R I sgn = 0))"
by auto
then have hyp: "∀ s. s ∈ set signs ∧ s ∉ consistent_sign_vec qs ` set (characterize_root_list_p p) ⟶ (z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}) = 0)"
by auto
then have "(∑s∈ set(signs). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈(set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
proof -
have "set(signs) =(set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p)))"
by blast
then have sum_rewrite: "(∑s∈ set(signs). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈ (set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
by auto
then have sum_split: "(∑s∈ (set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))) ∪
(set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
=
(∑s∈ (set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
+ (∑s∈ (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
by (metis (no_types, lifting) List.finite_set sum.Int_Diff)
have sum_zero: "(∑s∈ (set(signs)-(consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec 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 qs)
(characterize_root_list_p p))) = set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))"
using all_info apply (simp add: characterize_consistent_signs_at_roots_def subset_antisym)
by (smt (z3) Int_subset_iff consistent_sign_vec_def list.set_map map_eq_conv o_apply signs_at_def squash_def subsetI subset_antisym)
have hyp1: "(∑s←signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈set (signs). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using distinct_signs sum_list_distinct_conv_sum_set by blast
have hyp2: "(∑s←remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
= (∑s∈ set (remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using sum_list_distinct_conv_sum_set by blast
have set_sum_eq: "(∑s∈(set (signs) ∩ (consistent_sign_vec qs ` set (characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s∈ set (remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p))). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using set_eq by auto
then have "(∑s←signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s←remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using set_sum_eq hyp1 hyp2
using ‹(∑s∈set signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = (∑s∈set signs ∩ consistent_sign_vec qs ` set (characterize_root_list_p p). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))› by linarith
then have "consistent_sign_vec qs ` set (characterize_root_list_p p) ⊆ set signs ⟹
(⋀p qss.
characterize_consistent_signs_at_roots p qss =
remdups (map (consistent_sign_vec qss) (characterize_root_list_p p))) ⟹
(∑s←signs. z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
(∑s←remdups
(map (consistent_sign_vec qs)
(characterize_root_list_p p)). z_R I s * rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec 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 consistent_sign_vec_def characterize_consistent_signs_at_roots_def)
using all_info consistent_sign_vec_def characterize_consistent_signs_at_roots_def
by (smt (z3) list.set_map map_eq_conv o_apply set_remdups signs_at_def squash_def)
qed
lemma matrix_equation_helper_step_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*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 p qs) ⊆ set(signs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "(vec_of_list (mtx_row_R signs I) ∙ (construct_lhs_vector_R p qs signs)) =
rat_of_int (card {x. poly p x = 0 ∧ (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ poly (prod_list (retrieve_polys qs (snd I))) x > 0}) -
rat_of_int (card {x. poly p x = 0 ∧ (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ poly (prod_list (retrieve_polys qs (snd I))) x < 0})"
proof -
have finset: "finite (set (map (consistent_sign_vec qs) (characterize_root_list_p p)))" by auto
let ?gt = "(set (map (consistent_sign_vec qs) (characterize_root_list_p p)) ∩ {s. z_R I s = 1})"
let ?lt = " (set (map (consistent_sign_vec qs) (characterize_root_list_p p)) ∩ {s. z_R I s = -1})"
let ?zer = "(set (map (consistent_sign_vec qs) (characterize_root_list_p p)) ∩ {s. z_R I s = 0})"
have eq: "set (map (consistent_sign_vec qs) (characterize_root_list_p p)) = (?gt ∪ ?lt) ∪ ?zer"
proof safe
fix x
assume h:"x ∈ set (map (consistent_sign_vec qs) (characterize_root_list_p p))"
"z_R I x ≠ 0" "z_R I x ≠ - 1"
then have "x ∈ set (characterize_consistent_signs_at_roots p qs)"
unfolding characterize_consistent_signs_at_roots_def
by (smt (verit, del_insts) characterize_consistent_signs_at_roots_def characterize_root_list_p_def imageE in_set_R nonzero poly_roots_finite set_map sorted_list_of_set(1))
thus "z_R I x = 1"
using h welldefined1 welldefined2 z_lemma_R by blast
qed
have sumeq: "(∑s∈(?gt∪?lt). z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))
= (∑s∈?gt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?lt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
apply (rule sum.union_disjoint) by auto
from construct_lhs_vector_drop_consistent_R[OF assms(1-5)] have
"vec_of_list (mtx_row_R signs I) ∙ construct_lhs_vector_R p qs signs =
vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙
construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)" .
from lhs_dot_rewrite[OF assms(1)]
moreover have "... =
(∑s←characterize_consistent_signs_at_roots p qs.
z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))" .
moreover have "... =
(∑s∈set (map (consistent_sign_vec qs) (characterize_root_list_p p)).
z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))" unfolding characterize_consistent_signs_at_roots_def sum_code[symmetric]
apply (auto)
by (smt (verit, best) consistent_sign_vec_def list.set_map map_eq_conv o_apply signs_at_def squash_def sum.set_conv_list)
moreover have setc1:"... =
(∑s∈(?gt∪?lt). z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?zer. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) "
apply (subst eq)
apply (rule sum.union_disjoint) by auto
ultimately have setc: "... =
(∑s∈?gt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?lt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) +
(∑s∈?zer. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))"
using sumeq by auto
have "∀s ∈ ?zer. (z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = 0"
by auto
then have obvzer: "(∑s∈?zer. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) = 0"
by auto
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 qs x = s} =
{x ∈{x. poly p x = 0}. consistent_sign_vec qs x = s}"
by auto
have e1: "(∑s∈consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}.
card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}) =
(sum (λx. if (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd 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 qs) (characterize_root_list_p p)))› setroots apply auto[1]
apply (metis List.finite_set setroots)
proof safe
fix x
assume rt: "poly p x = 0"
then have 1: "{s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}. consistent_sign_vec qs x = s} =
{s. z_R I s = 1 ∧ consistent_sign_vec qs x = s}"
by auto
have 2: "... = {s. (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (0 < poly (prod_list (retrieve_polys qs (snd I))) x) ∧ consistent_sign_vec qs x = s}"
using horiz_vector_helper_pos_R assms welldefined1 welldefined2 rt by blast
have 3: "... = (if (∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (0 < poly (prod_list (retrieve_polys qs (snd I))) x) then {consistent_sign_vec qs x} else {})"
by auto
then have "card {s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}. consistent_sign_vec qs x = s} =
(if ((∀p ∈ set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 < poly (prod_list (retrieve_polys qs (snd I))) x)
then 1 else 0)" using 1 2 3 by auto
thus " card
{s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = 1}.
consistent_sign_vec qs x = s} =
(if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧
0 < poly (prod_list (retrieve_polys qs (snd I))) x
then 1 else 0)"
by auto
qed
have gtchr: "(∑s∈?gt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
rat_of_int (card {x. poly p x = 0 ∧ (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 < poly (prod_list (retrieve_polys qs (snd 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 e2: " (∑s∈consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = - 1}.
card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}) =
(sum (λx. if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (poly (prod_list (retrieve_polys qs (snd 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 qs) (characterize_root_list_p p)))› setroots apply auto[1]
apply (metis List.finite_set setroots)
proof safe
fix x
assume rt: "poly p x = 0"
then have 1: "{s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = -1}. consistent_sign_vec qs x = s} =
{s. z_R I s = -1 ∧ consistent_sign_vec qs x = s}"
by auto
have 2: "... = {s. ((∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 > poly (prod_list (retrieve_polys qs (snd I))) x) ∧ consistent_sign_vec qs x = s}"
using horiz_vector_helper_neg_R assms rt welldefined1 welldefined2 by blast
have 3: "... = (if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ (0 > poly (prod_list (retrieve_polys qs (snd I))) x) then {consistent_sign_vec qs x} else {})"
by auto
thus "card {s ∈ consistent_sign_vec qs ` {x. poly p x = 0} ∩ {s. z_R I s = -1}. consistent_sign_vec qs x = s} =
(if (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 > poly
(prod_list
(retrieve_polys qs (snd I)))
x
then 1 else 0)" using 1 2 3 by auto
qed
have ltchr: "(∑s∈?lt. z_R I s * rat_of_int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})) =
- rat_of_int (card {x. poly p x = 0 ∧ (∀p∈set (retrieve_polys qs (fst I)). poly p x = 0) ∧ 0 > poly (prod_list (retrieve_polys qs (snd 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 obvzer setc
using ‹(∑s←characterize_consistent_signs_at_roots p qs. z_R I s * rat_of_int (int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s}))) = (∑s∈set (map (consistent_sign_vec qs) (characterize_root_list_p p)). z_R I s * rat_of_int (int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})))› ‹vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙ construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs) = (∑s←characterize_consistent_signs_at_roots p qs. z_R I s * rat_of_int (int (card {x. poly p x = 0 ∧ consistent_sign_vec qs x = s})))› ‹vec_of_list (mtx_row_R signs I) ∙ construct_lhs_vector_R p qs signs = vec_of_list (mtx_row_R (characterize_consistent_signs_at_roots p qs) I) ∙ construct_lhs_vector_R p qs (characterize_consistent_signs_at_roots p qs)› setc1 by linarith
qed
lemma matrix_equation_main_step_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes I:: "nat list*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 p qs) ⊆ set(signs)"
assumes welldefined1: "list_constr (fst I) (length qs)"
assumes welldefined2: "list_constr (snd I) (length qs)"
shows "(vec_of_list (mtx_row_R signs I) ∙
(construct_lhs_vector_R p qs signs)) =
construct_NofI_R p (retrieve_polys qs (fst I)) (retrieve_polys qs (snd I))"
proof -
show ?thesis
unfolding construct_NofI_prop_R[OF nonzero]
using matrix_equation_helper_step_R[OF assms]
by linarith
qed
lemma mtx_row_length_R:
"list_all (λr. length r = length signs) (map (mtx_row_R signs) ls)"
apply (induction ls)
by (auto simp add: mtx_row_R_def)
theorem matrix_equation_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
fixes subsets:: "(nat list*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 p qs) ⊆ set(signs)"
assumes welldefined: "all_list_constr_R (subsets) (length qs)"
shows "satisfy_equation_R p qs subsets signs"
unfolding satisfy_equation_R_def matrix_A_R_def
construct_lhs_vector_R_def construct_rhs_vector_R_def all_list_constr_R_def
apply (subst mult_mat_vec_of_list)
apply (auto simp add: mtx_row_length_R intro!: map_vec_vec_of_list_eq_intro)
using matrix_equation_main_step_R[OF assms(1-3), unfolded construct_lhs_vector_R_def]
using all_list_constr_R_def in_set_member welldefined by fastforce
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_R:: "real poly ⇒ real poly list ⇒ rat list list ⇒ rat vec"
where "w_vec_R ≡ construct_lhs_vector_R"
abbreviation v_vec_R:: "real poly ⇒ real poly list ⇒ (nat list*nat list) list ⇒ rat vec"
where "v_vec_R ≡ construct_rhs_vector_R"
abbreviation M_mat_R:: "rat list list ⇒ (nat list*nat list) list ⇒ rat mat"
where "M_mat_R ≡ matrix_A_R"
theorem matrix_equation_pretty:
fixes subsets:: "(nat list*nat list) list"
assumes "p≠0"
assumes "distinct signs"
assumes "consistent_signs_at_roots p qs ⊆ set signs"
assumes "⋀a b i. (a, b) ∈ set ( subsets) ⟹ (i ∈ set a ∨ i ∈ set b) ⟹ i < length qs"
shows "M_mat_R signs subsets *⇩v w_vec_R p qs signs = v_vec_R p qs subsets"
unfolding satisfy_equation_R_def[symmetric]
using matrix_equation_R[of p signs qs subsets] assms
using consistent_signs_at_roots_eq unfolding all_list_constr_R_def list_constr_def apply (auto)
by (metis (no_types, lifting) Ball_set in_set_member)
section "Base Case"
definition satisfies_properties_R:: "real poly ⇒ real poly list ⇒ (nat list*nat list) list ⇒ rat list list ⇒ rat mat ⇒ bool"
where "satisfies_properties_R p qs subsets signs matrix =
( all_list_constr_R subsets (length qs) ∧ well_def_signs (length qs) signs ∧ distinct signs
∧ satisfy_equation_R p qs subsets signs ∧ invertible_mat matrix ∧ matrix = matrix_A_R signs subsets
∧ set (characterize_consistent_signs_at_roots p qs) ⊆ set(signs)
)"
lemma mat_base_case_R:
shows "matrix_A_R [[1],[0],[-1]] [([], []),([0], []),([], [0])] = (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]])"
unfolding matrix_A_R_def mtx_row_R_def z_R_def map_sgas_def apply (auto)
by (simp add: numeral_3_eq_3)
lemma base_case_sgas_R:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
shows "set (characterize_consistent_signs_at_roots p [q]) ⊆ {[1],[0], [- 1]}"
unfolding characterize_consistent_signs_at_roots_def signs_at_def apply (auto)
by (meson squash_def)
lemma base_case_sgas_alt_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes len1: "length qs = 1"
assumes nonzero: "p ≠ 0"
shows "set (characterize_consistent_signs_at_roots p qs) ⊆ {[1], [0], [- 1]}"
proof -
have ex_q: "∃(q::real poly). qs = [q]"
using len1
using length_Suc_conv[of qs 0] by auto
then show ?thesis using base_case_sgas_R nonzero
by auto
qed
lemma base_case_satisfy_equation_R:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
shows "satisfy_equation_R p [q] [([], []),([0], []),([], [0])] [[1],[0],[-1]] "
proof -
have h1: "set (characterize_consistent_signs_at_roots p [q]) ⊆ {[1], [0],[- 1]}"
using base_case_sgas_R assms by auto
have h2: "all_list_constr_R [([], []),([0], []),([], [0])] (Suc 0)" unfolding all_list_constr_R_def
by (simp add: list_constr_def member_def)
then show ?thesis using matrix_equation_R[where p = "p", where qs = "[q]", where signs = "[[1],[0],[-1]] ", where subsets = "[([], []),([0], []),([], [0])]"]
nonzero h1 h2 by auto
qed
lemma base_case_satisfy_equation_alt_R:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes len1: "length qs = 1"
assumes nonzero: "p ≠ 0"
shows "satisfy_equation_R p qs [([], []),([0], []),([], [0])] [[1],[0],[-1]]"
proof -
have ex_q: "∃(q::real poly). qs = [q]"
using len1
using length_Suc_conv[of qs 0] by auto
then show ?thesis using base_case_satisfy_equation_R nonzero
by auto
qed
lemma base_case_matrix_eq:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
shows "(mult_mat_vec (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]) (construct_lhs_vector_R p [q] [[1],[0],[-1]]) =
(construct_rhs_vector_R p [q] [([], []),([0], []),([], [0])]))"
using mat_base_case_R base_case_satisfy_equation_R unfolding satisfy_equation_R_def
by (simp add: nonzero)
lemma less_three: "(n::nat) < Suc (Suc (Suc 0)) ⟷ n = 0 ∨ n = 1 ∨ n = 2"
by auto
lemma inverse_mat_base_case_R:
shows "inverts_mat (mat_of_rows_list 3 [[1/2, -1/2, 1/2], [0, 1, 0], [1/2, -1/2, -1/2]]::rat mat) (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat)"
unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
unfolding less_three by (auto simp add: scalar_prod_def)
lemma inverse_mat_base_case_2_R:
shows "inverts_mat (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat) (mat_of_rows_list 3 [[1/2, -1/2, 1/2], [0, 1, 0], [1/2, -1/2, -1/2]]:: rat mat)"
unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
unfolding less_three by (auto simp add: scalar_prod_def)
lemma base_case_invertible_mat_R:
shows "invertible_mat (matrix_A_R [[1],[0], [- 1]] [([], []),([0], []),([], [0])])"
unfolding invertible_mat_def using inverse_mat_base_case_R inverse_mat_base_case_2_R
apply (auto)
apply (simp add: mat_base_case mat_of_rows_list_def)
using mat_base_case_R by auto
section "Inductive Step"
subsection "Lemmas on smashing subsets "
definition subsets_first_component_list::"(nat list*nat list) list ⇒ nat list list"
where "subsets_first_component_list I = map (λI. (fst I)) I"
definition subsets_second_component_list::"(nat list*nat list) list ⇒ nat list list"
where "subsets_second_component_list I = map (λI. (snd I)) I"
definition smash_list_list::"('a list*'a list) list ⇒ ('a list*'a list) list ⇒ ('a list*'a list) list"
where "smash_list_list s1 s2 = concat (map (λl1. map (λl2. (fst l1 @ fst l2, snd l1 @ snd l2)) s2) s1)"
lemma smash_list_list_property_set:
fixes l1 l2 :: "('a list*'a list) list"
fixes a b:: "nat"
shows "∀ (elem :: ('a list*'a list)). (elem ∈ (set (smash_list_list l1 l2)) ⟶
(∃ (elem1:: ('a list*'a list)). ∃ (elem2:: ('a list*'a list)).
(elem1 ∈ set(l1) ∧ elem2 ∈ set(l2) ∧ elem = (fst elem1@ fst elem2, snd elem1 @ snd elem2))))"
proof clarsimp
fix a b
assume assum: "(a, b) ∈ set (smash_list_list l1 l2)"
show "∃aa ba. (aa, ba) ∈ set l1 ∧ (∃ab bb. (ab, bb) ∈ set l2 ∧ a = aa @ ab ∧ b = ba @ bb)"
using assum unfolding smash_list_list_def
apply (auto) by blast
qed
lemma subsets_smash_property_R:
fixes subsets1 subsets2 :: "(nat list*nat list) list"
fixes n:: "nat"
shows "∀ (elem :: nat list*nat list). (List.member (subsets_smash_R n subsets1 subsets2) elem) ⟶
(∃ (elem1::nat list*nat list). ∃ (elem2::nat list*nat list).
(elem1 ∈ set(subsets1) ∧ elem2 ∈ set(subsets2) ∧ elem = ((fst elem1) @ (map ((+) n) (fst elem2)), (snd elem1) @ (map ((+) n) (snd elem2)))))"
proof -
let ?fst_component2 = "subsets_first_component_list subsets2"
let ?snd_component2 = "subsets_second_component_list subsets2"
let ?new_subsets = "map (λI. ((map ((+) n)) (fst I), (map ((+) n)) (snd I))) subsets2"
have "subsets_smash_R n subsets1 subsets2 = smash_list_list subsets1 ?new_subsets"
unfolding subsets_smash_R_def smash_list_list_def apply (auto)
by (simp add: comp_def)
then show ?thesis using smash_list_list_property_set[of subsets1 ?new_subsets] apply (auto)
using imageE in_set_member set_map smash_list_list_property_set
by (smt (z3) prod.exhaust_sel)
qed
subsection "Well-defined subsets preserved when smashing"
lemma well_def_step_R:
fixes qs1 qs2 :: "real poly list"
fixes subsets1 subsets2 :: "(nat list*nat list) list"
assumes well_def_subsets1: "all_list_constr_R (subsets1) (length qs1)"
assumes well_def_subsets2: "all_list_constr_R (subsets2) (length qs2)"
shows "all_list_constr_R ((subsets_smash_R (length qs1) subsets1 subsets2))
(length (qs1 @ qs2))"
proof -
let ?n = "(length qs1)"
have h1: "∀elem.
List.member (subsets_smash_R ?n subsets1 subsets2) elem ⟶
(∃ (elem1::nat list*nat list). ∃ (elem2::nat list*nat list).
(elem1 ∈ set(subsets1) ∧ elem2 ∈ set(subsets2) ∧ elem = ((fst elem1) @ (map ((+) ?n) (fst elem2)), (snd elem1) @ (map ((+) ?n) (snd elem2)))))"
using