Theory LP_Duality
section ‹Weak and Strong Duality of Linear Programming›
theory LP_Duality
imports
Linear_Inequalities.Farkas_Lemma
Minimum_Maximum
begin
lemma weak_duality_theorem:
fixes A :: "'a :: linordered_comm_semiring_strict mat"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and x: "x ∈ carrier_vec nc"
and Axb: "A *⇩v x ≤ b"
and y0: "y ≥ 0⇩v nr"
and yA: "A⇧T *⇩v y = c"
shows "c ∙ x ≤ b ∙ y"
proof -
from y0 have y: "y ∈ carrier_vec nr" unfolding less_eq_vec_def by auto
have "c ∙ x = (A⇧T *⇩v y) ∙ x" unfolding yA by simp
also have "… = y ∙ (A *⇩v x)" using x y A by (metis transpose_vec_mult_scalar)
also have "… ≤ y ∙ b"
unfolding scalar_prod_def using A b Axb y0
by (auto intro!: sum_mono mult_left_mono simp: less_eq_vec_def)
also have "… = b ∙ y" using y b by (metis comm_scalar_prod)
finally show ?thesis .
qed
corollary unbounded_primal_solutions:
fixes A :: "'a :: linordered_idom mat"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and unbounded: "∀ v. ∃ x ∈ carrier_vec nc. A *⇩v x ≤ b ∧ c ∙ x ≥ v"
shows "¬ (∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c)"
proof
assume "(∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c)"
then obtain y where y: "y ≥ 0⇩v nr" and Ayc: "A⇧T *⇩v y = c"
by auto
from unbounded[rule_format, of "b ∙ y + 1"]
obtain x where x: "x ∈ carrier_vec nc" and Axb: "A *⇩v x ≤ b"
and le: "b ∙ y + 1 ≤ c ∙ x" by auto
from weak_duality_theorem[OF A b c x Axb y Ayc]
have "c ∙ x ≤ b ∙ y" by auto
with le show False by auto
qed
corollary unbounded_dual_solutions:
fixes A :: "'a :: linordered_idom mat"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and unbounded: "∀ v. ∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c ∧ b ∙ y ≤ v"
shows "¬ (∃ x ∈ carrier_vec nc. A *⇩v x ≤ b)"
proof
assume "∃ x ∈ carrier_vec nc. A *⇩v x ≤ b"
then obtain x where x: "x ∈ carrier_vec nc" and Axb: "A *⇩v x ≤ b" by auto
from unbounded[rule_format, of "c ∙ x - 1"]
obtain y where y: "y≥0⇩v nr" and Ayc: "A⇧T *⇩v y = c" and le: "b ∙ y ≤ c ∙ x - 1" by auto
from weak_duality_theorem[OF A b c x Axb y Ayc]
have "c ∙ x ≤ b ∙ y" by auto
with le show False by auto
qed
text ‹A version of the strong duality theorem which demands
that both primal and dual problem are solvable. At this point
we do not use min- or max-operations›
theorem strong_duality_theorem_both_sat:
fixes A :: "'a :: trivial_conjugatable_linordered_field mat"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and primal: "∃ x ∈ carrier_vec nc. A *⇩v x ≤ b"
and dual: "∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c"
shows "∃ x y.
x ∈ carrier_vec nc ∧ A *⇩v x ≤ b ∧
y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c ∧
c ∙ x = b ∙ y"
proof -
define M_up where "M_up = four_block_mat A (0⇩m nr nr) (mat_of_row (- c)) (mat_of_row b)"
define M_low where "M_low = four_block_mat (0⇩m nc nc) (A⇧T) (0⇩m nc nc) (- (A⇧T))"
define M_last where "M_last = append_cols (0⇩m nr nc) (- 1⇩m nr :: 'a mat)"
define M where "M = (M_up @⇩r M_low) @⇩r M_last"
define bc where "bc = ((b @⇩v 0⇩v 1) @⇩v (c @⇩v -c)) @⇩v (0⇩v nr)"
let ?nr = "((nr + 1) + (nc + nc)) + nr"
let ?nc = "nc + nr"
have M_up: "M_up ∈ carrier_mat (nr + 1) ?nc"
unfolding M_up_def using A b c by auto
have M_low: "M_low ∈ carrier_mat (nc + nc) ?nc"
unfolding M_low_def using A by auto
have M_last: "M_last ∈ carrier_mat nr ?nc"
unfolding M_last_def by auto
have M: "M ∈ carrier_mat ?nr ?nc"
using carrier_append_rows[OF carrier_append_rows[OF M_up M_low] M_last]
unfolding M_def by auto
have bc: "bc ∈ carrier_vec ?nr" unfolding bc_def
by (intro append_carrier_vec, insert b c, auto)
have "(∃xy. xy ∈ carrier_vec ?nc ∧ M *⇩v xy ≤ bc)"
proof (subst gram_schmidt.Farkas_Lemma'[OF M bc], intro allI impI, elim conjE)
fix ulv
assume ulv0: "0⇩v ?nr ≤ ulv" and Mulv: "M⇧T *⇩v ulv = 0⇩v ?nc"
from ulv0[unfolded less_eq_vec_def]
have ulv: "ulv ∈ carrier_vec ?nr" by auto
define u1 where "u1 = vec_first ulv ((nr + 1) + (nc + nc))"
define u2 where "u2 = vec_first u1 (nr + 1)"
define u3 where "u3 = vec_last u1 (nc + nc)"
define t where "t = vec_last ulv nr"
have ulvid: "ulv = u1 @⇩v t" using ulv
unfolding u1_def t_def by auto
have t: "t ∈ carrier_vec nr" unfolding t_def by auto
have u1: "u1 ∈ carrier_vec ((nr + 1) + (nc + nc))"
unfolding u1_def by auto
have u1id: "u1 = u2 @⇩v u3" using u1
unfolding u2_def u3_def by auto
have u2: "u2 ∈ carrier_vec (nr + 1)" unfolding u2_def by auto
have u3: "u3 ∈ carrier_vec (nc + nc)" unfolding u3_def by auto
define v where "v = vec_first u3 nc"
define w where "w = vec_last u3 nc"
have u3id: "u3 = v @⇩v w" using u3
unfolding v_def w_def by auto
have v: "v ∈ carrier_vec nc" unfolding v_def by auto
have w: "w ∈ carrier_vec nc" unfolding w_def by auto
define u where "u = vec_first u2 nr"
define L where "L = vec_last u2 1"
have u2id: "u2 = u @⇩v L" using u2
unfolding u_def L_def by auto
have u: "u ∈ carrier_vec nr" unfolding u_def by auto
have L: "L ∈ carrier_vec 1" unfolding L_def by auto
define vec1 where "vec1 = A⇧T *⇩v u + mat_of_col (- c) *⇩v L"
have vec1: "vec1 ∈ carrier_vec nc"
unfolding vec1_def mat_of_col_def using A u c L
by (meson add_carrier_vec mat_of_row_carrier(1) mult_mat_vec_carrier transpose_carrier_mat uminus_carrier_vec)
define vec2 where "vec2 = A *⇩v (v - w)"
have vec2: "vec2 ∈ carrier_vec nr"
unfolding vec2_def using A v w by auto
define vec3 where "vec3 = mat_of_col b *⇩v L"
have vec3: "vec3 ∈ carrier_vec nr"
using A b L unfolding mat_of_col_def vec3_def
by (meson add_carrier_vec mat_of_row_carrier(1) mult_mat_vec_carrier transpose_carrier_mat uminus_carrier_vec)
have Mt: "M⇧T = (M_up⇧T @⇩c M_low⇧T) @⇩c M_last⇧T"
unfolding M_def append_cols_def by simp
have "M⇧T *⇩v ulv = (M_up⇧T @⇩c M_low⇧T) *⇩v u1 + M_last⇧T *⇩v t"
unfolding Mt ulvid
by (subst mat_mult_append_cols[OF carrier_append_cols _ u1 t],
insert M_up M_low M_last, auto)
also have "M_last⇧T = 0⇩m nc nr @⇩r - 1⇩m nr" unfolding M_last_def
unfolding append_cols_def by (simp, subst transpose_uminus, auto)
also have "… *⇩v t = 0⇩v nc @⇩v - t"
by (subst mat_mult_append[OF _ _ t], insert t, auto)
also have "(M_up⇧T @⇩c M_low⇧T) *⇩v u1 = (M_up⇧T *⇩v u2) + (M_low⇧T *⇩v u3)"
unfolding u1id
by (rule mat_mult_append_cols[OF _ _ u2 u3], insert M_up M_low, auto)
also have "M_low⇧T = four_block_mat (0⇩m nc nc) (0⇩m nc nc) A (- A)"
unfolding M_low_def
by (subst transpose_four_block_mat, insert A, auto)
also have "… *⇩v u3 = (0⇩m nc nc *⇩v v + 0⇩m nc nc *⇩v w) @⇩v (A *⇩v v + - A *⇩v w)" unfolding u3id
by (subst four_block_mat_mult_vec[OF _ _ A _ v w], insert A, auto)
also have "0⇩m nc nc *⇩v v + 0⇩m nc nc *⇩v w = 0⇩v nc"
using v w by auto
also have "A *⇩v v + - A *⇩v w = vec2" unfolding vec2_def using A v w
by (metis (full_types) carrier_matD(2) carrier_vecD minus_add_uminus_vec mult_mat_vec_carrier mult_minus_distrib_mat_vec uminus_mult_mat_vec)
also have "M_up⇧T = four_block_mat A⇧T (mat_of_col (- c)) (0⇩m nr nr) (mat_of_col b)"
unfolding M_up_def mat_of_col_def
by (subst transpose_four_block_mat[OF A], insert b c, auto)
also have "… *⇩v u2 = vec1 @⇩v vec3"
unfolding u2id vec1_def vec3_def
by (subst four_block_mat_mult_vec[OF _ _ _ _ u L], insert A b c u, auto)
also have "(vec1 @⇩v vec3)
+ (0⇩v nc @⇩v vec2) + (0⇩v nc @⇩v - t) =
(vec1 @⇩v (vec3 + vec2 - t))"
apply (subst append_vec_add[of _ nc _ _ nr, OF vec1 _ vec3 vec2])
subgoal by force
apply (subst append_vec_add[of _ nc _ _ nr])
subgoal using vec1 by auto
subgoal by auto
subgoal using vec2 vec3 by auto
subgoal using t by auto
subgoal using vec1 by auto
done
finally have "vec1 @⇩v (vec3 + vec2 - t) = 0⇩v ?nc"
unfolding Mulv by simp
also have "… = 0⇩v nc @⇩v 0⇩v nr" by auto
finally have "vec1 = 0⇩v nc ∧ vec3 + vec2 - t = 0⇩v nr"
by (subst (asm) append_vec_eq[OF vec1], auto)
hence 01: "vec1 = 0⇩v nc" and 02: "vec3 + vec2 - t = 0⇩v nr" by auto
from 01 have "vec1 + mat_of_col c *⇩v L = mat_of_col c *⇩v L"
using c L vec1 unfolding mat_of_col_def by auto
also have "vec1 + mat_of_col c *⇩v L = A⇧T *⇩v u"
unfolding vec1_def
using A u c L unfolding mat_of_col_def mat_of_row_uminus transpose_uminus
by (subst uminus_mult_mat_vec, auto)
finally have As: "A⇧T *⇩v u = mat_of_col c *⇩v L" .
from 02 have "(vec3 + vec2 - t) + t = 0⇩v nr + t"
by simp
also have "(vec3 + vec2 - t) + t = vec2 + vec3"
using vec3 vec2 t by auto
finally have t23: "t = vec2 + vec3" using t by auto
have id0: "0⇩v ?nr = ((0⇩v nr @⇩v 0⇩v 1) @⇩v (0⇩v nc @⇩v 0⇩v nc)) @⇩v 0⇩v nr"
by auto
from ulv0[unfolded id0 ulvid u1id u2id u3id]
have "0⇩v nr ≤ u ∧ 0⇩v 1 ≤ L ∧ 0⇩v nc ≤ v ∧ 0⇩v nc ≤ w ∧ 0⇩v nr ≤ t"
apply (subst (asm) append_vec_le[of _ "(nr + 1) + (nc + nc)"])
subgoal by (intro append_carrier_vec, auto)
subgoal by (intro append_carrier_vec u L v w)
apply (subst (asm) append_vec_le[of _ "(nr + 1)"])
subgoal by (intro append_carrier_vec, auto)
subgoal by (intro append_carrier_vec u L v w)
apply (subst (asm) append_vec_le[OF _ u], force)
apply (subst (asm) append_vec_le[OF _ v], force)
by auto
hence ineqs: "0⇩v nr ≤ u" "0⇩v 1 ≤ L" "0⇩v nc ≤ v" "0⇩v nc ≤ w" "0⇩v nr ≤ t"
by auto
have "ulv ∙ bc = u ∙ b + (v ∙ c + w ∙ (-c))"
unfolding ulvid u1id u2id u3id bc_def
apply (subst scalar_prod_append[OF _ t])
apply (rule append_carrier_vec[OF append_carrier_vec[OF u L] append_carrier_vec[OF v w]])
apply (rule append_carrier_vec[OF append_carrier_vec[OF b] append_carrier_vec]; use c in force)
apply force
apply (subst scalar_prod_append)
apply (rule append_carrier_vec[OF u L])
apply (rule append_carrier_vec[OF v w])
subgoal by (rule append_carrier_vec, insert b, auto)
subgoal by (rule append_carrier_vec, insert c, auto)
apply (subst scalar_prod_append[OF u L b], force)
apply (subst scalar_prod_append[OF v w c], use c in force)
apply (insert L t, auto)
done
also have "v ∙ c + w ∙ (-c) = c ∙ v + (-c) ∙ w"
by (subst (1 2) comm_scalar_prod, insert w c v, auto)
also have "… = c ∙ v - (c ∙ w)" using c w by simp
also have "… = c ∙ (v - w)" using c v w
by (simp add: scalar_prod_minus_distrib)
finally have ulvbc: "ulv ∙ bc = u ∙ b + c ∙ (v - w)" .
define lam where "lam = L $ 0"
from ineqs(2) L have lam0: "lam ≥ 0" unfolding less_eq_vec_def lam_def by auto
have As: "A⇧T *⇩v u = lam ⋅⇩v c" unfolding As using c L
unfolding lam_def mat_of_col_def
by (intro eq_vecI, auto simp: scalar_prod_def)
have vec3: "vec3 = lam ⋅⇩v b" unfolding vec3_def using b L
unfolding lam_def mat_of_col_def
by (intro eq_vecI, auto simp: scalar_prod_def)
note preconds = lam0 ineqs(1,3-)[unfolded t23[unfolded vec2_def vec3]] As
have "0 ≤ u ∙ b + c ∙ (v - w)"
proof (cases "lam > 0")
case True
hence "u ∙ b = inverse lam * (lam * (b ∙ u))"
using comm_scalar_prod[OF b u] by simp
also have "… = inverse lam * ((lam ⋅⇩v b) ∙ u)"
using b u by simp
also have "… ≥ inverse lam * (-(A *⇩v (v - w)) ∙ u)"
proof (intro mult_left_mono)
show "0 ≤ inverse lam" using preconds by auto
show "-(A *⇩v (v - w)) ∙ u ≤ (lam ⋅⇩v b) ∙ u"
unfolding scalar_prod_def
apply (rule sum_mono)
subgoal for i
using lesseq_vecD[OF _ preconds(2), of nr i] lesseq_vecD[OF _ preconds(5), of nr i] u v w b A
by (intro mult_right_mono, auto)
done
qed
also have "inverse lam * (-(A *⇩v (v - w)) ∙ u) =
- (inverse lam * ((A *⇩v (v - w)) ∙ u))"
by (subst scalar_prod_uminus_left, insert A u v w, auto)
also have "(A *⇩v (v - w)) ∙ u = (A⇧T *⇩v u) ∙ (v - w)"
apply (subst transpose_vec_mult_scalar[OF A _ u])
subgoal using v w by force
by (rule comm_scalar_prod[OF _ u], insert A v w, auto)
also have "inverse lam * … = c ∙ (v - w)" unfolding preconds(6)
using True
by (subst scalar_prod_smult_left, insert c v w, auto)
finally show ?thesis by simp
next
case False
with preconds have lam: "lam = 0" by auto
from primal obtain x0 where x0: "x0 ∈ carrier_vec nc"
and Ax0b: "A *⇩v x0 ≤ b" by auto
from dual obtain y0 where y00: "y0 ≥ 0⇩v nr"
and Ay0c: "A⇧T *⇩v y0 = c" by auto
from y00 have y0: "y0 ∈ carrier_vec nr"
unfolding less_eq_vec_def by auto
have Au: "A⇧T *⇩v u = 0⇩v nc"
unfolding preconds lam using c by auto
have "0 = (A⇧T *⇩v u) ∙ x0" unfolding Au using x0 by auto
also have "… = u ∙ (A *⇩v x0)"
by (rule transpose_vec_mult_scalar[OF A x0 u])
also have "… ≤ u ∙ b"
unfolding scalar_prod_def
apply (use A x0 b in simp)
apply (intro sum_mono)
subgoal for i
using lesseq_vecD[OF _ preconds(2), of nr i] lesseq_vecD[OF _ Ax0b, of nr i] u v w b A x0
by (intro mult_left_mono, auto)
done
finally have ub: "0 ≤ u ∙ b" .
have "c ∙ (v - w) = (A⇧T *⇩v y0) ∙ (v - w)" unfolding Ay0c by simp
also have "… = y0 ∙ (A *⇩v (v - w))"
by (subst transpose_vec_mult_scalar[OF A _ y0], insert v w, auto)
also have "… ≥ 0"
unfolding scalar_prod_def
apply (use A v w in simp)
apply (intro sum_nonneg)
subgoal for i
using lesseq_vecD[OF _ y00, of nr i] lesseq_vecD[OF _ preconds(5)[unfolded lam], of nr i] A y0 v w b
by (intro mult_nonneg_nonneg, auto)
done
finally show ?thesis using ub by auto
qed
thus "0 ≤ ulv ∙ bc" unfolding ulvbc .
qed
then obtain xy where xy: "xy ∈ carrier_vec ?nc" and le: "M *⇩v xy ≤ bc" by auto
define x where "x = vec_first xy nc"
define y where "y = vec_last xy nr"
have xyid: "xy = x @⇩v y" using xy
unfolding x_def y_def by auto
have x: "x ∈ carrier_vec nc" unfolding x_def by auto
have y: "y ∈ carrier_vec nr" unfolding y_def by auto
have At: "A⇧T ∈ carrier_mat nc nr" using A by auto
have Ax1: "A *⇩v x @⇩v vec 1 (λ_. b ∙ y - c ∙ x) ∈ carrier_vec (nr + 1)"
using A x by fastforce
have b0cc: "(b @⇩v 0⇩v 1) @⇩v c @⇩v - c ∈ carrier_vec ((nr + 1) + (nc + nc))"
using b c
by (intro append_carrier_vec, auto)
have "M *⇩v xy = (M_up *⇩v xy @⇩v M_low *⇩v xy) @⇩v (M_last *⇩v xy)"
unfolding M_def
unfolding mat_mult_append[OF carrier_append_rows[OF M_up M_low] M_last xy]
by (simp add: mat_mult_append[OF M_up M_low xy])
also have "M_low *⇩v xy = (0⇩m nc nc *⇩v x + A⇧T *⇩v y) @⇩v (0⇩m nc nc *⇩v x + - A⇧T *⇩v y)"
unfolding M_low_def xyid
by (rule four_block_mat_mult_vec[OF _ At _ _ x y], insert A, auto)
also have "0⇩m nc nc *⇩v x + A⇧T *⇩v y = A⇧T *⇩v y" using A x y by auto
also have "0⇩m nc nc *⇩v x + - A⇧T *⇩v y = - A⇧T *⇩v y" using A x y by auto
also have "M_up *⇩v xy = (A *⇩v x + 0⇩m nr nr *⇩v y) @⇩v
(mat_of_row (- c) *⇩v x + mat_of_row b *⇩v y)"
unfolding M_up_def xyid
by (rule four_block_mat_mult_vec[OF A _ _ _ x y], insert b c, auto)
also have "A *⇩v x + 0⇩m nr nr *⇩v y = A *⇩v x" using A x y by auto
also have "mat_of_row (- c) *⇩v x + mat_of_row b *⇩v y =
vec 1 (λ _. b ∙ y - c ∙ x)"
unfolding mult_mat_vec_def using c x by (intro eq_vecI, auto)
also have "M_last *⇩v xy = - y"
unfolding M_last_def xyid using x y
by (subst mat_mult_append_cols[OF _ _ x y], auto)
finally have "((A *⇩v x @⇩v vec 1 (λ_. b ∙ y - c ∙ x)) @⇩v (A⇧T *⇩v y @⇩v - A⇧T *⇩v y)) @⇩v -y
= M *⇩v xy" ..
also have "… ≤ bc" by fact
also have "… = ((b @⇩v 0⇩v 1) @⇩v (c @⇩v -c)) @⇩v 0⇩v nr" unfolding bc_def by auto
finally have ineqs: "A *⇩v x ≤ b ∧ vec 1 (λ_. b ∙ y - c ∙ x) ≤ 0⇩v 1
∧ A⇧T *⇩v y ≤ c ∧ - A⇧T *⇩v y ≤ -c ∧ -y ≤ 0⇩v nr"
apply (subst (asm) append_vec_le[OF _ b0cc])
subgoal using A x y by (intro append_carrier_vec, auto)
apply (subst (asm) append_vec_le[OF Ax1], use b in fastforce)
apply (subst (asm) append_vec_le[OF _ b], use A x in force)
apply (subst (asm) append_vec_le[OF _ c], use A y in force)
by auto
show ?thesis
proof (intro exI conjI)
from ineqs show Axb: "A *⇩v x ≤ b" by auto
from ineqs have "- A⇧T *⇩v y ≤ -c" "A⇧T *⇩v y ≤ c" by auto
hence "A⇧T *⇩v y ≥ c" "A⇧T *⇩v y ≤ c" unfolding less_eq_vec_def using A y by auto
then show Aty: "A⇧T *⇩v y = c" by simp
from ineqs have "- y ≤ 0⇩v nr" by simp
then show y0: "0⇩v nr ≤ y" unfolding less_eq_vec_def by auto
from ineqs have "b ∙ y ≤ c ∙ x" unfolding less_eq_vec_def by auto
with weak_duality_theorem[OF A b c x Axb y0 Aty]
show "c ∙ x = b ∙ y" by auto
qed (insert x)
qed
text ‹A version of the strong duality theorem which demands
that the primal problem is solvable and the objective function
is bounded.›
theorem strong_duality_theorem_primal_sat_bounded:
fixes bound :: "'a :: trivial_conjugatable_linordered_field"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and sat: "∃ x ∈ carrier_vec nc. A *⇩v x ≤ b"
and bounded: "∀ x ∈ carrier_vec nc. A *⇩v x ≤ b ⟶ c ∙ x ≤ bound"
shows "∃ x y.
x ∈ carrier_vec nc ∧ A *⇩v x ≤ b ∧
y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c ∧
c ∙ x = b ∙ y"
proof (rule strong_duality_theorem_both_sat[OF A b c sat])
show "∃y≥0⇩v nr. A⇧T *⇩v y = c"
proof (rule ccontr)
assume "¬ ?thesis"
hence "∃y. y ∈ carrier_vec nc ∧ 0⇩v nr ≤ A *⇩v y ∧ 0 > y ∙ c"
by (subst (asm) gram_schmidt.Farkas_Lemma[OF _ c], insert A, auto)
then obtain y where y: "y ∈ carrier_vec nc"
and Ay0: "A *⇩v y ≥ 0⇩v nr" and yc0: "y ∙ c < 0" by auto
from sat obtain x where x: "x ∈ carrier_vec nc"
and Axb: "A *⇩v x ≤ b" by auto
define diff where "diff = bound + 1 - c ∙ x"
from x Axb bounded have "c ∙ x < bound + 1" by auto
hence diff: "diff > 0" unfolding diff_def by auto
from yc0 have inv: "inverse (- (y ∙ c)) > 0" by auto
define fact where "fact = diff * (inverse (- (y ∙ c)))"
have fact: "fact > 0" unfolding fact_def using diff inv by (metis mult_pos_pos)
define z where "z = x - fact ⋅⇩v y"
have "A *⇩v z = A *⇩v x - A *⇩v (fact ⋅⇩v y)"
unfolding z_def using A x y by (meson mult_minus_distrib_mat_vec smult_carrier_vec)
also have "… = A *⇩v x - fact ⋅⇩v (A *⇩v y)" using A y by auto
also have "… ≤ b"
proof (intro lesseq_vecI[OF _ b])
show "A *⇩v x - fact ⋅⇩v (A *⇩v y) ∈ carrier_vec nr" using A x y by auto
fix i
assume i: "i < nr"
have "(A *⇩v x - fact ⋅⇩v (A *⇩v y)) $ i
= (A *⇩v x) $ i - fact * (A *⇩v y) $ i"
using i A x y by auto
also have "… ≤ b $ i - fact * (A *⇩v y) $ i"
using lesseq_vecD[OF b Axb i] by auto
also have "… ≤ b $ i - 0 * 0" using lesseq_vecD[OF _ Ay0 i] fact A y i
by (intro diff_left_mono mult_monom, auto)
finally show "(A *⇩v x - fact ⋅⇩v (A *⇩v y)) $ i ≤ b $ i" by simp
qed
finally have Azb: "A *⇩v z ≤ b" .
have z: "z ∈ carrier_vec nc" using x y unfolding z_def by auto
have "c ∙ z = c ∙ x - fact * (c ∙ y)" unfolding z_def
using c x y by (simp add: scalar_prod_minus_distrib)
also have "… = c ∙ x + diff"
unfolding comm_scalar_prod[OF c y] fact_def using yc0 by simp
also have "… = bound + 1" unfolding diff_def by simp
also have "… > c ∙ z" using bounded Azb z by auto
finally show False by simp
qed
qed
text ‹A version of the strong duality theorem which demands
that the dual problem is solvable and the objective function
is bounded.›
theorem strong_duality_theorem_dual_sat_bounded:
fixes bound :: "'a :: trivial_conjugatable_linordered_field"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and sat: "∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c"
and bounded: "∀ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c ⟶ bound ≤ b ∙ y"
shows "∃ x y.
x ∈ carrier_vec nc ∧ A *⇩v x ≤ b ∧
y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c ∧
c ∙ x = b ∙ y"
proof (rule strong_duality_theorem_both_sat[OF A b c _ sat])
show "∃x∈carrier_vec nc. A *⇩v x ≤ b"
proof (rule ccontr)
assume "¬ ?thesis"
hence "¬ (∃x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b)" by auto
then obtain y where y0: "y ≥ 0⇩v nr" and Ay0: "A⇧T *⇩v y = 0⇩v nc" and yb: "y ∙ b < 0"
by (subst (asm) gram_schmidt.Farkas_Lemma'[OF A b], auto)
from sat obtain x where x0: "x ≥ 0⇩v nr" and Axc: "A⇧T *⇩v x = c" by auto
define diff where "diff = b ∙ x - (bound - 1)"
from x0 Axc bounded have "bound ≤ b ∙ x" by auto
hence diff: "diff > 0" unfolding diff_def by auto
define fact where "fact = - inverse (y ∙ b) * diff"
have fact: "fact > 0" unfolding fact_def using diff yb by (auto intro: mult_neg_pos)
define z where "z = x + fact ⋅⇩v y"
from x0 have x: "x ∈ carrier_vec nr"
unfolding less_eq_vec_def by auto
from y0 have y: "y ∈ carrier_vec nr"
unfolding less_eq_vec_def by auto
have "A⇧T *⇩v z = A⇧T *⇩v x + A⇧T *⇩v (fact ⋅⇩v y)"
unfolding z_def using A x y by (simp add: mult_add_distrib_mat_vec)
also have "… = A⇧T *⇩v x + fact ⋅⇩v (A⇧T *⇩v y)" using A y by auto
also have "… = c" unfolding Ay0 Axc using c by auto
finally have Azc: "A⇧T *⇩v z = c" .
have z0: "z ≥ 0⇩v nr" unfolding z_def
by (intro lesseq_vecI[of _ nr], insert x y lesseq_vecD[OF _ x0, of nr] lesseq_vecD[OF _ y0, of nr] fact,
auto intro!: add_nonneg_nonneg)
from bounded Azc z0 have bz: "bound ≤ b ∙ z" by auto
also have "… = b ∙ x + fact * (b ∙ y)" unfolding z_def using b x y
by (simp add: scalar_prod_add_distrib)
also have "… = diff + (bound - 1) + fact * (b ∙ y)"
unfolding diff_def by auto
also have "fact * (b ∙ y) = - diff" using yb
unfolding fact_def comm_scalar_prod[OF y b] by auto
finally show False by simp
qed
qed
text ‹Now the previous three duality theorems are formulated via min/max.›
corollary strong_duality_theorem_min_max:
fixes A :: "'a :: trivial_conjugatable_linordered_field mat"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and primal: "∃ x ∈ carrier_vec nc. A *⇩v x ≤ b"
and dual: "∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c"
shows "Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}
= Minimum {b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
and "has_Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}"
and "has_Minimum {b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
proof -
let ?Prim = "{c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}"
let ?Dual = "{b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
define Prim where "Prim = ?Prim"
define Dual where "Dual = ?Dual"
from strong_duality_theorem_both_sat[OF assms]
obtain x y where x: "x ∈ carrier_vec nc" and Axb: "A *⇩v x ≤ b"
and y: "y ≥ 0⇩v nr" and Ayc: "A⇧T *⇩v y = c"
and eq: "c ∙ x = b ∙ y" by auto
have cxP: "c ∙ x ∈ Prim" unfolding Prim_def using x Axb by auto
have cxD: "c ∙ x ∈ Dual" unfolding eq Dual_def using y Ayc by auto
{
fix z
assume "z ∈ Prim"
from this[unfolded Prim_def] obtain x' where x': "x' ∈ carrier_vec nc"
and Axb': "A *⇩v x' ≤ b" and z: "z = c ∙ x'" by auto
from weak_duality_theorem[OF A b c x' Axb' y Ayc, folded eq]
have "z ≤ c ∙ x" unfolding z .
} note cxMax = this
have max: "Maximum Prim = c ∙ x"
by (intro eqMaximumI cxP cxMax)
show "has_Maximum ?Prim"
unfolding Prim_def[symmetric] has_Maximum_def using cxP cxMax by auto
{
fix z
assume "z ∈ Dual"
from this[unfolded Dual_def] obtain y' where y': "y' ≥ 0⇩v nr"
and Ayc': "A⇧T *⇩v y' = c" and z: "z = b ∙ y'" by auto
from weak_duality_theorem[OF A b c x Axb y' Ayc', folded z]
have "c ∙ x ≤ z" .
} note cxMin = this
show "has_Minimum ?Dual"
unfolding Dual_def[symmetric] has_Minimum_def using cxD cxMin by auto
have min: "Minimum Dual = c ∙ x"
by (intro eqMinimumI cxD cxMin)
from min max show "Maximum ?Prim = Minimum ?Dual"
unfolding Dual_def Prim_def by auto
qed
corollary strong_duality_theorem_primal_sat_bounded_min_max:
fixes bound :: "'a :: trivial_conjugatable_linordered_field"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and sat: "∃ x ∈ carrier_vec nc. A *⇩v x ≤ b"
and bounded: "∀ x ∈ carrier_vec nc. A *⇩v x ≤ b ⟶ c ∙ x ≤ bound"
shows "Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}
= Minimum {b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
and "has_Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}"
and "has_Minimum {b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
proof -
let ?Prim = "{c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}"
let ?Dual = "{b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
from strong_duality_theorem_primal_sat_bounded[OF assms]
have "∃y≥0⇩v nr. A⇧T *⇩v y = c" by blast
from strong_duality_theorem_min_max[OF A b c sat this]
show "Maximum ?Prim = Minimum ?Dual" "has_Maximum ?Prim" "has_Minimum ?Dual"
by blast+
qed
corollary strong_duality_theorem_dual_sat_bounded_min_max:
fixes bound :: "'a :: trivial_conjugatable_linordered_field"
assumes A: "A ∈ carrier_mat nr nc"
and b: "b ∈ carrier_vec nr"
and c: "c ∈ carrier_vec nc"
and sat: "∃ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c"
and bounded: "∀ y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c ⟶ bound ≤ b ∙ y"
shows "Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}
= Minimum {b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
and "has_Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}"
and "has_Minimum {b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
proof -
let ?Prim = "{c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩v x ≤ b}"
let ?Dual = "{b ∙ y | y. y ≥ 0⇩v nr ∧ A⇧T *⇩v y = c}"
from strong_duality_theorem_dual_sat_bounded[OF assms]
have "∃ x ∈ carrier_vec nc. A *⇩v x ≤ b" by blast
from strong_duality_theorem_min_max[OF A b c this sat]
show "Maximum ?Prim = Minimum ?Dual" "has_Maximum ?Prim" "has_Minimum ?Dual"
by blast+
qed
end