I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs
imports Complex_Main
begin
section \<open>Polyhedra\<close>
type_synonym coefficient = "rat"
type_synonym lin_term = "coefficient list"
datatype ineq = ineq "lin_term" "rat"
type_synonym polyhedron = "ineq list"
definition eval_term :: "lin_term \<Rightarrow> rat list \<Rightarrow> rat" where
"eval_term cs xs = sum_list (map (\<lambda>(c, x). c*x) (zip cs xs))"
definition ineq_sat :: "ineq \<Rightarrow> rat list \<Rightarrow> bool" where
"ineq_sat p xs = (case p of (ineq cs k) \<Rightarrow> k \<ge> (eval_term cs xs))"
definition pol_sat :: "polyhedron \<Rightarrow> rat list \<Rightarrow> bool" where
"pol_sat ps xs = (\<forall>p\<in>set ps. ineq_sat p xs)"
section \<open>Fourier-Motzkin Elimination\<close>
datatype triple = triple "ineq list" "ineq list" "ineq list"
definition "G ps n = filter (\<lambda>x. case x of ineq cs k => cs!n > 0) ps"
definition "Z xs n = filter (\<lambda>x. case x of ineq ys k => ys!n = 0) xs"
definition "L xs n = filter (\<lambda>x. case x of ineq ys k => ys!n < 0) xs"
definition GZL :: "ineq list \<Rightarrow> nat \<Rightarrow> triple" where
"GZL xs n = triple (G xs n) (Z xs n) (L xs n)"
definition triple_sat :: "triple \<Rightarrow> rat list \<Rightarrow> bool" where
"triple_sat ts xs = (case ts of (triple gs zs ls) \<Rightarrow> (pol_sat gs xs)\<and>(pol_sat zs xs)\<and>(pol_sat ls xs))"
\<comment> \<open>Divides all elements in a list by a constant.\<close>
definition list_div :: "rat list \<Rightarrow> rat \<Rightarrow> rat list" where
"list_div cs cn = map (\<lambda>c. c/cn) cs"
lemma "list_div [4,5] 2 = [2, 5 / 2]"
by eval
\<comment> \<open>Normalized an inequality by the absolute value of coefficient \<open>n\<close>.\<close>
definition ineq_div :: "ineq \<Rightarrow> nat \<Rightarrow> ineq" where
"ineq_div p n = (case p of ineq cs k \<Rightarrow> ineq (list_div cs (abs(cs!n))) (k/(abs(cs!n))))"
lemma "ineq_div (ineq [7,9] 3) 1 = ineq [7 / 9, 1] (1 / 3)"
by eval
\<comment> \<open>Normalizes all inequalities in a polyhedron by the absolute value of coefficient \<open>n\<close>.\<close>
definition pol_div :: "polyhedron \<Rightarrow> nat \<Rightarrow> ineq list" where
"pol_div ps n = map (\<lambda>p. ineq_div p n) ps"
lemma "pol_div [(ineq [-1,-1,-1] 0),
(ineq [3,-1,-1] 1),
(ineq [-1,3,-1] 2),
(ineq [-1,-1,3] 3)] 0
= [ineq [- 1, - 1, - 1] 0,
ineq [1, - (1 / 3), - (1 / 3)] (1 / 3),
ineq [- 1, 3, - 1] 2,
ineq [- 1, - 1, 3] 3]"
by eval
definition GZL_div :: "triple \<Rightarrow> nat \<Rightarrow> triple" where
"GZL_div ts n = (case ts of (triple xs ys zs) \<Rightarrow> triple (pol_div xs n) ys (pol_div zs n))"
lemma "GZL_div (GZL [(ineq [-1,-1,-1] 0),
(ineq [3,-1,-1] 1),
(ineq [-1,3,-1] 2),
(ineq [-1,-1,3] 3)] 0) 0
= triple [ineq [1, - (1 / 3), - (1 / 3)] (1 / 3)]
[]
[ineq [- 1, - 1, - 1] 0, ineq [- 1, 3, - 1] 2, ineq [- 1, - 1, 3] 3]"
by eval
\<comment> \<open>Computes the sum of two inequalities.\<close>
definition ineq_add :: "ineq \<Rightarrow> ineq \<Rightarrow> ineq" where
"ineq_add x y = (case (x,y) of (ineq xs k1, ineq ys k2) \<Rightarrow>
ineq (map (\<lambda>(x,y). (x+y)) (zip xs ys)) (k1+k2))"
lemma "ineq_add (ineq [1,2] 4) (ineq [3,5] 2) = ineq [4, 7] 6"
by eval
\<comment> \<open>Adds inequality \<open>g\<close> to every inequality in \<open>ls\<close>.\<close>
definition pol_add ::
"ineq \<Rightarrow> ineq list \<Rightarrow> ineq list" where
"pol_add g ls = map (\<lambda>l. ineq_add g l) ls"
lemma "pol_add (ineq [1,2] 3) [(ineq[2,3] 4), (ineq [4,6] 2)] = [ineq [3, 5] 7, ineq [5, 8] 5]"
by eval
\<comment> \<open>Computes the sum of all pairs of inequalities from two lists \<open>xs\<close> and \<open>ys\<close>.\<close>
definition term_pairing ::
"ineq list \<Rightarrow> ineq list \<Rightarrow> ineq list" where
"term_pairing xs ys = concat (map (\<lambda>x. (pol_add x ys)) xs)" for xs
\<comment> \<open>Computes all possible sums of pairs of \<open>G\<close> and \<open>L\<close> inequalities while leaving \<open>Z\<close> untouched.\<close>
definition GZL_product :: "triple \<Rightarrow> polyhedron" where
"GZL_product x = (case x of triple gs ys ls \<Rightarrow> ys@(term_pairing gs ls))"
\<comment> \<open>We can simply run the three phases in sequence to get the Fourier-Motzkin elimination algorithm.\<close>
definition FM :: "polyhedron \<Rightarrow> nat \<Rightarrow> polyhedron" where
"FM xs n = GZL_product (GZL_div (GZL xs n) n)"
end
theory Submission
imports Defs
begin
\<comment> \<open>What we want to prove:\<close>
theorem FM_sat_equivalent:
assumes "\<forall>p \<in> set ps. (case p of (ineq cs k) \<Rightarrow> length cs = length xs)" "n < length xs"
shows "pol_sat (FM ps n) xs \<longleftrightarrow> (\<exists>t. pol_sat ps (xs[n := t]))"
oops
text \<open>Prove the following helpful lemmas for proof of the main correctness theorem:\<close>
theorem ineq_add_cancel:
assumes "length gcs = length xs" "n < length xs" "gcs!n = 1" "length lcs = length xs" "lcs!n = -1"
shows
"ineq_sat (ineq_add (ineq gcs gk) (ineq lcs lk)) xs \<longleftrightarrow>
eval_term (gcs[n := 0]) xs + eval_term (lcs[n := 0]) xs \<le> gk + lk"
oops
theorem eval_term_nth_split:
assumes "length gcs = length xs" "n < length xs"
shows "eval_term gcs (xs[n := t]) = eval_term (gcs[n := 0]) xs + gcs!n * t"
using assms unfolding eval_term_def
oops
text \<open>We give partial credits for the two directions of the main theorem:\<close>
theorem FM_preserves_solution:
assumes "\<forall>p \<in> set ps. (case p of (ineq cs k) \<Rightarrow> length cs = length xs)" "n < length xs"
"pol_sat ps (xs[n := t])"
shows "pol_sat (FM ps n) xs"
oops
theorem FM_sat_has_solution:
assumes "\<forall>p \<in> set ps. (case p of (ineq cs k) \<Rightarrow> length cs = length xs)" "n < length xs"
"pol_sat (FM ps n) xs"
shows "\<exists>t. pol_sat ps (xs[n := t])"
oops
end
theory Check
imports Submission
begin
text \<open>Prove the following helpful lemmas for proof of the main correctness theorem:\<close>
theorem ineq_add_cancel:
assumes "length gcs = length xs" "n < length xs" "gcs!n = 1" "length lcs = length xs" "lcs!n = -1"
shows
"ineq_sat (ineq_add (ineq gcs gk) (ineq lcs lk)) xs \<longleftrightarrow>
eval_term (gcs[n := 0]) xs + eval_term (lcs[n := 0]) xs \<le> gk + lk"
using assms by (rule ineq_add_cancel)
theorem eval_term_nth_split:
assumes "length gcs = length xs" "n < length xs"
shows "eval_term gcs (xs[n := t]) = eval_term (gcs[n := 0]) xs + gcs!n * t"
using assms by (rule eval_term_nth_split)
text \<open>We give partial credits for the two directions of the main theorem:\<close>
theorem FM_preserves_solution:
assumes "\<forall>p \<in> set ps. (case p of (ineq cs k) \<Rightarrow> length cs = length xs)" "n < length xs"
"pol_sat ps (xs[n := t])"
shows "pol_sat (FM ps n) xs"
using assms by (rule FM_preserves_solution)
theorem FM_sat_has_solution:
assumes "\<forall>p \<in> set ps. (case p of (ineq cs k) \<Rightarrow> length cs = length xs)" "n < length xs"
"pol_sat (FM ps n) xs"
shows "\<exists>t. pol_sat ps (xs[n := t])"
using assms by (rule FM_sat_has_solution)
end
import data.real.sign /-! Fourier-Motzkin elimination In this problem we will show that the following algorithm of Fourier-Motzkin elimination is correct. This is an algorithm to eliminate variables from a linear system of inequalities. -/ open list /-- A linear term. `[a₁, ..., aₙ]` represents `a₁ * x₁ + ... + aₙ * xₙ`. -/ @[reducible] def lin_term : Type := list ℚ /-- A linear inequality. `([a₁, ..., aₙ], x)` represents `a₁ * x₁ + ... + aₙ * xₙ ≤ x`. -/ def ineq : Type := lin_term × ℚ /-- A polyhedron is a list of linear inequalities. `([a₁, ... aₙ], x)` represents `a₁ * x₁ + ... + aₙ * xₙ ≤ x`. -/ @[reducible] def polyhedron : Type := list ineq /-- The `eval_term [a₁, ..., aₙ] [x₁, ..., xₙ]` is `a₁ * x₁ + ... + aₙ * xₙ`. -/ def eval_term (t : lin_term) (qs : list ℚ) : ℚ := (zip_with (*) t qs).sum /-- The proposition that an inequality is satisfied on the given point `qs`. -/ def ineq_sat (p : ineq) (qs : list ℚ) : Prop := eval_term p.1 qs ≤ p.2 /-- The proposition that a point `qs` lies in the polyhedron `pol`. -/ def pol_sat (pol : polyhedron) (qs : list ℚ) : Prop := ∀ p ∈ pol, ineq_sat p qs /-! Fourier-Motzkin Elimination -/ /-- A triple of polyhedra. The three fields will have a different sign in front of the variable that we will eliminate. -/ structure triple := (pos : polyhedron) (zero : polyhedron) (neg : polyhedron) /-- The inequalities of `pol` where the coefficient in front of the `n`-th variable is positive. -/ def G (pol : polyhedron) (n : ℕ) : polyhedron := pol.filter $ λ p, p.1.inth n > 0 /-- The inequalities of `pol` where the coefficient in front of the `n`-th variable is 0. -/ def Z (pol : polyhedron) (n : ℕ) : polyhedron := pol.filter $ λ p, p.1.inth n = 0 /-- The inequalities of `pol` where the coefficient in front of the `n`-th variable is negative. -/ def L (pol : polyhedron) (n : ℕ) : polyhedron := pol.filter $ λ p, p.1.inth n < 0 def GZL (pol : polyhedron) (n : ℕ) : triple := ⟨G pol n, Z pol n, L pol n⟩ /-- takes an inequality and divides everything with the absolute value of the coefficient that is in place `n` -/ def ineq_div (p : ineq) (n : ℕ) : ineq := let x := abs (p.1.inth n) in (p.1.map (/ x), p.2 / x) example : ineq_div ([7,9], 3) 1 = ([7 / 9, 1], 1 / 3) := by norm_num [ineq_div, abs] /-- Isolates the `n`-th coefficients of all linear inequalities of a polyhedon. -/ def pol_div (pol : polyhedron) (n : ℕ) : polyhedron := pol.map $ λ p, ineq_div p n /-- Divide away the absolute value of the coefficients in front of the `n`-th variable, unless it is 0. -/ def GZL_div (t : triple) (n : ℕ) : triple := ⟨pol_div t.1 n, t.2, pol_div t.3 n⟩ /-- Adds two inequalities. -/ def ineq_add (p1 p2 : ineq) : ineq := (zip_with (+) p1.1 p2.1, p1.2 + p2.2) /-- Adds `p` to all inequalities in `pol` -/ def pol_add (p : ineq) (pol : polyhedron) : polyhedron := pol.map (ineq_add p) /-- given two lists of linear terms, for each pairing of linear terms from both lists, it creates a new linear term, that is the second added to the first -/ def term_pairing (pol1 pol2 : polyhedron) : polyhedron := (pol1.map (λ p, pol_add p pol2)).join /-- For ever. -/ def GZL_prod (t : triple) : polyhedron := t.zero ++ term_pairing t.pos t.neg /-- One Fourier-Motzkin elimination step. -/ def FM (pol : polyhedron) (n : ℕ) := GZL_prod $ GZL_div (GZL pol n) n /-- all lengths of the lists are the same. -/ def pol_lengths (pol : polyhedron) (N : ℕ) := ∀ p ∈ pol, (p : ineq).1.length = N
import .defs
open list
/-! Prove the following helpful lemmas for proof of the main correctness theorem: -/
theorem ineq_add_cancel {gcs lcs : lin_term} {gk lk : ℚ} {qs : list ℚ} {n : ℕ}
(h1 : gcs.length = qs.length) (h2 : n < qs.length) (h3 : gcs.inth n = 1)
(h4 : lcs.length = qs.length) (h5 : lcs.inth n = -1) :
ineq_sat (ineq_add (gcs, gk) (lcs, lk)) qs ↔
eval_term (gcs.update_nth n 0) qs + eval_term (lcs.update_nth n 0) qs ≤ gk + lk :=
sorry
theorem eval_term_nth_split {gcs : lin_term} {gk : ℚ} {qs : list ℚ} {n : ℕ} {t : ℚ}
(h1 : gcs.length = qs.length) (h2 : n < qs.length) :
eval_term gcs (qs.update_nth n t) = eval_term (gcs.update_nth n 0) qs + gcs.inth n * t :=
sorry
/-! We give partial credits for the two directions of the main theorem: -/
theorem FM_preserves_solution {N : ℕ} {pol : polyhedron} (hpol : pol_lengths pol N) {n : ℕ}
{qs : list ℚ} {t : ℚ} (hqs : n < qs.length) (ht : pol_sat pol (qs.update_nth n t)) :
pol_sat (FM pol n) qs :=
sorry
theorem FM_sat_has_solution {N : ℕ} {pol : polyhedron} (hpol : pol_lengths pol N) {n : ℕ}
{qs : list ℚ} (hqs : n < qs.length) (ht : pol_sat (FM pol n) qs) :
∃ t, pol_sat pol (qs.update_nth n t) :=
sorry
/-- These facts show that one Fourier-Motzkin elimination step gives the same polyhedron. -/
theorem FM_sat_equivalent {N : ℕ} {pol : polyhedron} (hpol : pol_lengths pol N) {n : ℕ}
{qs : list ℚ} (hqs : n < qs.length) :
pol_sat (FM pol n) qs ↔ ∃ t, pol_sat pol (qs.update_nth n t) :=
⟨FM_sat_has_solution hpol hqs, λ ⟨t, ht⟩, FM_preserves_solution hpol hqs ht⟩
import .submission
open list
theorem check1 : ∀ {gcs lcs : lin_term} {gk lk : ℚ} {qs : list ℚ} {n : ℕ}
(h1 : gcs.length = qs.length) (h2 : n < qs.length) (h3 : gcs.inth n = 1)
(h4 : lcs.length = qs.length) (h5 : lcs.inth n = -1),
ineq_sat (ineq_add (gcs, gk) (lcs, lk)) qs ↔
eval_term (gcs.update_nth n 0) qs + eval_term (lcs.update_nth n 0) qs ≤ gk + lk :=
@ineq_add_cancel
theorem check2 : ∀ {gcs : lin_term} {gk : ℚ} {qs : list ℚ} {n : ℕ} {t : ℚ}
(h1 : gcs.length = qs.length) (h2 : n < qs.length),
eval_term gcs (qs.update_nth n t) = eval_term (gcs.update_nth n 0) qs + gcs.inth n * t :=
@eval_term_nth_split
/-! We give partial credits for the two directions of the main theorem: -/
theorem check3 : ∀ {N : ℕ} {pol : polyhedron} (hpol : pol_lengths pol N) {n : ℕ}
{qs : list ℚ} {t : ℚ} (hqs : n < qs.length) (ht : pol_sat pol (qs.update_nth n t)),
pol_sat (FM pol n) qs :=
@FM_preserves_solution
theorem check4 : ∀ {N : ℕ} {pol : polyhedron} (hpol : pol_lengths pol N) {n : ℕ}
{qs : list ℚ} (hqs : n < qs.length) (ht : pol_sat (FM pol n) qs),
∃ t, pol_sat pol (qs.update_nth n t) :=
@FM_sat_has_solution
From Coq Require Export List QArith.
From Coq Require Import Qabs Qreduction Bool.
Import ListNotations.
(* Fourier-Motzkin elimination *)
Open Scope Q.
(* A linear term. `[a₁; ...; aₙ]` represents `a₁ * x₁ + ... + aₙ * xₙ`. *)
Definition lin_term : Type := list Q.
(* A linear inequality. `([a₁, ..., aₙ], x)` represents `a₁ * x₁ + ... + aₙ * xₙ ≤ x`. *)
Definition ineq : Type := lin_term * Q.
(* A polyhedron is a list of linear inequalities.
`([a₁, ... aₙ], x)` represents `a₁ * x₁ + ... + aₙ * xₙ ≤ x`. *)
Definition polyhedron : Type := list ineq.
(* The `eval_term [a₁, ..., aₙ] [x₁, ..., xₙ]` is `a₁ * x₁ + ... + aₙ * xₙ`. *)
Definition eval_term (t : lin_term) (qs : list Q) : Q :=
fold_right (fun '(a, x) sum => sum + a * x) 0 (combine t qs).
(* The proposition that an inequality is satisfied on the given point `qs`. *)
Definition ineq_sat (p : ineq) (qs : list Q) : Prop :=
eval_term (fst p) qs <= (snd p).
(* The proposition that a point `qs` lies in the polyhedron `pol`. *)
Definition pol_sat (pol : polyhedron) (qs : list Q) : Prop :=
forall p, In p pol -> ineq_sat p qs.
(* Fourier-Motzkin Elimination *)
(* A triple of polyhedra. The three fields will have a different sign in front of the variable
that we will eliminate. *)
Structure triple := Triple {
pos : polyhedron;
zero : polyhedron;
neg : polyhedron}.
(* The inequalities of `pol` where the coefficient in front of the `n`-th variable is positive. *)
Definition Qlt_bool (x y : Q) :=
(Qnum x * QDen y <? Qnum y * QDen x)%Z.
(* Definition Qlt_bool (q1 q2 : Q) : bool := *)
(* (Qle_bool q1 q2) && negb (Qeq_bool q1 q2). *)
Definition G (pol : polyhedron) (n : nat) : polyhedron :=
filter (fun '(tm, _) => Qlt_bool 0 (nth n tm 0)) pol.
(* The inequalities of `pol` where the coefficient in front of the `n`-th variable is 0. *)
Definition Z (pol : polyhedron) (n : nat) : polyhedron :=
filter (fun '(tm, _) => Qeq_bool 0 (nth n tm 0)) pol.
(* The inequalities of `pol` where the coefficient in front of the `n`-th variable is negative. *)
Definition L (pol : polyhedron) (n : nat) : polyhedron :=
filter (fun '(tm, _) => Qlt_bool (nth n tm 0) 0) pol.
Definition GZL (pol : polyhedron) (n : nat) : triple :=
Triple (G pol n) (Z pol n) (L pol n).
(* takes an inequality and divides everything with the absolute
value of the coefficient that is in place `n`,
the rational numbers in the result are normalized with `Qred` *)
Definition ineq_div (p : ineq) (n : nat) : ineq :=
let '(tm, v) := p in
let x := Qabs (nth n tm 0) in
(map (fun q => Qred (q / x)) tm, Qred (v / x)).
Check eq_refl : ineq_div ([7;9], 3) 1 = ([7 # 9; 1], 1 # 3).
(* Isolates the `n`-th coefficients of all linear inequalities of a polyhedon. *)
Definition pol_div (pol : polyhedron) (n : nat) : polyhedron :=
map (fun p => ineq_div p n) pol.
(* Divide away the absolute value of the coefficients in front of the `n`-th variable,
unless it is 0. *)
Definition GZL_div (t : triple) (n : nat) : triple :=
Triple (pol_div t.(pos) n) (t.(zero)) (pol_div t.(neg) n).
(* Adds two inequalities. *)
Definition ineq_add (p1 p2 : ineq) : ineq :=
(map (fun '(q1, q2) => q1 + q2) (combine (fst p1) (fst p2)), snd p1 + snd p2).
(* Adds `p` to all inequalities in `pol` *)
Definition pol_add (p : ineq) (pol : polyhedron) : polyhedron :=
map (ineq_add p) pol.
(* given two lists of linear terms, for each pairing of linear
terms from both lists, it creates a new linear term, that is
the second added to the first *)
Definition term_pairing (pol1 pol2 : polyhedron) : polyhedron :=
concat (map (fun p => pol_add p pol2) pol1).
(* For ever. *)
Definition GZL_prod (t : triple) : polyhedron :=
zero t ++ term_pairing t.(pos) t.(neg).
(* One Fourier-Motzkin elimination step. *)
Definition FM (pol : polyhedron) (n : nat) :=
GZL_prod (GZL_div (GZL pol n) n).
(* all lengths of the lists are the same. *)
Definition pol_lengths (pol : polyhedron) (N : nat) : Prop :=
forall p : ineq, In p pol -> length (fst p) = N.
(* Helper: update n-th element of a list xs with a value x. Zero-based indexing *)
Fixpoint update_nth {A} (n : nat) (x : A) (xs : list A) : list A :=
match n, xs with
| _, [] => xs
| O, _ :: xs' => x :: xs'
| S n', h :: xs' => h :: update_nth n' x xs'
end.
Notation "xs '[' n ':=' x ']'" := (update_nth n x xs) (at level 0).
From Coq Require Import List QArith Qabs Qreduction Bool.
Require Import Defs.
Open Scope Q.
(* Prove the following helpful lemmas for proof of the main correctness theorem: *)
Lemma ineq_add_cancel {gcs lcs : lin_term} {gk lk : Q} {qs : list Q} {n : nat} :
length gcs = length qs ->
(n < length qs)%nat ->
nth n gcs 0 = 1 ->
length lcs = length qs ->
nth n lcs 0 = -1 ->
ineq_sat (ineq_add (gcs, gk) (lcs, lk)) qs
<->
eval_term (gcs [n:=0]) qs + eval_term (lcs [n := 0]) qs <= gk + lk.
Proof.
Admitted.
Lemma eval_term_nth_split {gcs : lin_term} {qs : list Q} {n : nat} {t : Q} :
length gcs = length qs ->
(n < length qs)%nat ->
eval_term gcs (qs [n := t]) == eval_term (gcs [n := 0]) qs + nth n gcs 0 * t.
Proof.
Admitted.
(* We give partial credits for the two directions of the main theorem: *)
Lemma FM_preserves_solution {N : nat} {pol : polyhedron} (hpol : pol_lengths pol N) {n : nat} {qs : list Q} {t : Q} :
(n < length qs)%nat ->
pol_sat pol (qs [n := t]) ->
pol_sat (FM pol n) qs.
Proof.
Admitted.
Lemma FM_sat_has_solution {N : nat} {pol : polyhedron} (hpol : pol_lengths pol N) {n : nat} {qs : list Q} :
(n < length qs)%nat ->
pol_sat (FM pol n) qs ->
exists t, pol_sat pol (qs [n := t]).
Proof.
Admitted.
Check @FM_preserves_solution.
(* The main result we want to prove.These facts show that one Fourier-Motzkin
elimination step gives the same polyhedron. *)
Theorem FM_sat_equivalent {N : nat} {pol : polyhedron}
(hpol : pol_lengths pol N) {n : nat} {qs : list Q} :
(n < length qs)%nat ->
pol_sat (FM pol n) qs <-> exists t, pol_sat pol (qs [n := t]).
Proof.
Admitted.