| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Farkas/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 85 kB |
|
Quelle Farkas.thySprache: Isabelle |
|||||||||||||||
|
(* Authors: R. Bottesch, M. W. Haslbeck, R. Thiemann *) section ‹Farkas Coefficients via the Simplex Algorithm of Duterte and de~Moura› text ‹Let $c_1,\dots,c_n$ be a finite list of linear inequalities. Let $C$ be a list of pairs $(r_i,c_i)$ where $r_i$ is a rational number. We say that $C$ is a list of \emph{Farkas coefficients} if the sum of all products $r_i \cdot c_i$ results in an inequality that is trivially unsatisfiable. Farkas' Lemma states that a finite set of non-strict linear inequalities is unsatisfiable if and only if Farkas coefficients exist. We will prove this lemma with the help of the simplex algorithm of Dutertre and de~Moura's. Note that the simplex implementation works on four layers, and we will formulate a variant of Farkas' Lemma for each of these layers. theory Farkas imports Simplex.Simplex begin subsection ‹Linear Inequalities› text ‹Both Farkas' Lemma and Motzkin's Transposition Theorem require linear combi of inequalities. To this end we define one type that permits strict and non-stri inequalities which are always of the form ``polynomial R constant'' where R is e $\leq$ or $<$. On this type we can then define a commutative monoid. text ‹A type for the two relations: less-or-equal and less-than.› datatype le_rel = Leq_Rel | Lt_Rel primrec rel_of :: "le_rel ==> 'a :: lrv ==> 'a ==> bool" where "rel_of Leq_Rel = (≤)" | "rel_of Lt_Rel = (<)" instantiation le_rel :: comm_monoid_add begin definition "zero_le_rel = Leq_Rel" fun plus_le_rel where "plus_le_rel Leq_Rel Leq_Rel = Leq_Rel" | "plus_le_rel _ _ = Lt_Rel" instance proof fix a b c :: le_rel show "a + b + c = a + (b + c)" by (cases a; cases b; cases c, auto) show "a + b = b + a" by (cases a; cases b, auto) show "0 + a = a" unfolding zero_le_rel_def by (cases a, auto) qed end lemma Leq_Rel_0: "Leq_Rel = 0" unfolding zero_le_rel_def by simp datatype 'a le_constraint = Le_Constraint (lec_rel: le_rel) (lec_poly: linear_poly) (lec_ abbreviation (input) "Leqc ≡ Le_Constraint Leq_Rel" instantiation le_constraint :: (lrv) comm_monoid_add begin fun plus_le_constraint :: "'a le_constraint ==> 'a le_constraint ==> 'a le_constrai "plus_le_constraint (Le_Constraint r1 p1 c1) (Le_Constraint r2 p2 c2) = (Le_Constraint (r1 + r2) (p1 + p2) (c1 + c2))" definition zero_le_constraint :: "'a le_constraint" where "zero_le_constraint = Leqc 0 0" instance proof fix a b c :: "'a le_constraint" show "0 + a = a" by (cases a, auto simp: zero_le_constraint_def Leq_Rel_0) show "a + b = b + a" by (cases a; cases b, auto simp: ac_simps) show "a + b + c = a + (b + c)" by (cases a; cases b; cases c, auto simp: ac_simps) qed end primrec satisfiable_le_constraint :: "'a::lrv valuation ==> 'a le_constraint ==> bo "(v ⊨le (Le_Constraint rel l r)) ⟷ (rel_of rel (l{v}) r)" lemma satisfies_zero_le_constraint: "v ⊨le 0" by (simp add: valuate_zero zero_le_constraint_def) lemma satisfies_sum_le_constraints: assumes "v ⊨le c" "v ⊨le d" shows "v ⊨le (c + d)" proof - obtain lc rc ld rd rel1 rel2 where cd: "c = Le_Constraint rel1 lc rc" "d = Le_Constraint r by (cases c; cases d, auto) have 1: "rel_of rel1 (lc{v}) rc" using assms cd by auto have 2: "rel_of rel2 (ld{v}) rd" using assms cd by auto from 1 have le1: "lc{v} ≤ rc" by (cases rel1, auto) from 2 have le2: "ld{v} ≤ rd" by (cases rel2, auto) from 1 2 le1 le2 have "rel_of (rel1 + rel2) ((lc{v}) + (ld{v})) (rc + rd)" apply (cases rel1; cases rel2; simp add: add_mono) by (metis add.commute le_less_trans order.strict_iff_order plus_less)+ thus ?thesis by (auto simp: cd valuate_add) qed lemma satisfies_sumlist_le_constraints: assumes "∧ c. c ∈ set (cs :: 'a :: lrv le_constraint list) ==> v ⊨le c" shows "v ⊨le sum_list cs" using assms by (induct cs, auto intro: satisfies_zero_le_constraint satisfies_sum_le_constraints) lemma sum_list_lec: "sum_list ls = Le_Constraint (sum_list (map lec_rel ls)) (sum_list (map lec_poly ls)) (sum_list (map lec_const ls))" proof (induct ls) case Nil show ?case by (auto simp: zero_le_constraint_def Leq_Rel_0) next case (Cons l ls) show ?case by (cases l, auto simp: Cons) qed lemma sum_list_Leq_Rel: "((∑x←C. lec_rel (f x)) = Leq_Rel) ⟷ (∀ x ∈ set C. lec_rel proof (induct C) case (Cons c C) show ?case proof (cases "lec_rel (f c)") case Leq_Rel show ?thesis using Cons by (simp add: Leq_Rel Leq_Rel_0) qed simp qed (simp add: Leq_Rel_0) subsection ‹Farkas' Lemma on Layer 4› text ‹On layer 4 the algorithm works on a state containing a tableau, atoms (or b an assignment and a satisfiability flag. Only non-strict inequalities appear at In order to even state a variant of Farkas' Lemma on layer 4, we need conversions from atoms to non-strict constraints and then further to linear inequalities of type @{type le_constraint}. The latter conversion is a partial operation, since non-strict constraints of type @{type ns_constraint} permit greater-or-equal constraints, whereas @{typ allows only less-or-equal. text ‹The advantage of first going via @{type ns_constraint} is that this type pe with arbitrary rational numbers (the direction of the inequality must be flipped multiplying by a negative number, which is not possible with @{type le_constrain instantiation ns_constraint :: (scaleRat) scaleRat begin fun scaleRat_ns_constraint :: "rat ==> 'a ns_constraint ==> 'a ns_constraint" where "scaleRat_ns_constraint r (LEQ_ns p c) = (if (r < 0) then GEQ_ns (r *R p) (r *R c) else LEQ_ns (r *R p) (r *R c))" | "scaleRat_ns_constraint r (GEQ_ns p c) = (if (r > 0) then GEQ_ns (r *R p) (r *R c) else LEQ_ns (r *R p) (r *R c))" instance .. end lemma sat_scale_rat_ns: assumes "v ⊨ns ns" shows "v ⊨ns (f *R ns)" proof - have "f < 0 | f = 0 | f > 0" by auto then show ?thesis using assms by (cases ns, auto simp: valuate_scaleRat scaleRat_leq1 scaleR qed lemma scaleRat_scaleRat_ns_constraint: assumes "a ≠ 0 ==> b ≠ 0" shows "a *R (b *R (c :: 'a :: lrv ns_constraint)) = (a * b) *R c" proof - have "b > 0 ∨ b < 0 ∨ b = 0" by linarith moreover have "a > 0 ∨ a < 0 ∨ a = 0" by linarith ultimately show ?thesis using assms by (elim disjE; cases c, auto simp add: not_le not_less mult_neg_pos mult_neg_neg mult_nonpos_nonneg mult_nonpos_nonpos mult_nonneg_nonpos mu qed fun lec_of_nsc where "lec_of_nsc (LEQ_ns p c) = (Leqc p c)" fun is_leq_ns where "is_leq_ns (LEQ_ns p c) = True" | "is_leq_ns (GEQ_ns p c) = False" lemma lec_of_nsc: assumes "is_leq_ns c" shows "(v ⊨le lec_of_nsc c) ⟷ (v ⊨ns c)" using assms by (cases c, auto) fun nsc_of_atom where "nsc_of_atom (Leq var b) = LEQ_ns (lp_monom 1 var) b" | "nsc_of_atom (Geq var b) = GEQ_ns (lp_monom 1 var) b" lemma nsc_of_atom: "v ⊨ns nsc_of_atom a ⟷ v ⊨a a" by (cases a, auto) text ‹We say that $C$ is a list of Farkas coefficients \emph{for a given tableau it is a list of pairs $(r,a)$ such that $a \in as$, $r$ is non-zero, $r \cdot a$ `less-than-or-equal'-constraint, and the linear combination of inequalities must result in an inequality of the form $p \leq c$, where $c < 0$ p = 0$. definition farkas_coefficients_atoms_tableau where "farkas_coefficients_atoms_tableau (as :: 'a :: lrv atom set) t C = (∃ p c. (∀(r,a) ∈ set C. a ∈ as ∧ is_leq_ns (r *R nsc_of_atom a) ∧ r ≠ 0) ∧ (∑(r,a) ← C. lec_of_nsc (r *R nsc_of_atom a)) = Leqc p c ∧ c < 0 ∧ (∀ v :: 'a valuation. v ⊨t t ⟶(p{v} = 0)))" text ‹We first prove that if the check-function detects a conflict, then Farkas coefficients do exist for the tableau and atom set for which the conflict is detected.› definition bound_atoms :: "('i, 'a) state ==> 'a atom set" (‹BA›) where "bound_atoms s = (λ(v,x). Geq v x) ` (set_of_map (Bl s)) ∪ (λ(v,x). Leq v x) ` (set_of_map (Bu s))" context PivotUpdateMinVars begin lemma farkas_check: assumes check: "check s' = s" and U: "U s" "¬ U s'" and inv: "∇ s'" "△ (T s')" "⊨nolhs s'" "♢ s'" and index: "index_valid as s'" shows "∃ C. farkas_coefficients_atoms_tableau (snd ` as) (T s') C" proof - let ?Q = "λ s f p c C. set C ⊆ BA s ∧ distinct C ∧ (∀a ∈ set C. is_leq_ns (f (atom_var a) *R nsc_of_atom a) ∧ f (atom_var a) ≠ 0) ∧ (∑a ← C. lec_of_nsc (f (atom_var a) *R nsc_of_atom a)) = Leqc p c ∧ c < 0 ∧ (∀ v :: 'a valuation. v ⊨t T s ⟶(p{v} = 0))" let ?P = "λ s. U s ⟶ (∃ f p c C. ?Q s f p c C)" have "?P (check s')" proof (induct rule: check_induct''[OF inv, of ?P]) case (3 s xi dir I) have dir: "dir = Positive ∨ dir = Negative" by fact let ?eq = "(eq_for_lvar (T s) xi)" define Xj where "Xj = rvars_eq ?eq" define XLj where "XLj = Abstract_Linear_Poly.vars_list (rhs ?eq)" have [simp]: "set XLj = Xj" unfolding XLj_def Xj_def using set_vars_list by blast have XLj_distinct: "distinct XLj" unfolding XLj_def using distinct_vars_list by simp define A where "A = coeff (rhs ?eq)" have bounds_id: "BA (set_unsat I s) = BA s" "Bu (set_unsat I s) = Bu s" "Bl (set_uns by (auto simp: boundsl_def boundsu_def bound_atoms_def) have t_id: "T (set_unsat I s) = T s" by simp have u_id: "U (set_unsat I s) = True" by simp let ?p = "rhs ?eq - lp_monom 1 xi" have p_eval_zero: "?p { v } = 0" if "v ⊨t T s" for v :: "'a valuation" proof - have eqT: "?eq ∈ set (T s)" by (simp add: 3(7) eq_for_lvar local.min_lvar_not_in_bounds_lvars) have "v ⊨e ?eq" using that eqT satisfies_tableau_def by blast also have "?eq = (lhs ?eq, rhs ?eq)" by (cases ?eq, auto) also have "lhs ?eq = xi" by (simp add: 3(7) eq_for_lvar local.min_lvar_not_in_bounds_lva finally have "v ⊨e (xi, rhs ?eq)" . then show ?thesis by (auto simp: satisfies_eq_iff valuate_minus) qed have Xj_rvars: "Xj ⊆ rvars (T s)" unfolding Xj_def using 3 min_lvar_not_in_bounds_lvars rvars_of_lvar_rvars by blast have xi_lvars: "xi ∈ lvars (T s)" using 3 min_lvar_not_in_bounds_lvars rvars_of_lvar_rvars by blast have "lvars (T s) ∩ rvars (T s) = {}" using 3 normalized_tableau_def by auto with xi_lvars Xj_rvars have xi_Xj: "xi ∉ Xj" by blast have rhs_eval_xi: "(rhs (eq_for_lvar (T s) xi)) {⟨V s⟩} = ⟨V s⟩ xi" proof - have *: "(rhs eq) { v } = v (lhs eq)" if "v ⊨e eq" for v :: "'a valuation" and eq using satisfies_eq_def that by metis moreover have "⟨V s⟩ ⊨e eq_for_lvar (T s) xi" using 3 satisfies_tableau_def eq_for_lvar curr_val_satisfies_no_lhs_def xi_lvars by blast ultimately show ?thesis using eq_for_lvar xi_lvars by simp qed let ?Bl = "Direction.LB dir" let ?Bu = "Direction.UB dir" let ?lt = "Direction.lt dir" let ?le = "Simplex.le ?lt" let ?Geq = "Direction.GE dir" let ?Leq = "Direction.LE dir" have 0: "(if A x < 0 then ?Bl s x = Some (⟨V s⟩ x) else ?Bu s x = Some (⟨V s⟩ x)) ∧ A x if x: "x ∈ Xj" for x proof - have "Some (⟨V s⟩ x) = (?Bl s x)" if "A x < 0" proof - have cmp: "¬ ⊳lb ?lt (⟨V s⟩ x) (?Bl s x)" using x that dir min_rvar_incdec_eq_None[OF 3(9)] unfolding Xj_def A_def by auto then obtain c where c: "?Bl s x = Some c" by (cases "?Bl s x", auto simp: bound_compare_defs) also have "c = ⟨V s⟩ x" proof - have "x ∈ rvars (T s)" using that x Xj_rvars by blast then have "x ∈ (- lvars (T s))" using 3 unfolding normalized_tableau_def by auto moreover have "∀x∈(- lvars (T s)). in_bounds x ⟨V s⟩ (Bl s, Bu s)" using 3 unfolding curr_val_satisfies_no_lhs_def by (simp add: satisfies_bounds_set.simps) ultimately have "in_bounds x ⟨V s⟩ (Bl s, Bu s)" by blast moreover have "?le (⟨V s⟩ x) c" using cmp c dir unfolding bound_compare_defs by auto ultimately show ?thesis using c dir by (auto simp del: Simplex.bounds_lg) qed then show ?thesis using c by simp qed moreover have "Some (⟨V s⟩ x) = (?Bu s x)" if "0 < A x" proof - have cmp: "¬ ⊲ub ?lt (⟨V s⟩ x) (?Bu s x)" using x that min_rvar_incdec_eq_None[OF 3(9)] unfolding Xj_def A_def by auto then obtain c where c: "?Bu s x = Some c" by (cases "?Bu s x", auto simp: bound_compare_defs) also have "c = ⟨V s⟩ x" proof - have "x ∈ rvars (T s)" using that x Xj_rvars by blast then have "x ∈ (- lvars (T s))" using 3 unfolding normalized_tableau_def by auto moreover have "∀x∈(- lvars (T s)). in_bounds x ⟨V s⟩ (Bl s, Bu s)" using 3 unfolding curr_val_satisfies_no_lhs_def by (simp add: satisfies_bounds_set.simps) ultimately have "in_bounds x ⟨V s⟩ (Bl s, Bu s)" by blast moreover have "?le c (⟨V s⟩ x)" using cmp c dir unfolding bound_compare_defs by auto ultimately show ?thesis using c dir by (auto simp del: Simplex.bounds_lg) qed then show ?thesis using c by simp qed moreover have "A x ≠ 0" using that coeff_zero unfolding A_def Xj_def by auto ultimately show ?thesis using that by auto qed have l_Ba: "l ∈ BA s" if "l ∈ {?Geq xi (the (?Bl s xi))}" for l proof - from that have l: "l = ?Geq xi (the (?Bl s xi))" by simp from 3(8) obtain c where bl': "?Bl s xi = Some c" by (cases "?Bl s xi", auto simp: bound_compare_defs) hence bl: "(xi, c) ∈ set_of_map (?Bl s)" unfolding set_of_map_def by auto show "l ∈ BA s" unfolding l bound_atoms_def using bl bl' dir by auto qed let ?negA = "filter (λ x. A x < 0) XLj" let ?posA = "filter (λ x. ¬ A x < 0) XLj" define neg where "neg = (if dir = Positive then (λ x :: rat. x) else uminus)" define negP where "negP = (if dir = Positive then (λ x :: linear_poly. x) else uminu define nega where "nega = (if dir = Positive then (λ x :: 'a. x) else uminus)" from dir have dirn: "dir = Positive ∧ neg = (λ x. x) ∧ negP = (λ x. x) ∧ nega = (λ x. x ∨ dir = Negative ∧ neg = uminus ∧ negP = uminus ∧ nega = uminus" unfolding neg_def negP_def nega_def by auto define C where "C = map (λx. ?Geq x (the (?Bl s x))) ?negA @ map (λ x. ?Leq x (the (?Bu s x))) ?posA @ [?Geq xi (the (?Bl s xi))]" define f where "f = (λx. if x = xi then neg (-1) else neg (A x))" define c where "c = (∑x←C. lec_const (lec_of_nsc (f (atom_var x) *R nsc_of_atom x))) let ?q = "negP ?p" show ?case unfolding bounds_id t_id u_id proof (intro exI impI conjI allI) show "v ⊨t T s ==> ?q { v } = 0" for v :: "'a valuation" using dirn p_eval_zero[of v] by (auto simp: valuate_minus) show "set C ⊆ BA s" unfolding C_def set_append set_map set_filter list.simps using 0 l_Ba dir by (intro Un_least subsetI) (force simp: bound_atoms_def set_of_map_def)+ show is_leq: "∀a∈set C. is_leq_ns (f (atom_var a) *R nsc_of_atom a) ∧ f (atom_var using dirn xi_Xj 0 unfolding C_def f_def by (elim disjE, auto) show "(∑a ← C. lec_of_nsc (f (atom_var a) *R nsc_of_atom a)) = Leqc ?q c" unfolding sum_list_lec le_constraint.simps map_map o_def proof (intro conjI) define scale_poly :: "'a atom ==> linear_poly" where "scale_poly = (λx. lec_poly (lec_of_nsc (f (atom_var x) *R nsc_of_atom x)))" have "(∑x←C. scale_poly x) = (∑x←?negA. scale_poly (?Geq x (the (?Bl s x)))) + (∑x←?posA. scale_poly (?Leq x (the (?Bu s x)))) - negP (lp_monom 1 xi)" unfolding C_def using dirn by (auto simp add: comp_def scale_poly_def f_def) also have "(∑x←?negA. scale_poly (?Geq x (the (?Bl s x)))) = (∑x← ?negA. negP (A x *R lp_monom 1 x))" unfolding scale_poly_def f_def using dirn xi_Xj by (subst map_cong) auto also have "(∑x←?posA. scale_poly (?Leq x (the (?Bu s x)))) = (∑x← ?posA. negP (A x *R lp_monom 1 x))" unfolding scale_poly_def f_def using dirn xi_Xj by (subst map_cong) auto also have "(∑x← ?negA. negP (A x *R lp_monom 1 x)) + (∑x← ?posA. negP (A x *R lp_monom 1 x)) = negP (rhs (eq_for_lvar (T s) xi))" using dirn XLj_distinct coeff_zero by (elim disjE; intro poly_eqI, auto intro!: poly_eqI simp add: coeff_sum_list A_def Xj_def uminus_sum_list_map[unfolded o_def, symmetric]) finally show "(∑x←C. lec_poly (lec_of_nsc (f (atom_var x) *R nsc_of_atom x))) = ?q" unfolding scale_poly_def using dirn by auto show "(∑x←C. lec_rel (lec_of_nsc (f (atom_var x) *R nsc_of_atom x))) = Leq_Rel" unfolding sum_list_Leq_Rel proof fix c assume c: "c ∈ set C" show "lec_rel (lec_of_nsc (f (atom_var c) *R nsc_of_atom c)) = Leq_Rel" using is_leq[rule_format, OF c] by (cases "f (atom_var c) *R nsc_of_atom c", auto) qed qed (simp add: c_def) show "c < 0" proof - define scale_const_f :: "'a atom ==> 'a" where "scale_const_f x = lec_const (lec_of_nsc (f (atom_var x) *R nsc_of_atom x))" for x obtain d where bl': "?Bl s xi = Some d" using 3 by (cases "?Bl s xi", auto simp: bound_compare_defs) have "c = (∑x←map (λx. ?Geq x (the (?Bl s x))) ?negA. scale_const_f x) + (∑x← map (λx. ?Leq x (the (?Bu s x))) ?posA. scale_const_f x) - nega d" unfolding c_def C_def f_def scale_const_f_def using dirn rhs_eval_xi bl' by auto also have "(∑x←map (λx. ?Geq x (the (?Bl s x))) ?negA. scale_const_f x) = (∑x← ?negA. nega (A x *R the (?Bl s x)))" using xi_Xj dirn by (subst map_cong) (auto simp add: f_def scale_const_f_def) also have "… = (∑x←?negA. nega (A x *R ⟨V s⟩ x))" using 0 by (subst map_cong) auto also have "(∑x←map (λx. ?Leq x (the (?Bu s x))) ?posA. scale_const_f x) = (∑x← ?posA. nega (A x *R the (?Bu s x)))" using xi_Xj dirn by (subst map_cong) (auto simp add: f_def scale_const_f_def) also have "… = (∑x← ?posA. nega (A x *R ⟨V s⟩ x))" using 0 by (subst map_cong) auto also have "(∑x←?negA. nega (A x *R ⟨V s⟩ x)) + (∑x←?posA. nega (A x *R ⟨V s⟩ x)) = (∑x←?negA @ ?posA. nega (A x *R ⟨V s⟩ x))" by auto also have "… = (∑x∈ Xj. nega (A x *R ⟨V s⟩ x))" using XLj_distinct by (subst sum_list_distinct_conv_sum_set) (auto intro!: sum.cong) also have "… = nega (∑x∈ Xj. (A x *R ⟨V s⟩ x))" using dirn by (auto simp: sum_negf) also have "(∑x∈ Xj. (A x *R ⟨V s⟩ x)) = ((rhs ?eq) {⟨V s⟩})" unfolding A_def Xj_def by (subst linear_poly_sum) (auto simp add: sum_negf) also have "… = ⟨V s⟩ xi" using rhs_eval_xi by blast also have "nega (⟨V s⟩ xi) - nega d < 0" proof - have "?lt (⟨V s⟩ xi) d" using dirn 3(2-) bl' by (elim disjE, auto simp: bound_compare_defs) thus ?thesis using dirn unfolding minus_lt[symmetric] by auto qed finally show ?thesis . qed show "distinct C" unfolding C_def using XLj_distinct xi_Xj dirn by (auto simp add: inj_on_def distinct_map) qed qed (insert U, blast+) then obtain f p c C where Qs: "?Q s f p c C" using U unfolding check by blast from index[folded check_tableau_index_valid[OF U(2) inv(3,4,2,1)]] check have index: "index_valid as s" by auto from check_tableau_equiv[OF U(2) inv(3,4,2,1), unfolded check] have id: "v ⊨t T s = v ⊨t T s'" for v :: "'a valuation" by auto let ?C = "map (λ a. (f (atom_var a), a)) C" have "set C ⊆ BA s" using Qs by blast also have "… ⊆ snd ` as" using index unfolding bound_atoms_def index_valid_def set_of_map_def boundsl_def boundsu_def o_def finally have sub: "snd ` set ?C ⊆ snd ` as" by force show ?thesis unfolding farkas_coefficients_atoms_tableau_def by (intro exI[of _ p] exI[of _ c] exI[of _ ?C] conjI, insert Qs[unfolded id] sub, (force simp: o_def)+) qed end text ‹Next, we show that a conflict found by the assert-bound function also gives Farkas coefficients. context Update begin lemma farkas_assert_bound: assumes inv: "¬ U s" "⊨nolhs s" "△ (T s)" "∇ s" "♢ s" and index: "index_valid as s" and U: "U (assert_bound ia s)" shows "∃ C. farkas_coefficients_atoms_tableau (snd ` (insert ia as)) (T s) C" proof - obtain i a where ia[simp]: "ia = (i,a)" by force let ?A = "snd ` insert ia as" have "∃ x c d. Leq x c ∈ ?A ∧ Geq x d ∈ ?A ∧ c < d" proof (cases a) case (Geq x d) let ?s = "updateBI (Direction.UBI_upd (Direction (λx y. y < x) Biu Bil Bu Bl Iu Il Bi i x d s" have id: "U ?s = U s" by auto have norm: "△ (T ?s)" using inv by auto have val: "∇ ?s" using inv(4) unfolding tableau_valuated_def by simp have idd: "x ∉ lvars (T ?s) ==> U (update x d ?s) = U ?s" by (rule update_unsat_id[OF norm val]) from U[unfolded ia Geq] inv(1) id idd have "⊲lb (λx y. y < x) d (Bu s x)" by (auto split: if_splits simp: Let_def) then obtain c where Bu: "Bu s x = Some c" and lt: "c < d" by (cases "Bu s x", auto simp: bound_compare_defs) from Bu obtain j where "Mapping.lookup (Biu s) x = Some (j,c)" unfolding boundsu_def by auto with index[unfolded index_valid_def] have "(j, Leq x c) ∈ as" by auto hence xc: "Leq x c ∈ ?A" by force have xd: "Geq x d ∈ ?A" unfolding ia Geq by force from xc xd lt show ?thesis by auto next case (Leq x c) let ?s = "updateBI (Direction.UBI_upd (Direction (<) Bil Biu Bl Bu Il Iu Biu_update have id: "U ?s = U s" by auto have norm: "△ (T ?s)" using inv by auto have val: "∇ ?s" using inv(4) unfolding tableau_valuated_def by simp have idd: "x ∉ lvars (T ?s) ==> U (update x c ?s) = U ?s" by (rule update_unsat_id[OF norm val]) from U[unfolded ia Leq] inv(1) id idd have "⊲lb (<) c (Bl s x)" by (auto split: if_splits simp: Let_def) then obtain d where Bl: "Bl s x = Some d" and lt: "c < d" by (cases "Bl s x", auto simp: bound_compare_defs) from Bl obtain j where "Mapping.lookup (Bil s) x = Some (j,d)" unfolding boundsl_def by auto with index[unfolded index_valid_def] have "(j, Geq x d) ∈ as" by auto hence xd: "Geq x d ∈ ?A" by force have xc: "Leq x c ∈ ?A" unfolding ia Leq by force from xc xd lt show ?thesis by auto qed then obtain x c d where c: "Leq x c ∈ ?A" and d: "Geq x d ∈ ?A" and cd: "c < d" by blast show ?thesis unfolding farkas_coefficients_atoms_tableau_def proof (intro exI conjI allI) let ?C = "[(-1, Geq x d), (1,Leq x c)]" show "∀(r,a)∈set ?C. a ∈ ?A ∧ is_leq_ns (r *R nsc_of_atom a) ∧ r ≠ 0" using c d by aut show "c - d < 0" using cd using minus_lt by auto qed (auto simp: valuate_zero) qed end text ‹Moreover, we prove that all other steps of the simplex algorithm on layer~4 asserting bounds without conflict, etc., preserve Farkas coefficients. lemma farkas_coefficients_atoms_tableau_mono: assumes "as ⊆ bs" shows "farkas_coefficients_atoms_tableau as t C ==> farkas_coefficients_atoms_tab using assms unfolding farkas_coefficients_atoms_tableau_def by force locale AssertAllState''' = AssertAllState'' init ass_bnd chk + Update update + PivotUpdateMinVars eq_idx_for_lvar min_lvar_not_in_bounds min_rvar_incdec_eq pivot_a for init and ass_bnd :: "'i × 'a :: lrv atom ==> _" and chk :: "('i, 'a) state ==> ('i, ' and eq_idx_for_lvar :: "tableau ==> var ==> nat" and min_lvar_not_in_bounds :: "('i,'a::lrv) state ==> var option" and min_rvar_incdec_eq :: "('i,'a) Direction ==> ('i,'a) state ==> eq ==> 'i list + va pivot_and_update :: "var ==> var ==> 'a ==> ('i,'a) state ==> ('i,'a) state" + assumes ass_bnd: "ass_bnd = Update.assert_bound update" and chk: "chk = PivotUpdateMinVars.check eq_idx_for_lvar min_lvar_not_in_bounds min_r context AssertAllState''' begin lemma farkas_assert_bound_loop: assumes "U (assert_bound_loop as (init t))" and norm: "△ t" shows "∃ C. farkas_coefficients_atoms_tableau (snd ` set as) t C" proof - let ?P = "λ as s. U s ⟶ (∃ C. farkas_coefficients_atoms_tableau (snd ` as) (T s) C)" let ?s = "assert_bound_loop as (init t)" have "¬ U (init t)" by (rule init_unsat_flag) have "T (assert_bound_loop as (init t)) = t ∧ (U (assert_bound_loop as (init t)) ⟶ (∃ C. farkas_coefficients_atoms_tableau (sn proof (rule AssertAllState''Induct[OF norm], unfold ass_bnd, goal_cases) case 1 have "¬ U (init t)" by (rule init_unsat_flag) moreover have "T (init t) = t" by (rule init_tableau_id) ultimately show ?case by auto next case (2 as bs s) hence "snd ` as ⊆ snd ` bs" by auto from farkas_coefficients_atoms_tableau_mono[OF this] 2(2) show ?case by auto next case (3 s a ats) let ?s = "assert_bound a s" have tab: "T ?s = T s" unfolding ass_bnd by (rule assert_bound_nolhs_tableau_id, insert 3 have t: "t = T s" using 3 by simp show ?case unfolding t tab proof (intro conjI impI refl) assume "U ?s" from farkas_assert_bound[OF 3(1,3-6,8) this] show "∃ C. farkas_coefficients_atoms_tableau (snd ` insert a (set ats)) (T (init unfolding t[symmetric] init_tableau_id . qed qed thus ?thesis unfolding init_tableau_id using assms by blast qed text ‹Now we get to the main result for layer~4: If the main algorithm returns un then there are Farkas coefficients for the tableau and atom set that were given input for this layer. lemma farkas_assert_all_state: assumes U: "U (assert_all_state t as)" and norm: "△ t" shows "∃ C. farkas_coefficients_atoms_tableau (snd ` set as) t C" proof - let ?s = "assert_bound_loop as (init t)" show ?thesis proof (cases "U (assert_bound_loop as (init t))") case True from farkas_assert_bound_loop[OF this norm] show ?thesis by auto next case False from AssertAllState''_tableau_id[OF norm] have T: "T ?s = t" unfolding init_tableau_id . from U have U: "U (check ?s)" unfolding chk[symmetric] by simp show ?thesis proof (rule farkas_check[OF refl U False, unfolded T, OF _ norm]) from AssertAllState''_precond[OF norm, unfolded Let_def] False show "⊨nolhs ?s" "♢ ?s" "∇ ?s" by blast+ from AssertAllState''_index_valid[OF norm] show "index_valid (set as) ?s" . qed qed qed subsection ‹Farkas' Lemma on Layer 3› text ‹There is only a small difference between layers 3 and 4, namely that there simplex algorithm (@{const assert_all_state}) on layer 3, but just a tableau and text ‹Hence, one task is to link the unsatisfiability flag on layer 4 with unsatisfiability of the original tableau and atoms (layer 3). Th be done via the existing soundness results of the simplex algorithm. Moreover, we give an easy proof that the existence of Farkas coefficients for a set of atoms implies unsatisfiability. end lemma farkas_coefficients_atoms_tableau_unsat: assumes "farkas_coefficients_atoms_tableau as t C" shows "∄ v. v ⊨t t ∧ v ⊨as as" proof assume "∃ v. v ⊨t t ∧ v ⊨as as" then obtain v where *: "v ⊨t t ∧ v ⊨as as" by auto then obtain p c where isleq: "(∀(r,a) ∈ set C. a ∈ as ∧ is_leq_ns (r *R nsc_of_atom a) and leq: "(∑(r,a) ← C. lec_of_nsc (r *R nsc_of_atom a)) = Leqc p c" and cltz: "c < 0" and p0: "p{v} = 0" using assms farkas_coefficients_atoms_tableau_def by blast have fa: "∀(r,a) ∈ set C. v ⊨a a" using * isleq leq satisfies_atom_set_def by force { fix r a assume a: "(r,a) ∈ set C" from a fa have va: "v ⊨a a" unfolding satisfies_atom_set_def by auto hence v: "v ⊨ns (r *R nsc_of_atom a)" by (auto simp: nsc_of_atom sat_scale_rat_ns) from a isleq have "is_leq_ns (r *R nsc_of_atom a)" by auto from lec_of_nsc[OF this] v have "v ⊨le lec_of_nsc (r *R nsc_of_atom a)" by blast } note v = this have "v ⊨le Leqc p c" unfolding leq[symmetric] by (rule satisfies_sumlist_le_constraints, insert v, auto) then have "0 ≤ c" using p0 by auto then show False using cltz by auto qed text ‹Next is the main result for layer~3: a tableau and a finite set of atoms ar if and only if there is a list of Farkas coefficients for the set of atoms and t lemma farkas_coefficients_atoms_tableau: assumes norm: "△ t" and fin: "finite as" shows "(∃ C. farkas_coefficients_atoms_tableau as t C) ⟷ (∄ v. v ⊨t t ∧ v ⊨as as) proof from finite_list[OF fin] obtain bs where as: "as = set bs" by auto assume unsat: "∄ v. v ⊨t t ∧ v ⊨as as" let ?as = "map (λ x. ((),x)) bs" interpret AssertAllState''' init_state assert_bound_code check_code update_code eq_idx_for_lvar min_lvar_not_in_bounds min_rvar_incdec_eq pivot_and_update_code by (unfold_locales, auto simp: assert_bound_code_def check_code_def) let ?call = "assert_all t ?as" have id: "snd ` set ?as = as" unfolding as by force from assert_all_sat[OF norm, of ?as, unfolded id] unsat obtain I where "?call = Inl I" by (cases ?call, auto) from this[unfolded assert_all_def Let_def] have "U (assert_all_state_code t ?as)" by (auto split: if_splits simp: assert_all_state_code_def) from farkas_assert_all_state[OF this[unfolded assert_all_state_code_def] norm, unfold show "∃ C. farkas_coefficients_atoms_tableau as t C" . qed (insert farkas_coefficients_atoms_tableau_unsat, auto) subsection ‹Farkas' Lemma on Layer 2› text ‹The main difference between layers 2 and 3 is the introduction of slack-var via the preprocess-function. Our task here is to show that Farkas coefficients a slack-variables are used) can be converted into Farkas coefficients for layer 2 preprocessing). text ‹We also need to adapt the previos notion of Farkas coefficients, which was @{const farkas_coefficients_atoms_tableau}, for layer~2. At layer 3, Farkas coef are the coefficients in a linear combination of atoms that evaluates to an inequ the form $p \leq c$, where $p$ is a linear polynomial, $c < 0$, and $t \models p = At layer 2, the atoms are replaced by non-strict constraints where the left-hand polynomial in the original variables, but the corresponding linear combination ( coefficients) evaluates directly to the inequality $0 \leq c$, with $c < 0$. The i $t \models p = 0$ is no longer possible in this layer, since there is no tableau needed, since $p$ is $0$. Thus, the statement defining Farkas coefficients must accordingly. definition farkas_coefficients_ns where "farkas_coefficients_ns ns C = (∃ c. (∀(r, n) ∈ set C. n ∈ ns ∧ is_leq_ns (r *R n) ∧ r ≠ 0) ∧ (∑(r, n) ← C. lec_of_nsc (r *R n)) = Leqc 0 c ∧ c < 0)" text ‹The easy part is to prove that Farkas coefficients imply unsatisfiability.› lemma farkas_coefficients_ns_unsat: assumes "farkas_coefficients_ns ns C" shows "∄ v. v ⊨nss ns" proof assume "∃ v. v ⊨nss ns" then obtain v where *: "v ⊨nss ns" by auto obtain c where isleq: "(∀(a,n) ∈ set C. n ∈ ns ∧ is_leq_ns (a *R n) ∧ a ≠ 0)" and leq: "(∑(a,n) ← C. lec_of_nsc (a *R n)) = Leqc 0 c" and cltz: "c < 0" using assms farkas_coefficients_ns_def by blast { fix a n assume n: "(a,n) ∈ set C" from n * isleq have "v ⊨ns n" by auto hence v: "v ⊨ns (a *R n)" by (rule sat_scale_rat_ns) from n isleq have "is_leq_ns (a *R n)" by auto from lec_of_nsc[OF this] v have "v ⊨le lec_of_nsc (a *R n)" by blast } note v = this have "v ⊨le Leqc 0 c" unfolding leq[symmetric] by (rule satisfies_sumlist_le_constraints, insert v, auto) then show False using cltz by (metis leD satisfiable_le_constraint.simps valuate_zero rel_of.simps(1)) qed text ‹In order to eliminate the need for a tableau, we require the notion of an a on polynomials, where all variables can be replaced at once. The existing simple provides only a function to replace one variable at a time. definition subst_poly :: "(var ==> linear_poly) ==> linear_poly ==> linear_poly" whe "subst_poly σ p = (∑ x ∈ vars p. coeff p x *R σ x)" lemma subst_poly_0[simp]: "subst_poly σ 0 = 0" unfolding subst_poly_def by simp lemma valuate_subst_poly: "(subst_poly σ p) { v } = (p { (λ x. ((σ x) { v })) })" by (subst (2) linear_poly_sum, unfold subst_poly_def valuate_sum valuate_scaleRat, simp) lemma subst_poly_add: "subst_poly σ (p + q) = subst_poly σ p + subst_poly σ q" by (rule linear_poly_eqI, unfold valuate_add valuate_subst_poly, simp) fun subst_poly_lec :: "(var ==> linear_poly) ==> 'a le_constraint ==> 'a le_constra "subst_poly_lec σ (Le_Constraint rel p c) = Le_Constraint rel (subst_poly σ p) c" lemma subst_poly_lec_0[simp]: "subst_poly_lec σ 0 = 0" unfolding zero_le_constraint_d lemma subst_poly_lec_add: "subst_poly_lec σ (c1 + c2) = subst_poly_lec σ c1 + subst_ by (cases c1; cases c2, auto simp: subst_poly_add) lemma subst_poly_lec_sum_list: "subst_poly_lec σ (sum_list ps) = sum_list (map (sub by (induct ps, auto simp: subst_poly_lec_add) lemma subst_poly_lp_monom[simp]: "subst_poly σ (lp_monom r x) = r *R σ x" unfolding subst_poly_def by (simp add: vars_lp_monom) lemma subst_poly_scaleRat: "subst_poly σ (r *R p) = r *R (subst_poly σ p)" by (rule linear_poly_eqI, unfold valuate_scaleRat valuate_subst_poly, simp) text ‹We need several auxiliary properties of the preprocess-function which are n in the simplex formalization. lemma Tableau_is_monom_preprocess': assumes "(x, p) ∈ set (Tableau (preprocess' cs start))" shows "¬ is_monom p" using assms by(induction cs start rule: preprocess'.induct) (auto simp add: Let_def split: if_splits option.splits) lemma preprocess'_atoms_to_constraints': assumes "preprocess' cs start = S" shows "set (Atoms S) ⊆ {(i,qdelta_constraint_to_atom c v) | i c v. (i,c) ∈ set cs (¬ is_monom (poly c) ⟶ Poly_Mapping S (poly c) = Some v)}" unfolding assms(1)[symmetric] by (induct cs start rule: preprocess'.induct, auto simp: Let_def split: option.splits, forc lemma monom_of_atom_coeff: assumes "is_monom (poly ns)" "a = qdelta_constraint_to_atom ns v" shows "(monom_coeff (poly ns)) *R nsc_of_atom a = ns" using assms is_monom_monom_coeff_not_zero by(cases a; cases ns) (auto split: atom.split ns_constraint.split simp add: monom_poly_assemble field_simps) text ‹The next lemma provides the functionality that is required to convert an atom back to a non-strict constraint, i.e., it is a kind of inverse of the prepr lemma preprocess'_atoms_to_constraints: assumes S: "preprocess' cs start = S" and start: "start = start_fresh_variable cs" and ns: "ns = (case a of Leq v c ==> LEQ_ns q c | Geq v c ==> GEQ_ns q c)" and "a ∈ snd ` set (Atoms S)" shows "(atom_var a ∉ fst ` set (Tableau S) ⟶ (∃ r. r ≠ 0 ∧ r *R nsc_of_atom a ∈ s ∧ ((atom_var a, q) ∈ set (Tableau S) ⟶ ns ∈ snd ` set cs)" proof - let ?S = "preprocess' cs start" from assms(4) obtain i where ia: "(i,a) ∈ set (Atoms S)" by auto with preprocess'_atoms_to_constraints'[OF assms(1)] obtain c v where a: "a = qdelta_constraint_to_atom c v" and c: "(i,c) ∈ set cs" and nmonom: "¬ is_monom (poly c) ==> Poly_Mapping S (poly c) = Some v" by blast hence c': "c ∈ snd ` set cs" by force let ?p = "poly c" show ?thesis proof (cases "is_monom ?p") case True hence av: "atom_var a = monom_var ?p" unfolding a by (cases c, auto) from Tableau_is_monom_preprocess'[of _ ?p cs start] True have "(x, ?p) ∉ set (Tableau ?S)" for x by blast { assume "(atom_var a, q) ∈ set (Tableau S)" hence "(monom_var ?p, q) ∈ set (Tableau S)" unfolding av by simp hence "monom_var ?p ∈ lvars (Tableau S)" unfolding lvars_def by force from lvars_tableau_ge_start[rule_format, OF this[folded S]] have "monom_var ?p ≥ start" unfolding S . moreover have "monom_var ?p ∈ vars_constraints (map snd cs)" using True c by (auto intro!: bexI[of _ "(i,c)"] simp: monom_var_in_vars) ultimately have False using start_fresh_variable_fresh[of cs, folded start] by force } moreover from monom_of_atom_coeff[OF True a] True have "∃r. r ≠ 0 ∧ r *R nsc_of_atom a = c" by (intro exI[of _ "monom_coeff ?p"], auto, cases a, auto) ultimately show ?thesis using c' by auto next case False hence av: "atom_var a = v" unfolding a by (cases c, auto) from nmonom[OF False] have "Poly_Mapping S ?p = Some v" . from preprocess'_Tableau_Poly_Mapping_Some[OF this[folded S]] have tab: "(atom_var a, ?p) ∈ set (Tableau (preprocess' cs start))" unfolding av by si hence "atom_var a ∈ fst ` set (Tableau S)" unfolding S by force moreover { assume "(atom_var a, q) ∈ set (Tableau S)" from tab this have qp: "q = ?p" unfolding S using lvars_distinct[of cs start, unfolded S lhs_d by (simp add: case_prod_beta' eq_key_imp_eq_value) have "ns = c" unfolding ns qp using av a False by (cases c, auto) hence "ns ∈ snd ` set cs" using c' by blast } ultimately show ?thesis by blast qed qed text ‹Next follows the major technical lemma of this part, namely that Farkas coefficients on layer~3 for preprocessed constraints can be converted into Farkas coefficients on layer~2.› lemma farkas_coefficients_preprocess': assumes pp: "preprocess' cs (start_fresh_variable cs) = S" and ft: "farkas_coefficients_atoms_tableau (snd ` set (Atoms S)) (Tableau S) C" shows "∃ C. farkas_coefficients_ns (snd ` set cs) C" proof - note ft[unfolded farkas_coefficients_atoms_tableau_def] obtain p c where 0: "∀ (r,a) ∈ set C. a ∈ snd ` set (Atoms S) ∧ is_leq_ns (r *R nsc_o "(∑(r,a)←C. lec_of_nsc (r *R nsc_of_atom a)) = Leqc p c" "c < 0" "∧v :: QDelta valuation. v ⊨t Tableau S ==> p { v } = 0" using ft unfolding farkas_coefficients_atoms_tableau_def by blast note 0 = 0(1)[rule_format, of "(a, b)" for a b, unfolded split] 0(2-) let ?T = "Tableau S" define σ :: "var ==> linear_poly" where "σ = (λ x. case map_of ?T x of Some p ==> p | No let ?P = "(λr a s ns. ns ∈ (snd ` set cs) ∧ is_leq_ns (s *R ns) ∧ s ≠ 0 ∧ subst_poly_lec σ (lec_of_nsc (r *R nsc_of_atom a)) = lec_of_nsc (s *R ns))" have "∃s ns. ?P r a s ns" if ra: "(r,a) ∈ set C" for r a proof - have a: "a ∈ snd ` set (Atoms S)" using ra 0 by force from 0 ra have is_leq: "is_leq_ns (r *R nsc_of_atom a)" and r0: "r ≠ 0" by auto let ?x = "atom_var a" show ?thesis proof (cases "map_of ?T ?x") case (Some q) hence σ: "σ ?x = q" unfolding σ_def by auto from Some have xqT: "(?x, q) ∈ set ?T" by (rule map_of_SomeD) define ns where "ns = (case a of Leq v c ==> LEQ_ns q c | Geq v c ==> GEQ_ns q c)" from preprocess'_atoms_to_constraints[OF pp refl ns_def a] xqT have ns_mem: "ns ∈ snd ` set cs" by blast have id: "subst_poly_lec σ (lec_of_nsc (r *R nsc_of_atom a)) = lec_of_nsc (r *R ns)" using is_leq σ by (cases a, auto simp: ns_def subst_poly_scaleRat) from id is_leq σ have is_leq: "is_leq_ns (r *R ns)" by (cases a, auto simp: ns_def) show ?thesis by (intro exI[of _ r] exI[of _ ns] conjI ns_mem id is_leq conjI r0) next case None hence "?x ∉ fst ` set ?T" by (meson map_of_eq_None_iff) from preprocess'_atoms_to_constraints[OF pp refl refl a] this obtain rr where rr: "rr *R nsc_of_atom a ∈ (snd ` set cs)" and rr0: "rr ≠ 0" by blast from None have σ: "σ ?x = lp_monom 1 ?x" unfolding σ_def by simp define ns where "ns = rr *R nsc_of_atom a" define s where "s = r / rr" from rr0 r0 have s0: "s ≠ 0" unfolding s_def by auto from is_leq σ have "subst_poly_lec σ (lec_of_nsc (r *R nsc_of_atom a)) = lec_of_nsc (r *R nsc_of_atom a)" by (cases a, auto simp: subst_poly_scaleRat) moreover have "r *R nsc_of_atom a = s *R ns" unfolding ns_def s_def scaleRat_scaleRat_ns_constraint[OF rr0] using rr0 by simp ultimately have "subst_poly_lec σ (lec_of_nsc (r *R nsc_of_atom a)) = lec_of_nsc (s *R ns)" "is_leq_ns (s *R ns)" using is_leq by auto then show ?thesis unfolding ns_def using rr s0 by blast qed qed hence "∀ ra. ∃ s ns. (fst ra, snd ra) ∈ set C ⟶ ?P (fst ra) (snd ra) s ns" by blast from choice[OF this] obtain s where s: "∀ ra. ∃ ns. (fst ra, snd ra) ∈ set C ⟶ ?P (fst from choice[OF this] obtain ns where ns: "∧ r a. (r,a) ∈ set C ==> ?P r a (s (r,a)) (ns define NC where "NC = map (λ(r,a). (s (r,a), ns (r,a))) C" have "(∑(s, ns)←map (λ(r,a). (s (r,a), ns (r,a))) C'. lec_of_nsc (s *R ns)) = (∑(r, a)←C'. subst_poly_lec σ (lec_of_nsc (r *R nsc_of_atom a)))" if "set C' ⊆ set C" for C' using that proof (induction C') case Nil then show ?case by simp next case (Cons a C') have "(∑x←a # C'. lec_of_nsc (s x *R ns x)) = lec_of_nsc (s a *R ns a) + (∑x←C'. lec_of_nsc (s x *R ns x))" by simp also have "(∑x←C'. lec_of_nsc (s x *R ns x)) = (∑(r, a)←C'. subst_poly_lec σ (lec_of_ using Cons by (auto simp add: case_prod_beta' comp_def) also have "lec_of_nsc (s a *R ns a) = subst_poly_lec σ (lec_of_nsc (fst a *R nsc_of proof - have "a ∈ set C" using Cons by simp then show ?thesis using ns by auto qed finally show ?case by (auto simp add: case_prod_beta' comp_def) qed also have "(∑(r, a)←C. subst_poly_lec σ (lec_of_nsc (r *R nsc_of_atom a))) = subst_poly_lec σ (∑(r, a)←C. (lec_of_nsc (r *R nsc_of_atom a)))" by (auto simp add: subst_poly_lec_sum_list case_prod_beta' comp_def) also have "(∑(r, a)←C. (lec_of_nsc (r *R nsc_of_atom a))) = Leqc p c" using 0 by blast also have "subst_poly_lec σ (Leqc p c) = Leqc (subst_poly σ p) c" by simp also have "subst_poly σ p = 0" proof (rule all_valuate_zero) fix v :: "QDelta valuation" have "(subst_poly σ p) { v } = (p { λx. ((σ x) { v }) })" by (rule valuate_subst_poly) also have "… = 0" proof (rule 0(4)) have "(σ a) { v } = (q { λx. ((σ x) { v }) })" if "(a, q) ∈ set (Tableau S)" for a q proof - have "distinct (map fst ?T)" using normalized_tableau_preprocess' assms unfolding normalized_tableau_def lhs_def by (auto simp add: case_prod_beta') then have 0: "σ a = q" unfolding σ_def using that by auto have "q { v } = (q { λx. ((σ x) { v }) })" proof - have "vars q ⊆ rvars ?T" unfolding rvars_def using that by force moreover have "(σ x) { v } = v x" if "x ∈ rvars ?T" for x proof - have "x ∉ lvars (Tableau S)" using that normalized_tableau_preprocess' assms unfolding normalized_tableau_def by blast then have "x ∉ fst ` set (Tableau S)" unfolding lvars_def by force then have "map_of ?T x = None" using map_of_eq_None_iff by metis then have "σ x = lp_monom 1 x" unfolding σ_def by auto also have "(lp_monom 1 x) { v } = v x" by auto finally show ?thesis . qed ultimately show ?thesis by (auto intro!: valuate_depend) qed then show ?thesis using 0 by blast qed then show "(λx. ((σ x) { v })) ⊨t ?T" using 0 by (auto simp add: satisfies_tableau_def satisfies_eq_def) qed finally show "(subst_poly σ p) { v } = 0" . qed finally have "(∑(s, n)←NC. lec_of_nsc (s *R n)) = Le_Constraint Leq_Rel 0 c" unfolding NC_def by blast moreover have "ns (r,a) ∈ snd ` set cs" "is_leq_ns (s (r, a) *R ns (r, a))" "s (r, a using ns that by force+ ultimately have "farkas_coefficients_ns (snd ` set cs) NC" unfolding farkas_coefficients_ns_def NC_def using 0 by force then show ?thesis by blast qed lemma preprocess'_unsat_indexD: "i ∈ set (UnsatIndices (preprocess' ns j)) ==> ∃ c. poly c = 0 ∧ ¬ zero_satisfies c ∧ (i,c) ∈ set ns" by (induct ns j rule: preprocess'.induct, auto simp: Let_def split: if_splits option.splits lemma preprocess'_unsat_index_farkas_coefficients_ns: assumes "i ∈ set (UnsatIndices (preprocess' ns j))" shows "∃ C. farkas_coefficients_ns (snd ` set ns) C" proof - from preprocess'_unsat_indexD[OF assms] obtain c where contr: "poly c = 0" "¬ zero_satisfies c" and mem: "(i,c) ∈ set ns" by auto from mem have mem: "c ∈ snd ` set ns" by force let ?c = "ns_constraint_const c" define r where "r = (case c of LEQ_ns _ _ ==> 1 | _ ==> (-1 :: rat))" define d where "d = (case c of LEQ_ns _ _ ==> ?c | _ ==> - ?c)" have [simp]: "(- x < 0) = (0 < x)" for x :: QDelta using uminus_less_lrv[of _ 0] by simp show ?thesis unfolding farkas_coefficients_ns_def by (intro exI[of _ "[(r,c)]"] exI[of _ d], insert mem contr, cases "c", auto simp: r_def d_def) qed text ‹The combination of the previous results easily provides the main result of a finite set of non-strict constraints on layer~2 is unsatisfiable if and only i Again, here we use results from the simplex formalization, namely soundness of t lemma farkas_coefficients_ns: assumes "finite (ns :: QDelta ns_constraint set)" shows "(∃ C. farkas_coefficients_ns ns C) ⟷ (∄ v. v ⊨nss ns)" proof assume "∃ C. farkas_coefficients_ns ns C" from farkas_coefficients_ns_unsat this show "∄ v. v ⊨nss ns" by blast next assume unsat: "∄ v. v ⊨nss ns" from finite_list[OF assms] obtain nsl where ns: "ns = set nsl" by auto let ?cs = "map (Pair ()) nsl" obtain I t ias where part1: "preprocess_part_1 ?cs = (t,ias,I)" by (cases "preprocess_par let ?as = "snd ` set ias" let ?s = "start_fresh_variable ?cs" have fin: "finite ?as" by auto have id: "ias = Atoms (preprocess' ?cs ?s)" "t = Tableau (preprocess' ?cs ?s)" "I = UnsatIndices (preprocess' ?cs ?s)" using part1 unfolding preprocess_part_1_def Let_def by auto have norm: "△ t" using normalized_tableau_preprocess'[of ?cs] unfolding id . { fix v assume "v ⊨as ?as" "v ⊨t t" from preprocess'_sat[OF this[unfolded id], folded id] unsat[unfolded ns] have "set I ≠ {}" by auto then obtain i where "i ∈ set I" using all_not_in_conv by blast from preprocess'_unsat_index_farkas_coefficients_ns[OF this[unfolded id]] have "∃C. farkas_coefficients_ns (snd ` set ?cs) C" by simp } with farkas_coefficients_atoms_tableau[OF norm fin] obtain C where "farkas_coefficients_atoms_tableau ?as t C ∨ (∃C. farkas_coefficients_ns (snd ` set ?cs) C)" by blast from farkas_coefficients_preprocess'[of ?cs, OF refl] this have "∃ C. farkas_coefficients_ns (snd ` set ?cs) C" using part1 unfolding preprocess_part_1_def Let_def by auto also have "snd ` set ?cs = ns" unfolding ns by force finally show "∃ C. farkas_coefficients_ns ns C" . qed subsection ‹Farkas' Lemma on Layer 1› text ‹The main difference of layers 1 and 2 is the restriction to non-strict cons Since we now work with another constraint type, @{type constraint}, we again nee linear inequalities of type @{type le_constraint}. Moreover, we also need to def where flipping the comparison sign may be required. fun is_le :: "constraint ==> bool" where "is_le (LT _ _) = True" | "is_le (LEQ _ _) = True" | "is_le _ = False" fun lec_of_constraint where "lec_of_constraint (LEQ p c) = (Le_Constraint Leq_Rel p c)" | "lec_of_constraint (LT p c) = (Le_Constraint Lt_Rel p c)" lemma lec_of_constraint: assumes "is_le c" shows "(v ⊨le (lec_of_constraint c)) ⟷ (v ⊨c c)" using assms by (cases c, auto) instantiation constraint :: scaleRat begin fun scaleRat_constraint :: "rat ==> constraint ==> constraint" where "scaleRat_constraint r cc = (if r = 0 then LEQ 0 0 else (case cc of LEQ p c ==> (if (r < 0) then GEQ (r *R p) (r *R c) else LEQ (r *R p) (r *R c)) | LT p c ==> (if (r < 0) then GT (r *R p) (r *R c) else LT (r *R p) (r *R c)) | GEQ p c ==> (if (r > 0) then GEQ (r *R p) (r *R c) else LEQ (r *R p) (r *R c)) | GT p c ==> (if (r > 0) then GT (r *R p) (r *R c) else LT (r *R p) (r *R c)) | EQ p c ==> LEQ (r *R p) (r *R c) ― ‹We do not keep equality, since the aim is to convert the scaled constraints into inequalities, which will then be summed u ))" instance .. end lemma sat_scale_rat: assumes "(v :: rat valuation) ⊨c c" shows "v ⊨c (r *R c)" proof - have "r < 0 ∨ r = 0 ∨ r > 0" by auto then show ?thesis using assms by (cases c, auto simp: right_diff_distrib valuate_minus valuate_scaleRat scaleRat_leq1 scaleRat_leq2 valuate_zero) qed text ‹In the following definition of Farkas coefficients (for layer 1), the main @{const farkas_coefficients_ns} is that the linear combination evaluates either a strict inequality where the constant must be non-positive, or to a non-strict the constant must be negative. definition farkas_coefficients where "farkas_coefficients cs C = (∃ d rel. (∀ (r,c) ∈ set C. c ∈ cs ∧ is_le (r *R c) ∧ r ≠ 0) ∧ (∑ (r,c) ← C. lec_of_constraint (r *R c)) = Le_Constraint rel 0 d ∧ (rel = Leq_Rel ∧ d < 0 ∨ rel = Lt_Rel ∧ d ≤ 0))" text ‹Again, the existence Farkas coefficients immediately implies unsatisfiabili lemma farkas_coefficients_unsat: assumes "farkas_coefficients cs C" shows "∄ v. v ⊨cs cs" proof assume "∃ v. v ⊨cs cs" then obtain v where *: "v ⊨cs cs" by auto obtain d rel where isleq: "(∀(r,c) ∈ set C. c ∈ cs ∧ is_le (r *R c) ∧ r ≠ 0)" and leq: "(∑ (r,c) ← C. lec_of_constraint (r *R c)) = Le_Constraint rel 0 d" and choice: "rel = Lt_Rel ∧ d ≤ 0 ∨ rel = Leq_Rel ∧ d < 0" using assms farkas_coefficient { fix r c assume c: "(r,c) ∈ set C" from c * isleq have "v ⊨c c" by auto hence v: "v ⊨c (r *R c)" by (rule sat_scale_rat) from c isleq have "is_le (r *R c)" by auto from lec_of_constraint[OF this] v have "v ⊨le lec_of_constraint (r *R c)" by blast } note v = this have "v ⊨le Le_Constraint rel 0 d" unfolding leq[symmetric] by (rule satisfies_sumlist_le_constraints, insert v, auto) then show False using choice by (cases rel, auto simp: valuate_zero) qed text ‹Now follows the difficult implication. The major part is proving that the translation @{const constraint_to_qdelta_cons preserves the existence of Farkas coefficients via pointwise compatibility of th Here, compatibility links a strict or non-strict inequality from the input const a translated non-strict inequality over delta-rationals. fun compatible_cs where "compatible_cs (Le_Constraint Leq_Rel p c) (Le_Constraint Leq_Rel q d) = (q = p | "compatible_cs (Le_Constraint Lt_Rel p c) (Le_Constraint Leq_Rel q d) = (q = p | "compatible_cs _ _ = False" lemma compatible_cs_0_0: "compatible_cs 0 0" by code_simp lemma compatible_cs_plus: "compatible_cs c1 d1 ==> compatible_cs c2 d2 ==> compati by (cases c1; cases d1; cases c2; cases d2; cases "lec_rel c1"; cases "lec_rel d1"; cases "lec cases "lec_rel d2"; auto simp: plus_QDelta_def) lemma unsat_farkas_coefficients: assumes "∄ v. v ⊨cs cs" and fin: "finite cs" shows "∃ C. farkas_coefficients cs C" proof - from finite_list[OF fin] obtain csl where cs: "cs = set csl" by blast let ?csl = "map (Pair ()) csl" let ?ns = "(snd ` set (to_ns ?csl))" let ?nsl = "concat (map constraint_to_qdelta_constraint csl)" have id: "snd ` set ?csl = cs" unfolding cs by force have id2: "?ns = set ?nsl" unfolding to_ns_def set_concat by force from SolveExec'Default.to_ns_sat[of ?csl, unfolded id] assms have unsat: "∄ v. ⟨v⟩ ⊨nss ?ns" by metis have fin: "finite ?ns" by auto have "∄ v. v ⊨nss ?ns" proof assume "∃ v. v ⊨nss ?ns" then obtain v where model: "v ⊨nss ?ns" by blast let ?v = "Mapping.Mapping (λ x. Some (v x))" have "v = ⟨?v⟩" by (intro ext, auto simp: map2fun_def Mapping.lookup.abs_eq) from model this unsat show False by metis qed from farkas_coefficients_ns[OF fin] this id2 obtain N where farkas: "farkas_coefficients_ns (set ?nsl) N" by metis from this[unfolded farkas_coefficients_ns_def] obtain d where is_leq: "∧ a n. (a,n) ∈ set N ==> n ∈ set ?nsl ∧ is_leq_ns (a *R n) ∧ a ≠ 0" and sum: "(∑(a,n)←N. lec_of_nsc (a *R n)) = Le_Constraint Leq_Rel 0 d" and d0: "d < 0" by blast let ?prop = "λ NN C. (∀ (a,c) ∈ set C. c ∈ cs ∧ is_le (a *R c) ∧ a ≠ 0) ∧ compatible_cs (∑ (a,c) ← C. lec_of_constraint (a *R c)) (∑(a,n)←NN. lec_of_nsc (a *R n))" have "set NN ⊆ set N ==> ∃ C. ?prop NN C" for NN proof (induct NN) case Nil have "?prop Nil Nil" by (simp add: compatible_cs_0_0) thus ?case by blast next case (Cons an NN) obtain a n where an: "an = (a,n)" by force from Cons an obtain C where IH: "?prop NN C" and n: "(a,n) ∈ set N" by auto have compat_CN: "compatible_cs (∑(f, c)←C. lec_of_constraint (f *R c)) (∑(a,n)←NN. lec_of_nsc (a *R n))" using IH by blast from n is_leq obtain c where c: "c ∈ cs" and nc: "n ∈ set (constraint_to_qdelta_constraint unfolding cs by force from is_leq[OF n] have is_leq: "is_leq_ns (a *R n) ∧ a ≠ 0" by blast have is_less: "is_le (a *R c)" and a0: "a ≠ 0" and compat_cn: "compatible_cs (lec_of_constraint (a *R c)) (lec_of_nsc (a *R n))" by (atomize(full), cases c, insert is_leq nc, auto simp: QDelta_0_0 scaleRat_QDelta_def qds let ?C = "Cons (a, c) C" let ?N = "Cons (a, n) NN" have "?prop ?N ?C" unfolding an proof (intro conjI) show "∀ (a,c) ∈ set ?C. c ∈ cs ∧ is_le (a *R c) ∧ a ≠ 0" using IH is_less a0 c by auto show "compatible_cs (∑(a, c)←?C. lec_of_constraint (a *R c)) (∑(a,n)←?N. lec_of_nsc using compatible_cs_plus[OF compat_cn compat_CN] by simp qed thus ?case unfolding an by blast qed from this[OF subset_refl, unfolded sum] obtain C where is_less: "(∀(a, c)∈set C. c ∈ cs ∧ is_le (a *R c) ∧ a ≠ 0)" and compat: "compatible_cs (∑(f, c)←C. lec_of_constraint (f *R c)) (Le_Constraint Leq_ (is "compatible_cs ?sum _") by blast obtain rel p e where "?sum = Le_Constraint rel p e" by (cases ?sum) with compat have sum: "?sum = Le_Constraint rel 0 e" by (cases rel, auto) have e: "(rel = Leq_Rel ∧ e < 0 ∨ rel = Lt_Rel ∧ e ≤ 0)" using compat[unfolded sum] d0 by (cases rel, auto simp: less_QDelta_def qdfst_0 qdsnd_0) show ?thesis unfolding farkas_coefficients_def by (intro exI conjI, rule is_less, rule sum, insert e, auto) qed text ‹Finally we can prove on layer 1 that a finite set of constraints is unsatisfiable if and only if there are Farkas coefficients.› lemma farkas_coefficients: assumes "finite cs" shows "(∃ C. farkas_coefficients cs C) ⟷ (∄ v. v ⊨cs cs)" using farkas_coefficients_unsat unsat_farkas_coefficients[OF _ assms] by blast section ‹Corollaries from the Literature› text ‹In this section, we convert the previous variations of Farkas' Lemma into m well-known forms of this result. Moreover, instead of referring to the various constraint types of the simplex fo now speak solely about constraints of type @{type le_constraint}. subsection ‹Farkas' Lemma on Delta-Rationals› text ‹We start with Lemma~2 of cite‹"Bromberger2017"›, a variant of Farkas' Lemma for delta-rationals. To be more precise, it states that a set of non-strict inequalities over delta-rationals is unsatisfiable if and only if there is a linear combination of the inequalities that results in a trivial unsatisfiable constraint $0 < const$ for some negative constant $cons We can easily prove this statement via the lemma @{thm [source] farkas_coefficie and some conversions between the different constraint types. lemma Farkas'_Lemma_Delta_Rationals: fixes cs :: "QDelta le_constraint set" assumes only_non_strict: "lec_rel ` cs ⊆ {Leq_Rel}" and fin: "finite cs" shows "(∄ v. ∀ c ∈ cs. v ⊨le c) ⟷ (∃ C const. (∀ (r, c) ∈ set C. r > 0 ∧ c ∈ cs) ∧ (∑ (r,c) ← C. Leqc (r *R lec_poly c) (r *R lec_const c)) = Leqc 0 const ∧ const < 0)" (is "?lhs = ?rhs") proof - { fix c assume "c ∈ cs" with only_non_strict have "lec_rel c = Leq_Rel" by auto then have "∃ p const. c = Leqc p const" by (cases c, auto) } note leqc = this let ?to_ns = "λ c. LEQ_ns (lec_poly c) (lec_const c)" let ?ns = "?to_ns ` cs" from fin have fin: "finite ?ns" by auto have "v ⊨nss ?ns ⟷ (∀ c ∈ cs. v ⊨le c)" for v using leqc by fastforce hence "?lhs = (∄ v. v ⊨nss ?ns)" by simp also have "… = (∃C. farkas_coefficients_ns ?ns C)" unfolding farkas_coefficients_ns[ also have "… = ?rhs" proof assume "∃ C. farkas_coefficients_ns ?ns C" then obtain C const where is_leq: "∀ (s, n) ∈ set C. n ∈ ?ns ∧ is_leq_ns (s *R n) ∧ s and sum: "(∑(s, n)←C. lec_of_nsc (s *R n)) = Leqc 0 const" and c0: "const < 0" unfolding farkas_coefficients_ns_def by blast let ?C = "map (λ (s,n). (s,lec_of_nsc n)) C" show ?rhs proof (intro exI[of _ ?C] exI[of _ const] conjI c0, unfold sum[symmetric] map_map o_def set_ma intro ballI, clarify) { fix s n assume sn: "(s, n) ∈ set C" with is_leq have n_ns: "n ∈ ?ns" and is_leq: "is_leq_ns (s *R n)" "s ≠ 0" by force+ from n_ns obtain c where c: "c ∈ cs" and n: "n = LEQ_ns (lec_poly c) (lec_const c)" by auto with leqc[OF c] obtain p d where cs: "Leqc p d ∈ cs" and n: "n = LEQ_ns p d" by auto from is_leq[unfolded n] have s0: "s > 0" by (auto split: if_splits) let ?n = "lec_of_nsc n" from cs n have mem: "?n ∈ cs" by auto show "0 < s ∧ ?n ∈ cs" using s0 mem by blast have "Leqc (s *R lec_poly ?n) (s *R lec_const ?n) = lec_of_nsc (s *R n)" unfolding n using s0 by simp } note id = this show "(∑x←C. case case x of (s, n) ==> (s, lec_of_nsc n) of (r, c) ==> Leqc (r *R lec_poly c) (r *R lec_const c)) = (∑(s, n)←C. lec_of_nsc (s *R n))" (is "sum_list (map ?f C) = sum_list (map ?g C)") proof (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl]) fix pair assume mem: "pair ∈ set C" then obtain s n where pair: "pair = (s,n)" by force show "?f pair = ?g pair" unfolding pair split using id[OF mem[unfolded pair]] . qed qed next assume ?rhs then obtain C const where C: "∧ r c. (r,c) ∈ set C ==> 0 < r ∧ c ∈ cs" and sum: "(∑(r, c)←C. Leqc (r *R lec_poly c) (r *R lec_const c)) = Leqc 0 const" and const: "const < 0" by blast let ?C = "map (λ (r,c). (r, ?to_ns c)) C" show "∃ C. farkas_coefficients_ns ?ns C" unfolding farkas_coefficients_ns_def proof (intro exI[of _ ?C] exI[of _ const] conjI const, unfold sum[symmetric]) show "∀(s, n)∈set ?C. n ∈ ?ns ∧ is_leq_ns (s *R n) ∧ s ≠ 0" using C by fastforce show "(∑(s, n)←?C. lec_of_nsc (s *R n)) = (∑(r, c)←C. Leqc (r *R lec_poly c) (r *R lec_const c))" unfolding map_map o_def by (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl], insert C, force) qed qed finally show ?thesis . qed subsection ‹Motzkin's Transposition Theorem or the Kuhn-Fourier Theorem› text ‹Next, we prove a generalization of Farkas' Lemma that permits arbitrary com of strict and non-strict inequalities: Motzkin's Transposition Theorem which is also known as the Kuhn--Fourier Theorem. The proof is mainly based on the lemma @{thm [source] farkas_coefficients}, again requiring conversions between constraint types. theorem Motzkin's_transposition_theorem: fixes cs :: "rat le_constraint set" assumes fin: "finite cs" shows "(∄ v. ∀ c ∈ cs. v ⊨le c) ⟷ (∃ C const rel. (∀ (r, c) ∈ set C. r > 0 ∧ c ∈ cs) ∧ (∑ (r,c) ← C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)) = Le_Constraint rel 0 const ∧ (rel = Leq_Rel ∧ const < 0 ∨ rel = Lt_Rel ∧ const ≤ 0))" (is "?lhs = ?rhs") proof - let ?to_cs = "λ c. (case lec_rel c of Leq_Rel ==> LEQ | _ ==> LT) (lec_poly c) (lec_ have to_cs: "v ⊨c ?to_cs c ⟷ v ⊨le c" for v c by (cases c, cases "lec_rel c", auto) let ?cs = "?to_cs ` cs" from fin have fin: "finite ?cs" by auto have "v ⊨cs ?cs ⟷ (∀ c ∈ cs. v ⊨le c)" for v using to_cs by auto hence "?lhs = (∄ v. v ⊨cs ?cs)" by simp also have "… = (∃C. farkas_coefficients ?cs C)" unfolding farkas_coefficients[OF fin] also have "… = ?rhs" proof assume "∃ C. farkas_coefficients ?cs C" then obtain C const rel where is_leq: "∀ (s, n) ∈ set C. n ∈ ?cs ∧ is_le (s *R n) ∧ s ≠ and sum: "(∑(s, n)←C. lec_of_constraint (s *R n)) = Le_Constraint rel 0 const" and c0: "(rel = Leq_Rel ∧ const < 0 ∨ rel = Lt_Rel ∧ const ≤ 0)" unfolding farkas_coefficients_def by blast let ?C = "map (λ (s,n). (s,lec_of_constraint n)) C" show ?rhs proof (intro exI[of _ ?C] exI[of _ const] exI[of _ rel] conjI c0, unfold map_map o_def set_map su intro ballI, clarify) { fix s n assume sn: "(s, n) ∈ set C" with is_leq have n_ns: "n ∈ ?cs" and is_leq: "is_le (s *R n)" and s0: "s ≠ 0" by force+ from n_ns obtain c where c: "c ∈ cs" and n: "n = ?to_cs c" by auto from is_leq[unfolded n] have "s ≥ 0" by (cases "lec_rel c", auto split: if_splits) with s0 have s0: "s > 0" by auto let ?c = "lec_of_constraint n" from c n have mem: "?c ∈ cs" by (cases c, cases "lec_rel c", auto) show "0 < s ∧ ?c ∈ cs" using s0 mem by blast have "lec_of_constraint (s *R n) = Le_Constraint (lec_rel ?c) (s *R lec_poly ?c) unfolding n using s0 by (cases c, cases "lec_rel c", auto) } note id = this show "(∑x←C. case case x of (s, n) ==> (s, lec_of_constraint n) of (r, c) ==> Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)) = (∑(s, n)←C. lec_of_constraint (s *R n))" (is "sum_list (map ?f C) = sum_list (map ?g C)") proof (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl]) fix pair assume mem: "pair ∈ set C" obtain r c where pair: "pair = (r,c)" by force show "?f pair = ?g pair" unfolding pair split id[OF mem[unfolded pair]] .. qed qed next assume ?rhs then obtain C const rel where C: "∧ r c. (r,c) ∈ set C ==> 0 < r ∧ c ∈ cs" and sum: "(∑(r, c)←C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c = Le_Constraint rel 0 const" and const: "rel = Leq_Rel ∧ const < 0 ∨ rel = Lt_Rel ∧ const ≤ 0" by blast let ?C = "map (λ (r,c). (r, ?to_cs c)) C" show "∃ C. farkas_coefficients ?cs C" unfolding farkas_coefficients_def proof (intro exI[of _ ?C] exI[of _ const] exI[of _ rel] conjI const, unfold sum[symmetric]) show "∀(s, n)∈set ?C. n ∈ ?cs ∧ is_le (s *R n) ∧ s ≠ 0" using C by (fastforce split: le show "(∑(s, n)←?C. lec_of_constraint (s *R n)) = (∑(r, c)←C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c))" unfolding map_map o_def by (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl], insert C, fastforce split: le_rel qed qed finally show ?thesis . qed subsection ‹Farkas' Lemma› text ‹Finally we derive the commonly used form of Farkas' Lemma, which easily follows from @{thm [source] Motzkin's_transposition_theorem}. It only permits non-strict inequalities and, as a result, the sum of inequalities will always be non-strict.› lemma Farkas'_Lemma: fixes cs :: "rat le_constraint set" assumes only_non_strict: "lec_rel ` cs ⊆ {Leq_Rel}" and fin: "finite cs" shows "(∄ v. ∀ c ∈ cs. v ⊨le c) ⟷ (∃ C const. (∀ (r, c) ∈ set C. r > 0 ∧ c ∈ cs) ∧ (∑ (r,c) ← C. Leqc (r *R lec_poly c) (r *R lec_const c)) = Leqc 0 const ∧ const < 0)" (is "_ = ?rhs") proof - { fix c assume "c ∈ cs" with only_non_strict have "lec_rel c = Leq_Rel" by auto then have "∃ p const. c = Leqc p const" by (cases c, auto) } note leqc = this let ?lhs = "∃C const rel. (∀(r, c)∈set C. 0 < r ∧ c ∈ cs) ∧ (∑(r, c)←C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)) = Le_Constraint rel 0 const ∧ (rel = Leq_Rel ∧ const < 0 ∨ rel = Lt_Rel ∧ const ≤ 0)" show ?thesis unfolding Motzkin's_transposition_theorem[OF fin] proof assume ?rhs then obtain C const where C: "∧ r c. (r, c)∈set C ==> 0 < r ∧ c ∈ cs" and sum: "(∑(r, c)←C. Leqc (r *R lec_poly c) (r *R lec_const c)) = Leqc 0 const" and const: "const < 0" by blast show ?lhs proof (intro exI[of _ C] exI[of _ const] exI[of _ Leq_Rel] conjI) show "∀ (r,c) ∈ set C. 0 < r ∧ c ∈ cs" using C by force show "(∑(r, c)← C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)) Leqc 0 const" unfolding sum[symmetric] by (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl], insert C, force dest!: leqc) qed (insert const, auto) next assume ?lhs then obtain C const rel where C: "∧ r c. (r, c)∈set C ==> 0 < r ∧ c ∈ cs" and sum: "(∑(r, c)←C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c)) = Le_Constraint rel 0 const" and const: "rel = Leq_Rel ∧ const < 0 ∨ rel = Lt_Rel ∧ const ≤ 0" by blast have id: "(∑(r, c)←C. Le_Constraint (lec_rel c) (r *R lec_poly c) (r *R lec_const c (∑(r, c)←C. Leqc (r *R lec_poly c) (r *R lec_const c))" (is "_ = ?sum") by (rule arg_cong[of _ _ sum_list], rule map_cong, auto dest!: C leqc) have "lec_rel ?sum = Leq_Rel" unfolding sum_list_lec by (auto simp add: sum_list_Leq_Rel with sum[unfolded id] have rel: "rel = Leq_Rel" by auto with const have const: "const < 0" by auto show ?rhs by (intro exI[of _ C] exI[of _ const] conjI const, insert sum id C rel, force+) qed qed text ‹We also present slightly modified versions› lemma sum_list_map_filter_sum: fixes f :: "'a ==> 'b :: comm_monoid_add" shows "sum_list (map f (filter g xs)) + sum_list (map f (filter (Not o g) xs)) = by (induct xs, auto simp: ac_simps) text ‹A version where every constraint obtains exactly one coefficient and where lemma Farkas'_Lemma_set_sum: fixes cs :: "rat le_constraint set" assumes only_non_strict: "lec_rel ` cs ⊆ {Leq_Rel}" and fin: "finite cs" shows "(∄ v. ∀ c ∈ cs. v ⊨le c) ⟷ (∃ C const. (∀ c ∈ cs. C c ≥ 0) ∧ (∑ c ∈ cs. Leqc ((C c) *R lec_poly c) ((C c) *R lec_const c)) = Leqc 0 const ∧ const < 0)" unfolding Farkas'_Lemma[OF only_non_strict fin] proof ((standard; elim exE conjE), goal_cases) case (2 C const) from finite_distinct_list[OF fin] obtain csl where csl: "set csl = cs" and dist: "distinct by auto let ?list = "filter (λ c. C c ≠ 0) csl" let ?C = "map (λ c. (C c, c)) ?list" show ?case proof (intro exI[of _ ?C] exI[of _ const] conjI) have "(∑(r, c)←?C. Le_Constraint Leq_Rel (r *R lec_poly c) (r *R lec_const c)) = (∑(r, c)←map (λc. (C c, c)) csl. Le_Constraint Leq_Rel (r *R lec_poly c) (r *R l unfolding map_map by (rule sum_list_map_filter, auto simp: zero_le_constraint_def) also have "… = Le_Constraint Leq_Rel 0 const" unfolding 2(2)[symmetric] csl[symmetric unfolding sum.distinct_set_conv_list[OF dist] map_map o_def split .. finally show "(∑(r, c)←?C. Le_Constraint Leq_Rel (r *R lec_poly c) (r *R lec_const c)) = L by auto show "const < 0" by fact show "∀(r, c)∈set ?C. 0 < r ∧ c ∈ cs" using 2(1) unfolding set_map set_filter csl by auto qed next case (1 C const) define CC where "CC = (λ c. sum_list (map fst (filter (λ rc. snd rc = c) C)))" show "(∃ C const. (∀ c ∈ cs. C c ≥ 0) ∧ (∑ c ∈ cs. Leqc ((C c) *R lec_poly c) ((C c) *R lec_const c)) = Leqc 0 const ∧ const < 0)" proof (intro exI[of _ CC] exI[of _ const] conjI) show "∀c∈cs. 0 ≤ CC c" unfolding CC_def using 1(1) by (force intro!: sum_list_nonneg) show "const < 0" by fact from 1 have snd: "snd ` set C ⊆ cs" by auto show "(∑c∈cs. Le_Constraint Leq_Rel (CC c *R lec_poly c) (CC c *R lec_const c)) = unfolding 1(2)[symmetric] using fin snd unfolding CC_def proof (induct cs arbitrary: C rule: finite_induct) case empty hence C: "C = []" by auto thus ?case by simp next case *: (insert c cs C) let ?D = "filter (Not ∘ (λrc. snd rc = c)) C" from * have "snd ` set ?D ⊆ cs" by auto note IH = *(3)[OF this] have id: "(∑a← ?D. case a of (r, c) ==> Le_Constraint Leq_Rel (r *R lec_poly c) (r (∑(r, c)←?D. Le_Constraint Leq_Rel (r *R lec_poly c) (r *R lec_const c))" by (induct C, force+) show ?case unfolding sum.insert[OF *(1,2)] unfolding sum_list_map_filter_sum[of _ "λ rc. snd rc = c" C, symmetric] proof (rule arg_cong2[of _ _ _ _ "(+)"], goal_cases) case 2 show ?case unfolding IH[symmetric] by (rule sum.cong, insert *(2,1), auto intro!: arg_cong[of _ _ "λ xs. sum_list (map _ xs)"] next case 1 show ?case proof (rule sym, induct C) case (Cons rc C) thus ?case by (cases "rc", cases "snd rc = c", auto simp: field_simps scaleRat_left_distri qed (auto simp: zero_le_constraint_def) qed qed qed qed text ‹A version with indexed constraints, i.e., in particular where constraints m times. lemma Farkas'_Lemma_indexed: fixes c :: "nat ==> rat le_constraint" assumes only_non_strict: "lec_rel ` c ` Is ⊆ {Leq_Rel}" and fin: "finite Is" shows "(∄ v. ∀ i ∈ Is. v ⊨le c i) ⟷ (∃ C const. (∀ i ∈ Is. C i ≥ 0) ∧ (∑ i ∈ Is. Leqc ((C i) *R lec_poly (c i)) ((C i) *R lec_const (c i))) = Leqc 0 ∧ const < 0)" proof - let ?C = "c ` Is" have fin: "finite ?C" using fin by auto have "(∄ v. ∀ i ∈ Is. v ⊨le c i) = (∄ v. ∀ cc ∈ ?C. v ⊨le cc)" by force also have "… = (∃ C const. (∀ i ∈ Is. C i ≥ 0) ∧ (∑ i ∈ Is. Leqc ((C i) *R lec_poly (c i)) ((C i) *R lec_const (c i))) = Leqc 0 ∧ const < 0)" (is "?l = ?r") proof assume ?r then obtain C const where r: "(∀ i ∈ Is. C i ≥ 0)" and eq: "(∑ i ∈ Is. Leqc ((C i) *R lec_poly (c i)) ((C i) *R lec_const (c i))) = L and "const < 0" by auto from finite_distinct_list[OF ‹finite Is›] obtain Isl where isl: "set Isl = Is" and dist: "distinct Isl" by auto let ?CC = "filter (λ rc. fst rc ≠ 0) (map (λ i. (C i, c i)) Isl)" show ?l unfolding Farkas'_Lemma[OF only_non_strict fin] proof (intro exI[of _ ?CC] exI[of _ const] conjI) show "const < 0" by fact show "∀ (r, ca) ∈ set ?CC. 0 < r ∧ ca ∈ ?C" using r(1) isl by auto show "(∑(r, c)←?CC. Le_Constraint Leq_Rel (r *R lec_poly c) (r *R lec_const c)) = Le_Constraint Leq_Rel 0 const" unfolding eq[symmetric] by (subst sum_list_map_filter, force simp: zero_le_constraint_def, unfold map_map o_def, subst sum_list_distinct_conv_sum_set[OF dist], rule sum.cong, auto qed next assume ?l from this[unfolded Farkas'_Lemma_set_sum[OF only_non_strict fin]] obtain C const where nonneg: "(∀c∈ ?C. 0 ≤ C c)" and sum: "(∑c∈ ?C. Le_Constraint Leq_Rel (C c *R lec_poly c) (C c *R lec_const c)) Le_Constraint Leq_Rel 0 const" and const: "const < 0" by blast define I where "I = (λ i. (C (c i) / rat_of_nat (card (Is ∩ { j. c i = c j}))))" show ?r proof (intro exI[of _ I] exI[of _ const] conjI const) show "∀i ∈ Is. 0 ≤ I i" using nonneg unfolding I_def by auto show "(∑ i ∈ Is. Le_Constraint Leq_Rel (I i *R lec_poly (c i)) (I i *R lec_const Le_Constraint Leq_Rel 0 const" unfolding sum[symmetric] unfolding sum.image_gen[OF ‹finite Is›, of _ c] proof (rule sum.cong[OF refl], goal_cases) case (1 cc) define II where "II = (Is ∩ {j. cc = c j})" from 1 have "II ≠ {}" unfolding II_def by auto moreover have finII: "finite II" using ‹finite Is› unfolding II_def by auto ultimately have card: "card II ≠ 0" by auto let ?C = "λ II. rat_of_nat (card II)" define ii where "ii = C cc / rat_of_nat (card II)" have "(∑i∈{x ∈ Is. c x = cc}. Le_Constraint Leq_Rel (I i *R lec_poly (c i)) (I i = (∑ i∈ II. Le_Constraint Leq_Rel (ii *R lec_poly cc) (ii *R lec_const cc))" unfolding I_def ii_def II_def by (rule sum.cong, auto) also have "… = Le_Constraint Leq_Rel ((?C II * ii) *R lec_poly cc) ((?C II * ii) * using finII by (induct II rule: finite_induct, auto simp: zero_le_constraint_def field_sim scaleRat_left_distrib) also have "?C II * ii = C cc" unfolding ii_def using card by auto finally show ?case . qed qed qed finally show ?thesis . qed end
¤ Dauer der Verarbeitung: 0.43 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09