Theory DL_Rank_Submatrix

(* Author: Alexander Bentkamp, Universität des Saarlandes
*)

section ‹Rank and Submatrices›

theory DL_Rank_Submatrix
imports DL_Rank DL_Submatrix Matrix
begin

lemma row_submatrix_UNIV:
assumes "i < card {i. i < dim_row A  i  I}"
shows "row (submatrix A I UNIV) i = row A (pick I i)"
proof (rule eq_vecI)
  show dim_eq:"dim_vec (row (submatrix A I UNIV) i) = dim_vec (row A (pick I i))"
    unfolding carrier_vecD[OF row_carrier] dim_submatrix by auto
  fix j assume "j < dim_vec (row A (pick I i))"
  then have "j < dim_col (submatrix A I UNIV)" "j < dim_col A" "j < card {j. j < dim_col A  j  UNIV}" using dim_eq by auto
  show "row (submatrix A I UNIV) i $ j = row A (pick I i) $ j"
    unfolding row_def index_vec[OF j < dim_col (submatrix A I UNIV)] index_vec[OF j < dim_col A]
    using submatrix_index[OF assms j < card {j. j < dim_col A  j  UNIV}] using pick_UNIV by auto
qed

lemma distinct_cols_submatrix_UNIV:
assumes "distinct (cols (submatrix A I UNIV))"
shows "distinct (cols A)"
using assms proof (rule contrapos_pp)
  assume "¬ distinct (cols A)"
  then obtain i j where "i < dim_col A" "j < dim_col A" "(cols A)!i = (cols A)!j" "ij"
    using distinct_conv_nth cols_length by metis
  have "i < dim_col (submatrix A I UNIV)" "j < dim_col (submatrix A I UNIV)"
    unfolding dim_submatrix using i < dim_col A j < dim_col Aby simp_all
  then have "i < length (cols (submatrix A I UNIV))" "j < length (cols (submatrix A I UNIV))"
    unfolding cols_length by simp_all
  have "(cols (submatrix A I UNIV))!i = (cols (submatrix A I UNIV))!j"
  proof (rule eq_vecI)
    show "dim_vec (cols (submatrix A I UNIV) ! i) = dim_vec (cols (submatrix A I UNIV) ! j)"
      by (simp add: i < dim_col (submatrix A I UNIV) j < dim_col (submatrix A I UNIV))
    fix k assume "k < dim_vec (cols (submatrix A I UNIV) ! j)"
    then have "k < dim_row (submatrix A I UNIV)"
      using j < length (cols (submatrix A I UNIV))  by auto
    then have  "k < card {j. j < dim_row A  j  I}"  using dim_submatrix(1) by metis
    have i_transfer:"cols (submatrix A I UNIV) ! i $ k = (cols A) ! i $ (pick I k)"
      unfolding cols_nth[OF i < dim_col (submatrix A I UNIV)] col_def index_vec[OF k < dim_row (submatrix A I UNIV)]
      unfolding submatrix_index[OF k < card {j. j < dim_row A  j  I} i < dim_col (submatrix A I UNIV)[unfolded dim_submatrix]]
      unfolding pick_UNIV cols_nth[OF i < dim_col A] col_def index_vec[OF pick_le[OF k < card {j. j < dim_row A  j  I}]]
      by metis
    have j_transfer:"cols (submatrix A I UNIV) ! j $ k = (cols A) ! j $ (pick I k)"
      unfolding cols_nth[OF j < dim_col (submatrix A I UNIV)] col_def index_vec[OF k < dim_row (submatrix A I UNIV)]
      unfolding submatrix_index[OF k < card {j. j < dim_row A  j  I} j < dim_col (submatrix A I UNIV)[unfolded dim_submatrix]]
      unfolding pick_UNIV cols_nth[OF j < dim_col A] col_def index_vec[OF pick_le[OF k < card {j. j < dim_row A  j  I}]]
      by metis
    show "cols (submatrix A I UNIV) ! i $ k = cols (submatrix A I UNIV) ! j $ k"
      using cols A ! i = cols A ! j i_transfer j_transfer by auto
  qed
  then show "¬ distinct (cols (submatrix A I UNIV))" unfolding distinct_conv_nth
    using i < length (cols (submatrix A I UNIV)) j < length (cols (submatrix A I UNIV)) i  j by blast
qed

lemma cols_submatrix_subset: "set (cols (submatrix A UNIV J))  set (cols A)"
proof
  fix c assume "c  set (cols (submatrix A UNIV J))"
  then obtain j where "j < length (cols (submatrix A UNIV J))" "cols (submatrix A UNIV J) ! j = c"
    by (meson in_set_conv_nth)
  then have "j < dim_col (submatrix A UNIV J)" by simp
  then have "j < card {j. j < dim_col A  j  J}" by (simp add: dim_submatrix(2))
  have "cols (submatrix A UNIV J) ! j = cols A ! (pick J j)"
    unfolding cols_nth[OF j < dim_col (submatrix A UNIV J)] cols_nth[OF pick_le[OF j < card {j. j < dim_col A  j  J}]]
  proof (rule eq_vecI)
    show "dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))" unfolding dim_col dim_submatrix by auto
    fix i assume "i < dim_vec (col A (pick J j))"
    then have "i < dim_row A" by simp
    then have "i < dim_row (submatrix A UNIV J)" using dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j)) by auto
    show "col (submatrix A UNIV J) j $ i = col A (pick J j) $ i"
      unfolding col_def index_vec[OF i < dim_row (submatrix A UNIV J)] index_vec[OF i < dim_row A]
      using submatrix_index by (metis (no_types, lifting) dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))
      i < dim_vec (col A (pick J j)) j < dim_col (submatrix A UNIV J) dim_col dim_submatrix(1) dim_submatrix(2) pick_UNIV)
  qed
  then show "c  set (cols A)"
    using cols (submatrix A UNIV J) ! j = c
    using pick_le[OF j < card {j. j < dim_col A  j  J}] by (metis cols_length nth_mem)
