Theory CVP_vec
theory CVP_vec
imports
Main
Reduction
Lattice_int
Subset_Sum
infnorm
begin
section ‹CVP in $\ell_\infty$›
text ‹The closest vector problem.›
definition is_closest_vec :: "int_lattice ⇒ int vec ⇒ int vec ⇒ bool" where
"is_closest_vec L b v ≡ (is_lattice L) ∧
(∀x∈L. linf_norm_vec (x - b) ≥ linf_norm_vec (v - b) ∧ v∈L)"
text ‹The decision problem associated with solving CVP exactly.›
definition gap_cvp :: "(int_lattice × int vec × int) set" where
"gap_cvp ≡ {(L, b, r). (is_lattice L) ∧ (∃v∈L. linf_norm_vec (v - b) ≤ r)}"
text ‹Reduction function for CVP to subset sum›
definition gen_basis :: "int vec ⇒ int mat" where
"gen_basis as = mat (dim_vec as + 2) (dim_vec as) (λ (i, j). if i ∈ {0,1} then as$j
else (if i = j + 2 then 2 else 0))"
definition gen_t :: "int vec ⇒ int ⇒ int vec" where
"gen_t as s = vec (dim_vec as + 2) ((λ i. 1)(0:= s+1, 1:= s-1))"
definition reduce_cvp_subset_sum ::
"((int vec) * int) ⇒ (int_lattice * (int vec) * int)" where
"reduce_cvp_subset_sum ≡ (λ (as,s).
(gen_lattice (gen_basis as), gen_t as s, (1::int)))"
text ‹Lemmas for Proof›
lemma vec_lambda_eq[intro]: "(∀i<n. a i = b i) ⟶ vec n a = vec n b"
by auto
lemma eq_fun_applic: assumes "x = y" shows "f x = f y"
using assms by auto
lemma sum_if_zero:
assumes "finite A" "i∈A"
shows "(∑j∈A. (if i = j then a j else 0)) = a i"
proof -
have "(∑x∈A. if x = i then a x else 0) =
(if i = i then a i else 0) + (∑x∈A - {i}. if x = i then a x else 0)"
using sum.remove[OF assms, of "(λx. if x = i then a x else 0)"] by auto
then show ?thesis by (simp add: assms(1))
qed
lemma set_compr_elem:
assumes "finite A" "a∈A"
shows "{f i | i. i∈A} = {f a} ∪ {f i | i. i∈A-{a}}"
by (safe, use assms in ‹auto›)
lemma Bx_rewrite:
assumes x_dim: "dim_vec as = dim_vec x"
shows "(gen_basis as) *⇩v x =
vec (dim_vec as + 2) (λ i. if i ∈ {0,1} then (x ∙ as)
else (2 * x$(i-2)))"
(is "?init_vec = ?goal_vec")
proof -
define n::nat where n_def: "n = dim_vec as"
have "vec n (λj. (as $ j)) ∙ x = (x ∙ as)"
unfolding n_def scalar_prod_def using x_dim by (simp add: mult.commute)
moreover have "vec (dim_vec as) (λj. if i = Suc (Suc j) then 2 else 0) ∙ x = 2 * x $ (i - 2)"
if "i < Suc (Suc (dim_vec as))" "0 < i" "i ≠ Suc 0" for i
proof -
have "(∑ia = 0..<dim_vec x.
vec (dim_vec as) (λj. (if i = Suc (Suc j) then 2 else 0)) $ ia * x $ ia) =
(∑ia<n. (if i = ia+2 then 2 * (x $ ia) else 0))"
by (intro sum.cong, auto simp add: n_def x_dim)
also have "… = (∑ib∈{2..<n+2}.
(if i = ib then 2 * (x $ (ib-2)) else 0))"
proof -
have eq: "(λib. (if i = ib then 2 * x $ (ib - 2) else 0)) ∘ (+) 2
= (λia. (if i = ia + 2 then 2 * x $ ia else 0))"
by auto
then show ?thesis
by (subst sum.atLeastLessThan_shift_0[
of "(λib. (if i = ib then 2 * x $ (ib - 2) else 0))" 2 "n+2"])
(subst eq, use lessThan_atLeast0 in ‹auto›)
qed
also have "… = 2 * (x $ (i-2))"
proof -
have finite: "finite {2..<n+2}" by auto
have is_in: "i ∈ {2..<n+2}" using that by (auto simp add: n_def)
show ?thesis
by (subst sum_if_zero[OF finite is_in, of "(λk.2 * (x $ (k-2)))"], auto)
qed
finally show ?thesis unfolding scalar_prod_def by auto
qed
ultimately show ?thesis
unfolding gen_basis_def reduce_cvp_subset_sum_def gen_t_def
by (intro eq_vecI, auto simp add: n_def)
qed
lemma Bx_s_rewrite:
assumes x_dim: "dim_vec as = dim_vec x"
shows "(gen_basis as) *⇩v x - (gen_t as s) =
vec (dim_vec as + 2) (λ i. if i = 0 then (x ∙ as - s - 1) else (
if i = 1 then (x ∙ as - s + 1) else (2 * x$(i-2) - 1)))"
(is "?init_vec = ?goal_vec")
unfolding gen_t_def by (subst Bx_rewrite[OF assms], auto)
lemma linf_norm_vec_Bx_s:
assumes x_dim: "dim_vec as = dim_vec x"
shows "linf_norm_vec ((gen_basis as) *⇩v x - (gen_t as s)) =
Max (insert 0 ({ ¦x ∙ as - s - 1¦} ∪ { ¦x ∙ as - s + 1¦} ∪
{ ¦2*x$(i-2)-1¦ | i. 1<i ∧ i<dim_vec as+2 }))"
proof -
let ?init_vec = "(gen_basis as) *⇩v x - (gen_t as s)"
let ?goal_vec = "vec (dim_vec as + 2) (λ i. if i = 0 then (x ∙ as - s - 1) else (
if i = 1 then (x ∙ as - s + 1) else (2 * x$(i-2) - 1)))"
define n where n_def: "n = dim_vec as"
have "linf_norm_vec ?init_vec = linf_norm_vec ?goal_vec" using Bx_s_rewrite[OF x_dim] by auto
also have "… = Max (insert 0 {¦?goal_vec $i¦ | i. i<n+2})"
unfolding linf_norm_vec_Max n_def by auto
also have "… = Max (insert 0 ({ ¦x ∙ as - s - 1¦} ∪
{ ¦x ∙ as - s + 1¦} ∪
{ ¦2*x$(i-2)-1¦ | i. 1<i ∧ i<n+2}))"
proof -
have "{¦?goal_vec $i¦ | i. i<n+2} =
{¦?goal_vec $0¦} ∪ {¦?goal_vec $1¦} ∪ {¦?goal_vec $i¦ | i. 1<i ∧ i<n+2}"
proof -
have "{¦?goal_vec $i¦ | i. i∈{0..<n+2}} =
{¦?goal_vec $0¦} ∪ {¦?goal_vec $i¦ | i. i∈{1..<n+2}}"
by (subst set_compr_elem[of "{0..<n+2}" 0 "(λi. ¦?goal_vec $i¦)"], auto)
also have "… = {¦?goal_vec $0¦} ∪ {¦?goal_vec $1¦} ∪
{¦?goal_vec $i¦ | i. i∈{2..<n+2}}"
by (subst set_compr_elem[of _ 1], auto)
finally show ?thesis by auto
qed
also have "… = { ¦x ∙ as - s - 1¦} ∪ { ¦x ∙ as - s + 1¦} ∪
{¦?goal_vec $i¦ | i. 1<i ∧ i<n+2}" by auto
also have "{¦?goal_vec $i¦ | i. 1<i ∧ i<n+2} =
{ ¦2*x$(i-2)-1¦ | i. 1<i ∧ i<n+2}"
proof -
have "¦?goal_vec $i¦ = ¦2*x$(i-2)-1¦" if "1<i ∧ i<n+2" for i
using that n_def by force
then show ?thesis using n_def by force
qed
finally have eq: "{¦?goal_vec $i¦ | i. i<n+2} =
{ ¦x ∙ as - s - 1¦} ∪ { ¦x ∙ as - s + 1¦} ∪
{ ¦2*x$(i-2)-1¦ | i. 1<i ∧ i<n+2}" by blast
then show ?thesis by auto
qed
finally show ?thesis using n_def by blast
qed
text ‹‹gen_basis› actually generates a basis which is spans the ‹int_lattice› (by definition) and
is linearly independent.›
lemma is_indep_gen_basis:
"is_indep (gen_basis as)"
unfolding is_indep_int_def
proof (safe, goal_cases)
case (1 z)
let ?n = "dim_vec as"
have z_dim: "dim_vec z = ?n" using 1(2) unfolding gen_basis_def by auto
have dim_row: "dim_row (gen_basis as) = ?n + 2" unfolding gen_basis_def by auto
have eq: "(real_of_int_mat (gen_basis as)) *⇩v z = vec (?n + 2) (λ i. if i ∈ {0,1}
then (z ∙ (real_of_int_vec as)) else (2 * z$(i-2)))"
(is "(real_of_int_mat (gen_basis as)) *⇩v z = ?goal_vec")
proof -
have scal_prod_com: "z ∙ real_of_int_vec as = real_of_int_vec as ∙ z"
using comm_scalar_prod[of "real_of_int_vec as" ?n z] z_dim
by (metis carrier_dim_vec index_map_vec(2) real_of_int_vec_def)
have *: "row (of_int_hom.mat_hom (mat (?n+2) (?n) (λx.
(case x of (i, j) ⇒ if i = 0 ∨ i = Suc 0 then as $ j
else if i = j + 2 then 2 else 0)))) i =
(if i∈{0,1} then real_of_int_vec as else vec ?n (λj. if i = j + 2 then 2 else 0))"
(is "?row = ?vec")
if "i<?n+2" for i
using that by (auto simp add: real_of_int_vec_def)
moreover have "vec (dim_vec as) (λj. if i = Suc (Suc j) then 2 else 0) ∙ z = 2 * z $ (i - 2)"
if "i < Suc (Suc (dim_vec as))" "0 < i" "i ≠ Suc 0" for i
proof (goal_cases)
case 1
have plus_2: "(i-2 = j) = (i = j+2)" for j using 1 that by auto
have finite: "finite {0..<?n}" and elem: "i-2 ∈ {0..<?n}" using that 1 by auto
have vec: "vec (dim_vec as) (λj. if i = j+2 then 2 else 0) $ ia =
(if i = ia+2 then 2 else 0)" if "ia<?n" for ia
using index_vec that by blast
then have "(∑ia = 0..<dim_vec z.
vec (dim_vec as) (λj. if i = Suc (Suc j) then 2 else 0) $ ia * z $ ia) =
(∑ia = 0..<dim_vec as. (if i = ia+2 then 2 else 0) * z $ ia)"
using z_dim by auto
also have "… = (∑ia = 0..<dim_vec as. (if i = ia+2 then 2 * z $ ia else 0))"
proof -
have "(∀n. (0 = (if i = n + 2 then 2 else 0) * z $ n ∨ n + 2 = i) ∧
(2 * z $ n = (if i = n + 2 then 2 else 0) * z $ n ∨ n + 2 ≠ i)) ∨
(∑n = 0..<dim_vec as. (if i = n + 2 then 2 else 0) * z $ n) =
(∑n = 0..<dim_vec as. if i = n + 2 then 2 * z $ n else 0)" by simp
then show ?thesis by (metis (no_types))
qed
also have "… = 2*z$(i-2)" using sum_if_zero[OF finite elem, of "(λj. 2*z$j)"]
using plus_2 by auto
finally show ?case unfolding scalar_prod_def by blast
qed
ultimately have "?row i ∙ z =
(if i ∈ {0,1} then (real_of_int_vec as) ∙ z else 2 * z $ (i - 2))"
if "i<?n+2" for i
using that by (subst *[OF that], auto)
then have "?row i ∙ z =
(if i ∈ {0,1} then z ∙ real_of_int_vec as else 2 * z $ (i - 2))"
if "i<?n+2" for i using that by (subst scal_prod_com)
then show ?thesis
unfolding real_of_int_mat_def gen_basis_def mult_mat_vec_def by auto
qed
have "… = 0⇩v (?n + 2)" using 1(1) dim_row by (subst eq[symmetric], auto)
then have "2 * z$(i-2) = 0" if "1<i" and "i<?n +2" for i
using that by (smt (verit, best) cancel_comm_monoid_add_class.diff_cancel
empty_iff index_vec index_zero_vec(1) insert_iff not_less_zero zero_less_diff)
then have "z$i = 0" if "i<?n" for i using that by force
then show ?case using 1 z_dim unfolding gen_basis_def by auto
qed
text ‹The CVP is NP-hard in $\ell_\infty$.›
lemma well_defined_reduction:
assumes "(as, s) ∈ subset_sum"
shows "reduce_cvp_subset_sum (as, s) ∈ gap_cvp"
proof -
obtain x where
x_dim: "dim_vec x = dim_vec as" and
x_binary: "∀i<dim_vec x. x $ i ∈ {0, 1}" and
x_lin_combo: "x ∙ as = s"
using assms unfolding subset_sum_def by blast
define L where L_def: "L = fst (reduce_cvp_subset_sum (as, s))"
define b where b_def: "b = fst (snd (reduce_cvp_subset_sum (as, s)))"
define r where r_def: "r = snd (snd (reduce_cvp_subset_sum (as, s)))"
have "r = 1" by (simp add: r_def reduce_cvp_subset_sum_def Pair_inject prod.exhaust_sel)
define B where "B = gen_basis as"
define n where n_def: "n = dim_vec as"
have init_eq_goal: "B *⇩v x - b =
vec (n+2) (λ i. if i = 0 then (x ∙ as - s - 1) else (
if i = 1 then (x ∙ as - s + 1) else (2 * x$(i-2) - 1)))"
(is "?init_vec = ?goal_vec")
unfolding B_def b_def reduce_cvp_subset_sum_def
by (auto simp add: Bx_s_rewrite[OF x_dim[symmetric]] n_def)
have "linf_norm_vec (B *⇩v x - b) =
Max (insert 0 ({ ¦x ∙ as - s - 1¦} ∪ { ¦x ∙ as - s + 1¦} ∪
{ ¦2*x$(i-2)-1¦ | i. 1<i ∧ i<n+2 }))"
unfolding B_def b_def reduce_cvp_subset_sum_def
by (auto simp add: linf_norm_vec_Bx_s[OF x_dim[symmetric]] n_def)
also have "… ≤ r"
proof -
have elem: "x$(i-2)∈{0,1}" if "1<i ∧ i<n+2" for i
using that x_binary x_dim n_def
by (smt (verit) add_diff_cancel_right' diff_diff_left diff_less_mono2
less_add_same_cancel2 less_imp_add_positive less_one linorder_neqE_nat
nat_1_add_1 not_add_less2)
then have "¦2*x$(i-2)-1¦ = 1" if "1<i ∧ i<n+2" for i
using elem[OF that] by auto
then have "{ ¦2 * x $ (i - 2) - 1¦ |i. 1 < i ∧ i < n + 2} ⊆ {1}"
by (safe, auto)
then show ?thesis using x_lin_combo ‹r=1› by auto
qed
finally have "linf_norm_vec (?init_vec) ≤ r" by blast
moreover have "B *⇩v x∈L"
proof -
have "dim_vec x = dim_col (gen_basis as)" unfolding gen_basis_def using x_dim by auto
then show ?thesis
unfolding L_def reduce_cvp_subset_sum_def gen_lattice_def B_def by auto
qed
ultimately have witness: "∃v∈L. linf_norm_vec (v - b) ≤ r" by auto
have is_indep: "is_indep B"
unfolding B_def using is_indep_gen_basis[of as] by simp
have L_int_lattice: "is_lattice L" unfolding L_def reduce_cvp_subset_sum_def
using is_lattice_gen_lattice[OF is_indep] unfolding B_def by auto
show ?thesis unfolding gap_cvp_def using L_int_lattice witness L_def b_def r_def by force
qed
text ‹NP-hardness part of reduction.›
lemma NP_hardness_reduction:
assumes "reduce_cvp_subset_sum (as, s) ∈ gap_cvp"
shows "(as, s) ∈ subset_sum"
proof -
define n where "n = dim_vec as"
define B where "B = gen_basis as"
define L where "L = gen_lattice B"
define b where "b = gen_t as s"
have ex_v: "∃v∈L. linf_norm_vec (v - b) ≤ 1" and is_int_lattice: "is_lattice L"
using assms unfolding gap_cvp_def reduce_cvp_subset_sum_def L_def B_def b_def by auto
then obtain v where v_in_L:"v∈L" and ineq:"linf_norm_vec (v - b) ≤ 1" by blast
have "∃zs::int vec. v = B *⇩v zs ∧ dim_vec zs = dim_vec as"
using v_in_L unfolding L_def gen_lattice_def B_def gen_basis_def by auto
then obtain zs::"int vec" where v_def: "v = B *⇩v zs"
and zs_dim: "dim_vec zs = dim_vec as" by blast
have init_eq_goal: "v - b =
vec (n+2) (λ i. if i = 0 then (zs ∙ as - s - 1) else (
if i = 1 then (zs ∙ as - s + 1) else (2 * zs$(i-2) - 1)))"
(is "?init_vec = ?goal_vec")
unfolding v_def B_def b_def using Bx_s_rewrite[OF zs_dim[symmetric]] n_def by simp
have linf_norm_vec_ineq: "linf_norm_vec (v-b) = Max (insert 0 ({ ¦zs ∙ as - s - 1¦} ∪
{ ¦zs ∙ as - s + 1¦} ∪ { ¦2*zs$(i-2)-1¦ | i. 1<i ∧ i<n+2 }))"
unfolding v_def B_def b_def using linf_norm_vec_Bx_s[OF zs_dim[symmetric]] n_def by simp
have Max_le_1: "Max (insert 0 ({ ¦zs ∙ as - s - 1¦} ∪
{ ¦zs ∙ as - s + 1¦} ∪ { ¦2*zs$(i-2)-1¦ | i. 1<i ∧ i<n+2 }))≤1"
using ineq by (subst linf_norm_vec_ineq[symmetric])
have "¦2*zs$(i-2)-1¦≤1" if "1<i ∧ i<n+2" for i using Max_le_1 that by auto
then have "zs$(i-2) = 0 ∨ zs$(i-2) = 1" if "1<i ∧ i<n+2" for i
using that by force
then have "zs$i = 0 ∨ zs$i = 1" if "i<n" for i using that
by (metis One_nat_def Suc_less_eq add_2_eq_Suc' add_diff_cancel_right' zero_less_Suc)
then have "∀i<n. zs $ i ∈ {0, 1}" by simp
moreover have "zs ∙ as = s" using Max_le_1 by auto
ultimately have "(∀i<dim_vec zs. zs $ i ∈ {0, 1}) ∧ zs ∙ as = s ∧ dim_vec zs = dim_vec as"
using zs_dim n_def by auto
then show ?thesis unfolding subset_sum_def gap_cvp_def by auto
qed
text ‹The CVP is NP-hard in $\ell_\infty$.›
lemma "is_reduction reduce_cvp_subset_sum subset_sum gap_cvp"
unfolding is_reduction_def
proof (safe, goal_cases)
case (1 as s)
then show ?case using well_defined_reduction by auto
next
case (2 as s)
then show ?case using NP_hardness_reduction by auto
qed
end