Theory LLL_Basis_Reduction.LLL
section ‹The LLL Algorithm›
text ‹Soundness of the LLL algorithm is proven in four steps.
In the basic version, we do recompute the Gram-Schmidt ortogonal (GSO) basis
in every step. This basic version will have a full functional soundness proof,
i.e., termination and the property that the returned basis is reduced.
Then in LLL-Number-Bounds we will strengthen the invariant and prove that
all intermediate numbers stay polynomial in size.
Moreover, in LLL-Impl we will refine the basic version, so that
the GSO does not need to be recomputed in every step.
Finally, in LLL-Complexity, we develop an cost-annotated version
of the refined algorithm and prove a polynomial upper bound on the
number of arithmetic operations.›
text ‹This theory provides a basic implementation and a soundness proof of the LLL algorithm
to compute a "short" vector in a lattice.›
theory LLL
imports
Gram_Schmidt_2
Missing_Lemmas
Jordan_Normal_Form.Determinant
"Abstract-Rewriting.SN_Order_Carrier"
begin
subsection ‹Core Definitions, Invariants, and Theorems for Basic Version›
locale LLL =
fixes n :: nat
and m :: nat
and fs_init :: "int vec list"
and α :: rat
begin
sublocale vec_module "TYPE(int)" n.
abbreviation RAT where "RAT ≡ map (map_vec rat_of_int)"
abbreviation SRAT where "SRAT xs ≡ set (RAT xs)"
abbreviation Rn where "Rn ≡ carrier_vec n :: rat vec set"
sublocale gs: gram_schmidt_fs n "RAT fs_init" .
abbreviation lin_indep where "lin_indep fs ≡ gs.lin_indpt_list (RAT fs)"
abbreviation gso where "gso fs ≡ gram_schmidt_fs.gso n (RAT fs)"
abbreviation μ where "μ fs ≡ gram_schmidt_fs.μ n (RAT fs)"
abbreviation reduced where "reduced fs ≡ gram_schmidt_fs.reduced n (RAT fs) α"
abbreviation weakly_reduced where "weakly_reduced fs ≡ gram_schmidt_fs.weakly_reduced n (RAT fs) α"
text ‹lattice of initial basis›
definition "L = lattice_of fs_init"
text ‹maximum squared norm of initial basis›
definition "N = max_list (map (nat ∘ sq_norm) fs_init)"
text ‹maximum absolute value in initial basis›
definition "M = Max ({abs (fs_init ! i $ j) | i j. i < m ∧ j < n} ∪ {0})"
text ‹This is the core invariant which enables to prove functional correctness.›
definition "μ_small fs i = (∀ j < i. abs (μ fs i j) ≤ 1/2)"
definition LLL_invariant_weak :: "int vec list ⇒ bool" where
"LLL_invariant_weak fs = (
gs.lin_indpt_list (RAT fs) ∧
lattice_of fs = L ∧
length fs = m)"
lemma LLL_inv_wD: assumes "LLL_invariant_weak fs"
shows
"lin_indep fs"
"length (RAT fs) = m"
"set fs ⊆ carrier_vec n"
"⋀ i. i < m ⟹ fs ! i ∈ carrier_vec n"
"⋀ i. i < m ⟹ gso fs i ∈ carrier_vec n"
"length fs = m"
"lattice_of fs = L"
proof (atomize (full), goal_cases)
case 1
interpret gs': gram_schmidt_fs_lin_indpt n "RAT fs"
by (standard) (use assms LLL_invariant_weak_def gs.lin_indpt_list_def in auto)
show ?case
using assms gs'.fs_carrier gs'.f_carrier gs'.gso_carrier
by (auto simp add: LLL_invariant_weak_def gram_schmidt_fs.reduced_def)
qed
lemma LLL_inv_wI: assumes
"set fs ⊆ carrier_vec n"
"length fs = m"
"lattice_of fs = L"
"lin_indep fs"
shows "LLL_invariant_weak fs"
unfolding LLL_invariant_weak_def Let_def using assms by auto
definition LLL_invariant :: "bool ⇒ nat ⇒ int vec list ⇒ bool" where
"LLL_invariant upw i fs = (
gs.lin_indpt_list (RAT fs) ∧
lattice_of fs = L ∧
reduced fs i ∧
i ≤ m ∧
length fs = m ∧
(upw ∨ μ_small fs i)
)"
lemma LLL_inv_imp_w: "LLL_invariant upw i fs ⟹ LLL_invariant_weak fs"
unfolding LLL_invariant_def LLL_invariant_weak_def by blast
lemma LLL_invD: assumes "LLL_invariant upw i fs"
shows
"lin_indep fs"
"length (RAT fs) = m"
"set fs ⊆ carrier_vec n"
"⋀ i. i < m ⟹ fs ! i ∈ carrier_vec n"
"⋀ i. i < m ⟹ gso fs i ∈ carrier_vec n"
"length fs = m"
"lattice_of fs = L"
"weakly_reduced fs i"
"i ≤ m"
"reduced fs i"
"upw ∨ μ_small fs i"
proof (atomize (full), goal_cases)
case 1
interpret gs': gram_schmidt_fs_lin_indpt n "RAT fs"
by (standard) (use assms LLL_invariant_def gs.lin_indpt_list_def in auto)
show ?case
using assms gs'.fs_carrier gs'.f_carrier gs'.gso_carrier
by (auto simp add: LLL_invariant_def gram_schmidt_fs.reduced_def)
qed
lemma LLL_invI: assumes
"set fs ⊆ carrier_vec n"
"length fs = m"
"lattice_of fs = L"
"i ≤ m"
"lin_indep fs"
"reduced fs i"
"upw ∨ μ_small fs i"
shows "LLL_invariant upw i fs"
unfolding LLL_invariant_def Let_def split using assms by auto
end
locale fs_int' =
fixes n m fs_init fs
assumes LLL_inv: "LLL.LLL_invariant_weak n m fs_init fs"
sublocale fs_int' ⊆ fs_int_indpt
using LLL_inv unfolding LLL.LLL_invariant_weak_def by (unfold_locales) blast
context LLL
begin
lemma gso_cong: assumes "⋀ i. i ≤ x ⟹ f1 ! i = f2 ! i"
"x < length f1" "x < length f2"
shows "gso f1 x = gso f2 x"
by (rule gs.gso_cong, insert assms, auto)
lemma μ_cong: assumes "⋀ k. j < i ⟹ k ≤ j ⟹ f1 ! k = f2 ! k"
and i: "i < length f1" "i < length f2"
and "j < i ⟹ f1 ! i = f2 ! i"
shows "μ f1 i j = μ f2 i j"
by (rule gs.μ_cong, insert assms, auto)
definition reduction where "reduction = (4+α)/(4*α)"
definition d :: "int vec list ⇒ nat ⇒ int" where "d fs k = gs.Gramian_determinant fs k"
definition D :: "int vec list ⇒ nat" where "D fs = nat (∏ i < m. d fs i)"
definition "dμ gs i j = int_of_rat (of_int (d gs (Suc j)) * μ gs i j)"
definition logD :: "int vec list ⇒ nat"
where "logD fs = (if α = 4/3 then (D fs) else nat (floor (log (1 / of_rat reduction) (D fs))))"
definition LLL_measure :: "nat ⇒ int vec list ⇒ nat" where
"LLL_measure i fs = (2 * logD fs + m - i)"
context
fixes fs
assumes Linv: "LLL_invariant_weak fs"
begin
interpretation fs: fs_int' n m fs_init fs
by (standard) (use Linv in auto)
lemma Gramian_determinant:
assumes k: "k ≤ m"
shows "of_int (gs.Gramian_determinant fs k) = (∏ j<k. sq_norm (gso fs j))" (is ?g1)
"gs.Gramian_determinant fs k > 0" (is ?g2)
using assms fs.Gramian_determinant LLL_inv_wD[OF Linv] by auto
lemma LLL_d_pos [intro]: assumes k: "k ≤ m"
shows "d fs k > 0"
unfolding d_def using fs.Gramian_determinant k LLL_inv_wD[OF Linv] by auto
lemma LLL_d_Suc: assumes k: "k < m"
shows "of_int (d fs (Suc k)) = sq_norm (gso fs k) * of_int (d fs k)"
using assms fs.fs_int_d_Suc LLL_inv_wD[OF Linv] unfolding fs.d_def d_def by auto
lemma LLL_D_pos:
shows "D fs > 0"
using fs.fs_int_D_pos LLL_inv_wD[OF Linv] unfolding D_def fs.D_def fs.d_def d_def by auto
end
text ‹Condition when we can increase the value of $i$›
lemma increase_i:
assumes Linv: "LLL_invariant upw i fs"
assumes i: "i < m"
and upw: "upw ⟹ i = 0"
and red_i: "i ≠ 0 ⟹ sq_norm (gso fs (i - 1)) ≤ α * sq_norm (gso fs i)"
shows "LLL_invariant True (Suc i) fs" "LLL_measure i fs > LLL_measure (Suc i) fs"
proof -
note inv = LLL_invD[OF Linv]
from inv(8,10) have red: "weakly_reduced fs i"
and sred: "reduced fs i" by (auto)
from red red_i i have red: "weakly_reduced fs (Suc i)"
unfolding gram_schmidt_fs.weakly_reduced_def
by (intro allI impI, rename_tac ii, case_tac "Suc ii = i", auto)
from inv(11) upw have sred_i: "⋀ j. j < i ⟹ ¦μ fs i j¦ ≤ 1 / 2"
unfolding μ_small_def by auto
from sred sred_i have sred: "reduced fs (Suc i)"
unfolding gram_schmidt_fs.reduced_def
by (intro conjI[OF red] allI impI, rename_tac ii j, case_tac "ii = i", auto)
show "LLL_invariant True (Suc i) fs"
by (intro LLL_invI, insert inv red sred i, auto)
show "LLL_measure i fs > LLL_measure (Suc i) fs" unfolding LLL_measure_def using i by auto
qed
text ‹Standard addition step which makes $\mu_{i,j}$ small›
definition "μ_small_row i fs j = (∀ j'. j ≤ j' ⟶ j' < i ⟶ abs (μ fs i j') ≤ inverse 2)"
lemma basis_reduction_add_row_main: assumes Linv: "LLL_invariant_weak fs"
and i: "i < m" and j: "j < i"
and fs': "fs' = fs[ i := fs ! i - c ⋅⇩v fs ! j]"
shows "LLL_invariant_weak fs'"
"LLL_invariant True i fs ⟹ LLL_invariant True i fs'"
"c = round (μ fs i j) ⟹ μ_small_row i fs (Suc j) ⟹ μ_small_row i fs' j"
"c = round (μ fs i j) ⟹ abs (μ fs' i j) ≤ 1/2"
"LLL_measure i fs' = LLL_measure i fs"
"⋀ i. i < m ⟹ gso fs' i = gso fs i"
"⋀ i' j'. i' < m ⟹ j' < m ⟹
μ fs' i' j' = (if i' = i ∧ j' ≤ j then μ fs i j' - of_int c * μ fs j j' else μ fs i' j')"
"⋀ ii. ii ≤ m ⟹ d fs' ii = d fs ii"
proof -
define bnd :: rat where bnd: "bnd = 4 ^ (m - 1 - Suc j) * of_nat (N ^ (m - 1) * m)"
define M where "M = map (λi. map (μ fs i) [0..<m]) [0..<m]"
note inv = LLL_inv_wD[OF Linv]
note Gr = inv(1)
have ji: "j ≤ i" "j < m" and jstrict: "j < i"
and add: "set fs ⊆ carrier_vec n" "i < length fs" "j < length fs" "i ≠ j"
and len: "length fs = m"
and indep: "lin_indep fs"
using inv j i by auto
let ?R = rat_of_int
let ?RV = "map_vec ?R"
from inv i j
have Fij: "fs ! i ∈ carrier_vec n" "fs ! j ∈ carrier_vec n" by auto
let ?x = "fs ! i - c ⋅⇩v fs ! j"
let ?g = "gso fs"
let ?g' = "gso fs'"
let ?mu = "μ fs"
let ?mu' = "μ fs'"
from inv j i
have Fi:"⋀ i. i < length (RAT fs) ⟹ (RAT fs) ! i ∈ carrier_vec n"
and gs_carr: "?g j ∈ carrier_vec n"
"?g i ∈ carrier_vec n"
"⋀ i. i < j ⟹ ?g i ∈ carrier_vec n"
"⋀ j. j < i ⟹ ?g j ∈ carrier_vec n"
and len': "length (RAT fs) = m"
and add':"set (map ?RV fs) ⊆ carrier_vec n"
by auto
have RAT_F1: "RAT fs' = (RAT fs)[i := (RAT fs) ! i - ?R c ⋅⇩v (RAT fs) ! j]"
unfolding fs'
proof (rule nth_equalityI[rule_format], goal_cases)
case (2 k)
show ?case
proof (cases "k = i")
case False
thus ?thesis using 2 by auto
next
case True
hence "?thesis = (?RV (fs ! i - c ⋅⇩v fs ! j) =
?RV (fs ! i) - ?R c ⋅⇩v ?RV (fs ! j))"
using 2 add by auto
also have "…" by (rule eq_vecI, insert Fij, auto)
finally show ?thesis by simp
qed
qed auto
hence RAT_F1_i:"RAT fs' ! i = (RAT fs) ! i - ?R c ⋅⇩v (RAT fs) ! j" (is "_ = _ - ?mui")
using i len by auto
have uminus: "fs ! i - c ⋅⇩v fs ! j = fs ! i + -c ⋅⇩v fs ! j"
by (subst minus_add_uminus_vec, insert Fij, auto)
have "lattice_of fs' = lattice_of fs" unfolding fs' uminus
by (rule lattice_of_add[OF add, of _ "- c"], auto)
with inv have lattice: "lattice_of fs' = L" by auto
from add len
have "k < length fs ⟹ ¬ k ≠ i ⟹ fs' ! k ∈ carrier_vec n" for k
unfolding fs'
by (metis (no_types, lifting) nth_list_update nth_mem subset_eq carrier_dim_vec index_minus_vec(2)
index_smult_vec(2))
hence "k < length fs ⟹ fs' ! k ∈ carrier_vec n" for k
unfolding fs' using add len by (cases "k ≠ i",auto)
with len have F1: "set fs' ⊆ carrier_vec n" "length fs' = m" unfolding fs' by (auto simp: set_conv_nth)
hence F1': "length (RAT fs') = m" "SRAT fs' ⊆ Rn" by auto
from indep have dist: "distinct (RAT fs)" by (auto simp: gs.lin_indpt_list_def)
have Fij': "(RAT fs) ! i ∈ Rn" "(RAT fs) ! j ∈ Rn" using add'[unfolded set_conv_nth] i ‹j < m› len by auto
have uminus': "(RAT fs) ! i - ?R c ⋅⇩v (RAT fs) ! j = (RAT fs) ! i + - ?R c ⋅⇩v (RAT fs) ! j"
by (subst minus_add_uminus_vec[where n = n], insert Fij', auto)
have span_F_F1: "gs.span (SRAT fs) = gs.span (SRAT fs')" unfolding RAT_F1 uminus'
by (rule gs.add_vec_span, insert len add, auto)
have **: "?RV (fs ! i) + - ?R c ⋅⇩v (RAT fs) ! j = ?RV (fs ! i - c ⋅⇩v fs ! j)"
by (rule eq_vecI, insert Fij len i j, auto)
from i j len have "j < length (RAT fs)" "i < length (RAT fs)" "i ≠ j" by auto
from gs.lin_indpt_list_add_vec[OF this indep, of "- of_int c"]
have "gs.lin_indpt_list ((RAT fs) [i := (RAT fs) ! i + - ?R c ⋅⇩v (RAT fs) ! j])" (is "gs.lin_indpt_list ?F1") .
also have "?F1 = RAT fs'" unfolding fs' using i len Fij' **
by (auto simp: map_update)
finally have indep_F1: "lin_indep fs'" .
have conn1: "set (RAT fs) ⊆ carrier_vec n" "length (RAT fs) = m" "distinct (RAT fs)"
"gs.lin_indpt (set (RAT fs))"
using inv unfolding gs.lin_indpt_list_def by auto
have conn2: "set (RAT fs') ⊆ carrier_vec n" "length (RAT fs') = m" "distinct (RAT fs')"
"gs.lin_indpt (set (RAT fs'))"
using indep_F1 F1' unfolding gs.lin_indpt_list_def by auto
interpret gs1: gram_schmidt_fs_lin_indpt n "RAT fs"
by (standard) (use inv gs.lin_indpt_list_def in auto)
interpret gs2: gram_schmidt_fs_lin_indpt n "RAT fs'"
by (standard) (use indep_F1 F1' gs.lin_indpt_list_def in auto)
let ?G = "map ?g [0 ..< m]"
let ?G' = "map ?g' [0 ..< m]"
from gs1.span_gso gs2.span_gso gs1.gso_carrier gs2.gso_carrier conn1 conn2 span_F_F1 len
have span_G_G1: "gs.span (set ?G) = gs.span (set ?G')"
and lenG: "length ?G = m"
and Gi: "i < length ?G ⟹ ?G ! i ∈ Rn"
and G1i: "i < length ?G' ⟹ ?G' ! i ∈ Rn" for i
by auto
have eq: "x ≠ i ⟹ RAT fs' ! x = (RAT fs) ! x" for x unfolding RAT_F1 by auto
hence eq_part: "x < i ⟹ ?g' x = ?g x" for x
by (intro gs.gso_cong, insert len, auto)
have G: "i < m ⟹ (RAT fs) ! i ∈ Rn"
"i < m ⟹ fs ! i ∈ carrier_vec n" for i by(insert add len', auto)
note carr1[intro] = this[OF i] this[OF ji(2)]
have "x < m ⟹ ?g x ∈ Rn"
"x < m ⟹ ?g' x ∈ Rn"
"x < m ⟹ dim_vec (gso fs x) = n"
"x < m ⟹ dim_vec (gso fs' x) = n"
for x using inv G1i by (auto simp:o_def Gi G1i)
hence carr2[intro!]:"?g i ∈ Rn" "?g' i ∈ Rn"
"?g ` {0..<i} ⊆ Rn"
"?g ` {0..<Suc i} ⊆ Rn" using i by auto
have F1_RV: "?RV (fs' ! i) = RAT fs' ! i" using i F1 by auto
have F_RV: "?RV (fs ! i) = (RAT fs) ! i" using i len by auto
from eq_part
have span_G1_G: "gs.span (?g' ` {0..<i}) = gs.span (?g ` {0..<i})" (is "?ls = ?rs")
apply(intro cong[OF refl[of "gs.span"]],rule image_cong[OF refl]) using eq by auto
have "(RAT fs') ! i - ?g' i = ((RAT fs) ! i - ?g' i) - ?mui"
unfolding RAT_F1_i using carr1 carr2
by (intro eq_vecI, auto)
hence in1:"((RAT fs) ! i - ?g' i) - ?mui ∈ ?rs"
using gs2.oc_projection_exist[of i] conn2 i unfolding span_G1_G by auto
from ‹j < i› have Gj_mem: "(RAT fs) ! j ∈ (λ x. ((RAT fs) ! x)) ` {0 ..< i}" by auto
have id1: "set (take i (RAT fs)) = (λx. ?RV (fs ! x)) ` {0..<i}"
using ‹i < m› len
by (subst nth_image[symmetric], force+)
have "(RAT fs) ! j ∈ ?rs ⟷ (RAT fs) ! j ∈ gs.span ((λx. ?RV (fs ! x)) ` {0..<i})"
using gs1.partial_span ‹i < m› id1 inv by auto
also have "(λx. ?RV (fs ! x)) ` {0..<i} = (λx. ((RAT fs) ! x)) ` {0..<i}" using ‹i < m› len by force
also have "(RAT fs) ! j ∈ gs.span …"
by (rule gs.span_mem[OF _ Gj_mem], insert ‹i < m› G, auto)
finally have "(RAT fs) ! j ∈ ?rs" .
hence in2:"?mui ∈ ?rs"
apply(intro gs.prod_in_span) by force+
have ineq:"((RAT fs) ! i - ?g' i) + ?mui - ?mui = ((RAT fs) ! i - ?g' i)"
using carr1 carr2 by (intro eq_vecI, auto)
have cong': "A = B ⟹ A ∈ C ⟹ B ∈ C" for A B :: "'a vec" and C by auto
have *: "?g ` {0..<i} ⊆ Rn" by auto
have in_span: "(RAT fs) ! i - ?g' i ∈ ?rs"
by (rule cong'[OF eq_vecI gs.span_add1[OF * in1 in2,unfolded ineq]], insert carr1 carr2, auto)
{
fix x assume x:"x < i" hence "x < m" "i ≠ x" using i by auto
from gs2.orthogonal this inv assms
have "?g' i ∙ ?g' x = 0" by auto
}
hence G1_G: "?g' i = ?g i"
by (intro gs1.oc_projection_unique) (use inv i eq_part in_span in auto)
show eq_fs:"x < m ⟹ ?g' x = ?g x"
for x proof(induct x rule:nat_less_induct[rule_format])
case (1 x)
hence ind: "m < x ⟹ ?g' m = ?g m"
for m by auto
{ assume "x > i"
hence ?case unfolding gs2.gso.simps[of x] gs1.gso.simps[of x] unfolding gs1.μ.simps gs2.μ.simps
using ind eq by (auto intro: cong[OF _ cong[OF refl[of "gs.sumlist"]]])
} note eq_rest = this
show ?case by (rule linorder_class.linorder_cases[of x i],insert G1_G eq_part eq_rest,auto)
qed
hence Hs:"?G' = ?G" by (auto simp:o_def)
have red: "weakly_reduced fs i ⟹ weakly_reduced fs' i" using eq_fs ‹i < m›
unfolding gram_schmidt_fs.weakly_reduced_def by simp
let ?Mi = "M ! i ! j"
have Gjn: "dim_vec (fs ! j) = n" using Fij(2) carrier_vecD by blast
define E where "E = addrow_mat m (- ?R c) i j"
define M' where "M' = gs1.M m"
define N' where "N' = gs2.M m"
have E: "E ∈ carrier_mat m m" unfolding E_def by simp
have M: "M' ∈ carrier_mat m m" unfolding gs1.M_def M'_def by auto
have N: "N' ∈ carrier_mat m m" unfolding gs2.M_def N'_def by auto
let ?mat = "mat_of_rows n"
let ?GsM = "?mat ?G"
have Gs: "?GsM ∈ carrier_mat m n" by auto
hence GsT: "?GsM⇧T ∈ carrier_mat n m" by auto
have Gnn: "?mat (RAT fs) ∈ carrier_mat m n" unfolding mat_of_rows_def using len by auto
have "?mat (RAT fs') = addrow (- ?R c) i j (?mat (RAT fs))"
unfolding RAT_F1 by (rule eq_matI, insert Gjn ji(2), auto simp: len mat_of_rows_def)
also have "… = E * ?mat (RAT fs)" unfolding E_def
by (rule addrow_mat, insert j i, auto simp: mat_of_rows_def len)
finally have HEG: "?mat (RAT fs') = E * ?mat (RAT fs)" .
have "(E * M') * ?mat ?G = E * (M' * ?mat ?G)"
by (rule assoc_mult_mat[OF E M Gs])
also have "M' * ?GsM = ?mat (RAT fs)" using gs1.matrix_equality conn1 M'_def by simp
also have "E * … = ?mat (RAT fs')" unfolding HEG ..
also have "… = N' * ?mat ?G'" using gs2.matrix_equality conn2 unfolding N'_def by simp
also have "?mat ?G' = ?GsM" unfolding Hs ..
finally have "(E * M') * ?GsM = N' * ?GsM" .
from arg_cong[OF this, of "λ x. x * ?GsM⇧T"] E M N
have EMN: "(E * M') * (?GsM * ?GsM⇧T) = N' * (?GsM * ?GsM⇧T)"
by (subst (1 2) assoc_mult_mat[OF _ Gs GsT, of _ m, symmetric], auto)
have "det (?GsM * ?GsM⇧T) = gs.Gramian_determinant ?G m"
unfolding gs.Gramian_determinant_def
by (subst gs.Gramian_matrix_alt_def, auto simp: Let_def)
also have "… > 0"
proof -
have 1: "gs.lin_indpt_list ?G"
using conn1 gs1.orthogonal_gso gs1.gso_carrier by (intro gs.orthogonal_imp_lin_indpt_list) (auto)
interpret G: gram_schmidt_fs_lin_indpt n ?G
by (standard) (use 1 gs.lin_indpt_list_def in auto)
show ?thesis
by (intro G.Gramian_determinant) auto
qed
finally have "det (?GsM * ?GsM⇧T) ≠ 0" by simp
from vec_space.det_nonzero_congruence[OF EMN this _ _ N] Gs E M
have EMN: "E * M' = N'" by auto
{
fix i' j'
assume ij: "i' < m" "j' < m" and choice: "i' ≠ i ∨ j < j'"
have "?mu' i' j'
= N' $$ (i',j')" using ij F1 unfolding N'_def gs2.M_def by auto
also have "… = addrow (- ?R c) i j M' $$ (i',j')" unfolding EMN[symmetric] E_def
by (subst addrow_mat[OF M], insert ji, auto)
also have "… = (if i = i' then - ?R c * M' $$ (j, j') + M' $$ (i', j') else M' $$ (i', j'))"
by (rule index_mat_addrow, insert ij M, auto)
also have "… = M' $$ (i', j')"
proof (cases "i = i'")
case True
with choice have jj: "j < j'" by auto
have "M' $$ (j, j') = ?mu j j'"
using ij ji len unfolding M'_def gs1.M_def by auto
also have "… = 0" unfolding gs1.μ.simps using jj by auto
finally show ?thesis using True by auto
qed auto
also have "… = ?mu i' j'"
using ij len unfolding M'_def gs1.M_def by auto
also note calculation
} note mu_no_change = this
{
fix j'
assume jj': "j' ≤ j" with j i have j': "j' < m" by auto
have "?mu' i j'
= N' $$ (i,j')" using jj' j i F1 unfolding N'_def gs2.M_def by auto
also have "… = addrow (- ?R c) i j M' $$ (i,j')" unfolding EMN[symmetric] E_def
by (subst addrow_mat[OF M], insert ji, auto)
also have "… = - ?R c * M' $$ (j, j') + M' $$ (i, j')"
by (rule index_mat_addrow, insert j' i M, auto)
also have "… = M' $$ (i, j') - ?R c * M' $$ (j, j')" by simp
also have "M' $$ (i, j') = ?mu i j'"
using i j' len unfolding M'_def gs1.M_def by auto
also have "M' $$ (j, j') = ?mu j j'"
using i j j' len unfolding M'_def gs1.M_def by auto
finally have "?mu' i j' = ?mu i j' - ?R c * ?mu j j'" by auto
} note mu_change = this
show mu_update: "i' < m ⟹ j' < m ⟹
?mu' i' j' = (if i' = i ∧ j' ≤ j then ?mu i j' - ?R c * ?mu j j' else ?mu i' j')"
for i' j' using mu_change[of j'] mu_no_change[of i' j']
by auto
{
assume "LLL_invariant True i fs"
from LLL_invD[OF this] have "weakly_reduced fs i" and sred: "reduced fs i" by auto
from red[OF this(1)] have red: "weakly_reduced fs' i" .
have sred: "reduced fs' i"
unfolding gram_schmidt_fs.reduced_def
proof (intro conjI[OF red] impI allI, goal_cases)
case (1 i' j)
with mu_no_change[of i' j] sred[unfolded gram_schmidt_fs.reduced_def, THEN conjunct2, rule_format, of i' j] i
show ?case by auto
qed
show "LLL_invariant True i fs'"
by (intro LLL_invI[OF F1 lattice ‹i ≤ m› indep_F1 sred], auto)
}
show Linv': "LLL_invariant_weak fs'"
by (intro LLL_inv_wI[OF F1 lattice indep_F1])
have mudiff:"?mu i j - of_int c = ?mu' i j"
by (subst mu_change, auto simp: gs1.μ.simps)
have lin_indpt_list_fs: "gs.lin_indpt_list (RAT fs')"
unfolding gs.lin_indpt_list_def using conn2 by auto
{
assume c: "c = round (μ fs i j)"
have small: "abs (?mu i j - of_int c) ≤ inverse 2" unfolding j c
using of_int_round_abs_le by (auto simp add: abs_minus_commute)
from this[unfolded mudiff]
show mu'_2: "abs (?mu' i j) ≤ 1 / 2" by simp
assume mu_small: "μ_small_row i fs (Suc j)"
show "μ_small_row i fs' j"
unfolding μ_small_row_def
proof (intro allI, goal_cases)
case (1 j')
show ?case using mu'_2 mu_small[unfolded μ_small_row_def, rule_format, of j']
by (cases "j' > j", insert mu_update[of i j'] i, auto)
qed
}
{
fix i
assume i: "i ≤ m"
have "rat_of_int (d fs' i) = of_int (d fs i)"
unfolding d_def Gramian_determinant(1)[OF Linv i] Gramian_determinant(1)[OF Linv' i]
by (rule prod.cong[OF refl], subst eq_fs, insert i, auto)
thus "d fs' i = d fs i" by simp
} note d = this
have D: "D fs' = D fs"
unfolding D_def
by (rule arg_cong[of _ _ nat], rule prod.cong[OF refl], auto simp: d)
show "LLL_measure i fs' = LLL_measure i fs"
unfolding LLL_measure_def logD_def D ..
qed
text ‹Addition step which can be skipped since $\mu$-value is already small›
lemma basis_reduction_add_row_main_0: assumes Linv: "LLL_invariant_weak fs"
and i: "i < m" and j: "j < i"
and 0: "round (μ fs i j) = 0"
and mu_small: "μ_small_row i fs (Suc j)"
shows "μ_small_row i fs j" (is ?g1)
proof -
note inv = LLL_inv_wD[OF Linv]
from inv(5)[OF i] inv(5)[of j] i j
have id: "fs[i := fs ! i - 0 ⋅⇩v fs ! j] = fs"
by (intro nth_equalityI, insert inv i, auto)
show ?g1
using basis_reduction_add_row_main[OF Linv i j _, of fs] 0 id mu_small by auto
qed
lemma μ_small_row_refl: "μ_small_row i fs i"
unfolding μ_small_row_def by auto
lemma basis_reduction_add_row_done: assumes Linv: "LLL_invariant True i fs"
and i: "i < m"
and mu_small: "μ_small_row i fs 0"
shows "LLL_invariant False i fs"
proof -
note inv = LLL_invD[OF Linv]
from mu_small
have mu_small: "μ_small fs i" unfolding μ_small_row_def μ_small_def by auto
show ?thesis
using i mu_small by (intro LLL_invI[OF inv(3,6,7,9,1,10)], auto)
qed
lemma d_swap_unchanged: assumes len: "length F1 = m"
and i0: "i ≠ 0" and i: "i < m" and ki: "k ≠ i" and km: "k ≤ m"
and swap: "F2 = F1[i := F1 ! (i - 1), i - 1 := F1 ! i]"
shows "d F1 k = d F2 k"
proof -
let ?F1_M = "mat k n (λ(i, y). F1 ! i $ y)"
let ?F2_M = "mat k n (λ(i, y). F2 ! i $ y)"
have "∃ P. P ∈ carrier_mat k k ∧ det P ∈ {-1, 1} ∧ ?F2_M = P * ?F1_M"
proof cases
assume ki: "k < i"
hence H: "?F2_M = ?F1_M" unfolding swap
by (intro eq_matI, auto)
let ?P = "1⇩m k"
have "?P ∈ carrier_mat k k" "det ?P ∈ {-1, 1}" "?F2_M = ?P * ?F1_M" unfolding H by auto
thus ?thesis by blast
next
assume "¬ k < i"
with ki have ki: "k > i" by auto
let ?P = "swaprows_mat k i (i - 1)"
from i0 ki have neq: "i ≠ i - 1" and kmi: "i - 1 < k" by auto
have *: "?P ∈ carrier_mat k k" "det ?P ∈ {-1, 1}" using det_swaprows_mat[OF ki kmi neq] ki by auto
from i len have iH: "i < length F1" "i - 1 < length F1" by auto
have "?P * ?F1_M = swaprows i (i - 1) ?F1_M"
by (subst swaprows_mat[OF _ ki kmi], auto)
also have "… = ?F2_M" unfolding swap
by (intro eq_matI, rename_tac ii jj,
case_tac "ii = i", (insert iH, simp add: nth_list_update)[1],
case_tac "ii = i - 1", insert iH neq ki, auto simp: nth_list_update)
finally show ?thesis using * by metis
qed
then obtain P where P: "P ∈ carrier_mat k k" and detP: "det P ∈ {-1, 1}" and H': "?F2_M = P * ?F1_M" by auto
have "d F2 k = det (gs.Gramian_matrix F2 k)"
unfolding d_def gs.Gramian_determinant_def by simp
also have "… = det (?F2_M * ?F2_M⇧T)" unfolding gs.Gramian_matrix_def Let_def by simp
also have "?F2_M * ?F2_M⇧T = ?F2_M * (?F1_M⇧T * P⇧T)" unfolding H'
by (subst transpose_mult[OF P], auto)
also have "… = P * (?F1_M * (?F1_M⇧T * P⇧T))" unfolding H'
by (subst assoc_mult_mat[OF P], auto)
also have "det … = det P * det (?F1_M * (?F1_M⇧T * P⇧T))"
by (rule det_mult[OF P], insert P, auto)
also have "?F1_M * (?F1_M⇧T * P⇧T) = (?F1_M * ?F1_M⇧T) * P⇧T"
by (subst assoc_mult_mat, insert P, auto)
also have "det … = det (?F1_M * ?F1_M⇧T) * det P"
by (subst det_mult, insert P, auto simp: det_transpose)
also have "det (?F1_M * ?F1_M⇧T) = det (gs.Gramian_matrix F1 k)" unfolding gs.Gramian_matrix_def Let_def by simp
also have "… = d F1 k"
unfolding d_def gs.Gramian_determinant_def by simp
finally have "d F2 k = (det P * det P) * d F1 k" by simp
also have "det P * det P = 1" using detP by auto
finally show "d F1 k = d F2 k" by simp
qed
definition base where "base = real_of_rat ((4 * α) / (4 + α))"
definition g_bound :: "int vec list ⇒ bool" where
"g_bound fs = (∀ i < m. sq_norm (gso fs i) ≤ of_nat N)"
end
locale LLL_with_assms = LLL +
assumes α: "α ≥ 4/3"
and lin_dep: "lin_indep fs_init"
and len: "length fs_init = m"
begin
lemma α0: "α > 0" "α ≠ 0"
using α by auto
lemma fs_init: "set fs_init ⊆ carrier_vec n"
using lin_dep[unfolded gs.lin_indpt_list_def] by auto
lemma reduction: "0 < reduction" "reduction ≤ 1"
"α > 4/3 ⟹ reduction < 1"
"α = 4/3 ⟹ reduction = 1"
using α unfolding reduction_def by auto
lemma base: "α > 4/3 ⟹ base > 1" using reduction(1,3) unfolding reduction_def base_def by auto
lemma basis_reduction_swap_main: assumes Linvw: "LLL_invariant_weak fs"
and small: "LLL_invariant False i fs ∨ abs (μ fs i (i - 1)) ≤ 1/2"
and i: "i < m"
and i0: "i ≠ 0"
and norm_ineq: "sq_norm (gso fs (i - 1)) > α * sq_norm (gso fs i)"
and fs'_def: "fs' = fs[i := fs ! (i - 1), i - 1 := fs ! i]"
shows "LLL_invariant_weak fs'"
and "LLL_invariant False i fs ⟹ LLL_invariant False (i - 1) fs'"
and "LLL_measure i fs > LLL_measure (i - 1) fs'"
and "⋀ k. k < m ⟹ gso fs' k = (if k = i - 1 then
gso fs i + μ fs i (i - 1) ⋅⇩v gso fs (i - 1)
else if k = i then
gso fs (i - 1) - (RAT fs ! (i - 1) ∙ gso fs' (i - 1) / sq_norm (gso fs' (i - 1))) ⋅⇩v gso fs' (i - 1)
else gso fs k)" (is "⋀ k. _ ⟹ _ = ?newg k")
and "⋀ k. k < m ⟹ sq_norm (gso fs' k) = (if k = i - 1 then
sq_norm (gso fs i) + (μ fs i (i - 1) * μ fs i (i - 1)) * sq_norm (gso fs (i - 1))
else if k = i then
sq_norm (gso fs i) * sq_norm (gso fs (i - 1)) / sq_norm (gso fs' (i - 1))
else sq_norm (gso fs k))" (is "⋀ k. _ ⟹ _ = ?new_norm k")
and "⋀ ii j. ii < m ⟹ j < ii ⟹ μ fs' ii j = (
if ii = i - 1 then
μ fs i j
else if ii = i then
if j = i - 1 then
μ fs i (i - 1) * sq_norm (gso fs (i - 1)) / sq_norm (gso fs' (i - 1))
else
μ fs (i - 1) j
else if ii > i ∧ j = i then
μ fs ii (i - 1) - μ fs i (i - 1) * μ fs ii i
else if ii > i ∧ j = i - 1 then
μ fs ii (i - 1) * μ fs' i (i - 1) + μ fs ii i * sq_norm (gso fs i) / sq_norm (gso fs' (i - 1))
else μ fs ii j)" (is "⋀ ii j. _ ⟹ _ ⟹ _ = ?new_mu ii j")
and "⋀ ii. ii ≤ m ⟹ of_int (d fs' ii) = (if ii = i then
sq_norm (gso fs' (i - 1)) / sq_norm (gso fs (i - 1)) * of_int (d fs i)
else of_int (d fs ii))"
proof -
note inv = LLL_inv_wD[OF Linvw]
interpret fs: fs_int' n m fs_init fs
by (standard) (use Linvw in auto)
let ?mu1 = "μ fs"
let ?mu2 = "μ fs'"
let ?g1 = "gso fs"
let ?g2 = "gso fs'"
have m12: "¦?mu1 i (i - 1)¦ ≤ inverse 2" using small
proof
assume "LLL_invariant False i fs"
from LLL_invD(11)[OF this] i0 show ?thesis unfolding μ_small_def by auto
qed auto
note d = d_def
note Gd = Gramian_determinant(1)
note Gd12 = Gd[OF Linvw]
let ?x = "?g1 (i - 1)" let ?y = "?g1 i"
let ?cond = "α * sq_norm ?y < sq_norm ?x"
from inv have len: "length fs = m" and HC: "set fs ⊆ carrier_vec n"
and L: "lattice_of fs = L"
using i by auto
from i0 inv i have swap: "set fs ⊆ carrier_vec n" "i < length fs" "i - 1 < length fs" "i ≠ i - 1"
unfolding Let_def by auto
have RAT_fs': "RAT fs' = (RAT fs)[i := (RAT fs) ! (i - 1), i - 1 := (RAT fs) ! i]"
unfolding fs'_def using swap by (intro nth_equalityI, auto simp: nth_list_update)
have span': "gs.span (SRAT fs) = gs.span (SRAT fs')" unfolding fs'_def
by (rule arg_cong[of _ _ gs.span], insert swap, auto)
have lfs': "lattice_of fs' = lattice_of fs" unfolding fs'_def
by (rule lattice_of_swap[OF swap refl])
with inv have lattice: "lattice_of fs' = L" by auto
have len': "length fs' = m" using inv unfolding fs'_def by auto
have fs': "set fs' ⊆ carrier_vec n" using swap unfolding fs'_def set_conv_nth
by (auto, rename_tac k, case_tac "k = i", force, case_tac "k = i - 1", auto)
let ?rv = "map_vec rat_of_int"
from inv(1) have indepH: "lin_indep fs" .
from i i0 len have "i < length (RAT fs)" "i - 1 < length (RAT fs)" by auto
with distinct_swap[OF this] len have "distinct (RAT fs') = distinct (RAT fs)" unfolding RAT_fs'
by (auto simp: map_update)
with len' fs' span' indepH have indepH': "lin_indep fs'" unfolding fs'_def using i i0
by (auto simp: gs.lin_indpt_list_def)
have lenR': "length (RAT fs') = m" using len' by auto
have conn1: "set (RAT fs) ⊆ carrier_vec n" "length (RAT fs) = m" "distinct (RAT fs)"
"gs.lin_indpt (set (RAT fs))"
using inv unfolding gs.lin_indpt_list_def by auto
have conn2: "set (RAT fs') ⊆ carrier_vec n" "length (RAT fs') = m" "distinct (RAT fs')"
"gs.lin_indpt (set (RAT fs'))"
using indepH' lenR' unfolding gs.lin_indpt_list_def by auto
interpret gs2: gram_schmidt_fs_lin_indpt n "RAT fs'"
by (standard) (use indepH' lenR' gs.lin_indpt_list_def in auto)
have fs'_fs: "k < i - 1 ⟹ fs' ! k = fs ! k" for k unfolding fs'_def by auto
{
fix k
assume ki: "k < i - 1"
with i have kn: "k < m" by simp
have "?g2 k = ?g1 k"
by (rule gs.gso_cong, insert ki kn len, auto simp: fs'_def)
} note G2_G = this
have take_eq: "take (Suc i - 1 - 1) fs' = take (Suc i - 1 - 1) fs"
by (intro nth_equalityI, insert len len' i swap(2-), auto intro!: fs'_fs)
have i1n: "i - 1 < m" using i by auto
let ?R = rat_of_int
let ?RV = "map_vec ?R"
let ?f1 = "λ i. RAT fs ! i"
let ?f2 = "λ i. RAT fs' ! i"
let ?n1 = "λ i. sq_norm (?g1 i)"
let ?n2 = "λ i. sq_norm (?g2 i)"
have heq:"fs ! (i - 1) = fs' ! i" "take (i-1) fs = take (i-1) fs'"
"?f2 (i - 1) = ?f1 i" "?f2 i = ?f1 (i - 1)"
unfolding fs'_def using i len i0 by auto
have norm_pos2: "j < m ⟹ ?n2 j > 0" for j
using gs2.sq_norm_pos len' by simp
have norm_pos1: "j < m ⟹ ?n1 j > 0" for j
using fs.gs.sq_norm_pos inv by simp
have norm_zero2: "j < m ⟹ ?n2 j ≠ 0" for j using norm_pos2[of j] by linarith
have norm_zero1: "j < m ⟹ ?n1 j ≠ 0" for j using norm_pos1[of j] by linarith
have gs: "⋀ j. j < m ⟹ ?g1 j ∈ Rn" using inv by blast
have gs2: "⋀ j. j < m ⟹ ?g2 j ∈ Rn" using fs.gs.gso_carrier conn2 by auto
have g: "⋀ j. j < m ⟹ ?f1 j ∈ Rn" using inv by auto
have g2: "⋀ j. j < m ⟹ ?f2 j ∈ Rn" using gs2.f_carrier conn2 by blast
let ?fs1 = "?f1 ` {0..< (i - 1)}"
have G: "?fs1 ⊆ Rn" using g i by auto
let ?gs1 = "?g1 ` {0..< (i - 1)}"
have G': "?gs1 ⊆ Rn" using gs i by auto
let ?S = "gs.span ?fs1"
let ?S' = "gs.span ?gs1"
have S'S: "?S' = ?S"
by (rule fs.gs.partial_span', insert conn1 i, auto)
have "gs.is_oc_projection (?g2 (i - 1)) (gs.span (?g2 ` {0..< (i - 1)})) (?f2 (i - 1))"
using i len' by (intro gs2.gso_oc_projection_span(2)) auto
also have "?f2 (i - 1) = ?f1 i" unfolding fs'_def using len i by auto
also have "gs.span (?g2 ` {0 ..< (i - 1)}) = gs.span (?f2 ` {0 ..< (i - 1)})"
using i len' by (intro gs2.partial_span') auto
also have "?f2 ` {0 ..< (i - 1)} = ?fs1"
by (rule image_cong[OF refl], insert len i, auto simp: fs'_def)
finally have claim1: "gs.is_oc_projection (?g2 (i - 1)) ?S (?f1 i)" .
have list_id: "[0..<Suc (i - 1)] = [0..< i - 1] @ [i - 1]"
"[0..< Suc i] = [0..< i] @ [i]" "map f [x] = [f x]" for f x using i by auto
have f1i_sum: "?f1 i = gs.sumlist (map (λj. ?mu1 i j ⋅⇩v ?g1 j) [0 ..< i]) + ?g1 i" (is "_ = ?sum + _")
apply(subst fs.gs.fi_is_sum_of_mu_gso, insert len i, force)
unfolding map_append list_id
by (subst gs.M.sumlist_snoc, insert i gs conn1, auto simp: fs.gs.μ.simps)
have f1im1_sum: "?f1 (i - 1) = gs.sumlist (map (λj. ?mu1 (i - 1) j ⋅⇩v ?g1 j) [0..<i - 1]) + ?g1 (i - 1)" (is "_ = ?sum1 + _")
apply(subst fs.gs.fi_is_sum_of_mu_gso, insert len i, force)
unfolding map_append list_id
by (subst gs.M.sumlist_snoc, insert i gs, auto simp: fs.gs.μ.simps)
have sum: "?sum ∈ Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
have sum1: "?sum1 ∈ Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
from gs.span_closed[OF G] have S: "?S ⊆ Rn" by auto
from gs i have gs': "⋀ j. j < i - 1 ⟹ ?g1 j ∈ Rn" and gsi: "?g1 (i - 1) ∈ Rn" by auto
have "[0 ..< i] = [0 ..< Suc (i - 1)]" using i0 by simp
also have "… = [0 ..< i - 1] @ [i - 1]" by simp
finally have list: "[0 ..< i] = [0 ..< i - 1] @ [i - 1]" .
{
fix k
assume kn: "k ≤ m" and ki: "k ≠ i"
from d_swap_unchanged[OF len i0 i ki kn fs'_def]
have "d fs k = d fs' k" by simp
} note d = this
have g2_im1: "?g2 (i - 1) = ?g1 i + ?mu1 i (i - 1) ⋅⇩v ?g1 (i - 1)" (is "_ = _ + ?mu_f1")
proof (rule gs.is_oc_projection_eq[OF claim1 _ S g[OF i]])
show "gs.is_oc_projection (?g1 i + ?mu_f1) ?S (?f1 i)" unfolding gs.is_oc_projection_def
proof (intro conjI allI impI)
let ?sum' = "gs.sumlist (map (λj. ?mu1 i j ⋅⇩v ?g1 j) [0 ..< i - 1])"
have sum': "?sum' ∈ Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
show inRn: "(?g1 i + ?mu_f1) ∈ Rn" using gs[OF i] gsi i by auto
have carr: "?sum ∈ Rn" "?g1 i ∈ Rn" "?mu_f1 ∈ Rn" "?sum' ∈ Rn" using sum' sum gs[OF i] gsi i by auto
have "?f1 i - (?g1 i + ?mu_f1) = (?sum + ?g1 i) - (?g1 i + ?mu_f1)"
unfolding f1i_sum by simp
also have "… = ?sum - ?mu_f1" using carr by auto
also have "?sum = gs.sumlist (map (λj. ?mu1 i j ⋅⇩v ?g1 j) [0 ..< i - 1] @ [?mu_f1])"
unfolding list by simp
also have "… = ?sum' + ?mu_f1"
by (subst gs.sumlist_append, insert gs' gsi, auto)
also have "… - ?mu_f1 = ?sum'" using sum' gsi by auto
finally have id: "?f1 i - (?g1 i + ?mu_f1) = ?sum'" .
show "?f1 i - (?g1 i + ?mu_f1) ∈ gs.span ?S" unfolding id gs.span_span[OF G]
proof (rule gs.sumlist_in_span[OF G])
fix v
assume "v ∈ set (map (λj. ?mu1 i j ⋅⇩v ?g1 j) [0 ..< i - 1])"
then obtain j where j: "j < i - 1" and v: "v = ?mu1 i j ⋅⇩v ?g1 j" by auto
show "v ∈ ?S" unfolding v
by (rule gs.smult_in_span[OF G], unfold S'S[symmetric], rule gs.span_mem, insert gs i j, auto)
qed
fix x
assume "x ∈ ?S"
hence x: "x ∈ ?S'" using S'S by simp
show "(?g1 i + ?mu_f1) ∙ x = 0"
proof (rule gs.orthocompl_span[OF _ G' inRn x])
fix x
assume "x ∈ ?gs1"
then obtain j where j: "j < i - 1" and x_id: "x = ?g1 j" by auto
from j i x_id gs[of j] have x: "x ∈ Rn" by auto
{
fix k
assume k: "k > j" "k < m"
have "?g1 k ∙ x = 0" unfolding x_id
by (rule fs.gs.orthogonal, insert conn1 k, auto)
}
from this[of i] this[of "i - 1"] j i
have main: "?g1 i ∙ x = 0" "?g1 (i - 1) ∙ x = 0" by auto
have "(?g1 i + ?mu_f1) ∙ x = ?g1 i ∙ x + ?mu_f1 ∙ x"
by (rule add_scalar_prod_distrib[OF gs[OF i] _ x], insert gsi, auto)
also have "… = 0" using main
by (subst smult_scalar_prod_distrib[OF gsi x], auto)
finally show "(?g1 i + ?mu_f1) ∙ x = 0" .
qed
qed
qed
{
fix k
assume kn: "k < m"
and ki: "k ≠ i" "k ≠ i - 1"
have "?g2 k = gs.oc_projection (gs.span (?g2 ` {0..<k})) (?f2 k)"
by (rule gs2.gso_oc_projection_span, insert kn conn2, auto)
also have "gs.span (?g2 ` {0..<k}) = gs.span (?f2 ` {0..<k})"
by (rule gs2.partial_span', insert conn2 kn, auto)
also have "?f2 ` {0..<k} = ?f1 ` {0..<k}"
proof(cases "k≤i")
case True hence "k < i - 1" using ki by auto
then show ?thesis apply(intro image_cong) unfolding fs'_def using len i by auto
next
case False
have "?f2 ` {0..<k} = (?f1 ∘ transpose i (i - 1)) ` {0..<k}"
unfolding transpose_def fs'_def o_def using len i
by (intro image_cong, insert len kn, force+)
also have "… = ?f1 ` {0..<k}"
apply(rule swap_image_eq) using False by auto
finally show ?thesis.
qed
also have "gs.span … = gs.span (?g1 ` {0..<k})"
by (rule sym, rule fs.gs.partial_span', insert conn1 kn, auto)
also have "?f2 k = ?f1 k" using ki kn len unfolding fs'_def by auto
also have "gs.oc_projection (gs.span (?g1 ` {0..<k})) … = ?g1 k"
by (subst fs.gs.gso_oc_projection_span, insert kn conn1, auto)
finally have "?g2 k = ?g1 k" .
} note g2_g1_identical = this
{
fix jj ii
assume ii: "ii < i - 1"
have "?mu2 ii jj = ?mu1 ii jj" using ii i len
by (subst gs.μ_cong[of _ _ "RAT fs" "RAT fs'"], auto simp: fs'_def)
} note mu'_mu_small_i = this
{
fix jj
assume jj: "jj < i - 1"
hence id1: "jj < i - 1 ⟷ True" "jj < i ⟷ True" by auto
have id2: "?g2 jj = ?g1 jj" by (subst g2_g1_identical, insert jj i, auto)
have "?mu2 i jj = ?mu1 (i - 1) jj" "?mu2 (i - 1) jj = ?mu1 i jj"
unfolding gs2.μ.simps fs.gs.μ.simps id1 id2 if_True using len i i0 by (auto simp: fs'_def)
} note mu'_mu_i_im1_j = this
have im1: "i - 1 < m" using i by auto
let ?g2_im1 = "?g2 (i - 1)"
have g2_im1_Rn: "?g2_im1 ∈ Rn" using i conn2 by (auto intro!: fs.gs.gso_carrier)
{
let ?mu2_f2 = "λ j. - ?mu2 i j ⋅⇩v ?g2 j"
let ?sum = "gs.sumlist (map (λj. - ?mu1 (i - 1) j ⋅⇩v ?g1 j) [0 ..< i - 1])"
have mhs: "?mu2_f2 (i - 1) ∈ Rn" using i conn2 by (auto intro!: fs.gs.gso_carrier)
have sum': "?sum ∈ Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
have gim1: "?f1 (i - 1) ∈ Rn" using g i by auto
have "?g2 i = ?f2 i + gs.sumlist (map ?mu2_f2 [0 ..< i-1] @ [?mu2_f2 (i-1)])"
unfolding gs2.gso.simps[of i] list by simp
also have "?f2 i = ?f1 (i - 1)" unfolding fs'_def using len i i0 by auto
also have "map ?mu2_f2 [0 ..< i-1] = map (λj. - ?mu1 (i - 1) j ⋅⇩v ?g1 j) [0 ..< i - 1]"
by (rule map_cong[OF refl], subst g2_g1_identical, insert i, auto simp: mu'_mu_i_im1_j)
also have "gs.sumlist (… @ [?mu2_f2 (i - 1)]) = ?sum + ?mu2_f2 (i - 1)"
by (subst gs.sumlist_append, insert gs i mhs, auto)
also have "?f1 (i - 1) + … = (?f1 (i - 1) + ?sum) + ?mu2_f2 (i - 1)"
using gim1 sum' mhs by auto
also have "?f1 (i - 1) + ?sum = ?g1 (i - 1)" unfolding fs.gs.gso.simps[of "i - 1"] by simp
also have "?mu2_f2 (i - 1) = - (?f2 i ∙ ?g2_im1 / sq_norm ?g2_im1) ⋅⇩v ?g2_im1" unfolding gs2.μ.simps using i0 by simp
also have "… = - ((?f2 i ∙ ?g2_im1 / sq_norm ?g2_im1) ⋅⇩v ?g2_im1)" by auto
also have "?g1 (i - 1) + … = ?g1 (i - 1) - ((?f2 i ∙ ?g2_im1 / sq_norm ?g2_im1) ⋅⇩v ?g2_im1)"
by (rule sym, rule minus_add_uminus_vec[of _ n], insert gsi g2_im1_Rn, auto)
also have "?f2 i = ?f1 (i - 1)" by fact
finally have "?g2 i = ?g1 (i - 1) - (?f1 (i - 1) ∙ ?g2 (i - 1) / sq_norm (?g2 (i - 1))) ⋅⇩v ?g2 (i - 1)" .
} note g2_i = this
let ?n1 = "λ i. sq_norm (?g1 i)"
let ?n2 = "λ i. sq_norm (?g2 i)"
{
have "?n2 (i - 1) = sq_norm (?g1 i + ?mu_f1)" unfolding g2_im1 by simp
also have "… = (?g1 i + ?mu_f1) ∙ (?g1 i + ?mu_f1)"
by (simp add: sq_norm_vec_as_cscalar_prod)
also have "… = (?g1 i + ?mu_f1) ∙ ?g1 i + (?g1 i + ?mu_f1) ∙ ?mu_f1"
by (rule scalar_prod_add_distrib, insert gs i, auto)
also have "(?g1 i + ?mu_f1) ∙ ?g1 i = ?g1 i ∙ ?g1 i + ?mu_f1 ∙ ?g1 i"
by (rule add_scalar_prod_distrib, insert gs i, auto)
also have "(?g1 i + ?mu_f1) ∙ ?mu_f1 = ?g1 i ∙ ?mu_f1 + ?mu_f1 ∙ ?mu_f1"
by (rule add_scalar_prod_distrib, insert gs i, auto)
also have "?mu_f1 ∙ ?g1 i = ?g1 i ∙ ?mu_f1"
by (rule comm_scalar_prod, insert gs i, auto)
also have "?g1 i ∙ ?g1 i = sq_norm (?g1 i)"
by (simp add: sq_norm_vec_as_cscalar_prod)
also have "?g1 i ∙ ?mu_f1 = ?mu1 i (i - 1) * (?g1 i ∙ ?g1 (i - 1))"
by (rule scalar_prod_smult_right, insert gs[OF i] gs[OF ‹i - 1 < m›], auto)
also have "?g1 i ∙ ?g1 (i - 1) = 0"
using orthogonalD[OF fs.gs.orthogonal_gso, of i "i - 1"] i len i0
by (auto simp: o_def)
also have "?mu_f1 ∙ ?mu_f1 = ?mu1 i (i - 1) * (?mu_f1 ∙ ?g1 (i - 1))"
by (rule scalar_prod_smult_right, insert gs[OF i] gs[OF ‹i - 1 < m›], auto)
also have "?mu_f1 ∙ ?g1 (i - 1) = ?mu1 i (i - 1) * (?g1 (i - 1) ∙ ?g1 (i - 1))"
by (rule scalar_prod_smult_left, insert gs[OF i] gs[OF ‹i - 1 < m›], auto)
also have "?g1 (i - 1) ∙ ?g1 (i - 1) = sq_norm (?g1 (i - 1))"
by (simp add: sq_norm_vec_as_cscalar_prod)
finally have "?n2 (i - 1) = ?n1 i + (?mu1 i (i - 1) * ?mu1 i (i - 1)) * ?n1 (i - 1)"
by (simp add: ac_simps o_def)
} note sq_norm_g2_im1 = this
from norm_pos1[OF i] norm_pos1[OF im1] norm_pos2[OF i] norm_pos2[OF im1]
have norm0: "?n1 i ≠ 0" "?n1 (i - 1) ≠ 0" "?n2 i ≠ 0" "?n2 (i - 1) ≠ 0" by auto
hence norm0': "?n2 (i - 1) ≠ 0" using i by auto
{
have si: "Suc i ≤ m" and im1: "i - 1 ≤ m" using i by auto
have det1: "gs.Gramian_determinant (RAT fs) (Suc i) = (∏j<Suc i. ∥fs.gs.gso j∥⇧2)"
using fs.gs.Gramian_determinant si len by auto
have det2: "gs.Gramian_determinant (RAT fs') (Suc i) = (∏j<Suc i. ∥gs2.gso j∥⇧2)"
using gs2.Gramian_determinant si len' by auto
from norm_zero1[OF less_le_trans[OF _ im1]] have 0: "(∏j < i-1. ?n1 j) ≠ 0"
by (subst prod_zero_iff, auto)
have "rat_of_int (d fs' (Suc i)) = rat_of_int (d fs (Suc i))"
using d_swap_unchanged[OF len i0 i _ si fs'_def] by auto
also have "rat_of_int (d fs' (Suc i)) = gs.Gramian_determinant (RAT fs') (Suc i)" unfolding d_def
by (subst fs.of_int_Gramian_determinant[symmetric], insert conn2 i g fs', auto simp: set_conv_nth)
also have "… = (∏j<Suc i. ?n2 j)" unfolding det2 by (rule prod.cong, insert i, auto)
also have "rat_of_int (d fs (Suc i)) = gs.Gramian_determinant (RAT fs) (Suc i)" unfolding d_def
by (subst fs.of_int_Gramian_determinant[symmetric], insert conn1 i g, auto)
also have "… = (∏j<Suc i. ?n1 j)" unfolding det1 by (rule prod.cong, insert i, auto)
also have "{..<Suc i} = insert i (insert (i-1) {..<i-1})" (is "_ = ?set") by auto
also have "(∏j∈ ?set. ?n2 j) = ?n2 i * ?n2 (i - 1) * (∏j < i-1. ?n2 j)" using i0
by (subst prod.insert; (subst prod.insert)?; auto)
also have "(∏j∈ ?set. ?n1 j) = ?n1 i * ?n1 (i - 1) * (∏j < i-1. ?n1 j)" using i0
by (subst prod.insert; (subst prod.insert)?; auto)
also have "(∏j < i-1. ?n2 j) = (∏j < i-1. ?n1 j)"
by (rule prod.cong, insert G2_G, auto)
finally have "?n2 i = ?n1 i * ?n1 (i - 1) / ?n2 (i - 1)"
using 0 norm0' by (auto simp: field_simps)
} note sq_norm_g2_i = this
{
fix ii j
assume ii: "ii > i" "ii < m"
and ji: "j ≠ i" "j ≠ i - 1"
{
assume j: "j < ii"
have "?mu2 ii j = (?f2 ii ∙ ?g2 j) / sq_norm (?g2 j)"
unfolding gs2.μ.simps using j by auto
also have "?f2 ii = ?f1 ii" using ii len unfolding fs'_def by auto
also have "?g2 j = ?g1 j" using g2_g1_identical[of j] j ii ji by auto
finally have "?mu2 ii j = ?mu1 ii j"
unfolding fs.gs.μ.simps using j by auto
}
hence "?mu2 ii j = ?mu1 ii j" by (cases "j < ii", auto simp: gs2.μ.simps fs.gs.μ.simps)
} note mu_no_change_large_row = this
{
have "?mu2 i (i - 1) = (?f2 i ∙ ?g2 (i - 1)) / ?n2 (i - 1)"
unfolding gs2.μ.simps using i0 by auto
also have "?f2 i ∙ ?g2 (i - 1) = ?f1 (i - 1) ∙ ?g2 (i - 1)"
using len i i0 unfolding fs'_def by auto
also have "… = ?f1 (i - 1) ∙ (?g1 i + ?mu1 i (i - 1) ⋅⇩v ?g1 (i - 1))"
unfolding g2_im1 by simp
also have "… = ?f1 (i - 1) ∙ ?g1 i + ?f1 (i - 1) ∙ (?mu1 i (i - 1) ⋅⇩v ?g1 (i - 1))"
by (rule scalar_prod_add_distrib[of _ n], insert i gs g, auto)
also have "?f1 (i - 1) ∙ ?g1 i = 0"
by (subst fs.gs.fi_scalar_prod_gso, insert conn1 im1 i i0, auto simp: fs.gs.μ.simps fs.gs.μ.simps)
also have "?f1 (i - 1) ∙ (?mu1 i (i - 1) ⋅⇩v ?g1 (i - 1)) =
?mu1 i (i - 1) * (?f1 (i - 1) ∙ ?g1 (i - 1))"
by (rule scalar_prod_smult_distrib, insert gs g i, auto)
also have "?f1 (i - 1) ∙ ?g1 (i - 1) = ?n1 (i - 1)"
by (subst fs.gs.fi_scalar_prod_gso, insert conn1 im1, auto simp: fs.gs.μ.simps)
finally
have "?mu2 i (i - 1) = ?mu1 i (i - 1) * ?n1 (i - 1) / ?n2 (i - 1)"
by (simp add: sq_norm_vec_as_cscalar_prod)
} note mu'_mu_i_im1 = this
{
fix ii assume iii: "ii > i" and ii: "ii < m"
hence iii1: "i - 1 < ii" by auto
have "?mu2 ii (i - 1) = (?f2 ii ∙ ?g2 (i - 1)) / ?n2 (i - 1)"
unfolding gs2.μ.simps using i0 iii1 by auto
also have "?f2 ii ∙ ?g2 (i-1) = ?f1 ii ∙ ?g2 (i - 1)"
using len i i0 iii ii unfolding fs'_def by auto
also have "… = ?f1 ii ∙ (?g1 i + ?mu1 i (i - 1) ⋅⇩v ?g1 (i - 1))"
unfolding g2_im1 by simp
also have "… = ?f1 ii ∙ ?g1 i + ?f1 ii ∙ (?mu1 i (i - 1) ⋅⇩v ?g1 (i - 1))"
by (rule scalar_prod_add_distrib[of _ n], insert i ii gs g, auto)
also have "?f1 ii ∙ ?g1 i =