# 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```