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

(* 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
      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

(* 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
    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

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

(* 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"
      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

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

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

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

(* Overall:
  Start with a matrix equation.
  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</