qed

lemma (in vec_space) lin_dep_submatrix_UNIV:
assumes "A  carrier_mat n nc"
assumes "lin_dep (set (cols A))"
assumes "distinct (cols (submatrix A I UNIV))"
shows "LinearCombinations.module.lin_dep class_ring (module_vec TYPE('a) (card {i. i < n  i  I})) (set (cols (submatrix A I UNIV)))"
  (is "LinearCombinations.module.lin_dep class_ring ?M (set ?S')")
proof -
  obtain v where 2:"v  carrier_vec nc" and 3:"v  0v nc" and "A *v v = 0v n"
    using vec_space.lin_depE[OF assms(1) assms(2) distinct_cols_submatrix_UNIV[OF assms(3)]] by auto
  have 1: "submatrix A I UNIV  carrier_mat (card {i. i < n  i  I}) nc"
    apply (rule carrier_matI) unfolding dim_submatrix using A  carrier_mat n nc by auto
  have 4:"submatrix A I UNIV *v v = 0v (card {i. i < n  i  I})"
  proof (rule eq_vecI)
    show dim_eq:"dim_vec (submatrix A I UNIV *v v) = dim_vec (0v (card {i. i < n  i  I}))" using "1" by auto
    fix i assume "i < dim_vec (0v (card {i. i < n  i  I}))"
    then have i_le:"i < card {i. i < n  i  I}" by auto
    have "(submatrix A I UNIV *v v) $ i = row (submatrix A I UNIV) i  v" using dim_eq i_le by auto
    also have "... = row A (pick I i)  v" using row_submatrix_UNIV
      by (metis (no_types, lifting)  dim_eq dim_mult_mat_vec dim_submatrix(1) i < dim_vec (0v (card {i. i < n  i  I})))
    also have "... = 0"
      using A *v v = 0v n i_le[THEN pick_le] by (metis assms(1) index_mult_mat_vec carrier_matD(1) index_zero_vec(1))
    also have "... = 0v (card {i. i < n  i  I}) $ i" by (simp add: i_le)
    finally show "(submatrix A I UNIV *v v) $ i = 0v (card {i. i < n  i  I}) $ i" by metis
  qed
  show ?thesis using vec_space.lin_depI[OF 1 2 3 4] using assms(3) by auto
qed

lemma (in vec_space) rank_gt_minor:
assumes "A  carrier_mat n nc"
assumes "det (submatrix A I J)  0"
shows "card {j. j < nc  j  J}  rank A"
proof -
  have square:"dim_row (submatrix A I J) = dim_col (submatrix A I J)"
   using det_def det (submatrix A I J)  0 by metis
  then have full_rank:"vec_space.rank (dim_row (submatrix A I J)) (submatrix A I J) = dim_row (submatrix A I J)"
   using vec_space.low_rank_det_zero assms(2) carrier_matI by auto
  then have distinct:"distinct (cols (submatrix A I J))" 
    using vec_space.non_distinct_low_rank square less_irrefl carrier_matI by metis
  then have indpt:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (dim_row (submatrix A I J))) (set (cols (submatrix A I J)))"
     using vec_space.full_rank_lin_indpt[OF _ full_rank distinct] square by fastforce

  have distinct2: "distinct (cols (submatrix (submatrix A UNIV J) I UNIV))" using submatrix_split distinct by metis
  have indpt2:"LinearCombinations.module.lin_indpt class_ring (module_vec TYPE('a) (card {i. i < n  i  I})) (set (cols (submatrix (submatrix A UNIV J) I UNIV)))"
    using submatrix_split dim_submatrix(1) indpt by (metis (full_types) assms(1) carrier_matD(1))

  have "submatrix A UNIV J  carrier_mat n (dim_col (submatrix A UNIV J))"
    apply (rule carrier_matI) unfolding dim_submatrix(1) using A  carrier_mat n nc carrier_matD by simp_all
  have "lin_indpt (set (cols (submatrix A UNIV J)))"
    using indpt2 vec_space.lin_dep_submatrix_UNIV[OF submatrix A UNIV J  carrier_mat n (dim_col (submatrix A UNIV J)) _ distinct2] by blast
  have distinct3:"distinct (cols (submatrix A UNIV J))" by (metis distinct distinct_cols_submatrix_UNIV submatrix_split)
  show ?thesis using
    rank_ge_card_indpt[OF A  carrier_mat n nc cols_submatrix_subset lin_indpt (set (cols (submatrix A UNIV J))),
    unfolded distinct_card[OF distinct3, unfolded cols_length dim_submatrix], unfolded carrier_matD(2)[OF A  carrier_mat n nc]]
    by blast
qed

end