Theory Basis_Extension

section ‹Basis Extension›

text ‹We prove that every linear indepent set/list of vectors can be extended into a basis.
  Similarly, from every set of vectors one can extract a linear independent set of vectors
  that spans the same space.›

theory Basis_Extension
  imports
    LLL_Basis_Reduction.Gram_Schmidt_2
begin


context cof_vec_space
begin

lemma lin_indpt_list_length_le_n: assumes "lin_indpt_list xs"
  shows "length xs ≤ n"
proof -
  from assms[unfolded lin_indpt_list_def]
  have xs: "set xs ⊆ carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto
  from dist have "card (set xs) = length xs" by (rule distinct_card)
  moreover have "card (set xs) ≤ n"
    using lin xs dim_is_n li_le_dim(2) by auto
  ultimately show ?thesis by auto
qed

lemma lin_indpt_list_length_eq_n: assumes "lin_indpt_list xs"
  and "length xs = n"
shows "span (set xs) = carrier_vec n" "basis (set xs)"
proof -
  from assms[unfolded lin_indpt_list_def]
  have xs: "set xs ⊆ carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto
  from dist have "card (set xs) = length xs" by (rule distinct_card)
  with assms have "card (set xs) = n" by auto
  with lin xs show "span (set xs) = carrier_vec n" "basis (set xs)"  using dim_is_n
    by (metis basis_def dim_basis dim_li_is_basis fin_dim finite_basis_exists gen_ge_dim li_le_dim(1))+
qed

lemma expand_to_basis: assumes lin: "lin_indpt_list xs"
  shows "∃ ys. set ys ⊆ set (unit_vecs n) ∧ lin_indpt_list (xs @ ys) ∧ length (xs @ ys) = n"
proof -
  define y where "y = n - length xs"
  from lin have "length xs ≤ n" by (rule lin_indpt_list_length_le_n)
  hence "length xs + y = n" unfolding y_def by auto
  thus "∃ ys. set ys ⊆ set (unit_vecs n) ∧ lin_indpt_list (xs @ ys) ∧ length (xs @ ys) = n"
    using lin
  proof (induct y arbitrary: xs)
    case (0 xs)
    thus ?case by (intro exI[of _ Nil], auto)
  next
    case (Suc y xs)
    hence "length xs < n" by auto
    from Suc(3)[unfolded lin_indpt_list_def]
    have xs: "set xs ⊆ carrier_vec n" and dist: "distinct xs" and lin: "lin_indpt (set xs)" by auto
    from distinct_card[OF dist] Suc(2) have card: "card (set xs) < n" by auto
    have "span (set xs) ≠ carrier_vec n" using card dim_is_n xs basis_def dim_basis lin by auto
    with span_closed[OF xs] have "span (set xs) ⊂ carrier_vec n" by auto
    also have "carrier_vec n = span (set (unit_vecs n))"
      unfolding span_unit_vecs_is_carrier ..
    finally have sub: "span (set xs) ⊂ span (set (unit_vecs n))" .
    have "∃ u. u ∈ set (unit_vecs n) ∧ u ∉ span (set xs)"
      using span_subsetI[OF xs, of "set (unit_vecs n)"] sub by force
    then obtain u where uu: "u ∈ set (unit_vecs n)" and usxs: "u ∉ span (set xs)" by auto
    then have u: "u ∈ carrier_vec n" unfolding unit_vecs_def by auto
    let ?xs = "xs @ [u]"
    from span_mem[OF xs, of u] usxs have uxs: "u ∉ set xs" by auto
    with dist have dist: "distinct ?xs" by auto
    have lin: "lin_indpt (set ?xs)" using lin_dep_iff_in_span[OF xs lin u uxs] usxs by auto
    from lin dist u xs have lin: "lin_indpt_list ?xs" unfolding lin_indpt_list_def by auto
    from Suc(2) have "length ?xs + y = n" by auto
    from Suc(1)[OF this lin] obtain ys where
      "set ys ⊆ set (unit_vecs n)" "lin_indpt_list (?xs @ ys)" "length (?xs @ ys) = n" by auto
    thus ?case using uu
      by (intro exI[of _ "u # ys"], auto)
  qed
qed

definition "basis_extension xs = (SOME ys.
  set ys ⊆ set (unit_vecs n) ∧ lin_indpt_list (xs @ ys) ∧ length (xs @ ys) = n)"

lemma basis_extension: assumes "lin_indpt_list xs"
  shows "set (basis_extension xs) ⊆ set (unit_vecs n)"
    "lin_indpt_list (xs @ basis_extension xs)"
    "length (xs @ basis_extension xs) = n"
  using someI_ex[OF expand_to_basis[OF assms], folded basis_extension_def] by auto

lemma exists_lin_indpt_sublist: assumes X: "X ⊆ carrier_vec n"
  shows "∃ Ls. lin_indpt_list Ls ∧ span (set Ls) = span X ∧ set Ls ⊆ X"
proof -
  let ?T = ?thesis
  have "(∃ Ls. lin_indpt_list Ls ∧ span (set Ls) ⊆ span X ∧ set Ls ⊆ X ∧ length Ls = k) ∨ ?T" for k
  proof (induct k)
    case 0
    have "lin_indpt {}" by (simp add: lindep_span)
    thus ?case using span_is_monotone by (auto simp: lin_indpt_list_def)
  next
    case (Suc k)
    show ?case
    proof (cases ?T)
      case False
      with Suc obtain Ls where lin: "lin_indpt_list Ls"
        and span: "span (set Ls) ⊆ span X" and Ls: "set Ls ⊆ X"  and len: "length Ls = k" by auto
      from Ls X have LsC: "set Ls ⊆ carrier_vec n" by auto
      show ?thesis
      proof (cases "X ⊆ span (set Ls)")
        case True
        hence "span X ⊆ span (set Ls)" using LsC X by (metis span_subsetI)
        with span have "span (set Ls) = span X" by auto
        hence ?T by (intro exI[of _ Ls] conjI True lin Ls)
        thus ?thesis by auto
      next
        case False
        with span obtain x where xX: "x ∈ X" and xSLs: "x ∉ span (set Ls)" by auto
        from Ls X have LsC: "set Ls ⊆ carrier_vec n" by auto
        from span_mem[OF this, of x] xSLs have xLs: "x ∉ set Ls" by auto
        let ?Ls = "x # Ls"
        show ?thesis
        proof (intro disjI1 exI[of _ ?Ls] conjI)
          show "length ?Ls = Suc k" using len by auto
          show "lin_indpt_list ?Ls" using lin xSLs xLs unfolding lin_indpt_list_def
            using lin_dep_iff_in_span[OF LsC _ _ xLs] xX X by auto
          show "set ?Ls ⊆ X" using xX Ls by auto
          from span_is_monotone[OF this]
          show "span (set ?Ls) ⊆ span X" .
        qed
      qed
    qed auto
  qed
  from this[of "n + 1"] lin_indpt_list_length_le_n show ?thesis by fastforce
qed

lemma exists_lin_indpt_subset: assumes "X ⊆ carrier_vec n"
  shows "∃ Ls. lin_indpt Ls ∧ span (Ls) = span X ∧ Ls ⊆ X"
proof -
  from exists_lin_indpt_sublist[OF assms]
  obtain Ls where "lin_indpt_list Ls ∧ span (set Ls) = span X ∧ set Ls ⊆ X" by auto
  thus ?thesis by (intro exI[of _ "set Ls"], auto simp: lin_indpt_list_def)
qed
end

end