# Theory Rank_Argument_General

(* Title: Rank_Argument_General.thy
Author: Chelsea Edmonds
*)

section ‹Rank Argument - General ›
text ‹General lemmas to enable reasoning using the rank argument. This is described by Godsil
\<^cite>‹"godsilToolsLinearAlgebra"› and Bukh \<^cite>‹"bukhAlgebraicMethodsCombinatoricsa"›, both of whom
present it as a foundational technique ›
theory Rank_Argument_General imports Dual_Systems Jordan_Normal_Form.Determinant
Jordan_Normal_Form.DL_Rank Jordan_Normal_Form.Ring_Hom_Matrix BenOr_Kozen_Reif.More_Matrix
begin

subsection ‹Row/Column Operations ›
text ‹Extensions to the existing elementary operations are made to enable reasoning on multiple
operations at once, similar to mathematical literature›

"i < dim_row A ⟹ j < dim_col A ⟹ addrow a k l A $$(i,j) = (if k = i then ( a * (A$$ (l,j)) + (A $$(i,j))) else A$$ (i,j))"
"i < dim_row A ⟹ j < dim_col A ⟹ addrow a i l A $$(i,j) = (a * (A$$ (l,j)) + (A $$(i,j)))" "i < dim_row A ⟹ j < dim_col A ⟹ k ≠ i ⟹ addrow a k l A$$ (i,j) = A $$(i,j)" "dim_row (addrow a k l A) = dim_row A" "dim_col (addrow a k l A) = dim_col A" unfolding mat_addrow_def by auto text‹Function to add a column to multiple other columns › fun add_col_to_multiple :: "'a :: semiring_1 ⇒ nat list ⇒ nat ⇒ 'a mat ⇒ 'a mat" where "add_col_to_multiple a [] l A = A" | "add_col_to_multiple a (k # ks) l A = (addcol a k l (add_col_to_multiple a ks l A))" text ‹Function to add a row to multiple other rows › fun add_row_to_multiple :: "'a :: semiring_1 ⇒ nat list ⇒ nat ⇒ 'a mat ⇒ 'a mat" where "add_row_to_multiple a [] l A = A" | "add_row_to_multiple a (k # ks) l A = (addrow a k l (add_row_to_multiple a ks l A))" text ‹Function to add multiple rows to a single row › fun add_multiple_rows :: "'a :: semiring_1 ⇒ nat ⇒ nat list ⇒ 'a mat ⇒ 'a mat" where "add_multiple_rows a k [] A = A" | "add_multiple_rows a k (l # ls) A = (addrow a k l (add_multiple_rows a k ls A))" text ‹Function to add multiple columns to a single col › fun add_multiple_cols :: "'a :: semiring_1 ⇒ nat ⇒ nat list ⇒ 'a mat ⇒ 'a mat" where "add_multiple_cols a k [] A = A" | "add_multiple_cols a k (l # ls) A = (addcol a k l (add_multiple_cols a k ls A))" text ‹Basic lemmas on dimension and indexing of resulting matrix from above functions › lemma add_multiple_rows_dim [simp]: "dim_row (add_multiple_rows a k ls A) = dim_row A" "dim_col (add_multiple_rows a k ls A) = dim_col A" by (induct ls) simp_all lemma add_multiple_rows_index_unchanged [simp]: "i < dim_row A ⟹ j < dim_col A ⟹ k ≠ i ⟹ add_multiple_rows a k ls A$$ (i,j) = A $$(i,j)" by (induct ls) (simp_all) lemma add_multiple_rows_index_eq: assumes "i < dim_row A" and "j < dim_col A" and "i ∉ set ls" and "⋀ l . l ∈ set ls ⟹ l < dim_row A" shows "add_multiple_rows a i ls A$$ (i,j) = (∑l←ls. a * A $$(l,j)) + A$$(i,j)"
using assms proof (induct ls)
case Nil
then show ?case by simp
next
case (Cons aa ls)
then have ne: "i ≠ aa"
by auto
have lt: "aa < dim_row A" using assms(1)
have "(add_multiple_rows a i (aa # ls) A) $$(i, j) = (addrow a i aa (add_multiple_rows a i ls A))$$ (i, j)"
by simp
also have "... = a * add_multiple_rows a i ls A $$(aa, j) + (add_multiple_rows a i ls A)$$ (i, j)"
using assms(1) assms(2) index_mat_addrow_basic(2)[of "i" "(add_multiple_rows a i ls A)" "j" "a" "aa"]
by simp
also have "... = a * A $$(aa, j) + (add_multiple_rows a i ls A)$$ (i, j)"
using lt ne by (simp add: assms(2))
also have "... = a * A $$(aa, j) + (∑l←ls. a * A$$ (l, j)) + A $$(i, j)" using Cons.hyps assms(1) assms(2) Cons.prems(3) Cons.prems(4) by (metis (mono_tags, lifting) ab_semigroup_add_class.add_ac(1) list.set_intros(2)) finally show "(add_multiple_rows a i (aa # ls) A)$$ (i, j) =
(∑l←(aa #ls). a * A $$(l, j)) + A$$ (i, j)"
by simp
qed

assumes "i < dim_row A" and "j < dim_col A" and "i < low ∨ i ≥ up" and "up ≤ dim_row A"
shows "add_multiple_rows a i [low..<up] A $$(i,j) = (∑l=low..<up. a * A$$(l,j)) + A$$(i,j)" proof - have notin: "i ∉ set [low..<up]" using assms(3) by auto have "⋀ l . l ∈ set [low..<up] ⟹ l < dim_row A" using assms(4) by auto thus ?thesis using add_multiple_rows_index_eq[of i A j "[low..<up]"] sum_set_upt_eq_sum_list[of "λ l. a * A$$(l,j)" low up]  notin assms(1) assms(2) by simp
qed

"dim_row (add_multiple_cols a k ls A) = dim_row A"
"dim_col (add_multiple_cols a k ls A) = dim_col A"
by (induct ls) simp_all

"i < dim_row A ⟹ j < dim_col A ⟹ k ≠ j ⟹ add_multiple_cols a k ls A $$(i,j) = A$$(i,j)"
by (induct ls) (simp_all)

assumes "i < dim_row A" and "j < dim_col A" and "j ∉ set ls" and "⋀ l . l ∈ set ls ⟹ l < dim_col A"
shows "add_multiple_cols a j ls A $$(i,j) = (∑l←ls. a * A$$(i,l)) + A$$(i,j)" using assms proof (induct ls) case Nil then show ?case by simp next case (Cons aa ls) then have ne: "j ≠ aa" by auto have lt: "aa < dim_col A" using assms by (simp add: Cons.prems(4)) have "(add_multiple_cols a j (aa # ls) A)$$ (i, j) = (addcol a j aa (add_multiple_cols a j ls A)) $$(i, j)" by simp also have "... = a * add_multiple_cols a j ls A$$ (i, aa) + (add_multiple_cols a j ls A) $$(i, j)" using assms index_mat_addcol by simp also have "... = a * A$$(i, aa) + (add_multiple_cols a j ls A) $$(i, j)" using lt ne by (simp add: assms(1)) also have "... = a * A$$(i, aa) + (∑l←ls. a * A $$(i, l)) + A$$ (i, j)"
using Cons.hyps assms(1) assms(2)  Cons.prems(3) Cons.prems(4)
finally show ?case by simp
qed

assumes "i < dim_row A" and "j < dim_col A" and "j < low ∨ j ≥ up" and "up ≤ dim_col A"
shows "add_multiple_cols a j [low..<up] A $$(i,j) = (∑l=low..<up. a * A$$(i,l)) + A$$(i,j)" proof - have notin: "j ∉ set [low..<up]" using assms(3) by auto have "⋀ l . l ∈ set [low..<up] ⟹ l < dim_col A" using assms(4) by auto thus ?thesis using add_multiple_cols_index_eq[of i A j "[low..<up]" a] sum_set_upt_eq_sum_list[of "λ l. a * A$$(i,l)" low up] notin assms(1) assms(2) by simp
qed

"dim_row (add_row_to_multiple a ks l A) = dim_row A"
"dim_col (add_row_to_multiple a ks l A) = dim_col A"
by (induct ks) simp_all

"i < dim_row A ⟹ j < dim_col A ⟹ i ∉ set ks ⟹ add_row_to_multiple a ks l A $$(i,j) = A$$(i,j)"
by (induct ks) simp_all

"i < dim_row A ⟹ j < dim_col A ⟹ i < low ⟹ i ≥ up ⟹
add_row_to_multiple a [low..<up] l A $$(i,j) = A$$(i,j)"
by simp

assumes "i < dim_row A" and "j < dim_col A" and "i ∈ set ks" and "distinct ks" and "l ∉ set ks"
and "l < dim_row A"
shows "add_row_to_multiple a ks l A $$(i,j) = (a * A$$(l, j)) + A$$(i,j)" using assms proof (induct ks) case Nil then show ?case by simp next case (Cons aa ls) then have lnotin: "l ∉ set ls" using assms by simp then show ?case proof (cases "i = aa") case True then have inotin: "i ∉ set ls" using assms using Cons.prems(4) by fastforce have "add_row_to_multiple a (aa # ls) l A$$ (i, j) =
(addrow a aa l (add_row_to_multiple a ls l A)) $$(i, j)" by simp also have "... = (a * ((add_row_to_multiple a ls l A)$$ (l,j)) +
((add_row_to_multiple a ls l A) $$(i,j)))" using True assms(1) assms(2) by auto also have "... = a* A$$ (l, j) + ((add_row_to_multiple a ls l A) $$(i,j))" using assms lnotin by simp finally have "add_row_to_multiple a (aa # ls) l A$$ (i, j) = a* A $$(l,j) + A$$ (i, j)"
using inotin assms by simp
then show ?thesis by simp
next
case False
then have iin: "i ∈ set ls" using assms
by (meson Cons.prems(3) set_ConsD)
have "add_row_to_multiple a (aa # ls) l A $$(i, j) = (addrow a aa l (add_row_to_multiple a ls l A))$$ (i, j)"
by simp
also have "... =  ((add_row_to_multiple a ls l A) $$(i,j))" using False assms by auto finally have "add_row_to_multiple a (aa # ls) l A$$ (i, j) =  a * A $$(l, j) + A$$ (i, j)"
using Cons.hyps by (metis Cons.prems(4) assms(1) assms(2) assms(6) distinct.simps(2) iin lnotin)
then show ?thesis by simp
qed
qed

assumes "i < dim_row A" and "j < dim_col A" and "i ≥ low" and "i < up"  and "l < low ∨ l ≥ up"
and "l < dim_row A"
shows "add_row_to_multiple a [low..<up] l A $$(i,j) = (a * A$$(l, j)) + A$$(i,j)" proof - have d: "distinct [low..<up]" by simp have iin: "i ∈ set [low..<up]" using assms by auto have lnin: "l ∉ set [low..<up]" using assms by auto thus ?thesis using add_row_to_multiple_index_change d iin assms by blast qed lemma add_col_to_multiple_dim [simp]: "dim_row (add_col_to_multiple a ks l A) = dim_row A" "dim_col (add_col_to_multiple a ks l A) = dim_col A" by (induct ks) simp_all lemma add_col_to_multiple_index_unchanged [simp]: "i < dim_row A ⟹ j < dim_col A ⟹ j ∉ set ks ⟹ add_col_to_multiple a ks l A$$ (i,j) = A $$(i,j)" by (induct ks) simp_all lemma add_col_to_multiple_index_unchanged_bound: "i < dim_row A ⟹ j < dim_col A ⟹ j < low ⟹ j ≥ up ⟹ add_col_to_multiple a [low..<up] l A$$ (i,j) = A $$(i,j)" by simp lemma add_col_to_multiple_index_change: assumes "i < dim_row A" and "j < dim_col A" and "j ∈ set ks" and "distinct ks" and "l ∉ set ks" and "l < dim_col A" shows "add_col_to_multiple a ks l A$$ (i,j) = (a * A$$(i, l)) + A$$(i,j)"
using assms
proof (induct ks)
case Nil
then show ?case by simp
next
case (Cons aa ls)
then have lnotin: "l ∉ set ls" using assms by simp
then show ?case
proof (cases "j = aa")
case True
then have inotin: "j ∉ set ls" using assms
using Cons.prems(4) by fastforce
have "add_col_to_multiple a (aa # ls) l A $$(i, j) = (addcol a aa l (add_col_to_multiple a ls l A))$$ (i, j)" by simp
also have "... = (a * ((add_col_to_multiple a ls l A) $$(i,l)) + ((add_col_to_multiple a ls l A)$$ (i,j)))"
using True assms(1) assms(2) by auto
also have "... = a* A $$(i, l) + ((add_col_to_multiple a ls l A)$$ (i,j))"
using assms lnotin by simp
finally have "add_col_to_multiple a (aa # ls) l A $$(i, j) = a* A$$ (i,l) + A $$(i, j)" using inotin assms by simp then show ?thesis by simp next case False then have iin: "j ∈ set ls" using assms by (meson Cons.prems(3) set_ConsD) have "add_col_to_multiple a (aa # ls) l A$$ (i, j) =
(addcol a aa l (add_col_to_multiple a ls l A)) $$(i, j)" by simp also have "... = ((add_col_to_multiple a ls l A)$$ (i,j))"
using False assms by auto
finally have "add_col_to_multiple a (aa # ls) l A $$(i, j) = a * A$$ (i, l) + A $$(i, j)" using Cons.hyps by (metis Cons.prems(4) assms(1) assms(2) assms(6) distinct.simps(2) iin lnotin) then show ?thesis by simp qed qed lemma add_col_to_multiple_index_change_bounds: assumes "i < dim_row A" and "j < dim_col A" and "j ≥ low" and "j < up" and "l < low ∨ l ≥ up" and "l < dim_col A" shows "add_col_to_multiple a [low..<up] l A$$ (i,j) = (a * A$$(i, l)) + A$$(i,j)"
proof -
have d: "distinct [low..<up]" by simp
have jin: "j ∈ set [low..<up]" using assms by auto
have lnin: "l ∉ set [low..<up]" using assms by auto
thus ?thesis
using add_col_to_multiple_index_change d jin assms by blast
qed

text ‹ Operations specifically on 1st row/column ›

assumes "i < dim_row M" and "j < dim_col M"
shows "i = 0 ⟹ (add_row_to_multiple a [1..<dim_row M] 0 M) $$(i, j) = M$$ (i, j)"
and "i ≠ 0 ⟹ (add_row_to_multiple a [1..<dim_row M] 0 M) $$(i, j) = (a * M$$(0, j)) + M$$(i,j)" using assms add_row_to_multiple_index_change_bounds[of i "M" j 1 "dim_row M" 0 "a"] by (simp,linarith) lemma add_all_cols_to_first: assumes "i < dim_row (M)" assumes "j < dim_col (M)" shows "j ≠ 0 ⟹ add_multiple_cols 1 0 [1..<dim_col M] M$$ (i, j)  = M $$(i, j)" and "j = 0 ⟹ add_multiple_cols 1 0 [1..<dim_col M] M$$ (i, j) = (∑l = 1..<dim_col M.  M $$(i,l)) + M$$(i,0)"
using assms add_multiple_cols_index_eq_bounds[of "i" "M" "j" "1" "dim_col M" "1"] assms by (simp_all)

text ‹Lemmas on the determinant of the matrix under extended row/column operations ›

"A ∈ carrier_mat n n ⟹ add_row_to_multiple a ks l A ∈ carrier_mat n n"

"A ∈ carrier_mat n n ⟹ add_col_to_multiple a ks l A ∈ carrier_mat n n"
by (metis add_col_to_multiple_dim carrier_matD(1) carrier_matD(2) carrier_matI)

"A ∈ carrier_mat n n ⟹ add_multiple_rows a k ls A ∈ carrier_mat n n"
by (metis add_multiple_rows_dim carrier_matD(1) carrier_matD(2) carrier_matI)

"A ∈ carrier_mat n n ⟹ add_multiple_cols a k ls A ∈ carrier_mat n n"
by (metis add_multiple_cols_dim carrier_matD(1) carrier_matD(2) carrier_matI)

assumes "l ∉ set ks" and "l < n" and "A ∈ carrier_mat n n"
shows "det (add_row_to_multiple a ks l A) = det A"
using assms
proof (induct ks)
case Nil
then show ?case by simp
next
case (Cons aa ks)
have ne: "aa ≠ l"
using Cons.prems(1) by auto
have "det (add_row_to_multiple a (aa # ks) l A) = det (addrow a aa l (add_row_to_multiple a ks l A))"
by simp
also have "... = det (add_row_to_multiple a ks l A)"
finally have "det (add_row_to_multiple a (aa # ks) l A) = det A"
using Cons.hyps assms by (metis Cons.prems(1) list.set_intros(2))
then show ?case by simp
qed

assumes "l ∉ set ks" and "l < n" and "A ∈ carrier_mat n n"
shows "det (add_col_to_multiple a ks l A) = det A"
using assms
proof (induct ks)
case Nil
then show ?case by simp
next
case (Cons aa ks)
have ne: "aa ≠ l"
using Cons.prems(1) by auto
have "det (add_col_to_multiple a (aa # ks) l A) = det (addcol a aa l (add_col_to_multiple a ks l A))"
by simp
also have "... = det (add_col_to_multiple a ks l A)"
finally have "det (add_col_to_multiple a (aa # ks) l A) = det A"
using Cons.hyps assms by (metis Cons.prems(1) list.set_intros(2))
then show ?case by simp
qed

assumes "k ∉ set ls" and "⋀l. l ∈ set ls ⟹ l < n" and "A ∈ carrier_mat n n"
shows "det (add_multiple_cols a k ls A) = det A"
using assms
proof (induct ls)
case Nil
then show ?case by simp
next
case (Cons aa ls)
have ne: "aa ≠ k"
using Cons.prems(1) by auto
have "det (add_multiple_cols a k (aa # ls) A) = det (addcol a k aa (add_multiple_cols a k ls A))"
by simp
also have "... = det (add_multiple_cols a k ls A)"
finally have "det (add_multiple_cols a k (aa # ls) A) = det A"
using Cons.hyps assms by (metis Cons.prems(1) Cons.prems(2) list.set_intros(2))
then show ?case by simp
qed

assumes "k ∉ set ls" and "⋀l. l ∈ set ls ⟹ l < n" and "A ∈ carrier_mat n n"
shows "det (add_multiple_rows a k ls A) = det A"
using assms
proof (induct ls)
case Nil
then show ?case by simp
next
case (Cons aa ls)
have ne: "aa ≠ k"
using Cons.prems(1) by auto
have "det (add_multiple_rows a k (aa # ls) A) = det (addrow a k aa (add_multiple_rows a k ls A))"
by simp
also have "... = det (add_multiple_rows a k ls A)"
finally have "det (add_multiple_rows a k (aa # ls) A) = det A"
using Cons.hyps assms by (metis Cons.prems(1) Cons.prems(2) list.set_intros(2))
then show ?case by simp
qed

subsection ‹Rank and Linear Independence›

abbreviation "rank v M ≡ vec_space.rank v M"

text ‹Basic lemma: the rank of the multiplication of two matrices will be less than the minimum
of the individual ranks of those matrices. This directly follows from an existing lemmas in the
linear algebra library which show independently that the resulting matrices rank is less than either
the right or left matrix rank in the product ›
lemma rank_mat_mult_lt_min_rank_factor:
fixes A :: "'a::{conjugatable_ordered_field} mat"
assumes "A ∈ carrier_mat n m"
assumes "B ∈ carrier_mat m nc"
shows "rank n (A * B) ≤ min (rank n A) (rank m B)"
proof -
have 1: "rank n (A * B) ≤ (rank n A)"
using assms(1) assms(2) vec_space.rank_mat_mul_right by blast
have "rank n (A* B) ≤ rank m B"
by (meson assms(1) assms(2) rank_mat_mul_left)
thus ?thesis using 1 by simp
qed

text ‹Rank Argument 1: Given two a $x \times y$ matrix $M$ where $MM^T$ has rank x, $x \le y$›
lemma rank_argument:
fixes M :: "('c :: {conjugatable_ordered_field}) mat"
assumes "M ∈ carrier_mat x y"
assumes "vec_space.rank x (M* M⇧T) = x"
shows "x ≤ y"
proof -
let ?B = "(M * M⇧T)"
have Mt_car: "M⇧T ∈ carrier_mat y x" using assms by simp
have b_car: "?B ∈ carrier_mat x x"
using transpose_carrier_mat assms by simp
then have "rank x ?B ≤ min (rank x M) (rank y M⇧T)"
using rank_mat_mult_lt_min_rank_factor Mt_car b_car assms(1) by blast
thus ?thesis using le_trans vec_space.rank_le_nc
by (metis assms(1) assms(2) min.bounded_iff)
qed

text ‹Generalise the rank argument to use the determinant. If the determinant of the matrix
is non-zero, than it's rank must be equal to $x$. This removes the need for someone to use
facts on rank in their proofs. ›
lemma rank_argument_det:
fixes M :: "('c :: {conjugatable_ordered_field}) mat"
assumes "M ∈ carrier_mat x y"
assumes "det (M* M⇧T) ≠ 0"
shows "x ≤ y"
proof -
let ?B = "(M * M⇧T)"
have Mt_car: "M⇧T ∈ carrier_mat y x" using assms by simp
have b_car: "?B ∈ carrier_mat x x"
using transpose_carrier_mat assms by simp
then have b_rank: "vec_space.rank x ?B = x"
using vec_space.low_rank_det_zero assms(2) by blast
then have "rank x ?B ≤ min (rank x M) (rank y M⇧T)"
using rank_mat_mult_lt_min_rank_factor Mt_car b_car assms(1) by blast
thus ?thesis using le_trans vec_space.rank_le_nc
by (metis assms(1) b_rank min.bounded_iff)
qed

end