Theory Farkas
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 and prove
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 combinations
of inequalities. To this end we define one type that permits strict and non-strict
inequalities which are always of the form ``polynomial R constant'' where R is either
$\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