Quelle  SVP_vec.thy

theory SVP_vec

imports 
  BHLE
begin

section ‹SVP in $\ell_\infty$›
text ‹The reduction of SVP to BHLE in $l_\infty$ norm›

text ‹The shortest vector problem.›
definition is_shortest_vec :: "int_lattice ==> int vec ==> bool" where
  "is_shortest_vec L v ≡ (is_lattice L) ∧ (∀x∈L. ∥x∥_\<infinity> ≥ ∥v∥_\<infinity> ∧ v∈L) "


text ‹The decision problem associated with solving SVP exactly.›
definition gap_svp :: "(int_lattice × int) set" where
  "gap_svp ≡ {(L, r). (is_lattice L) ∧ (dim_lattice L ≥ 2) ∧
      (∃v∈L. ∥v∥_\<infinity> ≤ r ∧ v ≠ 0_v (dim_vec v))}"

text ‹Generate a lattice to solve SVP for reduction.›

text ‹Here, the factor $K''$ from the paper \cite{EmBo81}
 was changed to be $2\cdot\mathbf{k}\cdot(k+1)\cdot \sum_i \mathbf{| a_i |}$
  order for the proofs to finish.›

definition gen_svp_basis :: "int vec ==> int ==> int mat" where
  "gen_svp_basis a k = mat (dim_vec a + 1) (dim_vec a + 1)
    (λ (i, j). if (i < dim_vec a) ∧ (j< dim_vec a) then (if i = j then 1 else 0)
      else (if (i < dim_vec a) ∧ (j ≥ dim_vec a) then 0
      else (if (i ≥ dim_vec a) ∧ (j < dim_vec a) then (k+1) * (a $ j)
      else 2*k*(k+1)* (∑ i ∈ {0 ..< dim_vec a}. ∣a $ i∣) +1 )))"


text ‹Reduction SVP to bounded homogeneous linear equation problem in $\ell_\infty$ norm.›
definition reduce_svp_bhle:: "(int vec × int) ==> (int_lattice × int)" where
  "reduce_svp_bhle ≡ (λ (a, k). (gen_lattice (gen_svp_basis a k), k))"



text ‹Lemmas for proof›

lemma gen_svp_basis_mult: 
  assumes "dim_vec z = dim_vec a + 1"
  shows "(gen_svp_basis a k) *_v z = vec (dim_vec a + 1)
         (λi. if i < dim_vec a then z$i else (k+1) * (∑ i ∈ {0 ..< dim_vec a}. z $ i * a $ i) +
              (2*k*(k+1)* (∑ i ∈ {0 ..< dim_vec a}. ∣a $ i∣) +1) * (z$(dim_vec a)))"
using assms proof (subst vec_eq_iff, safe, goal_cases)
case 1
  then show ?case using assms unfolding gen_svp_basis_def by auto
next
case (2 i)
  then show ?case proof (cases "i<dim_vec a")
  case True
    have "{0..<dim_vec a} = insert i {0..<dim_vec a}" using True by auto
    then have "(∑ia = 0..<dim_vec a. (if i = ia then 1 else 0) * z $ ia) =
      (∑ia ∈ insert i {0..<dim_vec a}. (if i = ia then 1 else 0) * z $ ia)" by auto
    also have "… = z$i" by (subst sum.insert_remove, auto) 
    finally have "(∑ia = 0..<dim_vec a. (if i = ia then 1 else 0) * z $ ia) = z $ i" 
      by auto
    then show ?thesis unfolding mult_mat_vec_def gen_svp_basis_def scalar_prod_def 
      using True assms by auto
  next
  case False
    then have "i = dim_vec a" using 2 by auto
    then show ?thesis unfolding gen_svp_basis_def using assms 
      by (auto simp add: scalar_prod_def sum_distrib_left mult.commute mult.left_commute)
  qed
qed

lemma gen_svp_basis_mult_real: 
  assumes "dim_vec z = dim_vec a + 1"
  shows "real_of_int_mat (gen_svp_basis a k) *_v z = vec (dim_vec a + 1)
         (λi. if i < dim_vec a then z$i else (k+1) * (∑ i ∈ {0 ..< dim_vec a}. z $ i * a $ i) +
              (2*k*(k+1)* (∑ i ∈ {0 ..< dim_vec a}. ∣a $ i∣) +1) * (z$(dim_vec a)))"
