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.

# Fourier-Motzkin Elimination

[Fourier-Motzkin elimination](https://en.wikipedia.org/wiki/Fourier%E2%80%93Motzkin_elimination) is an algorithm to eliminate a variable from a system of linear inequalities (*polyhedron* in the following). The resulting polyhedron is *equisatisfiable*, i.e. it has a solution if and only if the original polyhedron had a solution. As a trivial example consider the polyhedron ``` 5x + 3y ≤ 11 2x - 3y ≤ -4 ``` By adding up the two inequalities we can eliminate `y` and obtain the polyhedron ``` 7x ≤ 7 ``` We can thus deduce that the original polyhedron had a solution if and only if `x ≤ 1`. In general, Fourier-Motzkin elimination proceeds in three phases to elminate variable `x_k`: - Sorting: we sort equations by the coefficients of `x_k` into sets `G` (`>0`), `Z` (`=0`), and `L` (`<0`). The set `Z` can stay untouched. - Normalization: we divide all equations in `G` and `L` by the absolute value of the coefficient of `x_k`, such that we end up with coefficients `1`/`-1` (`G`/`L`) for `x_k`. - Product Sum: we build the sums of all pairs of equations from `G` and `L` (like in the example). Your task is to prove equisatisfiability of the Fourier-Motzkin algorithm. Partial credit will be given for proving only one of the two directions of this theorem, and for proving two key lemmas on the way to get there (see template files).

## Resources

### Definitions File

```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>
"ineq \<Rightarrow> ineq list \<Rightarrow> ineq list" where

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```

### Template File

```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>
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```

### Check File

```theory Check
imports Submission
begin

text \<open>Prove the following helpful lemmas for proof of the main correctness theorem:\<close>
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"

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```

### Definitions File

```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⟩

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 :=

/-- 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```

### Template File

```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⟩

```

### Check File

```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 :=

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```

### Definitions File

```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).

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 :=

(* 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).
```

### Template File

```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.

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.

(* 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.

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.