# 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
have h3: "all_list_constr [[], [0]] (Suc 0)" unfolding all_list_constr_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)
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

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)
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)"
(* a slightly unorthodox use of signs_smash, but it closes the proof *)
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

(* If subsets for smaller systems are well-defined, then subsets for combined systems
are well-defined *)
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
then show ?thesis unfolding list_constr_def
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
then show ?thesis unfolding list_constr_def
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"

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

(* In this section we will show that if signs1 contains all consistent sign assignments and signs2
contains all consistent sign assignments, then their smash contains all consistent sign assignments.
Intuitively, this makes sense because signs1 and signs2 are carrying information about different
sets of polynomials, and their smash contains all possible combinations of that information.
*)
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
next
case True
moreover define j where ‹j = i - n›
ultimately have ‹i = n + j›
by simp
with Cons ‹n > 0› show ?thesis
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

(* Shows that the matrix of a smashed system is the Kronecker product of the matrices of the two
systems being combined *)
lemma matrix_construction_is_kronecker_product:
fixes qs1 :: "real poly list"
fixes subs1 subs2 :: "nat list list"
fixes signs1 signs2 :: "rat list list"
(* n1 is the number of polynomials in the "1" sets *)
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
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)
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

(* Given that two smaller systems satisfy some mild constraints, show that their combined system
(after smashing the signs and subsets) satisfies the matrix equation, and that the matrix of the
combined system is invertible. *)
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"

(* Some definitions *)
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))))"

(* Some basic lemmas *)
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)"
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)"
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)

(* If set(A) is a subset of B then for all n, nth c n = 0 means nth a n not in B  *)
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"
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
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]
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

(* Show that dropping columns doesn't affect the consistent sign assignments *)
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)"
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

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
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)"
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
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

(* Show that we are tracking the correct matrix in the algorithm *)
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)"
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 "
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
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)"
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
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)
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

(* gauss_jordan_single_rank is crucial in this section *)
subsection "Showing invertibility preserved when reducing"

(* Overall:
Input a matrix, subsets, and signs.
Drop columns of the matrix based on the 0's on the LHS---so extract a list of 0's. Reduce signs accordingly.
Then find a list of rows to delete based on using rank (use the transpose result, pivot positions!),
and delete those rows.  Reduce subsets accordingly.
End with a reduced system! *)
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 qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
shows "(⋀j. j ∈ set (find_nonzeros_from_input_vec
(solve_for_lhs p qs subsets (matrix_A signs subsets))) ⟹
j < length (cols (matrix_A signs subsets)))"
proof -
fix i
fix j
assume j_in: " j ∈ set (find_nonzeros_from_input_vec
(solve_for_lhs p qs subsets (matrix_A signs subsets))) "
let ?og_mat = "(matrix_A signs subsets)"
let ?lhs = "(solve_for_lhs p qs subsets ?og_mat)"
let ?new_mat = "(take_rows_from_matrix (reduce_mat_cols ?og_mat ?lhs) (rows_to_keep (reduce_mat_cols ?og_mat ?lhs)))"
have "square_mat (matrix_A signs subsets)" using inv
using invertible_mat_def by blast
then have mat_size: "?og_mat ∈ carrier_mat (length signs) (length signs)"
using size_of_mat
by auto
have "dim_vec (solve_for_lhs p qs subsets (matrix_A signs subsets)) = (length signs)"
using size_of_lhs construct_lhs_matches_solve_for_lhs assms
by (metis (full_types))
then have h: "j < (length signs)"
using j_in unfolding find_nonzeros_from_input_vec_def
by simp
then show "j <  length (cols (matrix_A signs subsets))"
using mat_size by auto
qed

lemma take_cols_subsets_og_cols:
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 qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
shows "set (take_indices (cols (matrix_A signs subsets))
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))
⊆ set (cols (matrix_A signs subsets))"
proof -
have well_def: "(⋀j. j ∈ set (find_nonzeros_from_input_vec
(solve_for_lhs p qs subsets (matrix_A signs subsets))) ⟹
j < length (cols (matrix_A signs subsets)))"
using assms well_def_find_zeros_from_lhs_vec by auto
have "∀x. x ∈ set (take_indices (cols (matrix_A signs subsets))
(find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))
⟶ x ∈  set (cols (matrix_A signs subsets))"
proof clarsimp
fix x
let ?og_list = "(cols (matrix_A signs subsets))"
let ?ind_list = "(find_nonzeros_from_input_vec
(solve_for_lhs p qs subsets (matrix_A signs subsets)))"
assume x_in: "x ∈ set (take_indices ?og_list ?ind_list)"
show "x ∈ set (cols (matrix_A signs subsets))"
using x_in unfolding take_indices_def using in_set_member apply (auto)
using in_set_conv_nth well_def by fastforce
qed
then show ?thesis
by blast
qed

lemma reduction_doesnt_break_things_invertibility_step1:
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 qs) ⊆ set(signs)"
assumes match: "satisfy_equation p qs subsets signs"
shows "vec_space.rank (length signs) (reduce_mat_cols (matrix_A signs subsets) (solve_for_lhs p qs subsets (matrix_A signs subsets))) =
(length (find_nonzeros_from_input_vec (solve_for_lhs p qs subsets (matrix_A signs subsets))))"
proof -
let ?og_mat = "(matrix_A signs subsets)"
let ?lhs = "(solve_for_lhs p qs subsets ?og_mat)"
let ?new_mat = "(take_rows_from_matrix (reduce_mat_cols ?og_mat ?lhs) (rows_to_keep (reduce_mat_cols ?og_mat ?lhs)))"
have "square_mat (matrix_A signs subsets)" using inv
using invertible_mat_def by blast
then have mat_size: "?og_mat ∈ carrier_mat (length signs) (length signs)"
using size_of_mat
by auto
then have mat_size_alt: "?og_mat ∈ carrier_mat (length subsets) (length subsets)"
using size_of_mat same_size assms
by auto
have det_h: "det ?og_mat ≠ 0"
using invertible_det[where A = "matrix_A signs subsets"] mat_size
using inv by blast
then have rank_h: "vec_space.rank (length signs) ?og_mat = (length signs)"
using vec_space.det_rank_iff  mat_size
by auto
then have dist_cols: "distinct (cols ?og_mat)" using mat_size vec_space.non_distinct_low_rank[where A = ?og_mat, where n = "length signs"]
by auto
have well_def: "(⋀j. j ∈ set (```