using assms proof (subst vec_eq_iff, safe, goal_cases)
case 1
  then show ?case using assms unfolding gen_svp_basis_def by auto
next
case (2 i)
  then show ?case proof (cases "i<dim_vec a")
  case True
    have "{0..<dim_vec a} = insert i {0..<dim_vec a}" using True by auto
    then have "(∑ia = 0..<dim_vec a. (if i = ia then 1 else 0) * z $ ia) =
      (∑ia ∈ insert i {0..<dim_vec a}. (if i = ia then 1 else 0) * z $ ia)" by auto
    also have "… = z$i" by (subst sum.insert_remove, auto) 
    finally have "(∑ia = 0..<dim_vec a. (if i = ia then 1 else 0) * z $ ia) = z $ i" 
      by auto
    then have "(∑ia = 0..<dim_vec a. real_of_int (if i = ia then 1 else 0) * z $ ia) = z $ i" 
      by (smt (verit, best) of_int_hom.hom_one of_int_hom.hom_zero sum.cong)
    then show ?thesis unfolding mult_mat_vec_def gen_svp_basis_def scalar_prod_def 
      using True assms by auto
  next
  case False
    then have "i = dim_vec a" using 2 by auto
    then show ?thesis unfolding gen_svp_basis_def using assms 
      by (auto simp add: scalar_prod_def sum_distrib_left mult.commute mult.left_commute)
  qed
qed

lemma gen_svp_basis_mult_last: 
  assumes "dim_vec z = dim_vec a + 1"
  shows "((gen_svp_basis a k) *_v z) $ (dim_vec a) =
         (k+1) * (∑ i ∈ {0 ..< dim_vec a}. z $ i * a $ i) +
              (2*k*(k+1)* (∑ i ∈ {0 ..< dim_vec a}. ∣a $ i∣) +1) * (z$(dim_vec a))"
using gen_svp_basis_mult[OF assms] by auto

text ‹The set generated by ‹gen_svp_basis› is indeed linearly independent.›
lemma is_indep_gen_svp_basis: 
  assumes "k>0"
  shows "is_indep (gen_svp_basis a k)"
unfolding is_indep_int_def
proof (safe, goal_cases)
case (1 z)
  have dim_row_dim_vec: "dim_row (gen_svp_basis a k) = dim_vec z" 
    using 1 unfolding gen_svp_basis_def by auto
  then have suc_dim_a_dim_z: "dim_vec z = dim_vec a + 1" unfolding gen_svp_basis_def by auto
  have alt1: "(real_of_int_mat (gen_svp_basis a k) *_v z) $ i = 0" if "i< dim_vec a +1"for i 
    using 1(1) that unfolding gen_svp_basis_def by auto
  have z_upto_last: "z$i = 0" if "i < dim_vec a" for i 
  proof -
    have elem: "(real_of_int_mat (gen_svp_basis a k) *_v z) $ i = z $ i" 
      using gen_svp_basis_mult_real[OF suc_dim_a_dim_z] that by auto
    show ?thesis by (subst elem[symmetric]) (use alt1[of i] that in ‹auto›) 
  qed
  moreover have "z $ (dim_vec a) = 0"
  proof -
    have "0 = (real_of_int_mat (gen_svp_basis a k) *_v z) $ (dim_vec a)" using alt1 by auto
    also have "… = (real_of_int k + 1) * (∑i = 0..<dim_vec a. z $ i * real_of_int (a $ i)) +
      (2 * real_of_int k * (real_of_int k + 1) * (∑x = 0..<dim_vec a. real_of_int (∣a $ x∣)) + 1) *
      z $ dim_vec a" 
      using gen_svp_basis_mult_real[OF suc_dim_a_dim_z] by auto
    also have "… = real_of_int (2 * k * (k + 1) * (∑x = 0..<dim_vec a. ∣a $ x∣) + 1 ) * (z$dim_vec a)"
      using suc_dim_a_dim_z using z_upto_last by auto
    finally have "0 = real_of_int (2 * k * (k + 1) * (∑x = 0..<dim_vec a. ∣a $ x∣) + 1 ) *
                      (z$dim_vec a)" by blast
    moreover have "real_of_int (2 * k * (k + 1) * (∑x = 0..<dim_vec a. ∣a $ x∣) + 1 ) ≠ 0"
    proof (rule ccontr, goal_cases)
    case 1
      then have eq: "real_of_int (∑x = 0..<dim_vec a. ∣a $ x∣) = - 1 / real_of_int (k * (k + 1))"
         using assms
         by (smt (verit, best) mult_minus_right of_int_hom.hom_0 pos_zmult_eq_1_iff 
          pos_zmult_eq_1_iff_lemma)
      have "k≥1" using assms by auto
      have "real_of_int (∑x = 0..<dim_vec a. ∣a $ x∣) ∈ ℤ" by auto
      moreover have "- 1 / real_of_int (k * (k + 1)) ∉ ℤ" using ‹k≥1›
      by (smt (verit, del_insts) "1" mult_pos_pos 
        mult_minus_right of_int_hom.hom_0 pos_zmult_eq_1_iff)
      ultimately show False using eq by auto
    qed
