Theory SVP_vec

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)  (xL. x  v  vL) "


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)  
      (vL. v  r  v  0v (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 |}$ 
in 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 "k1" 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 k1 
      by (smt (verit, del_insts) "1" linordered_semiring_strict_class.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≤k, not z$i≤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 > 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: "vgen_lattice (gen_svp_basis a k)" 
    and infnorm_v: "v  k" 
    and v_nonzero:  "v  0v (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 > 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  k" 
  proof -
    have "v  x" 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  0v (dim_vec v)" using 3(3) 
  proof (safe)
    assume "0 < dim_vec a" 
    assume "v = 0v (dim_vec v)"
    have fst: "x  0v (dim_vec x)" using 3(4) by blast
    have snd: "?x = 0v (dim_vec v)" using v = 0v (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  0v (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" "0v (dim_vec x)"] by auto
  qed 
  moreover have "real_of_int (x)  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 > 0" unfolding linf_norm_vec_Max by (subst Max_gr_iff, auto)
      then show ?thesis using 1 by auto
    qed
    then have "k1" 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  0v (dim_vec x)" 
    proof -
      have "idim_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  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 = v" 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
proof (safe, goal_cases)
  case (1 as s)
  then show ?case using well_defined_reduction_svp by auto
next
  case (2 as s)
  then show ?case using NP_hardness_reduction_svp by auto
qed



end