Quelle  LP_Duality.thy

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)" 
    (* M = ( A   0) bc = (  b)
           (-c   b)      (  0)
           ( 0  At)      (  c)
           ( 0 -At)      ( -c)
           ( 0  -I)      (  0) *)
  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