Theory BenOr_Kozen_Reif.BKR_Proofs
theory BKR_Proofs
imports Matrix_Equation_Construction
begin
definition well_def_signs:: "nat => rat list list ⇒ bool"
where "well_def_signs num_polys sign_conds ≡ ∀ signs ∈ set(sign_conds). (length signs = num_polys)"
definition satisfies_properties:: "real poly ⇒ real poly list ⇒ nat list list ⇒ rat list list ⇒ rat mat ⇒ bool"
where "satisfies_properties p qs subsets signs matrix =
( all_list_constr subsets (length qs) ∧ well_def_signs (length qs) signs ∧ distinct signs
∧ satisfy_equation p qs subsets signs ∧ invertible_mat matrix ∧ matrix = matrix_A signs subsets
∧ set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)
)"
section "Base Case"
lemma mat_base_case:
shows "matrix_A [[1],[-1]] [[],[0]] = (mat_of_rows_list 2 [[1, 1], [1, -1]])"
unfolding matrix_A_def mtx_row_def z_def by (auto simp add: numeral_2_eq_2)
lemma base_case_sgas:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
assumes rel_prime: "coprime p q"
shows "set (characterize_consistent_signs_at_roots_copr p [q]) ⊆ {[1], [- 1]}"
unfolding characterize_consistent_signs_at_roots_copr_def consistent_sign_vec_copr_def by auto
lemma base_case_sgas_alt:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes len1: "length qs = 1"
assumes nonzero: "p ≠ 0"
assumes rel_prime: "∀q. (List.member qs q) ⟶ coprime p q"
shows "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ {[1], [- 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 nonzero rel_prime
apply (auto)
using characterize_consistent_signs_at_roots_copr_def consistent_sign_vec_copr_def by auto
qed
lemma base_case_satisfy_equation:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
assumes rel_prime: "coprime p q"
shows "satisfy_equation p [q] [[],[0]] [[1],[-1]]"
proof -
have h1: "set (characterize_consistent_signs_at_roots_copr p [q]) ⊆ {[1], [- 1]}"
using base_case_sgas assms by auto
have h2: " ∀qa. List.member [q] qa ⟶ coprime p qa" using rel_prime
by (simp add: member_rec(1) member_rec(2))
have h3: "all_list_constr [[], [0]] (Suc 0)" unfolding all_list_constr_def
by (simp add: list_constr_def member_def)
then show ?thesis using matrix_equation[where p = "p", where qs = "[q]", where signs = "[[1],[-1]]", where subsets = "[[],[0]]"]
nonzero h1 h2 h3 by auto
qed
lemma base_case_satisfy_equation_alt:
fixes p:: "real poly"
fixes qs:: "real poly list"
assumes len1: "length qs = 1"
assumes nonzero: "p ≠ 0"
assumes rel_prime: "∀q. (List.member qs q) ⟶ coprime p q"
shows "satisfy_equation p qs [[],[0]] [[1],[-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 nonzero rel_prime
apply (auto)
by (simp add: member_rec(1))
qed
lemma base_case_matrix_eq:
fixes q p:: "real poly"
assumes nonzero: "p ≠ 0"
assumes rel_prime: "coprime p q"
shows "(mult_mat_vec (mat_of_rows_list 2 [[1, 1], [1, -1]]) (construct_lhs_vector p [q] [[1],[-1]]) =
(construct_rhs_vector p [q] [[],[0]]))"
using mat_base_case base_case_satisfy_equation unfolding satisfy_equation_def
by (simp add: nonzero rel_prime)
lemma less_two:
shows "j < Suc (Suc 0) ⟷ j = 0 ∨ j = 1" by auto
lemma inverse_mat_base_case:
shows "inverts_mat (mat_of_rows_list 2 [[1/2, 1/2], [1/2, -(1/2)]]::rat mat) (mat_of_rows_list 2 [[1, 1], [1, -1]]::rat mat)"
unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
unfolding less_two by (auto simp add: scalar_prod_def)
lemma inverse_mat_base_case_2:
shows "inverts_mat (mat_of_rows_list 2 [[1, 1], [1, -1]]::rat mat) (mat_of_rows_list 2 [[1/2, 1/2], [1/2, -(1/2)]]::rat mat) "
unfolding inverts_mat_def mat_of_rows_list_def mat_eq_iff apply auto
unfolding less_two by (auto simp add: scalar_prod_def)
lemma base_case_invertible_mat:
shows "invertible_mat (matrix_A [[1], [- 1]] [[], [0]])"
unfolding invertible_mat_def using inverse_mat_base_case inverse_mat_base_case_2
apply (auto)
apply (simp add: mat_base_case mat_of_rows_list_def)
using mat_base_case by auto
section "Inductive Step"
subsection "Lemmas on smashing subsets and signs"
lemma signs_smash_property:
fixes signs1 signs2 :: "'a list list"
fixes a b:: "nat"
shows "∀ (elem :: 'a list). (elem ∈ (set (signs_smash signs1 signs2)) ⟶
(∃ n m :: nat.
elem = ((nth signs1 n)@(nth signs2 m))))"
proof clarsimp
fix elem
assume assum: "elem ∈ set (signs_smash signs1 signs2)"
show "∃n m. elem = signs1 ! n @ signs2 ! m"
using assum unfolding signs_smash_def apply (auto)
by (metis in_set_conv_nth)
qed
lemma signs_smash_property_set:
fixes signs1 signs2 :: "'a list list"
fixes a b:: "nat"
shows "∀ (elem :: 'a list). (elem ∈ (set (signs_smash signs1 signs2)) ⟶
(∃ (elem1::'a list). ∃ (elem2::'a list).
(elem1 ∈ set(signs1) ∧ elem2 ∈ set(signs2) ∧ elem = (elem1@elem2))))"
proof clarsimp
fix elem
assume assum: "elem ∈ set (signs_smash signs1 signs2)"
show "∃elem1. elem1 ∈ set signs1 ∧ (∃elem2. elem2 ∈ set signs2 ∧ elem = elem1 @ elem2)"
using assum unfolding signs_smash_def by auto
qed
lemma subsets_smash_property:
fixes subsets1 subsets2 :: "nat list list"
fixes n:: "nat"
shows "∀ (elem :: nat list). (List.member (subsets_smash n subsets1 subsets2) elem) ⟶
(∃ (elem1::nat list). ∃ (elem2::nat list).
(elem1 ∈ set(subsets1) ∧ elem2 ∈ set(subsets2) ∧ elem = (elem1 @ ((map ((+) n) elem2)))))"
proof -
let ?new_subsets = "(map (map ((+) n)) subsets2)"
have "subsets_smash n subsets1 subsets2 = signs_smash subsets1 ?new_subsets"
unfolding subsets_smash_def signs_smash_def by (auto simp add: comp_def)
then show ?thesis
by (smt (verit) imageE in_set_member set_map signs_smash_property_set)
qed
subsection "Well-defined subsets preserved when smashing"
lemma list_constr_append:
"list_constr a n ∧ list_constr b n ⟶ list_constr (a@b) n"
apply (auto) unfolding list_constr_def
using list_all_append by blast
lemma well_def_step:
fixes qs1 qs2 :: "real poly list"
fixes subsets1 subsets2 :: "nat list list"
assumes well_def_subsets1: "all_list_constr (subsets1) (length qs1)"
assumes well_def_subsets2: "all_list_constr (subsets2) (length qs2)"
shows "all_list_constr ((subsets_smash (length qs1) subsets1 subsets2))
(length (qs1 @ qs2))"
proof -
have h1: "∀elem.
List.member (subsets_smash (length qs1) subsets1 subsets2) elem ⟶
(∃elem1 elem2. elem1 ∈ set subsets1 ∧ elem2 ∈ set subsets2 ∧ elem = elem1 @ map ((+) (length qs1)) elem2)"
using subsets_smash_property by blast
have h2: "∀elem1 elem2. (elem1 ∈ set subsets1 ∧ elem2 ∈ set subsets2) ⟶ list_constr (elem1 @ map ((+) (length qs1)) elem2) (length (qs1 @ qs2))"
proof clarsimp
fix elem1
fix elem2
assume e1: "elem1 ∈ set subsets1"
assume e2: "elem2 ∈ set subsets2"
have h1: "list_constr elem1 (length qs1 + length qs2) "
proof -
have h1: "list_constr elem1 (length qs1)" using e1 well_def_subsets1
unfolding all_list_constr_def
by (simp add: in_set_member)
then show ?thesis unfolding list_constr_def
by (simp add: list.pred_mono_strong)
qed
have h2: "list_constr (map ((+) (length qs1)) elem2) (length qs1 + length qs2)"
proof -
have h1: "list_constr elem2 (length qs2)" using e2 well_def_subsets2
unfolding all_list_constr_def
by (simp add: in_set_member)
then show ?thesis unfolding list_constr_def
by (simp add: list_all_length)
qed
show "list_constr (elem1 @ map ((+) (length qs1)) elem2) (length qs1 + length qs2)"
using h1 h2 list_constr_append
by blast
qed
then show ?thesis using h1 unfolding all_list_constr_def by auto
qed
subsection "Well def signs preserved when smashing"
lemma well_def_signs_step:
fixes qs1 qs2 :: "real poly list"
fixes signs1 signs2 :: "rat list list"
assumes "length qs1 > 0"
assumes "length qs2 > 0"
assumes well_def1: "well_def_signs (length qs1) signs1"
assumes well_def2: "well_def_signs (length qs2) signs2"
shows "well_def_signs (length (qs1@qs2)) (signs_smash signs1 signs2)"
using well_def1 well_def2 unfolding well_def_signs_def using signs_smash_property_set[of signs1 signs2] length_append by auto
subsection "Distinct signs preserved when smashing"
lemma distinct_map_append:
assumes "distinct ls"
shows "distinct (map ((@) xs) ls)"
unfolding distinct_map inj_on_def using assms by auto
lemma length_eq_append:
assumes "length y = length b"
shows "(x @ y = a @ b) ⟷ x=a ∧ y = b"
by (simp add: assms)
lemma distinct_step:
fixes qs1 qs2 :: "real poly list"
fixes signs1 signs2 :: "rat list list"
assumes well_def1: "well_def_signs n1 signs1"
assumes well_def2: "well_def_signs n2 signs2"
assumes distinct1: "distinct signs1"
assumes distinct2: "distinct signs2"
shows "distinct (signs_smash signs1 signs2)"
unfolding signs_smash_def
using distinct1
proof(induction signs1)
case Nil
then show ?case by auto
next
case (Cons a signs1)
then show ?case apply (auto simp add: distinct2 distinct_map_append)
using assms unfolding well_def_signs_def
by (simp add: distinct1 distinct2 length_eq_append)
qed
subsection "Consistent sign assignments preserved when smashing"
lemma subset_smash_signs:
fixes a1 b1 a2 b2:: "rat list list"
assumes sub1: "set a1 ⊆ set a2"
assumes sub2: "set b1 ⊆ set b2"
shows "set (signs_smash a1 b1) ⊆ set (signs_smash a2 b2)"
proof -
have h1: "∀x∈set (signs_smash a1 b1). x∈set (signs_smash a2 b2)"
proof clarsimp
fix x
assume x_in: "x ∈ set (signs_smash a1 b1)"
have h1: "∃ n m :: nat. x = (nth a1 n)@(nth b1 m)"
using signs_smash_property[of a1 b1] x_in
by blast
then have h2: "∃ p q::nat. x = (nth a2 p)@(nth b2 q)"
using sub1 sub2 apply (auto)
by (metis nth_find_first signs_smash_property_set subset_code(1) x_in)
then show "x ∈ set (signs_smash a2 b2)"
unfolding signs_smash_def apply (auto)
using signs_smash_property_set sub1 sub2 x_in by fastforce
qed
then show ?thesis
by blast
qed
lemma subset_helper:
fixes p:: "real poly"
fixes qs1 qs2 :: "real poly list"
fixes signs1 signs2 :: "rat list list"
shows "∀ x ∈ set (characterize_consistent_signs_at_roots_copr p (qs1 @ qs2)).
∃ x1 ∈ set (characterize_consistent_signs_at_roots_copr p qs1).
∃ x2 ∈ set (characterize_consistent_signs_at_roots_copr p qs2).
x = x1@x2"
proof clarsimp
fix x
assume x_in: "x ∈ set (characterize_consistent_signs_at_roots_copr p (qs1 @ qs2))"
have x_in_csv: "x ∈ set(map (consistent_sign_vec_copr (qs1 @ qs2)) (characterize_root_list_p p))"
using x_in unfolding characterize_consistent_signs_at_roots_copr_def by simp
have csv_hyp: "∀r. consistent_sign_vec_copr (qs1 @ qs2) r = (consistent_sign_vec_copr qs1 r)@(consistent_sign_vec_copr qs2 r)"
unfolding consistent_sign_vec_copr_def by auto
have exr_iff: "(∃r ∈ set (characterize_root_list_p p). x = consistent_sign_vec_copr (qs1 @ qs2) r) ⟷ (∃r ∈ set (characterize_root_list_p p). x = (consistent_sign_vec_copr qs1 r)@(consistent_sign_vec_copr qs2 r))"
using csv_hyp by auto
have exr: "x ∈ set(map (consistent_sign_vec_copr (qs1 @ qs2)) (characterize_root_list_p p)) ⟶ (∃r ∈ set (characterize_root_list_p p). x = consistent_sign_vec_copr (qs1 @ qs2) r)"
by auto
have mem_list1: "∀ r ∈ set (characterize_root_list_p p). (consistent_sign_vec_copr qs1 r) ∈ set(map (consistent_sign_vec_copr qs1) (characterize_root_list_p p))"
by simp
have mem_list2: "∀ r ∈ set (characterize_root_list_p p). (consistent_sign_vec_copr qs2 r) ∈ set(map (consistent_sign_vec_copr qs2) (characterize_root_list_p p))"
by simp
then show "∃x1∈set (characterize_consistent_signs_at_roots_copr p qs1).
∃x2∈set (characterize_consistent_signs_at_roots_copr p qs2). x = x1 @ x2"
using x_in_csv exr mem_list1 mem_list2 characterize_consistent_signs_at_roots_copr_def exr_iff by auto
qed
lemma subset_step:
fixes p:: "real poly"
fixes qs1 qs2 :: "real poly list"
fixes signs1 signs2 :: "rat list list"
assumes csa1: "set (characterize_consistent_signs_at_roots_copr p qs1) ⊆ set (signs1)"
assumes csa2: "set (characterize_consistent_signs_at_roots_copr p qs2) ⊆ set (signs2)"
shows "set (characterize_consistent_signs_at_roots_copr p
(qs1 @ qs2))
⊆ set (signs_smash signs1 signs2)"
proof -
have h0: "∀ x ∈ set (characterize_consistent_signs_at_roots_copr p (qs1 @ qs2)). ∃ x1 ∈ set (characterize_consistent_signs_at_roots_copr p qs1). ∃ x2 ∈ set (characterize_consistent_signs_at_roots_copr p qs2).
(x = x1@x2)" using subset_helper[of p qs1 qs2]
by blast
then have "∀x ∈ set (characterize_consistent_signs_at_roots_copr p (qs1 @ qs2)).
x ∈ set (signs_smash (characterize_consistent_signs_at_roots_copr p qs1)
(characterize_consistent_signs_at_roots_copr p qs2))"
unfolding signs_smash_def apply (auto)
by fastforce
then have "∀x ∈ set (characterize_consistent_signs_at_roots_copr p
(qs1 @ qs2)). x ∈ set (signs_smash signs1 signs2)"
using csa1 csa2 subset_smash_signs[of _ signs1 _ signs2] apply (auto)
by blast
thus ?thesis
by blast
qed
subsection "Main Results"
lemma dim_row_mat_of_rows_list[simp]:
shows "dim_row (mat_of_rows_list nr ls) = length ls"
unfolding mat_of_rows_list_def by auto
lemma dim_col_mat_of_rows_list[simp]:
shows "dim_col (mat_of_rows_list nr ls) = nr"
unfolding mat_of_rows_list_def by auto
lemma dim_row_matrix_A[simp]:
shows "dim_row (matrix_A signs subsets) = length subsets"
unfolding matrix_A_def by auto
lemma dim_col_matrix_A[simp]:
shows "dim_col (matrix_A signs subsets) = length signs"
unfolding matrix_A_def by auto
lemma length_signs_smash:
shows
"length (signs_smash signs1 signs2) = length signs1 * length signs2"
unfolding signs_smash_def length_concat
by (auto simp add: o_def sum_list_triv)
lemma length_subsets_smash:
shows
"length (subsets_smash n subs1 subs2) = length subs1 * length subs2"
unfolding subsets_smash_def length_concat
by (auto simp add: o_def sum_list_triv)
lemma length_eq_concat:
assumes "⋀x. x ∈ set ls ⟹ length x = n"
assumes "i < n * length ls"
shows "concat ls ! i = ls ! (i div n) ! (i mod n)"
using assms
proof (induct ls arbitrary: i)
case Nil
then show ?case
by simp
next
from assms have ‹n > 0›
by (cases ‹n = 0›) simp_all
case (Cons a ls)
show ?case
proof (cases ‹n ≤ i›)
case False
with Cons show ?thesis
by (simp add: nth_append)
next
case True
moreover define j where ‹j = i - n›
ultimately have ‹i = n + j›
by simp
with Cons ‹n > 0› show ?thesis
by (simp add: nth_append div_add_self1)
qed
qed
lemma z_append:
assumes "⋀i. i ∈ set xs ⟹ i < length as"
shows "z (xs @ (map ((+) (length as)) ys)) (as @ bs) = z xs as * z ys bs"
proof -
have 1: "map ((!) (as @ bs)) xs = map ((!) as) xs"
unfolding list_eq_iff_nth_eq
using assms by (auto simp add:nth_append)
have 2: "map ((!) (as @ bs) ∘ (+) (length as)) ys = map ((!) bs) ys"
unfolding list_eq_iff_nth_eq
using assms by auto
show ?thesis
unfolding z_def apply auto
unfolding 1 2 by auto
qed
lemma matrix_construction_is_kronecker_product:
fixes qs1 :: "real poly list"
fixes subs1 subs2 :: "nat list list"
fixes signs1 signs2 :: "rat list list"
assumes "⋀l i. l ∈ set subs1 ⟹ i ∈ set l ⟹ i < n1"
assumes "⋀j. j ∈ set signs1 ⟹ length j = n1"
shows "
(matrix_A (signs_smash signs1 signs2) (subsets_smash n1 subs1 subs2)) =
kronecker_product (matrix_A signs1 subs1) (matrix_A signs2 subs2)"
unfolding mat_eq_iff dim_row_matrix_A dim_col_matrix_A
length_subsets_smash length_signs_smash dim_kronecker
proof safe
fix i j
assume i: "i < length subs1 * length subs2"
and j: "j < length signs1 * length signs2"
have ld: "i div length subs2 < length subs1"
"j div length signs2 < length signs1"
using i j less_mult_imp_div_less by auto
have lm: "i mod length subs2 < length subs2"
"j mod length signs2 < length signs2"
using i j less_mult_imp_mod_less by auto
have n1: "n1 = length (signs1 ! (j div length signs2))"
using assms(2) ld(2) nth_mem by blast
have 1: "matrix_A (signs_smash signs1 signs2) (subsets_smash n1 subs1 subs2) $$ (i, j) =
z (subsets_smash n1 subs1 subs2 ! i) (signs_smash signs1 signs2 ! j)"
unfolding mat_of_rows_list_def matrix_A_def mtx_row_def
using i j
by (simp add: length_signs_smash length_subsets_smash)
have 2: " ... = z (subs1 ! (i div length subs2) @ map ((+) n1) (subs2 ! (i mod length subs2)))
(signs1 ! (j div length signs2) @ signs2 ! (j mod length signs2))"
unfolding signs_smash_def subsets_smash_def
apply (subst length_eq_concat)
using i apply (auto simp add: mult.commute)
apply (subst length_eq_concat)
using j apply (auto simp add: mult.commute)
using ld lm by auto
have 3: "... =
z (subs1 ! (i div length subs2)) (signs1 ! (j div length signs2)) *
z (subs2 ! (i mod length subs2)) (signs2 ! (j mod length signs2))"
unfolding n1
apply (subst z_append)
apply (auto simp add: n1[symmetric])
using assms(1) ld(1) nth_mem by blast
have 4: "kronecker_product (matrix_A signs1 subs1) (matrix_A signs2 subs2) $$ (i,j) =
z (subs1 ! (i div length subs2))
(signs1 ! (j div length signs2)) *
z (subs2 ! (i mod length subs2))
(signs2 ! (j mod length signs2))"
unfolding kronecker_product_def matrix_A_def mat_of_rows_list_def mtx_row_def
using i j apply (auto simp add: Let_def)
apply (subst index_mat(1)[OF ld])
apply (subst index_mat(1)[OF lm])
using ld lm by auto
show "matrix_A (signs_smash signs1 signs2) (subsets_smash n1 subs1 subs2) $$ (i, j) =
kronecker_product (matrix_A signs1 subs1) (matrix_A signs2 subs2) $$ (i, j)"
using 1 2 3 4 by auto
qed
lemma inductive_step:
fixes p:: "real poly"
fixes qs1 qs2 :: "real poly list"
fixes subsets1 subsets2 :: "nat list list"
fixes signs1 signs2 :: "rat list list"
assumes nonzero: "p ≠ 0"
assumes nontriv1: "length qs1 > 0"
assumes nontriv2: "length qs2 > 0"
assumes pairwise_rel_prime1: "∀q. ((List.member qs1 q) ⟶ (coprime p q))"
assumes pairwise_rel_prime2: "∀q. ((List.member qs2 q) ⟶ (coprime p q))"
assumes welldefined_signs1: "well_def_signs (length qs1) signs1"
assumes welldefined_signs2: "well_def_signs (length qs2) signs2"
assumes distinct_signs1: "distinct signs1"
assumes distinct_signs2: "distinct signs2"
assumes all_info1: "set (characterize_consistent_signs_at_roots_copr p qs1) ⊆ set(signs1)"
assumes all_info2: "set (characterize_consistent_signs_at_roots_copr p qs2) ⊆ set(signs2)"
assumes welldefined_subsets1: "all_list_constr (subsets1) (length qs1)"
assumes welldefined_subsets2: "all_list_constr (subsets2) (length qs2)"
assumes invertibleMtx1: "invertible_mat (matrix_A signs1 subsets1)"
assumes invertibleMtx2: "invertible_mat (matrix_A signs2 subsets2)"
shows "satisfy_equation p (qs1@qs2) (subsets_smash (length qs1) subsets1 subsets2) (signs_smash signs1 signs2)
∧ invertible_mat (matrix_A (signs_smash signs1 signs2) (subsets_smash (length qs1) subsets1 subsets2))"
proof -
have h1: "invertible_mat (matrix_A (signs_smash signs1 signs2) (subsets_smash (length qs1) subsets1 subsets2))"
using matrix_construction_is_kronecker_product
kronecker_invertible invertibleMtx1 invertibleMtx2
welldefined_subsets1 welldefined_subsets2 unfolding all_list_constr_def list_constr_def
by (smt (verit) Ball_set member_def well_def_signs_def welldefined_signs1)
have h2a: "distinct (signs_smash signs1 signs2)"
using distinct_signs1 distinct_signs2 welldefined_signs1 welldefined_signs2 nontriv1 nontriv2
distinct_step by auto
have h2ba: "∀ q. List.member (qs1 @ qs2) q ⟶ (List.member qs1 q ∨ List.member qs2 q)"
unfolding member_def
by auto
have h2b: "∀q. ((List.member (qs1@qs2) q) ⟶ (coprime p q))"
using h2ba pairwise_rel_prime1 pairwise_rel_prime2 by auto
have h2c: "all_list_constr ((subsets_smash (length qs1) subsets1 subsets2)) (length (qs1@qs2))"
using well_def_step
welldefined_subsets1 welldefined_subsets2
by blast
have h2d: "set (characterize_consistent_signs_at_roots_copr p (qs1@qs2)) ⊆ set(signs_smash signs1 signs2)"
using subset_step all_info1 all_info2
by simp
have h2: "satisfy_equation p (qs1@qs2) (subsets_smash (length qs1) subsets1 subsets2) (signs_smash signs1 signs2)"
using matrix_equation[where p="p", where qs="qs1@qs2", where subsets = "subsets_smash (length qs1) subsets1 subsets2",
where signs = "signs_smash signs1 signs2"]
h2a h2b h2c h2d apply (auto) using nonzero by blast
show ?thesis using h1 h2 by blast
qed
section "Reduction Step Proofs"
definition get_matrix:: "(rat mat × (nat list list × rat list list)) ⇒ rat mat"
where "get_matrix data = fst(data)"
definition get_subsets:: "(rat mat × (nat list list × rat list list)) ⇒ nat list list"
where "get_subsets data = fst(snd(data))"
definition get_signs:: "(rat mat × (nat list list × rat list list)) ⇒ rat list list"
where "get_signs data = snd(snd(data))"
definition reduction_signs:: "real poly ⇒ real poly list ⇒ rat list list ⇒ nat list list ⇒ rat mat ⇒ rat list list"
where "reduction_signs p qs signs subsets matr =
(take_indices signs (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets matr)))"
definition reduction_subsets:: "real poly ⇒ real poly list ⇒ rat list list ⇒ nat list list ⇒ rat mat ⇒ nat list list"
where "reduction_subsets p qs signs subsets matr =
(take_indices subsets (rows_to_keep (reduce_mat_cols matr (solve_for_lhs p qs subsets matr))))"
lemma reduction_signs_is_get_signs: "reduction_signs p qs signs subsets m = get_signs (reduce_system p (qs, (m, (subsets, signs))))"
unfolding reduction_signs_def get_signs_def
by (metis reduce_system.simps reduction_step.elims snd_conv)
lemma reduction_subsets_is_get_subsets: "reduction_subsets p qs signs subsets m = get_subsets (reduce_system p (qs, (m, (subsets, signs))))"
unfolding reduction_subsets_def get_subsets_def
by (metis fst_conv reduce_system.simps reduction_step.elims snd_conv)
lemma find_zeros_from_vec_prop:
fixes input_vec :: "rat vec"
shows "∀n < (dim_vec input_vec). ((input_vec $ n ≠ 0) ⟷
List.member (find_nonzeros_from_input_vec input_vec) n)"
proof -
have h1: "∀n < (dim_vec input_vec). ((input_vec $ n ≠ 0) ⟶ List.member (find_nonzeros_from_input_vec input_vec) n)"
unfolding find_nonzeros_from_input_vec_def List.member_def by auto
have h2: "∀n < (dim_vec input_vec). (List.member (find_nonzeros_from_input_vec input_vec) n ⟶ (input_vec $ n ≠ 0) )"
unfolding find_nonzeros_from_input_vec_def List.member_def by auto
show ?thesis using h1 h2 by auto
qed
subsection "Showing sign conditions preserved when reducing"
lemma take_indices_lem:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes arb_list :: "'a list list"
fixes index_list :: "nat list"
fixes n:: "nat"
assumes lest: "n < length (take_indices arb_list index_list)"
assumes well_def: "∀q.(List.member index_list q ⟶ q < length arb_list)"
shows "∃k<length arb_list.
(take_indices arb_list index_list) ! n = arb_list ! k"
using lest well_def unfolding take_indices_def apply (auto)
by (metis in_set_member nth_mem)
lemma invertible_means_mult_id:
fixes A:: "'a::field mat"
assumes assm: "invertible_mat A"
shows "matr_option (dim_row A)
(mat_inverse (A))*A = 1⇩m (dim_row A)"
proof (cases "mat_inverse(A)")
obtain n where n: "A ∈ carrier_mat n n"
using assms invertible_mat_def square_mat.simps by blast
case None
then have "A ∉ Units (ring_mat TYPE('a) n n)"
by (simp add: mat_inverse(1) n)
thus ?thesis
by (meson assms det_non_zero_imp_unit invertible_Units n unit_imp_det_non_zero)
next
case (Some a)
then show ?thesis
by (metis assms carrier_matI invertible_mat_def mat_inverse(2) matr_option.simps(2) square_mat.elims(2))
qed
lemma dim_invertible:
fixes A:: "'a::field mat"
fixes n:: "nat"
assumes assm: "invertible_mat A"
assumes dim: "A ∈ carrier_mat n n"
shows "matr_option (dim_row A)
(mat_inverse (A)) ∈ carrier_mat n n"
proof (cases "mat_inverse(A)")
obtain n where n: "A ∈ carrier_mat n n"
using assms invertible_mat_def square_mat.simps by blast
case None
then have "A ∉ Units (ring_mat TYPE('a) n n)"
by (simp add: mat_inverse(1) n)
thus ?thesis
by (meson assms det_non_zero_imp_unit invertible_Units n unit_imp_det_non_zero)
next
case (Some a)
then show ?thesis
using dim mat_inverse(2) by auto
qed
lemma mult_assoc:
fixes A B:: "rat mat"
fixes v:: "rat vec"
fixes n:: "nat"
assumes "A ∈ carrier_mat n n"
assumes "B ∈ carrier_mat n n"
assumes "dim_vec v = n"
shows "A *⇩v (mult_mat_vec B v) = (A*B)*⇩v v"
using assms(1) assms(2) assms(3) by auto
lemma size_of_mat:
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
shows "(matrix_A signs subsets) ∈ carrier_mat (length subsets) (length signs)"
unfolding matrix_A_def carrier_mat_def by auto
lemma size_of_lhs:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes signs :: "rat list list"
shows "dim_vec (construct_lhs_vector p qs signs) = length signs"
unfolding construct_lhs_vector_def
by simp
lemma size_of_rhs:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
shows "dim_vec (construct_rhs_vector p qs subsets) = length subsets"
unfolding construct_rhs_vector_def
by simp
lemma same_size:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes invertible_mat: "invertible_mat (matrix_A signs subsets)"
shows "length subsets = length signs"
using invertible_mat unfolding invertible_mat_def
using size_of_mat[of signs subsets] size_of_lhs[of p qs signs] size_of_rhs[of p qs subsets]
by simp
lemma mat_equal_list_lem:
fixes A:: "'a::field mat"
fixes B:: "'a::field mat"
shows "(dim_row A = dim_row B ∧ dim_col A = dim_col B ∧ mat_to_list A = mat_to_list B)
⟹ A = B"
proof -
assume hyp: "dim_row A = dim_row B ∧ dim_col A = dim_col B ∧ mat_to_list A = mat_to_list B"
then have "⋀i j. i < dim_row A ⟹ j < dim_col A ⟹ B $$ (i, j) = A $$ (i, j)"
unfolding mat_to_list_def by auto
then show ?thesis using hyp
unfolding mat_to_list_def
using eq_matI[of A B]
by metis
qed
lemma mat_inverse_same: "mat_inverse_var A = mat_inverse A"
unfolding mat_inverse_var_def mat_inverse_def mat_equal_def
by (smt (verit) mat_equal_list_lem split_cong)
lemma construct_lhs_matches_solve_for_lhs:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes match: "satisfy_equation p qs subsets signs"
assumes invertible_mat: "invertible_mat (matrix_A signs subsets)"
shows "(construct_lhs_vector p qs signs) = solve_for_lhs p qs subsets (matrix_A signs subsets)"
by (smt (verit) carrier_vec_dim_vec dim_invertible dim_row_matrix_A invertible_mat invertible_means_mult_id mat_inverse_same match mult_assoc one_mult_mat_vec same_size satisfy_equation_def size_of_lhs size_of_mat solve_for_lhs_def)
lemma reduction_signs_set_helper_lemma:
fixes A:: "rat list set"
fixes C:: "rat vec"
fixes B:: "rat list list"
assumes "dim_vec C = length B"
assumes sub: "A ⊆ set(B)"
assumes not_in_hyp: "∀ n < dim_vec C. C $ n = 0 ⟶ (nth B n) ∉ A"
shows "A ⊆ set (take_indices B
(find_nonzeros_from_input_vec C))"
proof -
have unfold: "⋀ x. (x ∈ A ⟹ x ∈ set (take_indices B
(find_nonzeros_from_input_vec C)))"
proof -
fix x
assume in_a: "x ∈ A"
have "x ∈ set (B)"
using sub in_a by blast
then have "∃ n < length B. nth B n = x"
by (simp add: in_set_conv_nth)
then have "∃ n < length B. (nth B n = x ∧ (List.member (find_nonzeros_from_input_vec C) n) = True)"
using not_in_hyp find_zeros_from_vec_prop[of C]
using assms(1) in_a by auto
thus "x ∈ set (take_indices B
(find_nonzeros_from_input_vec C))"
unfolding take_indices_def
using member_def by fastforce
qed
then show ?thesis
by blast
qed
lemma reduction_signs_set_helper_lemma2:
fixes A:: "rat list set"
fixes C:: "rat vec"
fixes B:: "rat list list"
assumes dist: "distinct B"
assumes eq_len: "dim_vec C = length B"
assumes sub: "A ⊆ set(B)"
assumes not_in_hyp: "∀ n < dim_vec C. C $ n ≠ 0 ⟶ (nth B n) ∈ A"
shows "set (take_indices B
(find_nonzeros_from_input_vec C)) ⊆ A"
proof -
have unfold: "⋀ x. (x ∈ (set (take_indices B
(find_nonzeros_from_input_vec C))) ⟹ x ∈ A)"
proof -
fix x
assume in_set: "x ∈ set (take_indices B (find_nonzeros_from_input_vec C))"
have h: "∃n< dim_vec C. (C $ n ≠ 0 ∧ (nth B n) = x)"
proof -
have h1: "∃n < length B.(nth B n) = x"
using in_set unfolding take_indices_def
find_nonzeros_from_input_vec_def eq_len by auto
have h2: "∀n< length B. (nth B n = x ⟶ List.member (find_nonzeros_from_input_vec C) n)"
proof clarsimp
fix n
assume leq_hyp: "n < length B"
assume x_eq: "x = B ! n"
have h: "(B !n) ∈ set (map ((!) B) (find_nonzeros_from_input_vec C))"
using x_eq in_set
by (simp add: take_indices_def)
then have h2: "List.member (map ((!) B) (find_nonzeros_from_input_vec C)) (B ! n)"
using in_set
by (meson in_set_member)
then have h3: "∃k< length B. (List.member (find_nonzeros_from_input_vec C) k ∧ ((B ! k) = (B ! n)))"
by (smt (verit) atLeastLessThan_iff eq_len find_nonzeros_from_input_vec_def imageE in_set_member mem_Collect_eq set_filter set_map set_upt)
have h4: "∀v< length B. ((B ! v) = (B ! n) ⟶ v = n)"
using dist by (metis find_first_unique leq_hyp)
then show "List.member (find_nonzeros_from_input_vec C) n"
using h2 h3 h4 by auto
qed
then have "∀n<length B. (nth B n = x ⟶ C $ n ≠ 0)"
using find_zeros_from_vec_prop [of C]
by (simp add: eq_len)
then show ?thesis using h1 eq_len
by auto
qed
thus "x ∈ A" using not_in_hyp
by blast
qed
then show ?thesis
by blast
qed
lemma reduction_doesnt_break_things_signs:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes nonzero: "p ≠ 0"
assumes welldefined_signs1: "well_def_signs (length qs) signs"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
assumes invertible_mat: "invertible_mat (matrix_A signs subsets)"
shows "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(reduction_signs p qs signs subsets (matrix_A signs subsets))"
proof -
have dim_hyp2: "matr_option (dim_row (matrix_A signs subsets))
(mat_inverse (matrix_A signs subsets)) ∈ carrier_mat (length signs) (length signs)"
using invertible_mat dim_invertible
using same_size by fastforce
have "(construct_lhs_vector p qs signs) = solve_for_lhs p qs subsets (matrix_A signs subsets)"
using construct_lhs_matches_solve_for_lhs assms by auto
then have "(solve_for_lhs p qs subsets (matrix_A signs subsets)) =
vec_of_list (map rat_of_nat (map (λs. card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}) signs))"
using construct_lhs_vector_cleaner assms
by (metis (mono_tags, lifting) list.map_cong map_map o_apply of_int_of_nat_eq)
then have "∀ n < (dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))).
(((solve_for_lhs p qs subsets (matrix_A signs subsets)) $ n = 0) ⟶
(nth signs n) ∉ set (characterize_consistent_signs_at_roots_copr p qs))"
proof -
have h0: "∀ n < (dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))).
(((solve_for_lhs p qs subsets (matrix_A signs subsets)) $ n = 0) ⟶
rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = (nth signs n)}) = 0)"
by (metis (mono_tags, lifting) ‹construct_lhs_vector p qs signs = solve_for_lhs p qs subsets (matrix_A signs subsets)› construct_lhs_vector_clean nonzero of_nat_0_eq_iff of_rat_of_nat_eq size_of_lhs)
have h1: "∀ w. (rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}) = 0 ⟶
(∄ x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w))"
proof clarsimp
fix x
assume card_asm: "card {xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = consistent_sign_vec_copr qs x} = 0"
assume zero_asm: "poly p x = 0"
have card_hyp: "{xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = consistent_sign_vec_copr qs x} = {}"
using card_eq_0_iff
using card_asm nonzero poly_roots_finite by fastforce
have "x ∈ {xa. poly p xa = 0 ∧ consistent_sign_vec_copr qs xa = consistent_sign_vec_copr qs x}"
using zero_asm by auto
thus "False" using card_hyp
by blast
qed
have h2: "⋀ w. (rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}) = 0 ⟹
(¬List.member (characterize_consistent_signs_at_roots_copr p qs) w))"
by (smt (verit, best) characterize_consistent_signs_at_roots_copr_def characterize_root_list_p_def h1 imageE in_set_member mem_Collect_eq nonzero poly_roots_finite set_map set_remdups sorted_list_of_set(1))
then have h3: "∀ w. rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}) = 0 ⟶
w ∉ set (characterize_consistent_signs_at_roots_copr p qs)"
by (simp add: in_set_member)
show ?thesis using h0 h3
by blast
qed
then have "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set (take_indices signs
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))"
using all_info
reduction_signs_set_helper_lemma[where A = "set (characterize_consistent_signs_at_roots_copr p qs)", where B = "signs",
where C = "(solve_for_lhs p qs subsets (matrix_A signs subsets))"]
using dim_hyp2 solve_for_lhs_def by (simp add: mat_inverse_same)
then show ?thesis unfolding reduction_signs_def by auto
qed
lemma reduction_deletes_bad_sign_conds:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes nonzero: "p ≠ 0"
assumes welldefined_signs1: "well_def_signs (length qs) signs"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
assumes invertible_mat: "invertible_mat (matrix_A signs subsets)"
shows "set (characterize_consistent_signs_at_roots_copr p qs) = set(reduction_signs p qs signs subsets (matrix_A signs subsets))"
proof -
have dim_hyp2: "matr_option (dim_row (matrix_A signs subsets))
(mat_inverse (matrix_A signs subsets)) ∈ carrier_mat (length signs) (length signs)"
using invertible_mat dim_invertible
using same_size by fastforce
have supset: "set (characterize_consistent_signs_at_roots_copr p qs) ⊇ set(reduction_signs p qs signs subsets (matrix_A signs subsets))"
proof -
have "(construct_lhs_vector p qs signs) = solve_for_lhs p qs subsets (matrix_A signs subsets)"
using construct_lhs_matches_solve_for_lhs assms by auto
then have "(solve_for_lhs p qs subsets (matrix_A signs subsets)) =
vec_of_list (map rat_of_nat (map (λs. card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}) signs))"
using construct_lhs_vector_cleaner assms
by (metis (mono_tags, lifting) list.map_cong map_map o_apply of_int_of_nat_eq)
then have "∀ n < (dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))).
(((solve_for_lhs p qs subsets (matrix_A signs subsets)) $ n ≠ 0) ⟶
(nth signs n) ∈ set (characterize_consistent_signs_at_roots_copr p qs))"
proof -
have h0: "∀ n < (dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))).
(((solve_for_lhs p qs subsets (matrix_A signs subsets)) $ n = 0) ⟶
rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = (nth signs n)}) = 0)"
by (metis (mono_tags, lifting) ‹construct_lhs_vector p qs signs = solve_for_lhs p qs subsets (matrix_A signs subsets)› construct_lhs_vector_clean nonzero of_nat_0_eq_iff of_rat_of_nat_eq size_of_lhs)
have h1: "∀ w. (rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}) ≠ 0 ⟶
(∃ x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w))"
proof clarsimp
fix w
assume card_asm: "0 < card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}"
show "∃x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w"
by (metis (mono_tags, lifting) Collect_empty_eq card_asm card_eq_0_iff gr_implies_not0)
qed
have h2: "⋀ w. (rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}) ≠ 0 ⟹
(List.member (characterize_consistent_signs_at_roots_copr p qs) w))"
proof clarsimp
fix w
assume card_asm: " 0 < card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}"
have h0: "∃x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w"
using card_asm
by (simp add: h1)
then show "List.member (characterize_consistent_signs_at_roots_copr p qs) w"
unfolding characterize_consistent_signs_at_roots_copr_def
using in_set_member nonzero poly_roots_finite characterize_root_list_p_def by fastforce
qed
then have h3: "∀ w. rat_of_nat (card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = w}) ≠ 0 ⟶
w ∈ set (characterize_consistent_signs_at_roots_copr p qs)"
by (simp add: in_set_member)
show ?thesis using h0 h3
by (metis (no_types, lifting) ‹solve_for_lhs p qs subsets (matrix_A signs subsets) = vec_of_list (map rat_of_nat (map (λs. card {x. poly p x = 0 ∧ consistent_sign_vec_copr qs x = s}) signs))› dim_vec_of_list length_map nth_map vec_of_list_index)
qed
then have "set (take_indices signs
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))) ⊆
set (characterize_consistent_signs_at_roots_copr p qs)"
using all_info
reduction_signs_set_helper_lemma2[where A = "set (characterize_consistent_signs_at_roots_copr p qs)", where B = "signs",
where C = "(solve_for_lhs p qs subsets (matrix_A signs subsets))"]
using distinct_signs dim_hyp2 solve_for_lhs_def
by (simp add: mat_inverse_same)
then show ?thesis unfolding reduction_signs_def by auto
qed
have subset: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(reduction_signs p qs signs subsets (matrix_A signs subsets))"
using reduction_doesnt_break_things_signs[of p qs signs subsets] assms
by blast
then show ?thesis using supset subset by auto
qed
theorem reduce_system_sign_conditions:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes nonzero: "p ≠ 0"
assumes welldefined_signs1: "well_def_signs (length qs) signs"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
assumes invertible_mat: "invertible_mat (matrix_A signs subsets)"
shows "set (get_signs (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs))))) = set (characterize_consistent_signs_at_roots_copr p qs)"
unfolding get_signs_def
using reduction_deletes_bad_sign_conds[of p qs signs subsets] apply (auto)
apply (simp add: all_info distinct_signs match nonzero reduction_signs_def welldefined_signs1)
using nonzero invertible_mat apply (metis snd_conv)
by (metis all_info distinct_signs invertible_mat match nonzero reduction_signs_def snd_conv welldefined_signs1)
subsection "Showing matrix equation preserved when reducing"
lemma rows_to_keep_lem:
fixes A:: "('a::field) mat"
shows "⋀ell. ell ∈ set (rows_to_keep A) ⟹ ell < dim_row A"
unfolding rows_to_keep_def
apply auto
using rref_pivot_positions
by (metis carrier_mat_triv gauss_jordan_single(2) gauss_jordan_single(3) index_transpose_mat(3))
lemma reduce_system_matrix_equation_preserved:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes nonzero: "p ≠ 0"
assumes welldefined_signs: "well_def_signs (length qs) signs"
assumes welldefined_subsets: "all_list_constr (subsets) (length qs)"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
assumes invertible_mat: "invertible_mat (matrix_A signs subsets)"
assumes pairwise_rel_prime: "∀q. ((List.member qs q) ⟶ (coprime p q))"
shows "satisfy_equation p qs (get_subsets (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))
(get_signs (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))"
proof -
have poly_type_hyp: "p ≠ 0" using nonzero by auto
have distinct_signs_hyp: "distinct (snd (snd (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs))))))"
proof -
let ?sym = "(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))"
have h1: "∀ i < length (take_indices signs ?sym). ∀j < length(take_indices signs ?sym).
i ≠ j ⟶ nth (take_indices signs ?sym) i ≠ nth (take_indices signs ?sym) j"
using distinct_signs unfolding take_indices_def
proof clarsimp
fix i
fix j
assume "distinct signs"
assume "i < length
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))"
assume "j < length
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))"
assume neq_hyp: "i ≠ j"
assume "signs ! (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets
(matrix_A signs subsets)) ! i) =
signs ! (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets
(matrix_A signs subsets)) ! j)"
have h1: "find_nonzeros_from_input_vec (solve_for_lhs p qs subsets
(matrix_A signs subsets)) ! i ≠ find_nonzeros_from_input_vec (solve_for_lhs p qs subsets
(matrix_A signs subsets)) ! j"
unfolding find_nonzeros_from_input_vec_def using neq_hyp
by (metis ‹i < length (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))› ‹j < length (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))› distinct_conv_nth distinct_filter distinct_upt find_nonzeros_from_input_vec_def)
then show "False" using distinct_signs
proof -
have f1: "∀p ns n. ((n::nat) ∈ {n ∈ set ns. p n}) = (n ∈ set ns ∧ n ∈ Collect p)"
by simp
then have f2: "filter (λn. solve_for_lhs p qs subsets (matrix_A signs subsets) $ n ≠ 0) [0..<dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))] ! i ∈ set [0..<length signs]"
by (metis (full_types) ‹i < length (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))› construct_lhs_matches_solve_for_lhs find_nonzeros_from_input_vec_def invertible_mat match nth_mem set_filter size_of_lhs)
have "filter (λn. solve_for_lhs p qs subsets (matrix_A signs subsets) $ n ≠ 0) [0..<dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))] ! j ∈ set [0..<length signs]"
using f1 by (metis (full_types) ‹j < length (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))› construct_lhs_matches_solve_for_lhs find_nonzeros_from_input_vec_def invertible_mat match nth_mem set_filter size_of_lhs)
then show ?thesis
using f2 by (metis ‹signs ! (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)) ! i) = signs ! (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)) ! j)› atLeastLessThan_iff distinct_conv_nth distinct_signs find_nonzeros_from_input_vec_def h1 set_upt)
qed
qed
then have "distinct (take_indices signs (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))"
using distinct_conv_nth by blast
then show ?thesis
using get_signs_def reduction_signs_def reduction_signs_is_get_signs by auto
qed
have all_info_hyp: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(snd (snd (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs))))))"
using reduce_system_sign_conditions assms unfolding get_signs_def by auto
have pairwise_rel_prime_hyp: "∀q. ((List.member qs q) ⟶ (coprime p q))"
using pairwise_rel_prime by auto
have welldefined_hyp: "all_list_constr (fst (snd (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))) (length qs)"
using welldefined_subsets rows_to_keep_lem
unfolding all_list_constr_def List.member_def list_constr_def list_all_def
apply (auto simp add: Let_def take_indices_def take_cols_from_matrix_def)
using nth_mem by fastforce
then show ?thesis using poly_type_hyp distinct_signs_hyp all_info_hyp pairwise_rel_prime_hyp welldefined_hyp
using matrix_equation unfolding get_subsets_def get_signs_def
by blast
qed
subsection "Showing matrix preserved"
lemma reduce_system_matrix_signs_helper_aux:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
fixes S:: "nat list"
assumes well_def_h: "∀x. List.member S x ⟶ x < length signs"
assumes nonzero: "p ≠ 0"
shows "alt_matrix_A (take_indices signs S) subsets = take_cols_from_matrix (alt_matrix_A signs subsets) S"
proof -
have h0a: "dim_col (take_cols_from_matrix (alt_matrix_A signs subsets) S) = length (take_indices signs S)"
unfolding take_cols_from_matrix_def apply (auto) unfolding take_indices_def by auto
have h0: "∀i < length (take_indices signs S). (col (alt_matrix_A (take_indices signs S) subsets ) i =
col (take_cols_from_matrix (alt_matrix_A signs subsets) S) i)"
proof clarsimp
fix i
assume asm: "i < length (take_indices signs S)"
have i_lt: "i < length (map ((!) (cols (alt_matrix_A signs subsets))) S)" using asm
apply (auto) unfolding take_indices_def by auto
have h0: " vec (length subsets) (λj. z (subsets ! j) (map ((!) signs) S ! i)) =
vec (length subsets) (λj. z (subsets ! j) (signs ! (S ! i)))" using nth_map
by (metis ‹i < length (take_indices signs S)› length_map take_indices_def)
have dim: "(map ((!) (cols (alt_matrix_A signs subsets))) S) ! i ∈ carrier_vec (dim_row (alt_matrix_A signs subsets))"
proof -
have "dim_col (alt_matrix_A signs subsets) = length (signs)"
by (simp add: alt_matrix_A_def)
have well_d: "S ! i < length (signs)" using well_def_h
using i_lt in_set_member by fastforce
have
map_eq: "(map ((!) (cols (alt_matrix_A signs subsets))) S) ! i = nth (cols (alt_matrix_A signs subsets)) (S ! i)"
using i_lt by auto
have "nth (cols (alt_matrix_A signs subsets)) (S ! i) ∈ carrier_vec (dim_row (alt_matrix_A signs subsets))"
using col_dim unfolding cols_def using nth_map well_d
by (simp add: ‹dim_col (alt_matrix_A signs subsets) = length signs›)
then show ?thesis using map_eq unfolding alt_matrix_A_def by auto
qed
have h1: "col (take_cols_from_matrix (alt_matrix_A signs subsets) S) i =
col (mat_of_cols (dim_row (alt_matrix_A signs subsets)) (map ((!) (cols (alt_matrix_A signs subsets))) S)) i "
by (simp add: take_cols_from_matrix_def take_indices_def)
have h2: "col (mat_of_cols (dim_row (alt_matrix_A signs subsets)) (map ((!) (cols (alt_matrix_A signs subsets))) S)) i
= nth (map ((!) (cols (alt_matrix_A signs subsets))) S) i "
using dim i_lt asm col_mat_of_cols[where j = "i", where n = "(dim_row (alt_matrix_A signs subsets))",
where vs = "(map ((!) (cols (alt_matrix_A signs subsets))) S)"]
by blast
have h3: "col (take_cols_from_matrix (alt_matrix_A signs subsets) S) i = (col (alt_matrix_A signs subsets) (S !i))"
using h1 h2 apply (auto)
by (metis alt_matrix_char asm cols_nth dim_col_mat(1) in_set_member length_map mat_of_rows_list_def matrix_A_def nth_map nth_mem take_indices_def well_def_h)
have "vec (length subsets) (λj. z (subsets ! j) (signs ! (S ! i))) = (col (alt_matrix_A signs subsets) (S !i))"
by (metis asm in_set_member length_map nth_mem signs_are_cols take_indices_def well_def_h)
then have "vec (length subsets) (λj. z (subsets ! j) (take_indices signs S ! i)) =
col (take_cols_from_matrix (alt_matrix_A signs subsets) S) i "
using h0 h3
by (simp add: take_indices_def)
then show "col (alt_matrix_A (take_indices signs S) subsets) i =
col (take_cols_from_matrix (alt_matrix_A signs subsets) S) i "
using asm signs_are_cols[where signs = "(take_indices signs S)", where subsets = "subsets"]
by auto
qed
then show ?thesis unfolding alt_matrix_A_def take_cols_from_matrix_def apply (auto)
using h0a mat_col_eqI
by (metis alt_matrix_A_def dim_col_mat(1) dim_row_mat(1) h0 mat_of_cols_def take_cols_from_matrix_def)
qed
lemma reduce_system_matrix_signs_helper:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
fixes S:: "nat list"
assumes well_def_h: "∀x. List.member S x ⟶ x < length signs"
assumes nonzero: "p ≠ 0"
shows "matrix_A (take_indices signs S) subsets = take_cols_from_matrix (matrix_A signs subsets) S"
using reduce_system_matrix_signs_helper_aux alt_matrix_char assms by auto
lemma reduce_system_matrix_subsets_helper_aux:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
fixes S:: "nat list"
assumes inv: "length subsets ≥ length signs"
assumes well_def_h: "∀x. List.member S x ⟶ x < length subsets"
assumes nonzero: "p ≠ 0"
shows "alt_matrix_A signs (take_indices subsets S) = take_rows_from_matrix (alt_matrix_A signs subsets) S"
proof -
have h0a: "dim_row (take_rows_from_matrix (alt_matrix_A signs subsets) S) = length (take_indices subsets S)"
unfolding take_rows_from_matrix_def apply (auto) unfolding take_indices_def by auto
have h0: "∀i < length (take_indices subsets S). (row (alt_matrix_A signs (take_indices subsets S) ) i =
row (take_rows_from_matrix (alt_matrix_A signs subsets) S) i)"
proof clarsimp
fix i
assume asm: "i < length (take_indices subsets S)"
have i_lt: "i < length (map ((!) (rows (alt_matrix_A signs subsets))) S)" using asm
apply (auto) unfolding take_indices_def by auto
have h0: "row (take_rows_from_matrix (alt_matrix_A signs subsets) S) i =
row (mat_of_rows (dim_col (alt_matrix_A signs subsets)) (map ((!) (rows (alt_matrix_A signs subsets))) S)) i "
unfolding take_rows_from_matrix_def take_indices_def by auto
have dim: "(map ((!) (rows (alt_matrix_A signs subsets))) S) ! i ∈ carrier_vec (dim_col (alt_matrix_A signs subsets))"
proof -
have "dim_col (alt_matrix_A signs subsets) = length (signs)"
by (simp add: alt_matrix_A_def)
then have lenh: "dim_col (alt_matrix_A signs subsets) ≤ length (subsets)"
using assms
by auto
have well_d: "S ! i < length (subsets)" using well_def_h
using i_lt in_set_member by fastforce
have
map_eq: "(map ((!) (rows (alt_matrix_A signs subsets))) S) ! i = nth (rows (alt_matrix_A signs subsets)) (S ! i)"
using i_lt by auto
have "nth (rows (alt_matrix_A signs subsets)) (S ! i) ∈ carrier_vec (dim_col (alt_matrix_A signs subsets))"
using col_dim unfolding rows_def using nth_map well_d
using lenh
by (simp add: alt_matrix_A_def)
then show ?thesis using map_eq unfolding alt_matrix_A_def by auto
qed
have h1: " row (mat_of_rows (dim_col (alt_matrix_A signs subsets)) (map ((!) (rows (alt_matrix_A signs subsets))) S)) i
= (row (alt_matrix_A signs subsets) (S ! i)) "
using dim i_lt mat_of_rows_row[where i = "i", where n = "(dim_col (alt_matrix_A signs subsets))",
where vs = "(map ((!) (rows (alt_matrix_A signs subsets))) S)"]
using alt_matrix_char in_set_member nth_mem well_def_h by fastforce
have "row (alt_matrix_A signs (take_indices subsets S) ) i = (row (alt_matrix_A signs subsets) (S ! i))"
using subsets_are_rows
proof -
have f1: "i < length S"
by (metis (no_types) asm length_map take_indices_def)
then have "List.member S (S ! i)"
by (meson in_set_member nth_mem)
then show ?thesis
using f1 by (simp add: ‹⋀subsets signs. ∀i<length subsets. row (alt_matrix_A signs subsets) i = vec (length signs) (λj. z (subsets ! i) (signs ! j))› take_indices_def well_def_h)
qed
then show "(row (alt_matrix_A signs (take_indices subsets S) ) i =
row (take_rows_from_matrix (alt_matrix_A signs subsets) S) i)"
using h0 h1 unfolding take_indices_def by auto
qed
then show ?thesis unfolding alt_matrix_A_def take_rows_from_matrix_def apply (auto)
using eq_rowI
by (metis alt_matrix_A_def dim_col_mat(1) dim_row_mat(1) h0 length_map mat_of_rows_def take_indices_def take_rows_from_matrix_def)
qed
lemma reduce_system_matrix_subsets_helper:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
fixes S:: "nat list"
assumes nonzero: "p ≠ 0"
assumes inv: "length subsets ≥ length signs"
assumes well_def_h: "∀x. List.member S x ⟶ x < length subsets"
shows "matrix_A signs (take_indices subsets S) = take_rows_from_matrix (matrix_A signs subsets) S"
using assms reduce_system_matrix_subsets_helper_aux alt_matrix_char
by auto
lemma reduce_system_matrix_match:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes nonzero: "p ≠ 0"
assumes welldefined_signs1: "well_def_signs (length qs) signs"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
assumes inv: "invertible_mat (matrix_A signs subsets)"
shows "matrix_A (get_signs (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))
(get_subsets (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs))))) =
(get_matrix (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))"
proof -
let ?A = "(matrix_A signs subsets)"
let ?lhs_vec = "(solve_for_lhs p qs subsets (matrix_A signs subsets))"
let ?red_mtx = "(take_rows_from_matrix (reduce_mat_cols (matrix_A signs subsets) ?lhs_vec) (rows_to_keep (reduce_mat_cols (matrix_A signs subsets) ?lhs_vec)))"
have h1: "matrix_A (get_signs (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))
(get_subsets (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))
= matrix_A (reduction_signs p qs signs subsets (matrix_A signs subsets)) (reduction_subsets p qs signs subsets (matrix_A signs subsets))"
using reduction_signs_is_get_signs reduction_subsets_is_get_subsets by auto
have h1_var: "matrix_A (get_signs (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))
(get_subsets (reduce_system p (qs, ((matrix_A signs subsets), (subsets, signs)))))
= matrix_A (take_indices signs (find_nonzeros_from_input_vec ?lhs_vec)) (take_indices subsets (rows_to_keep (reduce_mat_cols ?A ?lhs_vec)))"
using h1 reduction_signs_def reduction_subsets_def by auto
have h2: "?red_mtx = (take_rows_from_matrix (take_cols_from_matrix ?A (find_nonzeros_from_input_vec ?lhs_vec)) (rows_to_keep (take_cols_from_matrix ?A (find_nonzeros_from_input_vec ?lhs_vec))))"
by simp
have h30: "(construct_lhs_vector p qs signs) = ?lhs_vec"
using assms construct_lhs_matches_solve_for_lhs
by simp
have h3a: "∀x. List.member (find_nonzeros_from_input_vec ?lhs_vec) x ⟶x < length (signs)"
using h30 size_of_lhs unfolding find_nonzeros_from_input_vec_def apply (auto)
by (metis atLeastLessThan_iff filter_is_subset member_def set_upt subset_eq)
have h3b_a: "∀x. List.member (find_nonzeros_from_input_vec ?lhs_vec) x ⟶x < length (subsets)"
using assms h30 size_of_lhs same_size unfolding find_nonzeros_from_input_vec_def apply (auto)
by (simp add: find_nonzeros_from_input_vec_def h3a)
have h3ba: "length
(filter (λi. solve_for_lhs p qs subsets (matrix_A signs subsets) $ i ≠ 0)
[0..<length subsets])
≤ length subsets" using length_filter_le[where P = "(λi. solve_for_lhs p qs subsets (matrix_A signs subsets) $ i ≠ 0)",
where xs = "[0..<length subsets]"] length_upto by auto
have " length subsets = dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))"
using h30 inv size_of_lhs same_size[of signs subsets] apply (auto)
by metis
then have "length
(filter (λi. solve_for_lhs p qs subsets (matrix_A signs subsets) $ i ≠ 0)
[0..<dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))])
≤ length subsets" using h3ba
by auto
then have h3b: "length subsets ≥ length (take_indices signs (find_nonzeros_from_input_vec ?lhs_vec))"
unfolding take_indices_def find_nonzeros_from_input_vec_def by auto
have h3c: "∀x. List.member (rows_to_keep (reduce_mat_cols ?A ?lhs_vec)) x ⟶ x < length (subsets)"
proof clarsimp
fix x
assume x_mem: "List.member (rows_to_keep
(take_cols_from_matrix (matrix_A signs subsets)
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))) x"
obtain nn :: "rat list list ⇒ nat list ⇒ nat" where
"∀x2 x3. (∃v4. v4 ∈ set x3 ∧ ¬ v4 < length x2) = (nn x2 x3 ∈ set x3 ∧ ¬ nn x2 x3 < length x2)"
by moura
then have f4: "nn signs (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))) ∈ set (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))) ∧ ¬ nn signs (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))) < length signs ∨ matrix_A (take_indices signs (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))) subsets = take_cols_from_matrix (matrix_A signs subsets) (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))"
using h3a nonzero reduce_system_matrix_signs_helper by auto
then have "matrix_A (take_indices signs (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)))) subsets = take_cols_from_matrix (matrix_A signs subsets) (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))) ∧ x ∈ set (map snd (pivot_positions (gauss_jordan_single (take_cols_from_matrix (matrix_A signs subsets) (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))⇧T)))"
using f4
by (metis h3a in_set_member rows_to_keep_def x_mem)
thus "x < length (subsets)" using x_mem unfolding rows_to_keep_def
by (metis (no_types) dim_row_matrix_A rows_to_keep_def rows_to_keep_lem)
qed
have h3: "matrix_A (take_indices signs (find_nonzeros_from_input_vec ?lhs_vec)) (take_indices subsets (rows_to_keep (reduce_mat_cols ?A ?lhs_vec))) =
(take_rows_from_matrix (take_cols_from_matrix ?A (find_nonzeros_from_input_vec ?lhs_vec)) (rows_to_keep (take_cols_from_matrix ?A (find_nonzeros_from_input_vec ?lhs_vec))))"
using inv h3a h3b h3c reduce_system_matrix_subsets_helper reduce_system_matrix_signs_helper
assms by auto
show ?thesis using h1 h2 h3
by (metis fst_conv get_matrix_def h1_var reduce_system.simps reduction_step.simps)
qed
subsection "Showing invertibility preserved when reducing"
lemma well_def_find_zeros_from_lhs_vec:
fixes p:: "real poly"
fixes qs :: "real poly list"
fixes subsets :: "nat list list"
fixes signs :: "rat list list"
assumes len_eq: "length subsets = length signs"
assumes inv: "invertible_mat (matrix_A signs subsets)"
assumes nonzero: "p ≠ 0"
assumes welldefined_signs1: "well_def_signs (length qs) signs"
assumes distinct_signs: "distinct signs"
assumes all_info: "set (characterize_consistent_signs_at_roots_copr p