Theory LP_Preliminaries
theory LP_Preliminaries
imports
More_Jordan_Normal_Forms
Matrix_LinPoly
Jordan_Normal_Form.Matrix_Impl
Farkas.Simplex_for_Reals
"HOL-Library.Mapping"
begin
fun vars_from_index_geq_vec where
"vars_from_index_geq_vec index b = [GEQ (lp_monom 1 (i+index)) (b$i). i ← [0..<dim_vec b]]"
lemma constraints_set_vars_geq_vec_def:
"set (vars_from_index_geq_vec start b) =
{GEQ (lp_monom 1 (i+start)) (b$i) |i. i ∈ {0..<dim_vec b}}"
using set_comprehension_list_comprehension[of
"(λi. GEQ (lp_monom 1 (i+start)) (b$i))" "dim_vec b"] by auto
lemma vars_from_index_geq_sat:
assumes "⟨x⟩ ⊨⇩c⇩s set (vars_from_index_geq_vec start b)"
assumes "i < dim_vec b"
shows "⟨x⟩ (i+start) ≥ b$i"
proof -
have e_e:"GEQ (lp_monom 1 (i+start)) (b$i) ∈ set (vars_from_index_geq_vec start b)"
using constraints_set_vars_geq_vec_def[of start b] using assms(2) by auto
then have "⟨x⟩ ⊨⇩c GEQ (lp_monom 1 (i+start)) (b$i)"
using assms(1) by blast
then have "(lp_monom 1 (i+start)) ⦃⟨x⟩⦄ ≥ (b$i)"
using satisfies_constraint.simps(4)[of "⟨x⟩" "lp_monom 1 (i + start)" "b$i"]
by simp
then show ?thesis
by simp
qed
fun mat_x_leq_vec where
"mat_x_leq_vec A b = [LEQ (matrix_to_lpolies A!i) (b$i) . i <- [0..<dim_vec b]]"
lemma mat_x_leq_vec_sol:
assumes "⟨x⟩ ⊨⇩c⇩s set (mat_x_leq_vec A b)"
assumes "i < dim_vec b"
shows "((matrix_to_lpolies A)!i) ⦃⟨x⟩⦄ ≤ b$i"
proof -
have e_e: "LEQ ((matrix_to_lpolies A)!i) (b$i) ∈ set (mat_x_leq_vec A b)"
by (simp add: assms(2))
then have "⟨x⟩ ⊨⇩c LEQ ((matrix_to_lpolies A)!i) (b$i)"
using assms(1) by blast
then show ?thesis
using satisfies_constraint.simps by auto
qed
fun x_mat_eq_vec where
"x_mat_eq_vec b A = [EQ (matrix_to_lpolies A!i) (b$i) . i <- [0..<dim_vec b]]"
lemma x_mat_eq_vec_sol:
assumes "x ⊨⇩c⇩s set (x_mat_eq_vec b A)"
assumes "i < dim_vec b"
shows "((matrix_to_lpolies A)!i) ⦃ x ⦄ = b$i"
proof -
have e_e: "EQ ((matrix_to_lpolies A)!i) (b$i) ∈ set (x_mat_eq_vec b A)"
by (simp add: assms(2))
then have "x ⊨⇩c EQ ((matrix_to_lpolies A)!i) (b$i)"
using assms(1) by blast
then show ?thesis
using satisfies_constraint.simps by auto
qed
section ‹ Get different matrices into same space, without interference ›
fun two_block_non_interfering where
"two_block_non_interfering A B = (let z1 = 0⇩m (dim_row A) (dim_col B);
z2 = 0⇩m (dim_row B) (dim_col A) in
four_block_mat A z1 z2 B)"
lemma split_two_block_non_interfering:
assumes "split_block (two_block_non_interfering A B) (dim_row A) (dim_col A) = (Q1, Q2, Q3, Q4)"
shows "Q1 = A" "Q4 = B"
using split_four_block_dual_fst_lst[of A _ _ B Q1 Q2 Q3 Q4]
assms by auto
lemma two_block_non_interfering_dims:
"dim_row (two_block_non_interfering A B) = dim_row A + dim_row B"
"dim_col (two_block_non_interfering A B) = dim_col A + dim_col B"
by (simp)+
lemma two_block_non_interfering_zeros_are_0:
assumes "i < dim_row A"
and "j ≥ dim_col A"
and "j < dim_col (two_block_non_interfering A B)"
shows "(two_block_non_interfering A B)$$(i,j) = 0" "(two_block_non_interfering A B)$$(i,j) = 0"
using four_block_mat_def assms two_block_non_interfering_dims[of A B] by auto
lemma two_block_non_interfering_row_comp1:
assumes "i <dim_row A"
shows "row (two_block_non_interfering A B) i = row A i @⇩v (0⇩v (dim_col B))"
using assms by auto
lemma two_block_non_interfering_row_comp2:
assumes "i <dim_row (two_block_non_interfering A B)"
and "i ≥ dim_row A"
shows "row (two_block_non_interfering A B) i = (0⇩v (dim_col A)) @⇩v row B (i - dim_row A)"
using assms by (auto)
lemma first_vec_two_block_non_inter_is_first_vec:
assumes "dim_col A + dim_col B = dim_vec v"
assumes "dim_row A = n"
shows "vec_first (two_block_non_interfering A B *⇩v v) n = A *⇩v (vec_first v (dim_col A))"
proof
fix i
assume a: "i < dim_vec (A *⇩v vec_first v (dim_col A))"
let ?tb = "two_block_non_interfering A B"
have i_n: "i < n" using a assms(2) by auto
have "vec_first (?tb *⇩v v) n $ i = vec_first (vec (dim_row ?tb) (λ i. row ?tb i ∙ v)) n $ i"
unfolding mult_mat_vec_def by simp
also have "... = (vec n (λ i. row ?tb i ∙ v)) $ i"
unfolding vec_first_def using trans_less_add1
by (metis a assms(2) dim_mult_mat_vec index_vec two_block_non_interfering_dims(1))
also have "... = row ?tb i ∙ v" by (simp add: i_n)
also have "... = (row A i @⇩v 0⇩v (dim_col B)) ∙ v"
using assms(2) i_n two_block_non_interfering_row_comp1 by fastforce
also have "... = row A i ∙ vec_first v (dim_vec (row A i)) +
0⇩v (dim_col B) ∙ vec_last v (dim_vec (0⇩v (dim_col B)))"
using append_split_vec_distrib_scalar_prod[of "row A i" "0⇩v (dim_col B)" v] assms(1) by auto
then have "vec_first (two_block_non_interfering A B *⇩v v) n $ i =
row A i ∙ vec_first v (dim_vec (row A i))"
using calculation by auto
then show "vec_first (two_block_non_interfering A B *⇩v v) n $ i =
(A *⇩v vec_first v (dim_col A)) $ i"
by (simp add: assms(2) i_n)
next
have "dim_vec (A *⇩v v) = dim_row A" using dim_vec_def dim_mult_mat_vec[of A v] by auto
then have "dim_vec (vec_first (two_block_non_interfering A B *⇩v v) n) = n" by auto
then show "dim_vec (vec_first (two_block_non_interfering A B *⇩v v) n) =
dim_vec (A *⇩v vec_first v (dim_col A))"
by (simp add: assms(2))
qed
lemma last_vec_two_block_non_inter_is_last_vec:
assumes "dim_col A + dim_col B = dim_vec v"
assumes "dim_row B = n"
shows "vec_last ((two_block_non_interfering A B) *⇩v v) n = B *⇩v (vec_last v (dim_col B))"
proof
fix i
assume a: "i < dim_vec (B *⇩v vec_last v (dim_col B))"
let ?tb = "two_block_non_interfering A B"
let ?vl = "(vec (dim_row ?tb) (λ i. row ?tb i ∙ v))"
have i_n: "i < n" using assms(2) using a by auto
have in3: "(dim_row ?tb) - n + i ≥ dim_row A"
by (simp add: assms(2))
have in3': "(dim_row ?tb) - n + i < dim_row ?tb"
by (simp add: assms(2) i_n two_block_non_interfering_dims(1))
have "dim_row A + n = dim_row (two_block_non_interfering A B)"
by (simp add: assms(2) two_block_non_interfering_dims(1))
then have dim_a: "dim_row A = dim_row (two_block_non_interfering A B) - n"
by (metis (no_types) diff_add_inverse2)
have "vec_last (?tb *⇩v v) n $ i = vec_last (vec (dim_row ?tb) (λ i. row ?tb i ∙ v)) n $ i"
unfolding mult_mat_vec_def by auto
also have "... = ?vl $ (dim_vec ?vl - n + i)"
unfolding vec_last_def using i_n index_vec by blast
also have "... = row ?tb ((dim_row ?tb) - n + i) ∙ v"
unfolding index_vec by (simp add: assms(2) i_n two_block_non_interfering_dims(1))
also have "... = row B i ∙ vec_last v (dim_vec (row B i))"
proof -
have "dim_vec (0⇩v (dim_col A) @⇩v row B i) = dim_vec v"
by (simp add: ‹dim_col A + dim_col B = dim_vec v›)
then show ?thesis using dim_a assms(1) in3' two_block_non_interfering_row_comp2
append_split_vec_distrib_scalar_prod[of "0⇩v (dim_col A)" "row B i" v]
by (metis add.commute add.right_neutral diff_add_inverse
in3 index_zero_vec(2) scalar_prod_left_zero vec_first_carrier)
qed
also have "... = row B i ∙ vec_last v (dim_col B)" by simp
thus "vec_last (two_block_non_interfering A B *⇩v v) n $ i = (B *⇩v vec_last v (dim_col B)) $ i"
using assms(2) calculation i_n by auto
qed (simp add: assms(2))
lemma two_block_non_interfering_mult_decomposition:
assumes "dim_col A + dim_col B = dim_vec v"
shows "two_block_non_interfering A B *⇩v v =
A *⇩v vec_first v (dim_col A) @⇩v B *⇩v vec_last v (dim_col B)"
proof -
let ?tb = "two_block_non_interfering A B"
from first_vec_two_block_non_inter_is_first_vec[of A B v "dim_row A", OF assms]
have "vec_first (?tb *⇩v v) (dim_row A) = A *⇩v vec_first v (dim_col A)"
by blast
moreover from last_vec_two_block_non_inter_is_last_vec[of A B v "dim_row B", OF assms]
have "vec_last (?tb *⇩v v) (dim_row B) = B *⇩v vec_last v (dim_col B)"
by blast
ultimately show ?thesis using vec_first_last_append[of "?tb *⇩v v" "(dim_row A)" "(dim_row B)"]
dim_mult_mat_vec[of "?tb" v] two_block_non_interfering_dims(1)[of A B]
by (metis carrier_vec_dim_vec)
qed
fun mat_leqb_eqc where
"mat_leqb_eqc A b c = (let lst = matrix_to_lpolies (two_block_non_interfering A A⇧T) in
[LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]] @
[EQ (lst!i) ((b@⇩vc)$i) . i <- [dim_vec b ..< dim_vec (b@⇩vc)]])"
lemma mat_leqb_eqc_for_LEQ:
assumes "i < dim_vec b"
assumes "i < dim_row A"
shows "(mat_leqb_eqc A b c)!i = LEQ ((matrix_to_lpolies A)!i) (b$i)"
proof -
define lst where lst: "lst = (mat_leqb_eqc A b c)"
define l where l: "l = matrix_to_lpolies (two_block_non_interfering A A⇧T)"
have ileqA: "i < dim_row A" using assms by auto
have "l!i = vec_to_lpoly ((row A i)@⇩v 0⇩v (dim_row A))"
unfolding l using two_block_non_interfering_row_comp1[of i A "A⇧T", OF ileqA]
by (metis ileqA lpoly_of_v_equals_v_append0 matrix_to_lp_vec_to_lpoly_row
trans_less_add1 two_block_non_interfering_dims(1))
then have leq: "l!i = (matrix_to_lpolies A)!i"
using lpoly_of_v_equals_v_append0[of "row A i" "(dim_row A)"] l
by (simp add: ileqA)
have *: "lst = [LEQ (l!i) (b$i) . i <- [0..<dim_vec b]] @
[EQ (l!i) ((b@⇩vc)$i) . i <- [dim_vec b ..< dim_vec (b@⇩vc)] ]"
unfolding l lst by (metis mat_leqb_eqc.simps)
have "([LEQ (l!i) (b$i). i <- [0..<dim_vec b]] @
[EQ (l!i) ((b@⇩vc)$i). i <- [dim_vec b ..< dim_vec (b@⇩vc)]]) ! i =
[LEQ (l!i) (b$i). i <- [0..<dim_vec b]]!i"
using assms(2) lst by (simp add: assms(1) nth_append)
also have "... = LEQ (l!i) (b$i)"
using l lst
by (simp add: assms(1))
finally show ?thesis
using "*" leq lst using mat_leqb_eqc.simps[of A b c] by auto
qed
lemma mat_leqb_eqc_for_EQ:
assumes "dim_vec b ≤ i" and "i < dim_vec (b@⇩vc)"
assumes "dim_row A = dim_vec b" and "dim_col A ≥ dim_vec c"
shows "(mat_leqb_eqc A b c)!i =
EQ (vec_to_lpoly (0⇩v (dim_col A) @⇩v row A⇧T (i-dim_vec b))) (c$(i-dim_vec b))"
proof -
define lst where lst: "lst = (mat_leqb_eqc A b c)"
define l where l: "l = matrix_to_lpolies (two_block_non_interfering A A⇧T)"
have i_s: "i < dim_row (two_block_non_interfering A A⇧T)"
using assms by (simp add: assms(2) assms(3) two_block_non_interfering_dims(1))
have l':"l!i = vec_to_lpoly ((0⇩v (dim_col A)) @⇩v (row A⇧T (i - dim_vec b)))"
using l two_block_non_interfering_row_comp2[of i A "A⇧T", OF i_s]
assms(1) assms(3) i_s matrix_to_lp_vec_to_lpoly_row by presburger
have "([LEQ (l!i) (b$i) . i <- [0..<dim_vec b]] @
[EQ (l!i) ((b@⇩vc)$i) . i <- [dim_vec b ..< dim_vec (b@⇩vc)]])!i =
[EQ (l!i) ((b@⇩vc)$i) . i <- [dim_vec b..< dim_vec (b@⇩vc)]] ! (i - dim_vec b)"
by (simp add: assms(1) leD nth_append)
also have "... = EQ (l!i) ((b@⇩vc)$i)"
using assms(1) assms(2) by auto
also have "... = EQ (l!i) (c$(i-dim_vec b))"
using assms(1) assms(2) by auto
then show ?thesis
using mat_leqb_eqc.simps by (metis (full_types) calculation l l')
qed
lemma mat_leqb_eqc_satisfies1:
assumes "x ⊨⇩c⇩s set (mat_leqb_eqc A b c)"
assumes "i < dim_vec b"
and "i < dim_row A"
shows "(matrix_to_lpolies A!i) ⦃x⦄ ≤ b$i"
proof -
have e_e: "LEQ (matrix_to_lpolies A ! i) (b$i) ∈ set (mat_leqb_eqc A b c)"
using mat_leqb_eqc_for_LEQ[of i b A c, OF assms(2) assms(3)]
nth_mem[of i "matrix_to_lpolies A"] mat_leqb_eqc.simps
by (metis (no_types, lifting) assms(2) diff_zero in_set_conv_nth length_append length_map
length_upt trans_less_add1)
then have "x ⊨⇩c LEQ ((matrix_to_lpolies A)!i) (b$i)"
using assms by blast
then show ?thesis
using satisfies_constraint.simps by auto
qed
lemma mat_leqb_eqc_satisfies2:
assumes "x ⊨⇩c⇩s set (mat_leqb_eqc A b c)"
assumes "dim_vec b ≤ i" and "i < dim_vec (b@⇩vc)"
and "dim_row A = dim_vec b" and "dim_vec c ≤ dim_col A"
shows "(matrix_to_lpolies (two_block_non_interfering A A⇧T) ! i) ⦃x⦄ = (b @⇩v c) $ i"
proof -
have e_e: "EQ (vec_to_lpoly (0⇩v (dim_col A) @⇩v row A⇧T (i - dim_vec b))) (c $ (i - dim_vec b))
∈ set (mat_leqb_eqc A b c)"
using assms(2) mat_leqb_eqc.simps[of A b c]
nth_mem[of i "(mat_leqb_eqc A b c)"]
using mat_leqb_eqc_for_EQ[of b i c A, OF assms(2) assms(3) assms(4) assms(5)]
by (metis (mono_tags, lifting) add_diff_cancel_left' assms(3) diff_zero index_append_vec(2)
length_append length_map length_upt)
hence sateq: "x ⊨⇩c EQ (vec_to_lpoly (0⇩v (dim_col A) @⇩v
row A⇧T (i - dim_vec b))) (c $ (i - dim_vec b))"
using assms(1) by blast
have *: "i < dim_row (two_block_non_interfering A A⇧T)"
by (metis assms(3) assms(4) assms(5) dual_order.order_iff_strict dual_order.strict_trans
index_append_vec(2) index_transpose_mat(2) nat_add_left_cancel_less
two_block_non_interfering_dims(1))
have **: "dim_row A ≤ i"
by (simp add: assms(2) assms(4))
then have "x ⊨⇩c EQ ((matrix_to_lpolies (two_block_non_interfering A A⇧T))!i) ((b@⇩vc)$i)"
using two_block_non_interfering_row_comp2[of i A "A⇧T", OF * **]
by (metis "*" sateq assms(3) assms(4) index_append_vec(1) index_append_vec(2) leD
matrix_to_lp_vec_to_lpoly_row)
then show ?thesis
using satisfies_constraint.simps(5) by simp
qed
lemma mat_leqb_eqc_simplex_satisfies2:
assumes "simplex (mat_leqb_eqc A b c) = Sat x"
assumes "dim_vec b ≤ i" and "i < dim_vec (b@⇩vc)"
and "dim_row A = dim_vec b" and "dim_vec c ≤ dim_col A"
shows "(matrix_to_lpolies (two_block_non_interfering A A⇧T) ! i) ⦃⟨x⟩⦄ = (b @⇩v c) $ i"
using mat_leqb_eqc_satisfies2 assms(1) assms(2) assms(3) assms(4) assms(5) simplex(3) by blast
fun index_geq_n where
"index_geq_n i n = GEQ (lp_monom 1 i) n"
lemma index_geq_n_simplex:
assumes "⟨x⟩ ⊨⇩c (index_geq_n i n)"
shows "⟨x⟩ i ≥ n"
using assms by simp
fun from_index_geq0_vector where
"from_index_geq0_vector i v = [GEQ (lp_monom 1 (i+j)) (v$j) . j <-[0..<dim_vec v]]"
lemma from_index_geq_vector_simplex:
assumes "x ⊨⇩c⇩s set (from_index_geq0_vector i v)"
"j < dim_vec v"
shows "x (i + j) ≥ v$j"
proof -
have "GEQ (lp_monom 1 (i+j)) (v$j)∈ set (from_index_geq0_vector i v)"
by (simp add: assms(2))
moreover have "x ⊨⇩c GEQ (lp_monom 1 (i+j)) (v$j)"
using calculation(1) assms by force
ultimately show ?thesis by simp
qed
lemma from_index_geq0_vector_simplex2:
assumes "⟨x⟩ ⊨⇩c⇩s set (from_index_geq0_vector i v)"
assumes "i ≤ j" and "j < (dim_vec v) + i"
shows "⟨x⟩ j ≥ v$(j - i)"
by (metis assms(1) assms(2) assms(3) from_index_geq_vector_simplex
le_add_diff_inverse less_diff_conv2)
definition x_times_c_geq_y_times_b where
"x_times_c_geq_y_times_b c b = GEQ (
vec_to_lpoly (c @⇩v 0⇩v (dim_vec b)) - vec_to_lpoly (0⇩v (dim_vec c) @⇩v b)) 0"
lemma x_times_c_geq_y_times_b_correct:
assumes "simplex [x_times_c_geq_y_times_b c b] = Sat x"
shows "((vec_to_lpoly (c @⇩v 0⇩v (dim_vec b))) ⦃ ⟨x⟩ ⦄) ≥
((vec_to_lpoly (0⇩v (dim_vec c) @⇩v b)) ⦃ ⟨x⟩ ⦄)"
using simplex(3)[OF assms] unfolding x_times_c_geq_y_times_b_def
by (simp add: valuate_minus)
definition split_i_j_x where
"split_i_j_x i j x = (vec i ⟨x⟩, vec (j - i) (λy. ⟨x⟩ (y+i)))"
abbreviation split_n_m_x where
"split_n_m_x n m x ≡ split_i_j_x n (n+m) x"
lemma split_vec_dims:
assumes "split_i_j_x i j x = (a ,b)"
shows "dim_vec a = i" "dim_vec b = (j - i)"
using assms(1) unfolding split_i_j_x_def by auto+
lemma split_n_m_x_abbrev_dims:
assumes "split_n_m_x n m x = (a, b)"
shows "dim_vec a = n" "dim_vec b = m"
using split_vec_dims
using assms apply blast
using assms split_vec_dims(2) by fastforce
lemma split_access_fst_1:
assumes "k < i"
assumes "split_i_j_x i j x = (a, b)"
shows "a $ k = ⟨x⟩ k"
by (metis Pair_inject assms(1) assms(2) index_vec split_i_j_x_def)
lemma split_access_snd_1:
assumes "i ≤ k" and "k < j"
assumes "split_i_j_x i j x = (a, b)"
shows "b $ (k - i) = ⟨x⟩ k"
proof -
have "vec (j - i) (λn. ⟨x⟩ (n + i)) = b"
by (metis (no_types) assms(3) prod.sel(2) split_i_j_x_def)
then show ?thesis
using assms(1) assms(2) by fastforce
qed
lemma split_access_fst_2:
assumes "(x, y) = split_i_j_x i j Z"
assumes "k < dim_vec x"
shows "x$k = ⟨Z⟩ k"
by (metis assms(1) assms(2) split_access_fst_1 split_vec_dims(1))
lemma split_access_snd_2:
assumes "(x, y) = split_i_j_x i j Z"
assumes "k < dim_vec y"
shows "y$k = ⟨Z⟩ (k+dim_vec x)"
using assms split_i_j_x_def[of i j Z] by auto
lemma from_index_geq0_vector_split_snd:
assumes "⟨X⟩ ⊨⇩c⇩s set (from_index_geq0_vector d v)"
assumes "(x, y) = split_n_m_x d m X"
shows "⋀i. i < dim_vec v ⟹ i < m ⟹ y$i ≥ v$i"
using assms unfolding split_i_j_x_def
using from_index_geq_vector_simplex[of d v "⟨X⟩" _] index_vec by (simp add: add.commute)
lemma split_coeff_vec_index_sum:
assumes "(x,y) = split_i_j_x (dim_vec (lpoly_to_vec v)) l X"
shows "(∑i = 0..<dim_vec x. Abstract_Linear_Poly.coeff v i * ⟨X⟩ i) =
(∑i = 0..<dim_vec x. lpoly_to_vec v $ i * x $ i)"
proof -
from valuate_with_dim_poly[of v "⟨X⟩", symmetric]
have "(∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * ⟨X⟩ i) =
(∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * x $ i)"
by (metis (no_types, lifting) assms split_access_fst_1 split_vec_dims(1) sum.ivl_cong)
then show ?thesis
by (metis (no_types, lifting) assms dim_poly_dim_vec_equiv
lin_poly_to_vec_coeff_access split_vec_dims(1) sum.ivl_cong)
qed
lemma scalar_prod_valuation_after_split_equiv1:
assumes "(x,y) = split_i_j_x (dim_vec (lpoly_to_vec v)) l X"
shows "(lpoly_to_vec v) ∙ x = (v ⦃⟨X⟩⦄)"
proof -
from valuate_with_dim_poly[of v "⟨X⟩", symmetric]
have 1: "(v ⦃⟨X⟩⦄) = (∑i = 0..<dim_poly v. Abstract_Linear_Poly.coeff v i * ⟨X⟩ i)" by simp
have "(∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * ⟨X⟩ i) =
(∑i = 0..<dim_vec x. (lpoly_to_vec v) $ i * x $ i)"
by (metis (no_types, lifting) assms split_access_fst_1 split_vec_dims(1) sum.ivl_cong)
also have "... = (lpoly_to_vec v) ∙ x"
unfolding scalar_prod_def by blast
finally show ?thesis
by (metis (no_types, lifting) "1" dim_poly_dim_vec_equiv lin_poly_to_vec_coeff_access
split_vec_dims(1) sum.ivl_cong assms)
qed
definition mat_times_vec_leq ("[_*⇩v_]≤_" [1000,1000,100])
where
"[A *⇩v x]≤b ⟷ (∀i < dim_vec b. (A *⇩v x)$i ≤ b$i) ∧
(dim_row A = dim_vec b) ∧
(dim_col A = dim_vec x)"
definition vec_times_mat_eq ("[_⇩v*_]=_" [1000,1000,100])
where
"[y ⇩v* A]=c ⟷ (∀i < dim_vec c. (A⇧T *⇩v y)$i = c$i) ∧
(dim_col A⇧T = dim_vec y) ∧
(dim_row A⇧T = dim_vec c)"
definition vec_times_mat_leq ("[_⇩v*_]≤_" [1000,1000,100])
where
"[y ⇩v* A]≤c ⟷ (∀i < dim_vec c. (A⇧T *⇩v y)$i ≤ c$i) ∧
(dim_col A⇧T = dim_vec y) ∧
(dim_row A⇧T = dim_vec c)"
lemma mat_times_vec_leqI[intro]:
assumes "dim_row A = dim_vec b"
assumes "dim_col A = dim_vec x"
assumes "⋀i. i < dim_vec b ⟹ (A *⇩v x)$i ≤ b$i"
shows "[A *⇩v x]≤b"
unfolding mat_times_vec_leq_def using assms by auto
lemma mat_times_vec_leqD[dest]:
assumes "[A *⇩v x]≤b"
shows "dim_row A = dim_vec b" "dim_col A = dim_vec x" "⋀i. i < dim_vec b ⟹ (A *⇩v x)$i ≤ b$i"
using assms mat_times_vec_leq_def by blast+
lemma vec_times_mat_eqD[dest]:
assumes "[y ⇩v* A]=c"
shows "(∀i < dim_vec c. (A⇧T *⇩v y)$i = c$i)" "(dim_col A⇧T = dim_vec y)" "(dim_row A⇧T = dim_vec c)"
using assms vec_times_mat_eq_def by blast+
lemma vec_times_mat_leqD[dest]:
assumes "[y ⇩v* A]≤c"
shows "(∀i < dim_vec c. (A⇧T *⇩v y)$i ≤ c$i)" "(dim_col A⇧T = dim_vec y)" "(dim_row A⇧T = dim_vec c)"
using assms vec_times_mat_leq_def by blast+
lemma mat_times_vec_eqI[intro]:
assumes "dim_col A⇧T = dim_vec x"
assumes "dim_row A⇧T = dim_vec c"
assumes "⋀i. i < dim_vec c ⟹ (A⇧T *⇩v x)$i = c$i"
shows "[x ⇩v* A]=c"
unfolding vec_times_mat_eq_def using assms by blast
lemma mat_leqb_eqc_split_correct1:
assumes "dim_vec b = dim_row A"
assumes "⟨X⟩ ⊨⇩c⇩s set (mat_leqb_eqc A b c)"
assumes "(x,y) = split_i_j_x (dim_col A) l X"
shows "[A *⇩v x]≤b"
proof (standard, goal_cases)
case 1
then show ?case using assms(1)[symmetric] .
case 2
then show ?case using assms(3) unfolding split_i_j_x_def
using split_vec_dims[of 0 "dim_col A" X x y] by auto
case (3 i)
with mat_leqb_eqc_satisfies1[of A b c "⟨X⟩" i]
have m: "(matrix_to_lpolies A ! i) ⦃ ⟨X⟩ ⦄ ≤ b $ i"
using assms(1) assms(2) by linarith
have leq: "dim_poly (vec_to_lpoly (row A i)) ≤ dim_col A"
using vec_to_poly_dim_less[of "row A i"] by simp
have i: "i < dim_row A"
using "3" assms(1) by linarith
from two_block_non_interfering_row_comp1[of i A "A⇧T"]
have "row (two_block_non_interfering A A⇧T) i = row A i @⇩v 0⇩v (dim_col A⇧T)"
using "3" assms(1) by linarith
have "(vec_to_lpoly (row A i @⇩v 0⇩v (dim_col A⇧T))) ⦃⟨X⟩⦄ = ((vec_to_lpoly (row A i)) ⦃⟨X⟩⦄)"
using lpoly_of_v_equals_v_append0 by auto
also have "... = (∑a = 0..<dim_poly (vec_to_lpoly (row A i)).
Abstract_Linear_Poly.coeff (vec_to_lpoly (row A i)) a * ⟨X⟩ a)"
using valuate_with_dim_poly[of "vec_to_lpoly (row A i)" "⟨X⟩"] by blast
also have "... = (∑a = 0..<dim_col A. Abstract_Linear_Poly.coeff (vec_to_lpoly (row A i)) a * ⟨X⟩ a)"
using split_coeff_vec_index_sum[of x y]
sum_dim_vec_equals_sum_dim_poly[of "row A i" "⟨X⟩"] by auto
also have "... = row A i ∙ x"
unfolding scalar_prod_def using ‹dim_col A = dim_vec x› i assms(3)
using matrix_to_lpolies_coeff_access[of i A] matrix_to_lp_vec_to_lpoly_row[of i A]
split_access_fst_1[of _ "(dim_col A)" l X x y] by fastforce
finally show ?case
using m i lpoly_of_v_equals_v_append0 by auto
qed
lemma mat_leqb_eqc_split_simplex_correct1:
assumes "dim_vec b = dim_row A"
assumes "simplex (mat_leqb_eqc A b c) = Sat X"
assumes "(x,y) = split_i_j_x (dim_col A) l X"
shows "[A *⇩v x]≤b"
using mat_leqb_eqc_split_correct1[of b A c X x y] assms(1) assms(2) assms(3) simplex(3) by blast
lemma sat_mono:
assumes "set A ⊆ set B"
shows "⟨X⟩ ⊨⇩c⇩s set B ⟹ ⟨X⟩ ⊨⇩c⇩s set A"
using assms(1) assms by blast
lemma mat_leqb_eqc_split_subset_correct1:
assumes "dim_vec b = dim_row A"
assumes "set (mat_leqb_eqc A b c) ⊆ set S"
assumes "simplex S = Sat X"
assumes "(x,y) = split_i_j_x (dim_col A) l X"
shows "[A *⇩v x]≤b"
using sat_mono assms(1) assms(2) assms(3) assms(4)
mat_leqb_eqc_split_correct1 simplex(3) by blast
lemma mat_leqb_eqc_split_correct2:
assumes "dim_vec c = dim_row A⇧T"
assumes "dim_vec b = dim_col A⇧T"
assumes "⟨X⟩ ⊨⇩c⇩s set (mat_leqb_eqc A b c)"
assumes "(x, y) = split_n_m_x (dim_row A⇧T) (dim_col A⇧T) X"
shows "[y ⇩v* A]=c"
proof (standard, goal_cases)
case 1
then show ?case
using assms split_n_m_x_abbrev_dims(2)[OF assms(4)[symmetric]] by linarith
case 2
then show ?case using assms(1)[symmetric] .
case (3 i)
define lst where lst: "lst = matrix_to_lpolies (two_block_non_interfering A A⇧T)"
define db where db: "db = dim_vec b"
define dc where dc: "dc = dim_vec c"
have cA: "dim_vec c ≤ dim_col A"
by (simp add: assms(1))
have dbi_dim: "db+i < dim_vec (b @⇩v c)"
by (simp add: "3" db)
have *: "dim_vec b ≤ db+i"
by (simp add: db)
have "([LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]] @
[EQ (lst!i) ((b@⇩vc)$i) . i <- [dim_vec b ..< dim_vec (b@⇩vc)]]) ! (db + i) =
EQ (lst!(db+i)) ((b@⇩vc)$(db+i))" using mat_leqb_eqc_for_EQ[of b "db+i" c A]
nth_append[of "[LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]]"
"[EQ (lst!i) ((b@⇩vc)$i) . i <- [dim_vec b ..< dim_vec (b@⇩vc)]]"]
by (simp add: "3" db)
have rowA: "dim_vec b = dim_row A"
using assms index_transpose_mat(3)[of A] by linarith
have "⟨X⟩ ⊨⇩c EQ (lst!(db+i)) (c$i)"
proof -
have "db + i - dim_vec b = i"
using db diff_add_inverse by blast
then have "(lst ! (db + i)) ⦃ ⟨X⟩ ⦄ = c $ i"
by (metis dbi_dim rowA * cA assms(3) index_append_vec(1)
index_append_vec(2) leD lst mat_leqb_eqc_satisfies2)
then show ?thesis
using satisfies_constraint.simps(5)[of "⟨X⟩" "(lst ! (db + i))" "(c $ i)"] by simp
qed
then have sat: "(lst!(db+i)) ⦃⟨X⟩⦄ = c$i"
by simp
define V where V: "V = vec (db+dc) (λi. ⟨X⟩ i)"
have vdim: "dim_vec V = dim_vec (b@⇩vc)" using V db dc by simp
have *: "db + i < dim_row (two_block_non_interfering A A⇧T)"
by (metis dbi_dim assms(1) index_append_vec(2) rowA two_block_non_interfering_dims(1))
have **: "dim_row A ≤ db + i"
by (simp add: assms(2) db)
from two_block_non_interfering_row_comp2[of "db+i" A "A⇧T", OF * **]
have eql: "row (two_block_non_interfering A A⇧T) (db + i) = 0⇩v (dim_col A) @⇩v row A⇧T i"
by (simp add: assms(2) db)
with matrix_to_lp_vec_to_lpoly_row[of i "A⇧T"]
have eqv: "lst!(db+i) = vec_to_lpoly (0⇩v (dim_col A) @⇩v row A⇧T i)"
using "*" lst matrix_to_lp_vec_to_lpoly_row by presburger
then have "∀j<dim_col A. Abstract_Linear_Poly.coeff (lst!(db+i)) j = 0"
by (metis index_append_vec(1) index_append_vec(2) index_zero_vec(1) index_zero_vec(2)
vec_to_lin_poly_coeff_access trans_less_add1)
moreover have "∀j≥db+dc. Abstract_Linear_Poly.coeff (lst!(db+i)) j = 0"
by (metis (mono_tags, lifting) eqv index_transpose_mat(3) index_zero_vec(2) leD
add.commute assms(1) assms(2) coeff_nonzero_dim_vec_non_zero(2) index_append_vec(2)
index_row(2) index_transpose_mat(2) db dc)
moreover have "vars (lst!(db+i)) ⊆ {dim_col A..<db+dc}"
by (meson atLeastLessThan_iff calculation(1) calculation(2) coeff_zero not_le subsetI)
ultimately have "(lst!(db+i))⦃⟨X⟩⦄ = (∑j∈{dim_col A..<db+dc}. Abstract_Linear_Poly.coeff (lst!(db+i)) j * ⟨X⟩ j)"
using eval_poly_with_sum_superset[of "{dim_col A..<db+dc}" "lst!(db+i)" "⟨X⟩"] by blast
also have "... = (∑j∈{dim_col A..<db+dc}. Abstract_Linear_Poly.coeff (lst!(db+i)) j * V$j)"
using V by auto
also have "... = (∑j∈{dim_col A..<db+dc}. (0⇩v (dim_col A) @⇩v row A⇧T i)$j * V$j)"
proof -
have "∀j∈{dim_col A..<db+dc}. Abstract_Linear_Poly.coeff (lst!(db+i)) j = (0⇩v (dim_col A) @⇩v row A⇧T i)$j"
by (metis ‹V ≡ vec (db + dc) ⟨X⟩› vdim assms(1) assms(2) index_transpose_mat(2)
atLeastLessThan_iff dim_vec eql eqv index_append_vec(2) index_row(2)
vec_to_lin_poly_coeff_access semiring_normalization_rules(24)
two_block_non_interfering_dims(2))
then show ?thesis
by (metis (mono_tags, lifting) sum.cong)
qed
also have "... = (∑j∈{0..<dim_col A}. (0⇩v (dim_col A) @⇩v row A⇧T i)$j * V$j) +
(∑j∈{dim_col A..<db+dc}. (0⇩v (dim_col A) @⇩v row A⇧T i)$j * V$j)"
by (metis (no_types, lifting) add_cancel_left_left atLeastLessThan_iff mult_eq_0_iff
class_semiring.add.finprod_all1 index_append_vec(1) index_zero_vec(1)
index_zero_vec(2) trans_less_add1)
also have "... = (∑j∈{0..<db+dc}. (0⇩v (dim_col A) @⇩v row A⇧T i)$j * V$j)"
by (metis (no_types, lifting) add.commute assms(1) dc index_transpose_mat(2)
le_add1 le_add_same_cancel1 sum.atLeastLessThan_concat)
also have "... = (0⇩v (dim_col A) @⇩v row A⇧T i) ∙ V"
unfolding scalar_prod_def by (simp add: V)
also have "... = 0⇩v (dim_col A) ∙ vec_first V (dim_vec (0⇩v (dim_col A))) +
row A⇧T i ∙ vec_last V (dim_vec (row A⇧T i))"
using append_split_vec_distrib_scalar_prod[of "0⇩v (dim_col A)" "row A⇧T i" V]
by (metis (no_types, lifting) ‹dim_vec V = dim_vec (b @⇩v c)› add.commute assms(1)
assms(2) index_append_vec(2) index_row(2) index_transpose_mat(2)
index_transpose_mat(3) index_zero_vec(2))
also have "0⇩v (dim_col A) ∙ vec_first V (dim_vec (0⇩v (dim_col A))) +
row A⇧T i ∙ vec_last V (dim_vec (row A⇧T i)) = (row A⇧T i) ∙ y"
proof -
have "vec_last V (dim_vec (row A⇧T i)) = y"
proof (standard, goal_cases)
case (1 i)
then show ?case
proof -
have f1: "dim_col A⇧T = db"
by (simp add: assms(2) db)
then have "∀v va. vec db (λn. ⟨X⟩ (n + dc)) = v ∨ (x, y) ≠ (va, v)"
by (metis Pair_inject add_diff_cancel_left' assms(1) assms(4) dc split_i_j_x_def)
then show ?case
unfolding V vec_last_def
using split_access_fst_1[of "(dim_row A⇧T)" i "(dim_col A⇧T)" X x y]
by (metis "1" add.commute add_diff_cancel_left' add_less_cancel_left
dim_vec f1 index_row(2) index_vec)
qed
next
case 2
then show ?case
using ‹dim_col A⇧T = dim_vec y› by auto
qed
then show ?thesis
by (simp add: assms(1))
qed
then show ?case unfolding mult_mat_vec_def by (metis "3" assms(1) calculation index_vec sat)
qed
lemma mat_leqb_eqc_split_simplex_correct2:
assumes "dim_vec c = dim_row A⇧T"
assumes "dim_vec b = dim_col A⇧T"
assumes "simplex (mat_leqb_eqc A b c) = Sat X"
assumes "(x, y) = split_n_m_x (dim_row A⇧T) (dim_col A⇧T) X"
shows "[y ⇩v* A]=c"
using assms(1) assms(2) assms(3) assms(4) mat_leqb_eqc_split_correct2 simplex(3) by blast
lemma mat_leqb_eqc_correct:
assumes "dim_vec c = dim_row A⇧T"
and "dim_vec b = dim_col A⇧T"
assumes "simplex (mat_leqb_eqc A b c) = Sat X"
assumes "(x, y) = split_n_m_x (dim_row A⇧T) (dim_col A⇧T) X"
shows "[y ⇩v* A]=c" "[A *⇩v x]≤b"
using mat_leqb_eqc_split_simplex_correct1[of b A c X x y]
using assms(1) assms(2) assms(3) assms(4) mat_leqb_eqc_split_simplex_correct2 apply blast
using mat_leqb_eqc_split_correct2[of b A c X x y]
by (metis (no_types) Matrix.transpose_transpose assms(2) assms(3) assms(4) index_transpose_mat(3)
mat_leqb_eqc_split_simplex_correct1[of b A c X x y])
lemma eval_lpoly_eq_dot_prod_split1:
assumes "(x, y) = split_n_m_x (dim_vec c) (dim_vec b) X"
shows"(vec_to_lpoly c) ⦃⟨X⟩⦄ = c ∙ x"
proof -
have *: "(vec_to_lpoly c) ⦃⟨X⟩⦄ =
(∑i∈vars (vec_to_lpoly c). Abstract_Linear_Poly.coeff (vec_to_lpoly c) i * ⟨X⟩ i)"
using linear_poly_sum sum.cong eval_poly_with_sum by auto
also have "... = (∑i∈{0..<dim_vec c}. Abstract_Linear_Poly.coeff (vec_to_lpoly c) i * ⟨X⟩ i)"
using vars_subset_dim_vec_to_lpoly_dim[of c] linear_poly_sum[of "vec_to_lpoly c" "⟨X⟩"]
eval_poly_with_sum_superset[of "{0..<dim_vec c}" "vec_to_lpoly c" "⟨X⟩"] by auto
also have "... = (∑i∈{0..<dim_vec c}. c$i * x$i)"
using split_access_fst_1[of _ "dim_vec c" "(dim_vec c) + (dim_vec b)" X x y]
split_access_snd_1[of "dim_vec c" _ "((dim_vec c) + (dim_vec b))" X x y]
vec_to_lin_poly_coeff_access[of _ c] using assms by auto
also have "... = c ∙ x"
unfolding scalar_prod_def
using split_vec_dims(1)[of "dim_vec c" "(dim_vec c) + (dim_vec b)" X x y] assms by auto
finally show ?thesis .
qed
lemma eval_lpoly_eq_dot_prod_split2:
assumes "(x, y) = split_n_m_x (dim_vec b) (dim_vec c) X"
shows"(vec_to_lpoly (0⇩v (dim_vec b) @⇩v c)) ⦃⟨X⟩⦄ = c ∙ y"
proof -
let ?p = "(vec_to_lpoly ((0⇩v (dim_vec b) @⇩v c)))"
let ?v0 = "(0⇩v (dim_vec b) @⇩v c)"
have *: "∀i<dim_vec b. Abstract_Linear_Poly.coeff ?p i = 0"
using coeff_nonzero_dim_vec_non_zero(1) by fastforce
have **: "dim_vec ?v0 = dim_vec b + dim_vec c"
by simp
have "?p ⦃⟨X⟩⦄ = (∑i∈vars ?p. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
using eval_poly_with_sum by blast
also have "... = (∑i∈{0..<dim_vec ?v0}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
using eval_poly_with_sum_superset[of "{0..<dim_vec ?v0}" ?p "⟨X⟩"] calculation
vars_subset_dim_vec_to_lpoly_dim[of ?v0] by force
also have "... = (∑i∈{0..<dim_vec b}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i) +
(∑i∈{(dim_vec b)..<dim_vec ?v0}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
by (simp add: sum.atLeastLessThan_concat)
also have "... = (∑i∈{(dim_vec b)..<dim_vec ?v0}. Abstract_Linear_Poly.coeff ?p i * ⟨X⟩ i)"
using * by simp
also have "... = (∑i∈{(dim_vec b)..<dim_vec ?v0}. ?v0$i * ⟨X⟩ i)"
using vec_to_lin_poly_coeff_access by auto
also have "... = (∑i∈{0..<dim_vec c}. ?v0$(i+dim_vec b) * ⟨X⟩ (i+dim_vec b))"
using index_zero_vec(2)[of "dim_vec b"] index_append_vec(2)[of "0⇩v (dim_vec b)" c] ** *
sum.shift_bounds_nat_ivl[of "(λi. ?v0$i * ⟨X⟩ i)" 0 "dim_vec b" "dim_vec c"]
by (simp add: add.commute)
also have "... = (∑i∈{0..<dim_vec c}. c$i * ⟨X⟩ (i+dim_vec b))"
by auto
also have "... = (∑i∈{0..<dim_vec c}. c$i * y$i)"
using split_access_snd_2[of x y "(dim_vec b)" "(dim_vec c)" X] assms
by (metis (mono_tags, lifting) atLeastLessThan_iff split_access_snd_2
split_n_m_x_abbrev_dims(2) split_vec_dims(1) sum.cong)
also have "... = c ∙ y"
by (metis assms scalar_prod_def split_n_m_x_abbrev_dims(2))
finally show ?thesis .
qed
lemma x_times_c_geq_y_times_b_split_dotP:
assumes "⟨X⟩ ⊨⇩c x_times_c_geq_y_times_b c b"
assumes "(x, y) = split_n_m_x (dim_vec c) (dim_vec b) X"
shows "c ∙ x ≥ b ∙ y"
using assms lpoly_of_v_equals_v_append0 eval_lpoly_eq_dot_prod_split2[of x y c b X]
eval_lpoly_eq_dot_prod_split1[of x y c b X]
by (auto simp: x_times_c_geq_y_times_b_def valuate_minus)
lemma mult_right_leq:
fixes A :: "('a::{comm_semiring_1,ordered_semiring}) mat"
assumes "dim_vec y = dim_vec b"
and "∀i < dim_vec y. y$i ≥ 0"
and "[A *⇩v x]≤ b"
shows "(A *⇩v x) ∙ y ≤ b ∙ y"
proof -
have "(∑n<dim_vec b. (A *⇩v x) $ n * y $ n) ≤ (∑n<dim_vec b. b $ n * y $ n)"
by (metis (no_types, lifting) assms(1) assms(2) assms(3) lessThan_iff
mat_times_vec_leq_def mult_right_mono sum_mono)
then show ?thesis
by (metis (no_types) assms(1) atLeast0LessThan scalar_prod_def)
qed
lemma mult_right_eq:
assumes "dim_vec x = dim_vec c"
and "[y ⇩v* A]=c"
shows "(A⇧T *⇩v y) ∙ x = c ∙ x"
unfolding scalar_prod_def
using atLeastLessThan_iff[of _ 0 "dim_vec x"] vec_times_mat_eq_def[of y A c]
sum.cong[of _ _ "λi. (A⇧T *⇩v y) $ i * x $ i" "λi. c $ i * x $ i"]
by (metis (mono_tags, lifting) assms(1) assms(2))
lemma soundness_mat_x_leq:
assumes "dim_row A = dim_vec b"
assumes "simplex (mat_x_leq_vec A b) = Sat X"
shows "∃x. [A *⇩v x]≤b"
proof
define x where x: "x = fst (split_n_m_x (dim_col A) (dim_row A) X)"
have *: "dim_vec x = dim_col A" by (simp add: split_i_j_x_def x)
have "∀i<dim_vec b. (A *⇩v x) $ i ≤ b $ i"
proof (standard, standard)
fix i
assume "i < dim_vec b"
have "row A i ∙ x ≤ b$i"
using mat_x_leq_vec_sol[of A b X i]
by (metis ‹i < dim_vec b› assms(1) assms(2) eval_lpoly_eq_dot_prod_split1
fst_conv index_row(2) matrix_to_lp_vec_to_lpoly_row simplex(3) split_i_j_x_def x)
then show "(A *⇩v x) $ i ≤ b $ i"
by (simp add: ‹i < dim_vec b› assms(1))
qed
then show "[A *⇩v x]≤b"
using mat_times_vec_leqI[of A b x, OF assms(1) *[symmetric]] by auto
qed
lemma completeness_mat_x_leq:
assumes "∃x. [A *⇩v x]≤b"
shows "∃X. simplex (mat_x_leq_vec A b) = Sat X"
proof (rule ccontr)
assume 1: "∄X. simplex (mat_x_leq_vec A b) = Inr X"
have *: "∄v. v ⊨⇩c⇩s set (mat_x_leq_vec A b)"
using simplex(1)[of "mat_x_leq_vec A b"] using "1" sum.exhaust_sel by blast
then have "dim_vec b = dim_row A" using assms mat_times_vec_leqD(1)[of A _ b] by auto
then obtain x where x: "[A *⇩v x]≤b"
using assms by blast
have x_A: "dim_vec x = dim_col A"
using x by auto
define v where v: "v = (λi. (if i < dim_vec x then x$i else 0))"
have v_d: "∀i < dim_vec x. x$i = v i"
by (simp add: v)
have "v ⊨⇩c⇩s set (mat_x_leq_vec A b)"
proof
fix c
assume "c ∈ set (mat_x_leq_vec A b)"
then obtain i where i: "c = LEQ (matrix_to_lpolies A!i) (b$i)" "i < dim_vec b"
by auto
let ?p = "matrix_to_lpolies A!i"
have 2: "?p⦃ v ⦄ = (row A i) ∙ x"
using matrix_to_lpolies_lambda_valuate_scalarP[of i A x] v
by (metis ‹dim_vec b = dim_row A› i(2) x_A)
also have "... ≤ b$i"
by (metis i(2) index_mult_mat_vec mat_times_vec_leq_def x)
finally show "v ⊨⇩c c"
using i(1) satisfies_constraint.simps(3)[of v "(matrix_to_lpolies A ! i)" "b $ i"]
2 ‹row A i ∙ x ≤ b $ i› by simp
qed
then show False using * by auto
qed
lemma soundness_mat_x_eq_vec:
assumes "dim_row A⇧T = dim_vec c"
assumes "simplex (x_mat_eq_vec c A⇧T) = Sat X"
shows "∃x. [x ⇩v* A]=c"
proof
define x where x: "x = fst (split_n_m_x (dim_col A⇧T) (dim_row A⇧T) X)"
have "dim_vec x = dim_col A⇧T"
unfolding split_i_j_x_def using split_vec_dims(1)[of "(dim_col A⇧T)" _ X x] fst_conv[of x]
by (simp add: split_i_j_x_def x)
have "∀i < dim_vec c. (A⇧T *⇩v x)$i = c$i"
proof (standard, standard)
fix i
assume a: "i < dim_vec c"
have *: "⟨X⟩ ⊨⇩c⇩s set (x_mat_eq_vec c A⇧T)"
using assms(2) simplex(3) by blast
then have "row A⇧T i ∙ x = c$i"
using x_mat_eq_vec_sol[of c "A⇧T" "⟨X⟩" i, OF * a] eval_lpoly_eq_dot_prod_split1 fstI
by (metis a assms(1) index_row(2) matrix_to_lpolies_vec_of_row split_i_j_x_def x)
then show "(A⇧T *⇩v x) $ i = c $ i"
unfolding mult_mat_vec_def using a assms(1) by auto
qed
then show "[x ⇩v* A]=c"
using mat_times_vec_eqI[of A x c, OF ‹dim_vec x = dim_col A⇧T›[symmetric] assms(1)] by auto
qed
lemma completeness_mat_x_eq_vec:
assumes "∃x. [x ⇩v* A]=c"
shows "∃X. simplex (x_mat_eq_vec c A⇧T) = Sat X"
proof (rule ccontr)
assume 1: "∄X. simplex (x_mat_eq_vec c A⇧T) = Inr X"
then have *: "∄v. v ⊨⇩c⇩s set (x_mat_eq_vec c A⇧T)"
using simplex(1)[of "x_mat_eq_vec c A⇧T"] using sum.exhaust_sel 1 by blast
then have "dim_vec c = dim_col A" using assms
by (metis index_transpose_mat(2) vec_times_mat_eqD(3))
obtain x where " [x ⇩v* A]=c" using assms by auto
then have "dim_vec x = dim_col A⇧T" using assms
by (metis ‹[x ⇩v* A]=c› vec_times_mat_eq_def)
define v where v: "v = (λi. (if i < dim_vec x then x$i else 0))"
have v_d: "∀i < dim_vec x. x$i = v i"
by (simp add: v)
have "v ⊨⇩c⇩s set (x_mat_eq_vec c A⇧T)"
proof
fix a
assume "a ∈ set (x_mat_eq_vec c A⇧T)"
then obtain i where i: "a = EQ (matrix_to_lpolies A⇧T!i) (c$i)" "i < dim_vec c"
by (metis (no_types, lifting) add_cancel_right_left diff_zero in_set_conv_nth length_map length_upt nth_map_upt x_mat_eq_vec.simps)
let ?p = "matrix_to_lpolies A⇧T!i"
have 2: "?p⦃ v ⦄ = (row A⇧T i) ∙ x"
using matrix_to_lpolies_lambda_valuate_scalarP[of i "A⇧T" x] v
by (metis ‹dim_vec c = dim_col A› ‹dim_vec x = dim_col A⇧T› i(2) index_transpose_mat(2))
also have "... = c$i"
by (metis ‹[x ⇩v* A]=c› ‹dim_vec c = dim_col A› i(2) index_mult_mat_vec index_transpose_mat(2) vec_times_mat_eqD(1))
finally show "v ⊨⇩c a"
using i(1) satisfies_constraint.simps(5)[of v "(matrix_to_lpolies A⇧T ! i)" "(c $ i)"] by simp
qed
then show False
using "*" by blast
qed
lemma soundness_mat_leqb_eqc1:
assumes "dim_row A = dim_vec b"
assumes "simplex (mat_leqb_eqc A b c) = Sat X"
shows "∃x. [A *⇩v x]≤b"
proof
define x where x: "x = fst (split_n_m_x (dim_col A) (dim_row A) X)"
have *: "dim_vec x = dim_col A" by (simp add: split_i_j_x_def x)
have "∀i<dim_vec b. (A *⇩v x) $ i ≤ b $ i"
proof (standard, standard)
fix i
assume "i < dim_vec b"
have "row A i ∙ x ≤ b$i"
using mat_x_leq_vec_sol[of A b X i]
by (metis ‹i < dim_vec b› assms(1) assms(2) fst_conv split_i_j_x_def x
index_mult_mat_vec mat_leqb_eqc_split_simplex_correct1 mat_times_vec_leqD(3))
then show "(A *⇩v x) $ i ≤ b $ i"
by (simp add: ‹i < dim_vec b› assms(1))
qed
then show "[A *⇩v x]≤b"
using mat_times_vec_leqI[of A b x, OF assms(1) *[symmetric]] by auto
qed
lemma soundness_mat_leqb_eqc2:
assumes "dim_row A⇧T = dim_vec c"
assumes "dim_col A⇧T = dim_vec b"
assumes "simplex (mat_leqb_eqc A b c) = Sat X"
shows "∃y. [y ⇩v* A]=c"
proof (standard, intro mat_times_vec_eqI)
define y where x: "y = snd (split_n_m_x (dim_col A) (dim_row A) X)"
have *: "dim_vec y = dim_row A" by (simp add: split_i_j_x_def x)
show "dim_col A⇧T = dim_vec y" by (simp add: "*")
show "dim_row A⇧T = dim_vec c" using assms(1) by blast
show "⋀i. i < dim_vec c ⟹ (A⇧T *⇩v y) $ i = c $ i"
proof -
fix i
assume a: "i < dim_vec c"
have "[y ⇩v* A]=c"
using mat_leqb_eqc_split_correct2[of c A b _ _ y, OF assms(1)[symmetric] assms(2)[symmetric]]
by (metis Matrix.transpose_transpose assms(3) index_transpose_mat(2)
simplex(3) snd_conv split_i_j_x_def x)
then show "(A⇧T *⇩v y) $ i = c $ i"
by (metis a vec_times_mat_eq_def)
qed
qed
lemma completeness_mat_leqb_eqc:
assumes "∃x. [A *⇩v x]≤b"
and "∃y. [y ⇩v* A]=c"
shows "∃X. simplex (mat_leqb_eqc A b c) = Sat X"
proof (rule ccontr)
assume 1: "∄X. simplex (mat_leqb_eqc A b c) = Sat X"
have *: "∄v. v ⊨⇩c⇩s set (mat_leqb_eqc A b c)"
using simplex(1)[of "mat_leqb_eqc A b c"] using "1" sum.exhaust_sel by blast
then have "dim_vec b = dim_row A"
using assms mat_times_vec_leqD(1)[of A _ b] by presburger
then obtain x y where x: "[A *⇩v x]≤b" "[y ⇩v* A]=c"
using assms by blast
have x_A: "dim_vec x = dim_col A"
using x by auto
have yr: "dim_vec y = dim_row A"
using vec_times_mat_eq_def x(2) by force
define v where v: "v = (λi. (if i < dim_vec (x@⇩vy) then (x@⇩vy)$i else 0))"
have v_d: "∀i < dim_vec (x@⇩vy). (x@⇩vy)$i = v i"
by (simp add: v)
have i_in: "∀i ∈ {0..< dim_vec y}. y$i = v (i+dim_vec x)"
by (simp add: v)
have "v ⊨⇩c⇩s set (mat_leqb_eqc A b c)"
proof
fix e
assume asm: "e ∈ set (mat_leqb_eqc A b c)"
define lst where lst: "lst = matrix_to_lpolies (two_block_non_interfering A A⇧T)"
let ?L = "[LEQ (lst!i) (b$i) . i <- [0..<dim_vec b]] @
[EQ (lst!i) ((b@⇩vc)$i) . i <- [dim_vec b ..< dim_vec (b@⇩vc)]]"
have L: "mat_leqb_eqc A b c = ?L"
by (metis (full_types) lst mat_leqb_eqc.simps)
then obtain i where i: "e = ?L!i" "i ∈{0..<length ?L}"
using asm by (metis atLeastLessThan_iff in_set_conv_nth not_le not_less0)
have ldimbc: "length ?L = dim_vec (b@⇩vc)"
using i(2) by auto
consider (leqb) "i ∈ {0..<dim_vec b}" | (eqc) "i ∈ {dim_vec b..<length ?L}"
using i(2) leI by auto
then show "v ⊨⇩c e"
proof (cases)
case leqb
have il: "i < dim_vec b"
using atLeastLessThan_iff leqb by blast
have iA: "i < dim_row A"
using ‹dim_vec b = dim_row A› ‹i < dim_vec b› by linarith
then have *: "e = LEQ (lst!i) (b$i)"
by (simp add: i(1) nth_append il)
then have "... = LEQ ((matrix_to_lpolies A)!i) (b$i)"
using mat_leqb_eqc_for_LEQ[of i b A c, OF il ‹i < dim_row A›] L i(1) by simp
then have eqmp: "lst!i = ((matrix_to_lpolies A)!i)"
by blast
have sset: "vars (lst!i) ⊆ {0..<dim_vec x}" using matrix_to_lpolies_vec_of_row
by (metis ‹i < dim_row A› eqmp index_row(2)
vars_subset_dim_vec_to_lpoly_dim x_A)
have **: "((lst!i) ⦃ v ⦄) = ((vec_to_lpoly (row A i)) ⦃ v ⦄)"
by (simp add: ‹i < dim_row A› eqmp)
also have "... = (∑j∈vars(lst!i). Abstract_Linear_Poly.coeff (lst!i) j * v j)"
using ** eval_poly_with_sum by auto
also have "... = (∑j∈{0..<dim_vec x}. Abstract_Linear_Poly.coeff (lst!i) j * v j)"
using sset eval_poly_with_sum_superset[of "{0..<dim_vec x}" "lst!i" v,
OF finite_atLeastLessThan sset] "**" using calculation by linarith
also have "... = (∑j∈{0..<dim_vec x}. Abstract_Linear_Poly.coeff (lst!i) j * x$j)"
using v by (auto split: if_split)
also have "... = (∑j∈{0..<dim_vec x}. (row A i)$j * x$j)"
using matrix_to_lpolies_vec_of_row[of i A, OF iA]
vec_to_lin_poly_coeff_access[of _ "row A i"] index_row(2)[of A i]
atLeastLessThan_iff by (metis (no_types, lifting) eqmp sum.cong x_A)
also have "... = row A i ∙ x" unfolding scalar_prod_def by (simp)
also have "... ≤ b$i"
by (metis ‹i < dim_vec b› index_mult_mat_vec mat_times_vec_leq_def x(1))
finally show ?thesis
by (simp add: "*")
next
case eqc
have igeq: "i ≥ dim_vec b"
using atLeastLessThan_iff eqc by blast
have *: "i < length ?L"
using atLeastLessThan_iff eqc by blast
have "e =?L!i"
using L i(1) by presburger
have "?L!i ∈ set [EQ (lst!i) ((b@⇩vc)$i). i <- [dim_vec b..< dim_vec (b@⇩vc)]]"
using in_second_append_list length_map
by (metis (no_types, lifting) igeq * length_upt minus_nat.diff_0)
then have "?L!i = [EQ (lst!i) ((b@⇩vc)$i). i <- [dim_vec b..< dim_vec (b@⇩vc)]]!(i-dim_vec b)"
by (metis (no_types, lifting) ‹dim_vec b ≤ i› diff_zero leD
length_map length_upt nth_append)
then have "?L!i = EQ (lst!i) ((b@⇩vc)$i)"
using add_diff_inverse_nat diff_less_mono
by (metis (no_types, lifting) ‹dim_vec b ≤ i› * ldimbc leD nth_map_upt)
then have e: "e = EQ (lst!i) ((b@⇩vc)$i)"
using i(1) by blast
with mat_leqb_eqc_for_EQ[of b i c A, OF igeq]
have lsta: "(lst!i) = (vec_to_lpoly (0⇩v (dim_col A) @⇩v row A⇧T (i - dim_vec b)))"
by (metis (no_types, lifting) ‹dim_vec b = dim_row A› * ldimbc assms(2) igeq
index_append_vec(2) lst matrix_to_lpolies_vec_of_row vec_times_mat_eq_def
two_block_non_interfering_dims(1) two_block_non_interfering_row_comp2 )
let ?p = "(vec_to_lpoly (0⇩v (dim_col A) @⇩v row A⇧T (i - dim_vec b)))"
have "dim_poly ?p ≤ dim_col A + dim_row A"
using dim_poly_of_append_vec[of "0⇩v (dim_col A)" "row A⇧T (i - dim_vec b)"]
index_zero_vec(2)[of "dim_col A"]
by (metis ‹dim_vec (0⇩v (dim_col A)) = dim_col A› index_row(2) index_transpose_mat(3))
have "∀i < dim_col A. Abstract_Linear_Poly.coeff ?p i = 0"
using vec_coeff_append1[of _ "0⇩v (dim_col A)" "row A⇧T (i - dim_vec b)"]
by (metis atLeastLessThan_iff index_zero_vec(1) index_zero_vec(2) zero_le)
then have "dim_vec (0⇩v (dim_col A) @⇩v row A⇧T (i - dim_vec b)) = dim_col A + dim_row A"
by (metis index_append_vec(2) index_row(2) index_transpose_mat(3) index_zero_vec(2))
then have allcr: "∀j∈{0..<dim_row A}. Abstract_Linear_Poly.coeff ?p (j+dim_col A) = (row A⇧T (i - dim_vec b))$j"
by (metis add_diff_cancel_right' atLeastLessThan_iff diff_add_inverse index_zero_vec(2)
le_add_same_cancel2 less_diff_conv vec_coeff_append2)
have vs: "vars ?p ⊆ {dim_col A..<dim_col A + dim_row A}"
using vars_vec_append_subset by (metis index_row(2) index_transpose_mat(3))
have "?p ⦃ v ⦄ = (∑j∈vars ?p. Abstract_Linear_Poly.coeff ?p j * v j)"
using eval_poly_with_sum by blast
also have "... = (∑j∈{dim_col A..<dim_col A + dim_row A}. Abstract_Linear_Poly.coeff ?p j * v j)"
by (metis (mono_tags, lifting) DiffD2 vs coeff_zero finite_atLeastLessThan
mult_not_zero sum.mono_neutral_left)
also have "... = (∑j∈{0..<dim_row A}. Abstract_Linear_Poly.coeff ?p (j+dim_col A) * v (j+dim_col A))"
using sum.shift_bounds_nat_ivl[of "λj. Abstract_Linear_Poly.coeff ?p j * v j" 0 "dim_col A" "dim_row A"]
by (metis (no_types, lifting) add.commute add_cancel_left_left)
also have "... = (∑j∈{0..<dim_row A}. Abstract_Linear_Poly.coeff ?p (j+dim_col A) * y$j)"
using v i_in yr by (metis (no_types, lifting) sum.cong x_A)
also have "... = (∑j∈{0..<dim_row A}. (row A⇧T (i - dim_vec b))$j * y$j)"
using allcr by (metis (no_types, lifting) sum.cong)
also have "... = (row A⇧T (i - dim_vec b)) ∙ y"
by (metis ‹dim_vec y = dim_row A› scalar_prod_def)
also have "... = (b@⇩vc)$i"
using vec_times_mat_eqD[OF x(2)] * igeq by auto
finally show ?thesis
using e lsta satisfies_constraint.simps(5)[of _ "(lst ! i)" "((b @⇩v c) $ i)"] by simp
qed
qed
then show False using * by blast
qed
lemma sound_and_compltete_mat_leqb_eqc [iff]:
assumes "dim_row A⇧T = dim_vec c"
assumes "dim_col A⇧T = dim_vec b"
shows "(∃x. [A *⇩v x]≤b) ∧ (∃y. [y ⇩v* A]=c) ⟷ (∃X. simplex (mat_leqb_eqc A b c) = Sat X)"
by (metis assms(1) assms(2) completeness_mat_leqb_eqc index_transpose_mat(3)
soundness_mat_leqb_eqc1 soundness_mat_leqb_eqc2)
section ‹ Translate Inequalities to Matrix Form ›
fun nonstrict_constr where
"nonstrict_constr (LEQ p r) = True" |
"nonstrict_constr (GEQ p r) = True" |
"nonstrict_constr (EQ p r) = True" |
"nonstrict_constr _ = False"
abbreviation "nonstrict_constrs cs ≡ (∀a ∈ set cs. nonstrict_constr a)"
fun transf_constraint where
"transf_constraint (LEQ p r) = [LEQ p r]" |
"transf_constraint (GEQ p r) = [LEQ (-p) (-r)]" |
"transf_constraint (EQ p r) = [LEQ p r, LEQ (-p) (-r)]" |
"transf_constraint _ = []"
fun transf_constraints where
"transf_constraints [] = []" |
"transf_constraints (x#xs) = transf_constraint x @ (transf_constraints xs)"
lemma trans_constraint_creats_LEQ_only:
assumes "transf_constraint x ≠ []"
shows "(∀x ∈ set (transf_constraint x). ∃a b. x = LEQ a b)"
using assms by (cases x, auto+)
lemma trans_constraints_creats_LEQ_only:
assumes "transf_constraints xs ≠ []"
assumes "x ∈ set (transf_constraints xs)"
shows "∃p r. LEQ p r = x"
using assms apply(induction xs)
using trans_constraint_creats_LEQ_only apply(auto)
apply fastforce
apply (metis in_set_simps(3) trans_constraint_creats_LEQ_only)
by fastforce
lemma non_strict_constr_no_LT:
assumes "nonstrict_constrs cs"
shows "∀x ∈ set cs. ¬(∃a b. LT a b = x)"
using assms nonstrict_constr.simps(4) by blast
lemma non_strict_constr_no_GT:
assumes "nonstrict_constrs cs"
shows "∀x ∈ set cs. ¬(∃a b. GT a b = x)"
using assms nonstrict_constr.simps(5) by blast
lemma non_strict_consts_cond:
assumes "⋀x. x ∈ set cs ⟹ ¬(∃a b. LT a b = x)"
assumes "⋀x. x ∈ set cs ⟹ ¬(∃a b. GT a b = x)"
shows "nonstrict_constrs cs"
by (metis assms(1-2) nonstrict_constr.elims(3))
lemma sat_constr_sat_transf_constrs:
assumes "v ⊨⇩c cs"
shows "v ⊨⇩c⇩s set (transf_constraint cs)"
using assms by (cases cs) (simp add: valuate_uminus valuate_minus)+
lemma sat_constrs_sat_transf_constrs:
assumes "v ⊨⇩c⇩s set cs"
shows "v ⊨⇩c⇩s set (transf_constraints cs)"
using assms by(induction cs, simp) (metis UnE list.set_intros(1)
list.set_intros(2) sat_constr_sat_transf_constrs set_append transf_constraints.simps(2))
lemma sat_transf_constrs_sat_constr:
assumes "nonstrict_constr cs"
assumes "v ⊨⇩c⇩s set (transf_constraint cs)"
shows "v ⊨⇩c cs"
using assms by (cases cs) (simp add: valuate_uminus valuate_minus)+
lemma sat_transf_constrs_sat_constrs:
assumes "nonstrict_constrs cs"
assumes "v ⊨⇩c⇩s set (transf_constraints cs)"
shows "v ⊨⇩c⇩s set cs"
using assms by (induction cs, auto) (simp add: sat_transf_constrs_sat_constr)
end