Theory BHLE
theory BHLE
imports
Main
Additional_Lemmas
begin
section ‹Bounded Homogeneous Linear Equation Problem›
definition bhle :: "(int vec * int) set" where
"bhle ≡ {(a,k). ∃x. a ∙ x = 0 ∧ dim_vec x = dim_vec a ∧ dim_vec a > 0 ∧
x ≠ 0⇩v (dim_vec x) ∧ ∥x∥⇩∞ ≤ k}"
text ‹Reduction of bounded homogeneous linear equation to partition problem›
text ‹For the reduction function, one defines five-tuples for every element in a.
The last tuple plays an important role. It consists only of four elements in order
to add constraints to the other tuples.
These values are formed in a way such that they form all constraints needed for the
reductions.
Note, that some indices have been changed with respect to \cite{EmBo81}
to enable better indexing in the vectors/lists.›
definition b1 :: "nat ⇒ int ⇒ int ⇒ int" where
"b1 i M a = a + M * (5^(4*i-4) + 5^(4*i-3) + 5^(4*i-1))"
definition b2 :: "nat ⇒ int ⇒ int" where
"b2 i M = M * (5^(4*i-3) + 5^(4*i))"
definition b2_last :: "nat ⇒ int ⇒ int" where
"b2_last i M = M * (5^(4*i-3) + 1)"
definition b3 :: "nat ⇒ int ⇒ int" where
"b3 i M = M * (5^(4*i-4) + 5^(4*i-2))"
definition b4 :: "nat ⇒ int ⇒ int ⇒ int" where
"b4 i M a = a + M * (5^(4*i-2) + 5^(4*i-1) + 5^(4*i))"
definition b4_last :: "nat ⇒ int ⇒ int ⇒ int" where
"b4_last i M a = a + M * (5^(4*i-2) + 5^(4*i-1) + 1)"
definition b5 :: "nat ⇒ int ⇒ int" where
"b5 i M = M * (5^(4*i-1))"
text ‹Change order of indices in \cite{EmBo81} such that $b3$ is in last place and can be omitted
in the last entry. This ensures that the weight of the solution is $1$ or $-1$,
essential for the proof of NP-hardnes.›
definition b_list :: "int list ⇒ nat ⇒ int ⇒ int list" where
"b_list as i M = [b1 (i+1) M (as!i), b2 (i+1) M, b4 (i+1) M (as!i), b5 (i+1) M, b3 (i+1) M]"
definition b_list_last :: "int list ⇒ nat ⇒ int ⇒ int list" where
"b_list_last as n M = [b1 n M (last as), b2_last n M, b4_last n M (last as), b5 n M]"
definition gen_bhle :: "int list ⇒ int vec" where
"gen_bhle as = (let M = 2*(∑i<length as. ¦as!i¦)+1; n = length as in
vec_of_list (concat
(map (λi. b_list as i M) [0..<n-1])
@ (if n>0 then b_list_last as n M else [])))"
text ‹The reduction function.›
definition reduce_bhle_partition:: "(int list) ⇒ ((int vec) * int)" where
"reduce_bhle_partition ≡ (λ a. (gen_bhle a, 1))"
text ‹Lemmas for proof›
lemma dim_vec_gen_bhle:
assumes "as≠[]"
shows "dim_vec (gen_bhle as) = 5 * (length as) - 1"
using assms
proof (induct as rule: list_nonempty_induct)
case (single x)
then show ?case unfolding gen_bhle_def Let_def b_list_def b_list_last_def by auto
next
case (cons x xs)
define M where "M = (2 * (∑i<length (x # xs). ¦(x # xs) ! i¦) + 1)"
then show ?case using cons unfolding gen_bhle_def b_list_def b_list_last_def
Let_def M_def[symmetric]
by (subst dim_vec_of_list)+
(use length_concat_map_5[of
"(λi. b1 (i + 1) M ((x#xs) ! i))"
"(λi. b2 (i + 1) M )"
"(λi. b4 (i + 1) M ((x#xs) ! i))"
"(λi. b5 (i + 1) M )"
"(λi. b3 (i + 1) M )"] in ‹simp›)
qed
lemma dim_vec_gen_bhle_empty:
"dim_vec (gen_bhle []) = 0"
unfolding gen_bhle_def by auto
text ‹Lemmas about length›
lemma length_b_list:
"length (b_list a i M) = 5" unfolding b_list_def by auto
lemma length_b_list_last:
"length (b_list_last a n M) = 4" unfolding b_list_last_def by auto
lemma length_concat_map_b_list:
"length (concat (map (λi. b_list as i M) [0..<k])) = 5 * k"
by (subst length_concat)(simp add: comp_def length_b_list sum_list_triv)
text ‹Last values of ‹gen_bhle››
lemma gen_bhle_last0:
assumes "length as > 0"
shows "(gen_bhle as) $ ((length as -1) * 5) =
b1 (length as) (2*(∑i<length as. ¦as!i¦)+1) (last as)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1), goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_splits,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
then show ?case using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(auto split: if_splits simp add: b_list_last_def)
qed
lemma gen_bhle_last1:
assumes "length as > 0"
shows "(gen_bhle as) $ ((length as -1) * 5 + 1) =
b2_last (length as) (2*(∑i<length as. ¦as!i¦)+1)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1),
goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
then show ?case using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(auto split: if_splits simp add: b_list_last_def)
qed
text ‹The third entry of the last tuple is omitted, thus we skip one lemma›
lemma gen_bhle_last3:
assumes "length as > 0"
shows "(gen_bhle as) $ ((length as -1) * 5 + 2) =
b4_last (length as) (2*(∑i<length as. ¦as!i¦)+1) (last as)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1),
goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
then show ?case using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(auto split: if_splits simp add: b_list_last_def)
qed
lemma gen_bhle_last4:
assumes "length as > 0"
shows "(gen_bhle as) $ ((length as-1) * 5 + 3) =
b5 (length as) (2*(∑i<length as. ¦as!i¦)+1)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1),
goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
then show ?case using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(auto split: if_splits simp add: b_list_last_def)
qed
text ‹Up to last values of ‹gen_bhle››
lemma b_list_nth:
assumes "i<length as-1" "j<5"
shows "concat (map (λi. b_list as i M) [0..<length as - 1]) ! (i * 5 + j) =
b_list as i M ! j"
proof -
have "map (λi. b_list as i M) [0..<length as - 1] =
map (λi. b_list as i M) [0..<i] @
map (λi. b_list as i M) [i..<length as - 1]"
using assms
by (metis append_self_conv2 less_zeroE linorder_neqE_nat map_append upt.simps(1) upt_append)
then have "concat (map (λi. b_list as i M) [0..<length as - 1]) =
concat (map (λi. b_list as i M) [0..<i]) @
concat (map (λi. b_list as i M) [i..<length as - 1])"
by (subst concat_append[of "map (λi. b_list as i M) [0..<i]"
"map (λi. b_list as i M) [i..<length as -1]", symmetric], auto)
moreover have "concat (map (λi. b_list as i M) [i..<length as - 1]) =
(b_list as i M @ concat (map (λi. b_list as i M) [i+1..<length as - 1]))"
using assms upt_conv_Cons by fastforce
ultimately have concat_unfold: "concat (map (λi. b_list as i M) [0..<length as - 1]) =
concat (map (λi. b_list as i M) [0..<i]) @
(b_list as i M @ concat (map (λi. b_list as i M) [i+1..<length as - 1]))"
by auto
have "concat (map (λi. b_list as i M) [0..<length as - 1]) ! (i * 5 + j) =
(b_list as i M @ concat (map (λi. b_list as i M) [i+1..<length as - 1])) ! j"
unfolding concat_unfold
by (subst nth_append_length_plus[of "concat (map (λi. b_list as i M) [0..<i])"
"b_list as i M @ concat (map (λi. b_list as i M) [i + 1..<length as - 1])" j, symmetric])
(subst length_concat_map_b_list, simp add: mult.commute)
moreover have "(b_list as i M @ concat (map (λi. b_list as i M) [i+1..<length as - 1])) ! j =
b_list as i M ! j" using assms length_b_list
by (subst nth_append[of "b_list as i M" "concat (map (λi. b_list as i M)
[i+1..<length as - 1])" j], auto)
ultimately show ?thesis by auto
qed
lemma b_list_nth0:
assumes "i<length as-1"
shows "concat (map (λi. b_list as i M) [0..<length as - 1]) ! (i * 5) =
b_list as i M ! 0"
using b_list_nth[OF assms, of 0] by auto
lemma gen_bhle_0:
assumes "i<length as-1"
shows "(gen_bhle as) $ (i * 5) =
b1 (i+1) (2*(∑i<length as. ¦as!i¦)+1) (as!i)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1), goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
define M where "M = (2 * (∑i<length as. ¦as ! i¦) + 1)"
then show ?case unfolding M_def[symmetric] using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(subst b_list_nth0[OF assms, of M], auto split: if_splits, simp add: b_list_def)
qed
lemma gen_bhle_1:
assumes "i<length as-1"
shows "(gen_bhle as) $ (i * 5 + 1) =
b2 (i+1) (2*(∑i<length as. ¦as!i¦)+1)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1), goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
define M where "M = (2 * (∑i<length as. ¦as ! i¦) + 1)"
then show ?case unfolding M_def[symmetric] using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(subst b_list_nth[OF assms, of 1 M], auto split: if_splits, simp add: b_list_def)
qed
lemma gen_bhle_4:
assumes "i<length as-1"
shows "(gen_bhle as) $ (i * 5 + 4) =
b3 (i+1) (2*(∑i<length as. ¦as!i¦)+1)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1), goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
define M where "M = (2 * (∑i<length as. ¦as ! i¦) + 1)"
then show ?case unfolding M_def[symmetric] using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(subst b_list_nth[OF assms, of 4 M], auto split: if_splits, simp add: b_list_def)
qed
lemma gen_bhle_2:
assumes "i<length as-1"
shows "(gen_bhle as) $ (i * 5 + 2) =
b4 (i+1) (2*(∑i<length as. ¦as!i¦)+1) (as!i)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1), goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
define M where "M = (2 * (∑i<length as. ¦as ! i¦) + 1)"
then show ?case unfolding M_def[symmetric] using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(subst b_list_nth[OF assms, of 2 M], auto split: if_splits, simp add: b_list_def)
qed
lemma gen_bhle_3:
assumes "i<length as-1"
shows "(gen_bhle as) $ (i * 5 + 3) =
b5 (i+1) (2*(∑i<length as. ¦as!i¦)+1)"
unfolding gen_bhle_def Let_def
proof (subst vec_of_list_append, subst index_append_vec(1), goal_cases)
case 1
then show ?case using assms
by (subst dim_vec_of_list)+ (split if_split,
subst length_b_list_last, subst length_concat_map_b_list, auto)
next
case 2
define M where "M = (2 * (∑i<length as. ¦as ! i¦) + 1)"
then show ?case unfolding M_def[symmetric] using assms
by (subst dim_vec_of_list, subst length_concat_map_b_list, subst vec_index_vec_of_list)+
(subst b_list_nth[OF assms, of 3 M], auto split: if_splits, simp add: b_list_def)
qed
text ‹Well-definedness of reduction function›
lemma well_defined_reduction_subset_sum:
assumes "a ∈ partition_problem_nonzero"
shows "reduce_bhle_partition a ∈ bhle"
using assms unfolding partition_problem_nonzero_def reduce_bhle_partition_def bhle_def
proof (safe, goal_cases)
case (1 I)
text ‹Given a subset $I$, we must construct a vector $x$ such that the properties of ‹bhle› hold.›
have "finite I" using 1 by (meson subset_eq_atLeast0_lessThan_finite)
have "length a > 0" using ‹a≠[]› by auto
define n where "n = length a"
define minus_x::"int list" where "minus_x = [0,0,-1,1,1]"
define plus_x::"int list" where "plus_x = [1,-1,0,-1,0]"
define plus_x_last::"int list" where "plus_x_last = [1,-1,0,-1]"
define plus_minus::"int list" where "plus_minus = (if n-1∈I then plus_x else minus_x)"
define minus_plus::"int list" where "minus_plus = (if n-1∈I then minus_x else plus_x)"
define x::"int vec" where
"x = vec_of_list(concat (map (λi. if i∈I then plus_minus else minus_plus) [0..<n-1])
@ plus_x_last)"
have length_plus_minus: "length plus_minus = 5"
unfolding plus_minus_def plus_x_def minus_x_def by auto
have length_minus_plus: "length minus_plus = 5"
unfolding minus_plus_def plus_x_def minus_x_def by auto
have length_concat_map: "length (concat (map (λi. if i ∈ I then plus_minus else minus_plus)
[0..<b])) = b*5" for b
using length_plus_minus length_minus_plus by (induct b, auto)
have dimx_eq_5dima:"dim_vec x = length a * 5 - 1"
unfolding x_def dim_vec_of_list length_append length_concat_map plus_x_last_def
using ‹length a > 0› unfolding n_def[symmetric] by auto
have "0 < dim_vec x" unfolding dimx_eq_5dima using ‹length a > 0› by linarith
define M where "M = 2*(∑i<length a. ¦a!i¦)+1"
text ‹Some conditional lemmas for the proof.›
have x_nth:
"x $ (i*5+j) = (if i∈I then plus_minus ! j else minus_plus ! j)" if "i<n-1" "j<5" for i j
proof -
have lt: "i * 5 + j < length (concat (map (λi. if i ∈ I then plus_minus else minus_plus)
[0..<n - 1]))"
using that length_concat_map by auto
have len_rew: "i*5 = length (concat (map (λi. if i ∈ I then plus_minus else minus_plus)
[0..<i]))"
proof -
have if_rew: "(λi. if i∈I then plus_minus else minus_plus) =
(λi. [(if i∈I then plus_minus!0 else minus_plus!0),
(if i∈I then plus_minus!1 else minus_plus!1),
(if i∈I then plus_minus!2 else minus_plus!2),
(if i∈I then plus_minus!3 else minus_plus!3),
(if i∈I then plus_minus!4 else minus_plus!4)])"
unfolding plus_minus_def minus_plus_def plus_x_def minus_x_def by auto
then show ?thesis
unfolding if_rew length_concat_map_5[of
"(λi. if i∈I then plus_minus!0 else minus_plus!0)"
"(λi. if i∈I then plus_minus!1 else minus_plus!1)"
"(λi. if i∈I then plus_minus!2 else minus_plus!2)"
"(λi. if i∈I then plus_minus!3 else minus_plus!3)"
"(λi. if i∈I then plus_minus!4 else minus_plus!4)"
"[0..<i]"] by auto
qed
have map_rew: "map f [0..<n-1] = map f [0..<i] @ map f [i..<n-1]"
for f ::"nat ⇒ int list"
using that(1) by (metis append_Nil map_append not_gr_zero upt_0 upt_append)
have "concat (map (λi. if i ∈ I then plus_minus else minus_plus) [0..<n-1]) ! (i * 5 + j) =
concat (map (λi. if i ∈ I then plus_minus else minus_plus) [i..<n-1]) ! j"
by (subst map_rew, subst concat_append, subst len_rew)
(subst nth_append_length_plus[of
"concat (map (λi. if i ∈ I then plus_minus else minus_plus) [0..<i])"], simp)
also have "… = (if i ∈ I then plus_minus!j else minus_plus!j)"
proof -
have concat_rewr: "concat (map f [i..<n-1])=
(f i) @ (concat (map f [i+1..<n-1]))" for f::"nat ⇒ int list"
using that(1) upt_conv_Cons by force
have length_if: "length (if i ∈ I then plus_minus else minus_plus) = 5"
using length_plus_minus length_minus_plus by auto
show ?thesis unfolding concat_rewr nth_append length_if using ‹j<5› by auto
qed
finally show ?thesis unfolding x_def by (subst vec_index_vec_of_list)
(subst nth_append, use lt in ‹auto›)
qed
have x_nth0:
"x $ (i*5) = (if i∈I then plus_minus ! 0 else minus_plus ! 0)" if "i<n-1" for i
using that by (subst x_nth[of i 0,symmetric], auto)
have x_nth_last:
"x $ ((length a -1)*5+j) = plus_x_last ! j"
if "j<4" for j
using that unfolding x_def vec_of_list_index using nth_append_length_plus[of
"concat (map (λi. if i ∈ I then plus_minus else minus_plus) [0..<n - 1])"
"plus_x_last" j] unfolding length_concat_map n_def
by auto
have x_nth0_last:
"x $ ((length a-1) *5) = plus_x_last ! 0"
by (subst x_nth_last[of 0,symmetric], auto)
have gen_bhle_in_I_plus:
"(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M)" if "i∈I-{length a-1}" "n-1∈I" for i
proof -
have "(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(gen_bhle a) $ (i*5) * x $ (i*5) +
(gen_bhle a) $ (i*5+1) * x $ (i*5+1) +
(gen_bhle a) $ (i*5+2) * x $ (i*5+2) +
(gen_bhle a) $ (i*5+3) * x $ (i*5+3) +
(gen_bhle a) $ (i*5+4) * x $ (i*5+4)"
by (simp add: eval_nat_numeral)
also have "… = (b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M)"
using that 1 n_def ‹length a > 0›
apply (subst gen_bhle_0[of i a], fastforce)
apply (subst gen_bhle_1[of i a], fastforce)
apply (subst gen_bhle_2[of i a], fastforce)
apply (subst gen_bhle_3[of i a], fastforce)
apply (subst gen_bhle_4[of i a], fastforce)
apply (subst x_nth[of i], fastforce, fastforce)+
apply (subst x_nth0[of i], fastforce)
apply (unfold M_def plus_minus_def minus_plus_def plus_x_def minus_x_def)
apply (simp add: eval_nat_numeral)
done
finally show ?thesis by auto
qed
have gen_bhle_in_I_minus:
"(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M)" if "i∈I-{length a-1}" "n-1∉I" for i
proof -
have "(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(gen_bhle a) $ (i*5) * x $ (i*5) +
(gen_bhle a) $ (i*5+1) * x $ (i*5+1) +
(gen_bhle a) $ (i*5+2) * x $ (i*5+2) +
(gen_bhle a) $ (i*5+3) * x $ (i*5+3) +
(gen_bhle a) $ (i*5+4) * x $ (i*5+4)"
by (simp add: eval_nat_numeral)
also have "… = (b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M)"
using that 1 n_def ‹length a > 0›
apply (subst gen_bhle_0[of i a], fastforce)
apply (subst gen_bhle_1[of i a], fastforce)
apply (subst gen_bhle_2[of i a], fastforce)
apply (subst gen_bhle_3[of i a], fastforce)
apply (subst gen_bhle_4[of i a], fastforce)
apply (subst x_nth[of i], fastforce, fastforce)+
apply (subst x_nth0[of i], fastforce)
apply (unfold M_def plus_minus_def minus_x_def)
apply (simp add: eval_nat_numeral)
done
finally show ?thesis by auto
qed
have gen_bhle_not_in_I_plus:
"(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M)" if "i∈{0..<n}-I-{n-1}" "n-1∈I" for i
proof -
have "(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(gen_bhle a) $ (i*5) * x $ (i*5) +
(gen_bhle a) $ (i*5+1) * x $ (i*5+1) +
(gen_bhle a) $ (i*5+2) * x $ (i*5+2) +
(gen_bhle a) $ (i*5+3) * x $ (i*5+3) +
(gen_bhle a) $ (i*5+4) * x $ (i*5+4)"
by (simp add: eval_nat_numeral)
also have "… = (b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M)"
using that 1 n_def ‹length a > 0›
apply (subst gen_bhle_0[of i a], fastforce)
apply (subst gen_bhle_1[of i a], fastforce)
apply (subst gen_bhle_2[of i a], fastforce)
apply (subst gen_bhle_3[of i a], fastforce)
apply (subst gen_bhle_4[of i a], fastforce)
apply (subst x_nth[of i], fastforce, fastforce)+
apply (subst x_nth0[of i], fastforce)
apply (unfold M_def minus_plus_def minus_x_def)
apply (simp add: eval_nat_numeral)
done
finally show ?thesis by auto
qed
have gen_bhle_not_in_I_minus:
"(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M)" if "i∈{0..<n}-I-{n-1}" "n-1∉I" for i
proof -
have "(∑j=0..<5. (gen_bhle a) $ (i*5+j) * x $ (i*5+j)) =
(gen_bhle a) $ (i*5) * x $ (i*5) +
(gen_bhle a) $ (i*5+1) * x $ (i*5+1) +
(gen_bhle a) $ (i*5+2) * x $ (i*5+2) +
(gen_bhle a) $ (i*5+3) * x $ (i*5+3) +
(gen_bhle a) $ (i*5+4) * x $ (i*5+4)"
by (simp add: eval_nat_numeral)
also have "… = (b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M)"
using that 1 n_def ‹length a > 0›
apply (subst gen_bhle_0[of i a], fastforce)
apply (subst gen_bhle_1[of i a], fastforce)
apply (subst gen_bhle_2[of i a], fastforce)
apply (subst gen_bhle_3[of i a], fastforce)
apply (subst gen_bhle_4[of i a], fastforce)
apply (subst x_nth[of i], fastforce, fastforce)+
apply (subst x_nth0[of i], fastforce)
apply (unfold M_def minus_plus_def plus_x_def)
apply (simp add: eval_nat_numeral)
done
finally show ?thesis by auto
qed
have gen_bhle_last:
"(∑j=0..<4. (gen_bhle a) $ ((n-1)*5+j) * x $ ((n-1)*5+j)) =
(b1 n M (a!(n-1))) - (b2_last n M) - (b5 n M)"
proof -
have "(∑j=0..<4. (gen_bhle a) $ ((n-1)*5+j) * x $ ((n-1)*5+j)) =
(gen_bhle a) $ ((n-1)*5) * x $ ((n-1)*5) +
(gen_bhle a) $ ((n-1)*5+1) * x $ ((n-1)*5+1) +
(gen_bhle a) $ ((n-1)*5+2) * x $ ((n-1)*5+2) +
(gen_bhle a) $ ((n-1)*5+3) * x $ ((n-1)*5+3)"
by (simp add: eval_nat_numeral)
also have "… = (b1 n M (a!(n-1))) - (b2_last n M) - (b5 n M)"
using 1 n_def ‹length a > 0› unfolding n_def
apply (subst gen_bhle_last0[of a, OF ‹length a > 0›])
apply (subst gen_bhle_last1[of a, OF ‹length a > 0›])
apply (subst gen_bhle_last3[of a, OF ‹length a > 0›])
apply (subst gen_bhle_last4[of a, OF ‹length a > 0›])
apply (subst x_nth_last, simp)+
apply (subst x_nth0_last, simp add: n_def)
apply (unfold M_def plus_x_last_def)
apply (auto simp add: eval_nat_numeral last_conv_nth)
done
finally show ?thesis by auto
qed
text ‹The actual proof. ›
have "(gen_bhle a) ∙ x = 0"
proof -
define f where "f = (λi. (∑j = 0..<5. gen_bhle a $ (i*5+j) * x $ (i*5+j)))"
have "(gen_bhle a) ∙ x = (∑i<n*5 -1. (gen_bhle a) $ i * x $ i) "
unfolding M_def n_def gen_bhle_def scalar_prod_def dimx_eq_5dima
using lessThan_atLeast0 by auto
also have "… = (∑i<(n-1)*5. (gen_bhle a) $ i * x $ i) +
(∑i = (n-1)*5..<(n-1)*5 +4. (gen_bhle a) $ i * x $ i)"
proof (subst split_sum_mid_less[of "(n-1)*5" "n*5-1"], goal_cases)
case 1
then show ?case unfolding n_def using ‹0 < length a› by linarith
next
case 2
have "n * 5 - 1 = (n-1) * 5 + 4" unfolding n_def using ‹0 < length a› by linarith
then show ?case by auto
qed
also have "… = (∑i = 0..<n-1. f i) +
(∑j=0..<4. gen_bhle a $ ((n-1)*5+j) * x $ ((n-1)*5+j))"
proof -
have *: "(+) ((n - 1) * 5) ` {0..<4} = {(n-1)*5..<(n-1)*5+4}" by auto
have "(∑i = (n - 1) * 5..<(n - 1) * 5 + 4. gen_bhle a $ i * x $ i) =
(∑j = 0..<4. gen_bhle a $ ((n - 1) * 5 + j) * x $ ((n - 1) * 5 + j))"
using sum.reindex[of "(λj. (n-1)*5+j)" "{0..<4}" "(λi. gen_bhle a $ i * x $ i)"]
unfolding comp_def * by auto
then show ?thesis unfolding f_def lessThan_atLeast0
by (subst sum_split_idx_prod[of "(λi. (gen_bhle a) $ i * x $ i)" "n-1" 5], auto)
qed
also have "… = (∑i∈I-{n-1}. f i) + (∑i∈{0..<n}-I-{n-1}. f i) +
(∑j=0..<4. gen_bhle a $ ((n-1)*5+j) * x $ ((n-1)*5+j))"
proof -
have "I - {n - 1} ∪ (({0..<n} - I) - {n - 1}) = {0..<n-1}"
using "1"(1) n_def by auto
then show ?thesis
by (subst sum.union_disjoint[of "I - {n - 1}" "{0..<n} - I - {n - 1}", symmetric])
(auto simp add: ‹finite I›)
qed
also have "… = M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ M * 5^(4*n-4) - M"
proof (cases "n-1∈I")
case True
have "sum f (I - {n - 1}) + sum f ({0..<n} - I - {n - 1}) +
(∑j = 0..<4. gen_bhle a $ ((n - 1) * 5 + j) * x $ ((n - 1) * 5 + j)) =
(∑i∈I-{n-1}. (b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M))
+ (∑i∈{0..<n}-I-{n-1}. (b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M))
+ (b1 n M (a!(n-1))) - (b2_last n M) - (b5 n M)"
proof -
have "(∑i∈I-{n-1}. f i) =
(∑i∈I-{n-1}. (b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M)) "
unfolding f_def using gen_bhle_in_I_plus[OF _ True] by (simp add: n_def)
moreover have "(∑i∈{0..<n}-I-{n-1}. f i) =
(∑i∈{0..<n}-I-{n-1}. (b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M)) "
unfolding f_def using gen_bhle_not_in_I_plus[OF _ True] by (meson sum.cong)
ultimately show ?thesis unfolding f_def using gen_bhle_last by auto
qed
also have "… = (∑i∈I-{n-1}. (a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1))))
+ (∑i∈{0..<n}-I-{n-1}. - (a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1))))
+ (a!(n-1)) + M * 5^(4*n-4) - M*1"
proof -
have "b1 (i + 1) M (a ! i) - b2 (i + 1) M - b5 (i + 1) M =
(a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1)))" if "i∈I-{n-1}" for i
unfolding b1_def b2_def b5_def
by (smt (verit, best) add_uminus_conv_diff right_diff_distrib)
moreover have "b3 (i + 1) M - b4 (i + 1) M (a ! i) + b5 (i + 1) M =
- (a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1)))" if "i∈{0..<n} - I - {n - 1}" for i
unfolding b3_def b4_def b5_def
by (smt (verit, best) add_uminus_conv_diff right_diff_distrib)
moreover have "b1 n M (a ! (n - 1)) - b2_last n M - b5 n M =
(a!(n-1)) + M * 5^(4*n-4) - M"
unfolding b1_def b2_last_def b5_def by (simp add: distrib_left)
moreover have "- b4_last n M (a ! (n - 1)) + b5 n M =
-(a!(n-1)) - M * 5^(4*n-2) - M"
unfolding b4_last_def b5_def by (simp add: distrib_left)
ultimately show ?thesis by auto
qed
also have "… = (∑i∈I-{n-1}. (a!i)) + (∑i∈{0..<n}-I-{n-1}. - (a!i))
+ M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ (a!(n-1)) + M * 5^(4*n-4) - M"
proof -
have sets1: "{0..<n - 1} ∩ I = I - {n -1}" using "1"(1) n_def by auto
have sets2: "{0..<n - 1} - I = {0..<n}- I - {n-1}" using "1"(1) n_def by auto
have subs: "(∑i∈I-{n-1}. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1)) +
(∑i∈{0..<n}-I-{n-1}. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1)) =
(∑i = 0..<n-1. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1))"
using sum.Int_Diff[of "{0..<n-1}" "(λi. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1))" "I"]
‹finite I› unfolding sets1 sets2 by auto
show ?thesis
apply (subst distrib_left)+
apply (subst sum.distrib)+
apply (subst sum_distrib_left)
apply (subst right_diff_distrib)+
apply (subst subs[symmetric])
apply auto
done
qed
also have "… = (∑i∈I. (a!i)) + (∑i∈{0..<n}-I. - (a!i))
+ M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ M * 5^(4*n-4) - M"
proof -
have *: "a ! (n-1) = sum ((!) a) (I ∩ {n-1})" using True by auto
have "sum ((!) a) (I - {n-1}) + a ! (n-1) = sum ((!) a) I"
by (subst sum.Int_Diff[of "I" _ "{n-1}"], unfold *, auto simp add: ‹finite I›)
then show ?thesis using True by auto
qed
also have "… = M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ M * 5^(4*n-4) - M "
unfolding n_def using 1(2) by (subst sum_negf, auto)
finally show ?thesis by auto
next
case False
have "sum f (I - {n - 1}) + sum f ({0..<n} - I - {n - 1}) +
(∑j = 0..<4. gen_bhle a $ ((n - 1) * 5 + j) * x $ ((n - 1) * 5 + j)) =
(∑i∈{0..<n}-I-{n-1}. (b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M))
+ (∑i∈I-{n-1}. (b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M))
+ (b1 n M (a!(n-1))) - (b2_last n M) - (b5 n M)"
proof -
have "(∑i∈{0..<n}-I-{n-1}. f i) =
(∑i∈{0..<n}-I-{n-1}. (b1 (i+1) M (a!i)) - (b2 (i+1) M) - (b5 (i+1) M)) "
unfolding f_def using gen_bhle_not_in_I_minus[OF _ False] by (simp add: n_def)
moreover have "(∑i∈I-{n-1}. f i) =
(∑i∈I-{n-1}. (b3 (i+1) M) - (b4 (i+1) M (a!i)) + (b5 (i+1) M)) "
unfolding f_def using gen_bhle_in_I_minus[OF _ False] by (simp add: n_def)
ultimately show ?thesis unfolding f_def using gen_bhle_last by auto
qed
also have "… = (∑i∈{0..<n}-I-{n-1}. (a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1))))
+ (∑i∈I-{n-1}. - (a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1))))
+ (a!(n-1)) + M * 5^(4*n-4) - M*1"
proof -
have "b1 (i + 1) M (a ! i) - b2 (i + 1) M - b5 (i + 1) M =
(a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1)))" if "i∈{0..<n} - I - {n - 1}" for i
unfolding b1_def b2_def b5_def
by (smt (verit, best) add_uminus_conv_diff right_diff_distrib)
moreover have "b3 (i + 1) M - b4 (i + 1) M (a ! i) + b5 (i + 1) M =
- (a!i) + (M * 5^(4*(i+1)-4) - M * 5^(4*(i+1)))" if "i∈I-{n-1}" for i
unfolding b3_def b4_def b5_def
by (smt (verit, best) add_uminus_conv_diff right_diff_distrib)
moreover have "b1 n M (a ! (n - 1)) - b2_last n M - b5 n M =
(a!(n-1)) + M * 5^(4*n-4) - M"
unfolding b1_def b2_last_def b5_def by (simp add: distrib_left)
moreover have "- b4_last n M (a ! (n - 1)) + b5 n M =
-(a!(n-1)) - M * 5^(4*n-2) - M"
unfolding b4_last_def b5_def by (simp add: distrib_left)
ultimately show ?thesis by auto
qed
also have "… = (∑i∈{0..<n}-I-{n-1}. (a!i)) + (∑i∈I-{n-1}. - (a!i))
+ M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ (a!(n-1)) + M * 5^(4*n-4) - M"
proof -
have sets1: "{0..<n - 1} ∩ I = I - {n -1}" using "1"(1) n_def by auto
have sets2: "{0..<n - 1} - I = {0..<n}- I - {n-1}" using "1"(1) n_def by auto
have subs: "(∑i∈{0..<n}-I-{n-1}. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1)) +
(∑i∈I-{n-1}. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1)) =
(∑i = 0..<n-1. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1))"
using sum.Int_Diff[of "{0..<n-1}" "(λi. M * 5^(4*i+4*1-4) - M * 5^(4*i+4*1))" "I"]
‹finite I› unfolding sets1 sets2 by auto
show ?thesis
apply (subst distrib_left)+
apply (subst sum.distrib)+
apply (subst sum_distrib_left)
apply (subst right_diff_distrib)+
apply (subst subs[symmetric])
apply auto
done
qed
also have "… = (∑i∈{0..<n}-I. (a!i)) + (∑i∈I. - (a!i))
+ M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ M * 5^(4*n-4) - M"
proof -
have *: "({0..<n}-I) ∩ {n-1} = {n-1}" using False n_def ‹length a > 0› by auto
then have **: "a ! (n-1) = sum ((!) a) (({0..<n}-I) ∩ {n-1})" using False by auto
have "sum ((!) a) (({0..<n}-I) - {n-1}) + a ! (n-1) = sum ((!) a) ({0..<n}-I)"
by (subst sum.Int_Diff[of "{0..<n}-I" _ "{n-1}"], unfold * **, auto simp add: ‹finite I›)
then show ?thesis using False by auto
qed
also have "… = M * (∑i∈{0..<n-1}. 5^(4*(i+1)-4) - 5^(4*(i+1)))
+ M * 5^(4*n-4) - M "
unfolding n_def using 1(2) by (subst sum_negf, auto)
finally show ?thesis by auto
qed
also have "… = M * ((∑i∈{1..<n}. 5^(4*i-4) - 5^(4*i)) + 5^(4*n-4) - 1)"
proof -
have sums: "(∑i = Suc 0..<Suc (n - 1). 5 ^ (4 * i - 4) - 5 ^ (4 * i)) =
sum ((λi. 5 ^ (4*(i+1) - 4) - 5 ^ (4*(i+1)))) {0..<n - 1}"
using sum.atLeast_Suc_lessThan_Suc_shift[of "(λi. 5^(4*i-4) - 5^(4*i))" 0 "n-1"]
unfolding comp_def by auto
show ?thesis
by (subst distrib_left[symmetric], subst right_diff_distrib, subst mult_1_right)
(subst sums[symmetric], use ‹0 < length a› n_def in ‹force›)
qed
also have "… = M * (((∑i∈{1..<n}. 5^(4*i-4)) + 5^(4*n-4)) - ((∑i∈{1..<n}. 5^(4*i)) + 1))"
using sum.distrib[of "(λi. 5^(4*i-4))" "(λi. (-1) * 5^(4*i))" "{1..<n}"]
by (simp add: sum_subtractf)
also have "… = M * ((∑i∈{1..<n+1}. 5^(4*i-4)) - (∑i∈{0..<n}. 5^(4*i)))"
using sum.atLeastLessThan_Suc[of 1 n "(λi. 5^(4*i-4))"]
sum.atLeast_Suc_lessThan[of 0 n "(λi. 5^(4*i))"]
by (smt (verit, best) One_nat_def Suc_eq_plus1 Suc_leI ‹0 < length a› mult_eq_0_iff
n_def power_0)
also have "… = M * ((∑i∈{0..<n}. 5^(4*i)) - (∑i∈{0..<n}. 5^(4*i)))"
using sum.atLeast_Suc_lessThan_Suc_shift[of "(λi. 5^(4*i-4))" 0 n] by auto
also have "… = 0" by auto
finally show ?thesis by blast
qed
moreover have "dim_vec x = dim_vec (gen_bhle a)"
using dim_vec_gen_bhle[OF ‹a≠[]›] dimx_eq_5dima by simp
moreover have "x ≠ 0⇩v (dim_vec x)"
proof (rule ccontr)
assume "¬ x ≠ 0⇩v (dim_vec x)"
then have "x = 0⇩v (dim_vec x)" by auto
have "dim_vec x > 3" using ‹0 < length a› dimx_eq_5dima by linarith
have "(n - Suc 0) * 5 + 3 < dim_vec x"
unfolding dimx_eq_5dima n_def using ‹length a > 0› by linarith
then have "x $ ((n-1)*5 + 3) = 0" using ‹dim_vec x > 3›
by (subst ‹x=0⇩v (dim_vec x)›, subst index_zero_vec(1)[of "(n-1)*5+3"], auto)
moreover have "x $ ((n-1)*5+3) ≠ 0"
proof -
have "¬ ((n - 1) * 5 + 3 < (n - 1) * 5)" by auto
then show ?thesis unfolding x_def vec_of_list_index nth_append length_concat_map
plus_x_last_def by auto
qed
ultimately show False by auto
qed
moreover have "∥x∥⇩∞ ≤ 1"
proof -
let ?x_list = "(concat (map (λi. if i ∈ I then plus_minus
else minus_plus) [0..<n-1]))"
have set: "set (?x_list) ⊆ {-1,0,1::int}"
using ‹length a > 0› 1 unfolding n_def plus_minus_def minus_plus_def
plus_x_def minus_x_def
by (subst set_concat, subst set_map)(auto simp add: atLeast0LessThan)
have "?x_list ! i ∈ {-1,0,1::int}" if "i< length ?x_list" for i
using nth_mem[OF that] set by auto
then have *:"?x_list ! i ∈ {-1,0,1::int}" if "i< (n - 1) * 5" for i using that
unfolding length_concat_map by auto
have **: "plus_x_last ! (i - (n - 1) * 5)∈{-1,0,1::int}"
if "¬ (i<(n-1)*5)" "i<dim_vec x" for i
proof -
have "(i - (n - 1) * 5)<4" using that ‹length a > 0›
unfolding dimx_eq_5dima n_def by auto
then show ?thesis unfolding plus_x_last_def
by (smt (z3) add.assoc add_diff_cancel_right' diff_is_0_eq insertCI less_Suc_eq not_le
not_less_iff_gr_or_eq nth_Cons' numeral_1_eq_Suc_0 numeral_Bit0 plus_1_eq_Suc)
qed
have "x$i∈{-1,0,1::int}" if "i<dim_vec x" for i
using that * ** unfolding x_def vec_of_list_index nth_append length_concat_map
plus_x_last_def by auto
then have "¦x$i¦≤1" if "i<dim_vec x" for i using that by fastforce
then show ?thesis unfolding linf_norm_vec_Max
by (subst Max_le_iff, auto simp add: exI[of "(λi. dim_vec x > i)" 0] ‹dim_vec x > 0›)
qed
ultimately show ?case by (subst exI[of _ x], auto)
qed
text ‹NP-hardness of reduction function›
lemma NP_hardness_reduction_subset_sum:
assumes "reduce_bhle_partition a ∈ bhle"
shows "a ∈ partition_problem_nonzero"
using assms unfolding reduce_bhle_partition_def bhle_def partition_problem_nonzero_def
proof (safe, goal_cases)
case (1 x)
text ‹Given a vector $x$ from ‹bhle› find the subset $I$ such that it has the same sum as
its complement.›
have "length a > 0" using 1(3) dim_vec_gen_bhle dim_vec_gen_bhle_empty by auto
define I where "I = {i∈{0..<length a}. x $ (5*i)≠0}"
define n where "n = length a"
then have "n > 0" using ‹length a>0› by auto
have dim_vec_x_5n: "dim_vec x = 5 * n - 1" unfolding n_def using 1
by (metis dim_vec_gen_bhle dim_vec_gen_bhle_empty less_not_refl2)
have "I⊆{0..<length a}" using 1 I_def by auto
text ‹This is the trickiest part in the proof. One first has to generate equations from $x$
which form conditions on the entries of $x$. To do so, we consider the formula
‹gen_bhle a ∙ x = 0› and rewrite it in basis $5$. Every digit then gives us an
arithmetic expression in entries of $x$ equals to zero.
From these equations, we can deduce the wanted properties.›
moreover have "sum ((!) a) I = sum ((!) a) ({0..<length a} - I)"
proof -
define M where "M = 2 * (∑i<length a. ¦a ! i¦) + 1"
text ‹Rewriting the first formula in a huge sum.›
define a0 where "a0 = (λi. if i mod (5::nat) ∈ {0,2} then a!(i div 5) else 0)"
define a1 where "a1 = (λi. if i mod (5::nat) ∈ {0,4} then 1 else 0::int)"
define a1_last where "a1_last = (λi. if i mod (5::nat) ∈ {0} then 1 else 0::int)"
define a2 where "a2 = (λi. if i mod (5::nat) ∈ {0,1} then 1 else 0::int)"
define a3 where "a3 = (λi. if i mod (5::nat) ∈ {4,2} then 1 else 0::int)"
define a3_last where "a3_last = (λi. if i mod (5::nat) ∈ {2} then 1 else 0::int)"
define a4 where "a4 = (λi. if i mod (5::nat) ∈ {0,2,3} then 1 else 0::int)"
define a5 where "a5 = (λi. if i mod (5::nat) ∈ {1,2} then
(if i div 5 < n-1 then 5^(4*(i div 5 +1)) else 1) else 0::int)"
define a0_rest' where "a0_rest' =
(λi. a1 i * 5 ^ (4 * (i div 5)) + a2 i * 5 ^ (4 * (i div 5) + 1) +
a3 i * 5 ^ (4 * (i div 5) + 2) + a4 i * 5 ^ (4 * (i div 5) + 3) + a5 i)"
define a0_last where "a0_last = (λi.
a1_last i * 5 ^ (4 * (i div 5)) + a2 i * 5 ^ (4 * (i div 5) + 1) +
a3_last i * 5 ^ (4 * (i div 5) + 2) + a4 i * 5 ^ (4 * (i div 5) + 3) +
a5 i)"
define a0_rest where "a0_rest = (λi. if i div 5 < n-1 then a0_rest' i else a0_last i)"
let ?P0 = "(λi. b1 (i div 5 + 1) M (a!(i div 5)))"
let ?P1 = "(λi. (if i div 5 < n-1 then b2 (i div 5 + 1) M else b2_last (i div 5 + 1) M))"
let ?P4 = "(λi. (if i div 5 < n-1 then b3 (i div 5 + 1) M else 0))"
let ?P2 = "(λi. (if i div 5 < n-1 then b4 (i div 5 + 1) M (a!(i div 5))
else b4_last (i div 5 + 1) M (a!(i div 5))))"
let ?P3 = "(λi. b5 (i div 5 + 1) M)"
have cases_a0: "(a0 i + M * (a0_rest i)) =
(if i mod 5 = 0 then ?P0 i else
(if i mod 5 = 1 then ?P1 i else
(if i mod 5 = 2 then ?P2 i else
(if i mod 5 = 3 then ?P3 i else ?P4 i))))"
if "i<5*n" for i
proof (cases "i div 5 < n-1")
case True
then show ?thesis
by (subst mod_5_if_split[of i "a0 i + M * (a0_rest i)" ?P0 ?P1 ?P2 ?P3 ?P4])
(auto simp add: a0_def a0_rest_def a0_rest'_def
a1_def a2_def a3_def a4_def a5_def b1_def b2_def b3_def b4_def b5_def)
next
case False
then have "i div 5 = n-1" using that by auto
then show ?thesis
by (subst mod_5_if_split[of i "a0 i + M * (a0_rest i)" ?P0 ?P1