(*Problems here when changing 2*(k+1) to k*(k+1). 
  This is necessary since k'a only is smaller than k'' under the assumtion that z$i\<le>k, not z$i\<le>2.*)
    ultimately show ?thesis by auto
  qed
  ultimately have "z$i = 0" if "i < dim_vec z" for i using that suc_dim_a_dim_z
    by (cases ‹dim_vec a = i›) simp_all
  then show ?case
    by auto
qed



lemma insert_set_comprehension:
  "insert (f x) {f i |i. i<(x::nat)} = {f i | i. i<x+1}"
using less_SucE by fastforce

lemma bhle_k_pos:
  assumes "(a,k) ∈ bhle"
  shows "k>0"
using assms unfolding bhle_def 
proof (safe, goal_cases)
case (1 v)
  have "∃i<dim_vec v. ∣v $ i∣ > 0" using 1 by auto
  then have "∥v∥_\<infinity> > 0" unfolding linf_norm_vec_Max using 1 by (subst Max_gr_iff, auto)
  then show ?thesis using 1 by auto
qed 

lemma svp_k_pos:
  assumes "reduce_svp_bhle (a, k) ∈ gap_svp"
  shows "k>0"
proof -
  obtain v where v_in_lattice: "v∈gen_lattice (gen_svp_basis a k)" 
    and infnorm_v: "∥v∥_\<infinity> ≤ k" 
    and v_nonzero:  "v ≠ 0_v (dim_vec v)" 
    using assms unfolding reduce_svp_bhle_def gap_svp_def by force
  have "∃ i < dim_vec v. ∣v $ i∣ > 0" using v_nonzero by auto
  then have "∥v∥_\<infinity> > 0" unfolding linf_norm_vec_Max by (subst Max_gr_iff, auto)
  then show ?thesis using infnorm_v by auto
qed


lemma svp_dim_vec_a:
  assumes "reduce_svp_bhle (a, k) ∈ gap_svp"
  shows "dim_vec a > 0"
proof -
  have "2 ≤ dim_lattice (gen_lattice (gen_svp_basis a k))" 
    using assms unfolding reduce_svp_bhle_def gap_svp_def by auto
  then have "2 ≤ dim_col (gen_svp_basis a k)" 
    using dim_lattice_gen_lattice[of "gen_svp_basis a k",OF is_indep_gen_svp_basis]
      svp_k_pos[OF assms] by auto
  then show ?thesis unfolding gen_svp_basis_def by auto
qed

lemma bhle_dim_vec_a:
  assumes "(a, k) ∈ bhle"
  shows "dim_vec a > 0"
using assms unfolding bhle_def by auto


lemma first_lt_second:
  assumes "k>0" and z_le_k:"∧i. i< dim_vec a ==> ∣z $ i∣ ≤ k"
  shows "2 * ∣(k + 1) * (∑i = 0..<dim_vec a. z $ i * a $ i)∣
      < (∣2 * k * (k + 1) * (∑i = 0..<dim_vec a. ∣a $ i∣) + 1∣::int)"
proof - 
  have take_k1_out: "∣(k + 1) * (∑i = 0..<dim_vec a. z $ i * a $ i)∣ =
    (k+1) * ∣∑i=0..<dim_vec a. z $ i * a $ i∣"
    using ‹k>0› by (smt (verit, best) mult_minus_right mult_nonneg_nonneg)
  have "∣∑i = 0..<dim_vec a. z $ i * a $ i∣ ≤ (∑i = 0..<dim_vec a. ∣z $ i * a $ i∣)"
    by (subst sum_abs[of "(λi. z$i * a$i)" "{0..<dim_vec a}"],simp)
  also have "… = (∑i=0..<dim_vec a. ∣z $ i∣ * ∣a $ i∣)"
    by (meson abs_mult)
  also have "… ≤ (∑i=0..<dim_vec a. k * ∣a $ i∣)" 
    by (subst sum_mono) (auto simp add: z_le_k mult_right_mono)
  also have "… = k * (∑i=0..<dim_vec a. ∣a $ i∣)"
  by (metis mult_hom.hom_sum)
  finally have "∣(∑i=0..<dim_vec a. z $ i * a $ i)∣ ≤ k * (∑i=0..<dim_vec a. ∣a $ i∣)"
    by blast
  then show ?thesis using take_k1_out using ‹0 < k› by auto
qed


text ‹Well-definedness of reduction function›

lemma well_defined_reduction_svp:
  assumes "(a,k) ∈ bhle"
  shows "reduce_svp_bhle (a,k) ∈ gap_svp"
using assms unfolding reduce_svp_bhle_def gap_svp_def bhle_def
proof (safe, goal_cases)
  case (1 x)
  have "k>0" using assms bhle_k_pos by auto
  then show ?case using is_lattice_gen_lattice is_indep_gen_svp_basis by auto
next 
  case (2 x)
  have "dim_lattice (gen_lattice (gen_svp_basis a k)) = dim_col (gen_svp_basis a k)"
    using dim_lattice_gen_lattice assms bhle_k_pos is_indep_gen_svp_basis by presburger
  also have "… = dim_vec a + 1" unfolding gen_svp_basis_def by auto
  also have "… ≥ 2" using bhle_dim_vec_a[OF assms] by auto                              
  finally show ?case by auto
next
  case (3 x)
  let ?x = "vec (dim_vec x + 1) (λi. if i< dim_vec x then x$i else 0)"
  define v where "v = (gen_svp_basis a k) *_v ?x"
  have eigen_v: "v = ?x" unfolding v_def 
  apply (subst gen_svp_basis_mult[where a= a and k=k and z=" ?x"], auto simp add: 3(2) comp_def)
  apply (subst vec_eq_iff, auto simp add: 3(1) scalar_prod_def)
  proof (goal_cases one two)
    case (one i)
    then show ?case by (auto simp add: comp_def 3(2))
  next
    case (two i)
    have "(∑i = 0..<dim_vec a. (x $ i) * (a $ i)) = 0" 
      using 3 unfolding scalar_prod_def
      by (smt (verit) mult.commute of_int_hom.hom_zero of_int_mult of_int_sum sum.cong)
    then show ?case using 3 by auto
  qed
  have "dim_vec ?x = dim_col (gen_svp_basis a k)" 
    using 3(2) unfolding gen_svp_basis_def by auto
  then have "v ∈ gen_lattice (gen_svp_basis a k)"  
    unfolding v_def gen_lattice_def by auto
  moreover have "∥v∥_\<infinity> ≤ k" 
  proof -
    have "∥v∥_\<infinity> ≤ ∥x∥_\<infinity>" unfolding eigen_v linf_norm_vec_Max
    proof (rule Max.boundedI, goal_cases _ _ three)
    case (three b)
      have dim_x_nonzero: "dim_vec x ≠ 0" using 3(3) 3(2) by auto
      then have nonempty: "(∃a∈{∣x $ i∣ |i. i < dim_vec x}. 0 ≤ a)"
        using abs_ge_zero by blast
      have " ∣x $ i∣ ≤ Max (insert 0 {∣x $ j∣ |j. j < dim_vec x})" 
        if "i < dim_vec x" for i 
      using that by (subst Max_ge, auto)
      moreover have "0 ≤ Max (insert 0 {∣x $ i∣ |i. i < dim_vec x})" using 3 nonempty
        by (subst Max_ge_iff, auto)
      ultimately show ?case using three by auto
    qed auto
    then show ?thesis using 3 by auto
  qed
  moreover have "v ≠ 0_v (dim_vec v)" using 3(3) 
  proof (safe)
    assume "0 < dim_vec a" 
    assume "v = 0_v (dim_vec v)"
    have fst: "x ≠ 0_v (dim_vec x)" using 3(4) by blast
    have snd: "?x = 0_v (dim_vec v)" using ‹v = 0_v (dim_vec v)›  eigen_v by auto
    have "x$i = 0" if "i< dim_vec x" for i using snd
    by (smt (z3) add.commute dim_vec eigen_v index_map_vec(2) index_vec index_zero_vec(1) 
      of_int_eq_iff of_int_hom.hom_zero that 
      trans_less_add2)
  then show False using fst by auto
  qed
  ultimately show ?case by blast
qed





text ‹NP-hardness of reduction function›

lemma NP_hardness_reduction_svp:
  assumes "reduce_svp_bhle (a,k) ∈ gap_svp"
  shows "(a,k) ∈ bhle"
proof (cases "(∑i<dim_vec a. a$i) = 0")
  case True
  have a_nonempty: "dim_vec a > 0" using svp_dim_vec_a[OF assms] by auto
  have "k>0" using svp_k_pos[OF assms] by auto
  define x where "x = vec (dim_vec a) (λi. k)"
  have "a ∙ x = 0" unfolding x_def scalar_prod_def 
  by (auto simp add: True sum_distrib_right[symmetric])
     (metis True lessThan_atLeast0)
  moreover have "dim_vec x = dim_vec a" unfolding x_def by auto
  moreover have "x ≠ 0_v (dim_vec x)"
  proof -
    have "∃i< dim_vec x. x $ i ≠ 0" unfolding x_def using ‹k>0› a_nonempty by auto
    then show ?thesis using vec_eq_iff[of "x" "0_v (dim_vec x)"] by auto
  qed 
  moreover have "real_of_int (∥x∥_\<infinity>) ≤ k"
  proof -
    have "vec (dim_vec a) (λi. k) $ j = k" if "j < dim_vec a" for j using that by auto
    then have "Max {∣vec (dim_vec a) (λi. k) $ i∣ |i. i < dim_vec a} =
               Max {∣k∣ |i. i < dim_vec a}" by metis
    also have "… = Max {k}" using ‹k>0› a_nonempty
      by (smt (verit, best) Collect_cong singleton_conv)
    also have "… = k" by auto
    finally have "Max {∣vec (dim_vec a) (λi. k) $ i∣ |i. i < dim_vec a} = k" by blast
    then show ?thesis unfolding x_def linf_norm_vec_Max using ‹k>0› by auto 
  qed
  ultimately show ?thesis using assms unfolding reduce_svp_bhle_def gap_svp_def bhle_def
    by fastforce 
next
  case False
  show ?thesis using assms unfolding reduce_svp_bhle_def gap_svp_def bhle_def
  proof (safe, goal_cases)
    case (1 v)
    have a_nonempty: "dim_vec a > 0" using svp_dim_vec_a[OF assms] by auto  
    have "k>0"  unfolding linf_norm_vec_Max
    proof -
      have "∃i<dim_vec v. ∣v $ i∣ > 0" using 1 by auto
      then have "∥v∥_\<infinity> > 0" unfolding linf_norm_vec_Max by (subst Max_gr_iff, auto)
      then show ?thesis using 1 by auto
    qed
    then have "k≥1" by auto
    obtain z where z_def:
      "v = (gen_svp_basis a k) *_v z" 
      "dim_vec z = dim_vec a + 1"
      using 1 unfolding gen_lattice_def gen_svp_basis_def by auto
    have dim_v_dim_a:"dim_vec v = dim_vec a + 1" 
      using 1 unfolding gen_lattice_def gen_svp_basis_def by auto
    define x where "x = vec (dim_vec a) (($) z)"
    have v_eq_z_upto_last: "v $ i = z $ i" if "i< dim_vec a" for i 
      by (subst z_def) (subst gen_svp_basis_mult; use that z_def in ‹auto›)
    have v_le_k: "∣v $ i∣ ≤ k" if "i< dim_vec a + 1" for i
      using 1 dim_v_dim_a that unfolding linf_norm_vec_Max
      using Max_le_iff[of "{∣v $ i∣ |i. i < dim_vec v}" k]
      by fastforce
    then have z_le_k: "∣z $ i∣ ≤ k" if "i< dim_vec a" for i
      using v_eq_z_upto_last[OF that] that
      by (metis less_add_one less_trans)

    have v_last_zero: "v$(dim_vec a) = 0"
    proof (rule ccontr)
      assume ccontr_assms:"v $ dim_vec a ≠ 0"
      have v_last: "v$(dim_vec a) =
        (k+1) * (∑i = 0..<dim_vec a. z $ i * a $ i) +
        (2*k*(k+1) * (∑x = 0..<dim_vec a. ∣a $ x∣) + 1) * (z $ dim_vec a) "
        (is "v$(dim_vec a) = ?first + ?second")
        by (auto simp: z_def gen_svp_basis_mult_last)
      then have "?first ≠ 0 ∨ ?second ≠ 0"
        using ccontr_assms by auto
      then consider 
        (first) "?first ≠ 0 ∧ ?second = 0" | 
        (second) "?second ≠ 0 ∧ ?first = 0" |
        (both) "?first ≠ 0 ∧ ?second ≠ 0"
        by blast
      then show False 
      proof (cases)
        case first
        then have gr_1: "∣∑i = 0..<dim_vec a. z $ i * a $ i∣ ≥ 1" 
          using ‹k>0› by auto
        have "∣v$ dim_vec a∣ = ∣?first∣" using first v_last by auto
        also have "… = (k+1) * ∣∑i = 0..<dim_vec a. z $ i * a $ i∣"
          using ‹k>0›
          by (smt (z3) mult_le_0_iff mult_minus_right)
        also have "… > k" using first gr_1 ‹k>0›
        by (smt (verit, best) mult_le_cancel_left1)
        finally have "∣v$ dim_vec a∣ > k" by auto
        then show ?thesis using v_le_k[of "dim_vec a"] by auto
      next
        case second
        have "∣z $ dim_vec a∣ ≥ 1" using second by auto
        have sum_a_ge_1:"(∑x<dim_vec a. ∣a $ x∣) ≥1" 
          using False atLeast0LessThan
          by (metis abs_sum_abs int_one_le_iff_zero_less not_less sum_abs zero_less_abs_iff)
        then have "2*k*(k+1)*(∑x<dim_vec a. ∣a $ x∣) + 1 > k"
        proof -
          have "2*(k+1)*(∑x<dim_vec a. ∣a $ x∣)≥1" using ‹k>0›
            by (smt (verit, ccfv_SIG) int_distrib(2) sum_a_ge_1 zmult_zless_mono2)
          then show ?thesis using ‹k>0›
            by (smt (verit, best) pos_mult_pos_ge sum_a_ge_1)
        qed
        moreover have "∣?second∣ ≥ ∣2*k*(k+1)*(∑x<dim_vec a. ∣a $ x∣) + 1∣"
          using ‹∣z $ dim_vec a∣ ≥ 1›
          by (subst abs_mult) (simp add: lessThan_atLeast0 mult_le_cancel_left1)
        ultimately have "∣v $ dim_vec a∣ > k" using second v_last by linarith
        then show ?thesis using v_le_k[of "dim_vec a"] by auto
      next
        case both
        have z_gr_one:"∣real_of_int (z$dim_vec a)∣≥1" using both by auto
        let ?second' = "2 * k * (k + 1) * (∑i=0..<dim_vec a. ∣a $ i∣) + 1"
        have "(∑i = 0..<dim_vec a. z $ i * a $ i) ≠ 0" using both by auto
        then have one: "k < ∣?first∣"
          by (smt (z3) mult_less_cancel_left2 mult_minus_right)
        then have first_nonzero: "∣?first∣ ≠ 0" using ‹k>0› by auto
        have two'':"2 * ∣?first∣ < ∣?second'∣"
          using first_lt_second[OF ‹k>0› z_le_k] by auto
        then have two': "∣real_of_int ?second' / real_of_int ?first∣ > 2" 
        proof - 
          have "0<real_of_int ∣?first∣" using first_nonzero by presburger
          have "2 * real_of_int ∣?first∣ < real_of_int ∣?second'∣" using two'' by linarith
          then have "2 < real_of_int ∣?second'∣ / real_of_int ∣?first∣" 
            by (subst pos_less_divide_eq[OF ‹0<real_of_int ∣?first∣›], auto)
          also have "… = ∣real_of_int ?second' / real_of_int ?first∣" by simp
          finally show ?thesis by presburger
        qed
        then have two:"∣(real_of_int ?second' / real_of_int ?first) *
            real_of_int (z$dim_vec a)∣ > 2"
        proof -
          have "∣(real_of_int ?second' / real_of_int ?first) *
            real_of_int (z$dim_vec a)∣ = ∣real_of_int ?second' / real_of_int ?first∣ *
            ∣real_of_int (z$dim_vec a)∣" by (subst abs_mult, auto)
          also have ineq: "… ≥ ∣real_of_int ?second' / real_of_int ?first∣"
            using z_gr_one by (smt (z3) mult_less_cancel_left2)
          finally have "∣(real_of_int ?second' / real_of_int ?first) *
            real_of_int (z$dim_vec a)∣≥ ∣real_of_int ?second' / real_of_int ?first∣" by blast
          then show ?thesis using two' by linarith
        qed
        have "real_of_int ∣v $ dim_vec a∣ / real_of_int ∣?first∣ ≥ 1"
        proof -
          have "real_of_int ∣v $ dim_vec a∣ / real_of_int ∣?first∣ =
            ∣real_of_int (v $ dim_vec a)∣ / ∣real_of_int ?first∣"
            using of_int_abs[of "v $ dim_vec a"] of_int_abs[of "?first"] by auto
          also have "… = ∣real_of_int (v $ dim_vec a) / real_of_int ?first∣"
            using abs_divide[symmetric] by auto
          also have "… = ∣(real_of_int ?first + real_of_int ?second' * real_of_int (z$dim_vec a)) /
            real_of_int ?first∣" using v_last by auto
          also have "… = ∣real_of_int ?first / real_of_int ?first +
            (real_of_int ?second' / real_of_int ?first)* real_of_int (z$dim_vec a)∣"
            by (metis (no_types, lifting) add_divide_distrib times_divide_eq_left)
          also have "… = ∣1 + (real_of_int ?second' / real_of_int ?first) *
            real_of_int (z$dim_vec a)∣"
            using first_nonzero by (smt (verit, del_insts) of_int_eq_0_iff one_eq_divide_iff)
          also have "… ≥ 1" using two by linarith
          finally show "real_of_int ∣v $ dim_vec a∣ / real_of_int ∣?first∣ ≥ 1" by blast
        qed
        then have "real_of_int ∣v $ dim_vec a∣ ≥ real_of_int ∣?first∣"
          by (simp add: le_divide_eq_1)
        then have "∣v $ dim_vec a∣ ≥ ∣?first∣" using of_int_le_iff by blast
        then have "∣v $ dim_vec a∣ > k" using one by auto
        then show ?thesis using v_le_k[of "dim_vec a"] by auto
      qed
    qed
    have z_last_zero: "z$dim_vec a = 0" 
    proof (rule ccontr)
      assume ccontr_assms:"z $ dim_vec a ≠ 0"
      then have "∣z $ dim_vec a∣ ≥ 1" by auto
      have "(k+1) * (∑ i ∈ {0 ..< dim_vec a}. z $ i * a $ i) +
        (2*k*(k+1)* (∑ i ∈ {0 ..< dim_vec a}. ∣a $ i∣) +1) * (z$(dim_vec a)) = 0"
        (is "?first + ?second * (z$(dim_vec a)) = 0")
        using v_last_zero z_def gen_svp_basis_mult_last by auto
      then have abs_eq: "∣?first∣ = ∣?second * (z$(dim_vec a))∣" by linarith
      moreover have "∣?first∣ < ∣?second * (z$(dim_vec a))∣"
      proof - 
        have "∣?first∣ ≤ 2*∣?first∣" by auto
        then have "∣?first∣ < ∣?second∣" using first_lt_second[OF ‹k>0› z_le_k, of a] by auto
        moreover have "∣?second∣ ≤ ∣?second∣*∣z$dim_vec a∣" 
          using ‹∣z $ dim_vec a∣ ≥ 1› by (simp add: mult_le_cancel_left1)
        ultimately have "∣?first∣ < ∣?second∣*∣z$dim_vec a∣" by linarith
        then show ?thesis by linarith
      qed
      ultimately show False by auto
    qed
 
    have v_real_z: "v = z" using v_eq_z_upto_last v_last_zero z_last_zero
      by (metis Suc_eq_plus1 dim_v_dim_a less_Suc_eq vec_eq_iff z_def(2))

    have "a ∙ x = 0" 
    proof -
      have "0 = ((gen_svp_basis a k) *_v z) $ (dim_vec a)" 
        using v_last_zero z_def by auto
      also have "… = (k+1) * (∑ i ∈ {0 ..< dim_vec a}. z $ i * a $ i)" 
        by (subst gen_svp_basis_mult, auto simp add: z_def z_last_zero)
      finally have zero: "(k+1) * (∑ i ∈ {0 ..< dim_vec a}. z $ i * a $ i) = 0" by auto
      then show ?thesis unfolding scalar_prod_def using x_def ‹k>0›
      by (smt (verit, ccfv_SIG) atLeastLessThan_iff dim_vec index_vec mult.commute
         mult_eq_0_iff of_int_hom.hom_0 sum.cong)
    qed
    moreover have "dim_vec x = dim_vec a" unfolding x_def by auto
    moreover have "x ≠ 0_v (dim_vec x)" 
    proof -
      have "∃i≤dim_vec a. v$i ≠ 0" using 1 unfolding gen_lattice_def gen_svp_basis_def by auto
      then obtain i where ‹i ≤ dim_vec a› ‹v $ i ≠ 0› by blast
      then have ‹dim_vec a ≠ i› using v_last_zero by auto
      with ‹i ≤ dim_vec a› have ‹i < dim_vec a› by simp
      with ‹v $ i ≠ 0› have "z $ i ≠ 0" using v_real_z z_def 
        by auto
      then have "∃i< dim_vec a. x$i ≠ 0" using x_def ‹i<dim_vec a› by auto
      then show ?thesis using x_def by auto
    qed
    moreover have "∥x∥_\<infinity> ≤ k"
    proof - 
      have "∣z$i∣ = ∣vec (dim_vec a) (($) z) $ i∣" if "i < dim_vec a" for i using that by auto
      then have "Max (insert 0 {∣vec (dim_vec a) (($) z) $ i∣ |i. i < dim_vec a}) =
            Max (insert 0 {∣z $ i∣ |i. i < dim_vec a})" 
        by (smt (z3) Collect_cong Setcompr_eq_image mem_Collect_eq)
      also have "… = Max (insert 0 {∣z $ i∣ |i. i < dim_vec a + 1})" 
      proof -
        have "Max (insert 0 {∣z $ i∣ |i. i < dim_vec a}) =
          Max (insert 0 (insert ( ∣z$dim_vec a∣) {∣z $ i∣ |i. i < dim_vec a}))"
        proof -
          have "Max {∣z $ i∣ |i. i < dim_vec a} ≥ 0" 
            using ‹dim_vec a >0› by (subst Max_ge_iff, auto)
          then have "Max {∣z $ i∣ |i. i < dim_vec a} ≥ ∣z$dim_vec a∣"
            using z_last_zero by simp
          then have max_subst: "Max {∣z $ i∣ |i. i < dim_vec a} =
              Max (insert ∣z $ dim_vec a∣ {∣z $ i∣ |i. i < dim_vec a})" 
            using ‹dim_vec a > 0› by (subst Max_insert)+ (auto)
          then show ?thesis using ‹dim_vec a > 0› by (subst Max_insert)+ (auto)
        qed
        then show ?thesis 
          using insert_set_comprehension[of "(λi. ∣z $ i∣)" "dim_vec a"] by auto
      qed
      finally have "Max (insert 0 {∣vec (dim_vec a) (($) z) $ i∣ |i. i < dim_vec a}) =
                    Max (insert 0 {∣z $ i∣ |i. i < dim_vec a +1})"
        by blast
      then have "∥x∥_\<infinity> = ∥v∥_\<infinity>" unfolding linf_norm_vec_Max
        using x_def z_def v_real_z  by auto
      then show ?thesis using 1 by auto
    qed
    ultimately show ?case by force
  qed
qed


text ‹The SVP is NP-hard in $\ell_\infty$.›
lemma "is_reduction reduce_svp_bhle bhle gap_svp"
unfolding is_reduction_def
  using NP_hardness_reduction_svp well_defined_reduction_svp by fastforce

end