Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis
Ported by: Scott Morrison
-/
import Mathlib.Tactic.Linarith.Datatypes

/-!
# The Fourier-Motzkin elimination procedure

The Fourier-Motzkin procedure is a variable elimination method for linear inequalities.


Given a set of linear inequalities `comps = {táµ¢ Ráµ¢ 0}`,
we aim to eliminate a single variable `a` from the set.
We partition `comps` into `comps_pos`, `comps_neg`, and `comps_zero`,
where `comps_pos` contains the comparisons `táµ¢ Ráµ¢ 0` in which
the coefficient of `a` in `táµ¢` is positive, and similar.

For each pair of comparisons `tᵢ Rᵢ 0 ∈ comps_pos`, `tⱼ Rⱼ 0 ∈ comps_neg`,
we compute coefficients `vᵢ, vⱼ ∈ ℕ` such that `vᵢ*tᵢ + vⱼ*tⱼ` cancels out `a`.
We collect these sums `vᵢ*tᵢ + vⱼ*tⱼ R' 0` in a set `S` and set `comps' = S ∪ comps_zero`,
a new set of comparisons in which `a` has been eliminated.

Theorem: `comps` and `comps'` are equisatisfiable.

We recursively eliminate all variables from the system. If we derive an empty clause `0 < 0`,
we conclude that the original system was unsatisfiable.
-/

open Std

namespace Linarith

/-!
### Datatypes

The `CompSource` and `PComp` datatypes are specific to the FM elimination routine;
they are not shared with other components of `linarith`.
-/

/--
`CompSource` tracks the source of a comparison.
The atomic source of a comparison is an assumption, indexed by a natural number.
Two comparisons can be added to produce a new comparison,
and one comparison can be scaled by a natural number to produce a new comparison.
 -/
inductive 
CompSource: Type
CompSource
:
Type: Type 1
Type
|
assump: ℕ → CompSource
assump
:
Nat: Type
Nat
→
CompSource: Type
CompSource
|
add: CompSource → CompSource → CompSource
add
:
CompSource: Type
CompSource
→
CompSource: Type
CompSource
→
CompSource: Type
CompSource
|
scale: ℕ → CompSource → CompSource
scale
:
Nat: Type
Nat
→
CompSource: Type
CompSource
→
CompSource: Type
CompSource
deriving
Inhabited: Sort u → Sort (max1u)
Inhabited
/-- Given a `CompSource` `cs`, `cs.flatten` maps an assumption index to the number of copies of that assumption that appear in the history of `cs`. For example, suppose `cs` is produced by scaling assumption 2 by 5, and adding to that the sum of assumptions 1 and 2. `cs.flatten` maps `1 ↦ 1, 2 ↦ 6`. -/ def
CompSource.flatten: CompSource → HashMap ℕ ℕ
CompSource.flatten
:
CompSource: Type
CompSource
→
HashMap: (α : Type ?u.939) → Type ?u.938 → [inst : BEq α] → [inst : Hashable α] → Type (max0?u.939?u.938)
HashMap
Nat: Type
Nat
Nat: Type
Nat
| (
CompSource.assump: ℕ → CompSource
CompSource.assump
n) =>
HashMap.empty: {α : Type ?u.963} → {β : Type ?u.962} → [inst : BEq α] → [inst_1 : Hashable α] → HashMap α β
HashMap.empty
.
insert: {α : Type ?u.1002} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.1001} → HashMap α β → α → β → HashMap α β
insert
n
1: ?m.1025
1
| (
CompSource.add: CompSource → CompSource → CompSource
CompSource.add
c1 c2) => (
CompSource.flatten: CompSource → HashMap ℕ ℕ
CompSource.flatten
c1).
mergeWith: {α : Type ?u.1052} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.1051} → (α → β → β → β) → HashMap α β → HashMap α β → HashMap α β
mergeWith
(fun
_: ?m.1065
_
b: ?m.1068
b
b': ?m.1071
b'
=>
b: ?m.1068
b
+
b': ?m.1071
b'
) (
CompSource.flatten: CompSource → HashMap ℕ ℕ
CompSource.flatten
c2) | (
CompSource.scale: ℕ → CompSource → CompSource
CompSource.scale
n c) => (
CompSource.flatten: CompSource → HashMap ℕ ℕ
CompSource.flatten
c).
mapVal: {α : Type ?u.1137} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.1136} → {γ : Type ?u.1135} → (α → β → γ) → HashMap α β → HashMap α γ
mapVal
(fun
_: ?m.1151
_
v: ?m.1154
v
=>
v: ?m.1154
v
* n) /-- Formats a `CompSource` for printing. -/ def
CompSource.toString: CompSource → String
CompSource.toString
:
CompSource: Type
CompSource
→
String: Type
String
| (
CompSource.assump: ℕ → CompSource
CompSource.assump
e) =>
ToString.toString: {α : Type ?u.3434} → [self : ToString α] → α → String
ToString.toString
e | (
CompSource.add: CompSource → CompSource → CompSource
CompSource.add
c1 c2) =>
CompSource.toString: CompSource → String
CompSource.toString
c1 ++
" + ": String
" + "
++
CompSource.toString: CompSource → String
CompSource.toString
c2 | (
CompSource.scale: ℕ → CompSource → CompSource
CompSource.scale
n c) =>
ToString.toString: {α : Type ?u.3557} → [self : ToString α] → α → String
ToString.toString
n ++
" * ": String
" * "
++
CompSource.toString: CompSource → String
CompSource.toString
c instance :
ToFormat: Type ?u.4009 → Type ?u.4009
ToFormat
CompSource: Type
CompSource
:= ⟨fun
a: ?m.4017
a
=>
CompSource.toString: CompSource → String
CompSource.toString
a: ?m.4017
a
⟩ /-- A `PComp` stores a linear comparison `Σ cᵢ*xᵢ R 0`, along with information about how this comparison was derived. The original expressions fed into `linarith` are each assigned a unique natural number label. The *historical set* `PComp.history` stores the labels of expressions that were used in deriving the current `PComp`. Variables are also indexed by natural numbers. The sets `PComp.effective`, `PComp.implicit`, and `PComp.vars` contain variable indices. * `PComp.vars` contains the variables that appear in any inequality in the historical set. * `PComp.effective` contains the variables that have been effectively eliminated from `PComp`. A variable `n` is said to be *effectively eliminated* in `p : PComp` if the elimination of `n` produced at least one of the ancestors of `p` (or `p` itself). * `PComp.implicit` contains the variables that have been implicitly eliminated from `PComp`. A variable `n` is said to be *implicitly eliminated* in `p` if it satisfies the following properties: - `n` appears in some inequality in the historical set (i.e. in `p.vars`). - `n` does not appear in `p.c.vars` (i.e. it has been eliminated). - `n` was not effectively eliminated. We track these sets in order to compute whether the history of a `PComp` is *minimal*. Checking this directly is expensive, but effective approximations can be defined in terms of these sets. During the variable elimination process, a `PComp` with non-minimal history can be discarded. -/ structure
PComp: Type
PComp
:
Type: Type 1
Type
where /-- The comparison `Σ cᵢ*xᵢ R 0`. -/
c: PComp → Comp
c
:
Comp: Type
Comp
/-- We track how the comparison was constructed by adding and scaling previous comparisons, back to the original assumptions. -/
src: PComp → CompSource
src
:
CompSource: Type
CompSource
/-- The set of original assumptions which have been used in constructing this comparison. -/
history: PComp → RBSet ℕ compare
history
:
RBSet: (α : Type ?u.4133) → (α → α → Ordering) → Type ?u.4133
RBSet
ℕ: Type
ℕ
Ord.compare: {α : Type ?u.4134} → [self : Ord α] → α → α → Ordering
Ord.compare
/-- The variables which have been *effectively eliminated*, i.e. the by running the elimination algorithm on that variable. -/
effective: PComp → RBSet ℕ compare
effective
:
RBSet: (α : Type ?u.4169) → (α → α → Ordering) → Type ?u.4169
RBSet
ℕ: Type
ℕ
Ord.compare: {α : Type ?u.4170} → [self : Ord α] → α → α → Ordering
Ord.compare
/-- The variables which have been *implicitly eliminated*. These are variables that appear in the historical set, do not appear in `c` itself, and are not in `effective.-/
implicit: PComp → RBSet ℕ compare
implicit
:
RBSet: (α : Type ?u.4193) → (α → α → Ordering) → Type ?u.4193
RBSet
ℕ: Type
ℕ
Ord.compare: {α : Type ?u.4194} → [self : Ord α] → α → α → Ordering
Ord.compare
/-- The union of all variables appearing in those original assumptions which appear in the `history` set. -/
vars: PComp → RBSet ℕ compare
vars
:
RBSet: (α : Type ?u.4217) → (α → α → Ordering) → Type ?u.4217
RBSet
ℕ: Type
ℕ
Ord.compare: {α : Type ?u.4218} → [self : Ord α] → α → α → Ordering
Ord.compare
/-- Any comparison whose history is not minimal is redundant, and need not be included in the new set of comparisons. `elimedGE : ℕ` is a natural number such that all variables with index ≥ `elimedGE` have been removed from the system. This test is an overapproximation to minimality. It gives necessary but not sufficient conditions. If the history of `c` is minimal, then `c.maybeMinimal` is true, but `c.maybeMinimal` may also be true for some `c` with non-minimal history. Thus, if `c.maybeMinimal` is false, `c` is known not to be minimal and must be redundant. See https://doi.org/10.1016/B978-0-444-88771-9.50019-2 (Theorem 13). The condition described there considers only implicitly eliminated variables that have been officially eliminated from the system. This is not the case for every implicitly eliminated variable. Consider eliminating `z` from `{x + y + z < 0, x - y - z < 0}`. The result is the set `{2*x < 0}`; `y` is implicitly but not officially eliminated. This implementation of Fourier-Motzkin elimination processes variables in decreasing order of indices. Immediately after a step that eliminates variable `k`, variable `k'` has been eliminated iff `k' ≥ k`. Thus we can compute the intersection of officially and implicitly eliminated variables by taking the set of implicitly eliminated variables with indices ≥ `elimedGE`. -/ def
PComp.maybeMinimal: PComp → ℕ → Bool
PComp.maybeMinimal
(c :
PComp: Type
PComp
) (
elimedGE: ℕ
elimedGE
:
ℕ: Type
ℕ
) :
Bool: Type
Bool
:= c.
history: PComp → RBSet ℕ compare
history
.
size: {α : Type ?u.5062} → {cmp : α → α → Ordering} → RBSet α cmp → ℕ
size
≤
1: ?m.5078
1
+ ((c.
implicit: PComp → RBSet ℕ compare
implicit
.
filter: {α : Type ?u.5088} → {cmp : α → α → Ordering} → RBSet α cmp → (α → Bool) → RBSet α cmp
filter
(· ≥
elimedGE: ℕ
elimedGE
)).
union: {α : Type ?u.5142} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
union
c.
effective: PComp → RBSet ℕ compare
effective
).
size: {α : Type ?u.5151} → {cmp : α → α → Ordering} → RBSet α cmp → ℕ
size
/-- The `src : CompSource` field is ignored when comparing `PComp`s. Two `PComp`s proving the same comparison, with different sources, are considered equivalent. -/ def
PComp.cmp: PComp → PComp → Ordering
PComp.cmp
(
p1: PComp
p1
p2: PComp
p2
:
PComp: Type
PComp
) :
Ordering: Type
Ordering
:=
p1: PComp
p1
.
c: PComp → Comp
c
.
cmp: Comp → Comp → Ordering
cmp
p2: PComp
p2
.
c: PComp → Comp
c
/-- `PComp.scale c n` scales the coefficients of `c` by `n` and notes this in the `CompSource`. -/ def
PComp.scale: PComp → ℕ → PComp
PComp.scale
(c :
PComp: Type
PComp
) (n :
ℕ: Type
ℕ
) :
PComp: Type
PComp
:= { c with c := c.
c: PComp → Comp
c
.
scale: Comp → ℕ → Comp
scale
n, src := c.
src: PComp → CompSource
src
.
scale: ℕ → CompSource → CompSource
scale
n } /-- `PComp.add c1 c2 elimVar` creates the result of summing the linear comparisons `c1` and `c2`, during the process of eliminating the variable `elimVar`. The computation assumes, but does not enforce, that `elimVar` appears in both `c1` and `c2` and does not appear in the sum. Computing the sum of the two comparisons is easy; the complicated details lie in tracking the additional fields of `PComp`. * The historical set `pcomp.history` of `c1 + c2` is the union of the two historical sets. * `vars` is the union of `c1.vars` and `c2.vars`. * The effectively eliminated variables of `c1 + c2` are the union of the two effective sets, with `elim_var` inserted. * The implicitly eliminated variables of `c1 + c2` are those that appear in `vars` but not `c.vars` or `effective`. (Note that the description of the implicitly eliminated variables of `c1 + c2` in the algorithm described in Section 6 of https://doi.org/10.1016/B978-0-444-88771-9.50019-2 seems to be wrong: that says it should be `(c1.implicit.union c2.implicit).sdiff explicit`. Since the implicitly eliminated sets start off empty for the assumption, this formula would leave them always empty.) -/ def
PComp.add: PComp → PComp → ℕ → PComp
PComp.add
(
c1: PComp
c1
c2: PComp
c2
:
PComp: Type
PComp
) (
elimVar: ℕ
elimVar
:
ℕ: Type
ℕ
) :
PComp: Type
PComp
:= let
c: ?m.5617
c
:=
c1: PComp
c1
.
c: PComp → Comp
c
.
add: Comp → Comp → Comp
add
c2: PComp
c2
.
c: PComp → Comp
c
let
src: ?m.5622
src
:=
c1: PComp
c1
.
src: PComp → CompSource
src
.
add: CompSource → CompSource → CompSource
add
c2: PComp
c2
.
src: PComp → CompSource
src
let
history: ?m.5627
history
:=
c1: PComp
c1
.
history: PComp → RBSet ℕ compare
history
.
union: {α : Type ?u.5628} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
union
c2: PComp
c2
.
history: PComp → RBSet ℕ compare
history
let
vars: ?m.5643
vars
:=
c1: PComp
c1
.
vars: PComp → RBSet ℕ compare
vars
.
union: {α : Type ?u.5644} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
union
c2: PComp
c2
.
vars: PComp → RBSet ℕ compare
vars
let
effective: ?m.5655
effective
:= (
c1: PComp
c1
.
effective: PComp → RBSet ℕ compare
effective
.
union: {α : Type ?u.5656} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
union
c2: PComp
c2
.
effective: PComp → RBSet ℕ compare
effective
).
insert: {α : Type ?u.5665} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert
elimVar: ℕ
elimVar
let
implicit: ?m.5676
implicit
:= (
vars: ?m.5643
vars
.
sdiff: {α : Type ?u.5677} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
sdiff
(
.ofList: {α : Type ?u.5686} → List α → (cmp : α → α → Ordering) → RBSet α cmp
.ofList
c: ?m.5617
c
.
vars: Comp → List ℕ
vars
_: ?m.5687 → ?m.5687 → Ordering
_
)).
sdiff: {α : Type ?u.5694} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
sdiff
effective: ?m.5655
effective
⟨
c: ?m.5617
c
,
src: ?m.5622
src
,
history: ?m.5627
history
,
effective: ?m.5655
effective
,
implicit: ?m.5676
implicit
,
vars: ?m.5643
vars
⟩ /-- `PComp.assump c n` creates a `PComp` whose comparison is `c` and whose source is `CompSource.assump n`, that is, `c` is derived from the `n`th hypothesis. The history is the singleton set `{n}`. No variables have been eliminated (effectively or implicitly). -/ def
PComp.assump: Comp → ℕ → PComp
PComp.assump
(
c: Comp
c
:
Comp: Type
Comp
) (n :
ℕ: Type
ℕ
) :
PComp: Type
PComp
where c :=
c: Comp
c
src :=
CompSource.assump: ℕ → CompSource
CompSource.assump
n history :=
RBSet.empty: {α : Type ?u.6357} → {cmp : α → α → Ordering} → RBSet α cmp
RBSet.empty
.
insert: {α : Type ?u.6360} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert
n effective :=
.empty: {α : Type ?u.6379} → {cmp : α → α → Ordering} → RBSet α cmp
.empty
implicit :=
.empty: {α : Type ?u.6384} → {cmp : α → α → Ordering} → RBSet α cmp
.empty
vars :=
.ofList: {α : Type ?u.6389} → List α → (cmp : α → α → Ordering) → RBSet α cmp
.ofList
c: Comp
c
.
vars: Comp → List ℕ
vars
_: ?m.6390 → ?m.6390 → Ordering
_
instance: ToFormat PComp
instance
:
ToFormat: Type ?u.6499 → Type ?u.6499
ToFormat
PComp: Type
PComp
:= ⟨fun
p: ?m.6507
p
=>
format: {α : Type ?u.6515} → [self : ToFormat α] → α → Format
format
p: ?m.6507
p
.
c: PComp → Comp
c
.
coeffs: Comp → Linexp
coeffs
++
toString: {α : Type ?u.6542} → [self : ToString α] → α → String
toString
p: ?m.6507
p
.
c: PComp → Comp
c
.
str: Comp → Ineq
str
++
"0": String
"0"
⟩
instance: ToString PComp
instance
:
ToString: Type ?u.7044 → Type ?u.7044
ToString
PComp: Type
PComp
:= ⟨fun
p: ?m.7052
p
=>
toString: {α : Type ?u.7060} → [self : ToString α] → α → String
toString
p: ?m.7052
p
.
c: PComp → Comp
c
.
coeffs: Comp → Linexp
coeffs
++
toString: {α : Type ?u.7077} → [self : ToString α] → α → String
toString
p: ?m.7052
p
.
c: PComp → Comp
c
.
str: Comp → Ineq
str
++
"0": String
"0"
⟩ /-- A collection of comparisons. -/ abbrev
PCompSet: Type
PCompSet
:=
RBSet: (α : Type ?u.7298) → (α → α → Ordering) → Type ?u.7298
RBSet
PComp: Type
PComp
PComp.cmp: PComp → PComp → Ordering
PComp.cmp
/-! ### Elimination procedure -/ /-- If `c1` and `c2` both contain variable `a` with opposite coefficients, produces `v1` and `v2` such that `a` has been cancelled in `v1*c1 + v2*c2`. -/ def
elimVar: Comp → Comp → ℕ → Option (ℕ × ℕ)
elimVar
(
c1: Comp
c1
c2: Comp
c2
:
Comp: Type
Comp
) (a :
ℕ: Type
ℕ
) :
Option: Type ?u.7308 → Type ?u.7308
Option
(
ℕ: Type
ℕ
×
ℕ: Type
ℕ
) := let
v1: ?m.7316
v1
:=
c1: Comp
c1
.
coeffOf: Comp → ℕ → ℤ
coeffOf
a let
v2: ?m.7321
v2
:=
c2: Comp
c2
.
coeffOf: Comp → ℕ → ℤ
coeffOf
a if
v1: ?m.7316
v1
*
v2: ?m.7321
v2
<
0: ?m.7330
0
then let
vlcm: ?m.7419
vlcm
:=
Nat.lcm: ℕ → ℕ → ℕ
Nat.lcm
v1: ?m.7316
v1
.
natAbs: ℤ → ℕ
natAbs
v2: ?m.7321
v2
.
natAbs: ℤ → ℕ
natAbs
some: {α : Type ?u.7423} → α → Option α
some
⟨
vlcm: ?m.7419
vlcm
/
v1: ?m.7316
v1
.
natAbs: ℤ → ℕ
natAbs
,
vlcm: ?m.7419
vlcm
/
v2: ?m.7321
v2
.
natAbs: ℤ → ℕ
natAbs
⟩ else
none: {α : Type ?u.7524} → Option α
none
/-- `pelimVar p1 p2` calls `elimVar` on the `Comp` components of `p1` and `p2`. If this returns `v1` and `v2`, it creates a new `PComp` equal to `v1*p1 + v2*p2`, and tracks this in the `CompSource`. -/ def
pelimVar: PComp → PComp → ℕ → Option PComp
pelimVar
(
p1: PComp
p1
p2: PComp
p2
:
PComp: Type
PComp
) (a :
ℕ: Type
ℕ
) :
Option: Type ?u.7704 → Type ?u.7704
Option
PComp: Type
PComp
:= do let (
n1: ℕ
n1
,
n2: ℕ
n2
) ←
elimVar: Comp → Comp → ℕ → Option (ℕ × ℕ)
elimVar
p1: PComp
p1
.
c: PComp → Comp
c
p2: PComp
p2
.
c: PComp → Comp
c
a return (
p1: PComp
p1
.
scale: PComp → ℕ → PComp
scale
n1: ℕ
n1
).
add: PComp → PComp → ℕ → PComp
add
(
p2: PComp
p2
.
scale: PComp → ℕ → PComp
scale
n2: ℕ
n2
) a /-- A `PComp` represents a contradiction if its `Comp` field represents a contradiction. -/ def
PComp.isContr: PComp → Bool
PComp.isContr
(p :
PComp: Type
PComp
) :
Bool: Type
Bool
:= p.
c: PComp → Comp
c
.
isContr: Comp → Bool
isContr
/-- `elimWithSet a p comps` collects the result of calling `pelimVar p p' a` for every `p' ∈ comps`. -/ def
elimWithSet: ℕ → PComp → PCompSet → PCompSet
elimWithSet
(a :
ℕ: Type
ℕ
) (p :
PComp: Type
PComp
) (
comps: PCompSet
comps
:
PCompSet: Type
PCompSet
) :
PCompSet: Type
PCompSet
:=
comps: PCompSet
comps
.
foldl: {σ : Sort ?u.8258} → {α : Type ?u.8257} → {cmp : α → α → Ordering} → (σ → α → σ) → σ → RBSet α cmp → σ
foldl
(fun
s: ?m.8269
s
pc: ?m.8272
pc
=> match
pelimVar: PComp → PComp → ℕ → Option PComp
pelimVar
p
pc: ?m.8272
pc
a with |
some: {α : Type ?u.8275} → α → Option α
some
pc: PComp
pc
=> if
pc: PComp
pc
.
maybeMinimal: PComp → ℕ → Bool
maybeMinimal
a then
s: ?m.8269
s
.
insert: {α : Type ?u.8384} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert
pc: PComp
pc
else
s: ?m.8269
s
|
none: {α : Type ?u.8398} → Option α
none
=>
s: ?m.8269
s
)
RBSet.empty: {α : Type ?u.8471} → {cmp : α → α → Ordering} → RBSet α cmp
RBSet.empty
/-- The state for the elimination monad. * `maxVar`: the largest variable index that has not been eliminated. * `comps`: a set of comparisons The elimination procedure proceeds by eliminating variable `v` from `comps` progressively in decreasing order. -/ structure
LinarithData: Type
LinarithData
:
Type: Type 1
Type
where /-- The largest variable index that has not been (officially) eliminated. -/
maxVar: LinarithData → ℕ
maxVar
:
ℕ: Type
ℕ
/-- The set of comparisions. -/
comps: LinarithData → PCompSet
comps
:
PCompSet: Type
PCompSet
/-- The linarith monad extends an exceptional monad with a `LinarithData` state. An exception produces a contradictory `PComp`. -/ @[reducible] def
LinarithM: Type → Type
LinarithM
:
Type: Type 1
Type
→
Type: Type 1
Type
:=
StateT: Type ?u.10445 → (Type ?u.10445 → Type ?u.10444) → Type ?u.10445 → Type (max?u.10445?u.10444)
StateT
LinarithData: Type
LinarithData
(
ExceptT: Type ?u.10449 → (Type ?u.10449 → Type ?u.10448) → Type ?u.10449 → Type ?u.10448
ExceptT
PComp: Type
PComp
Id: Type ?u.10452 → Type ?u.10452
Id
) /-- Returns the current max variable. -/ def
getMaxVar: LinarithM ℕ
getMaxVar
:
LinarithM: Type → Type
LinarithM
ℕ: Type
ℕ
:=
LinarithData.maxVar: LinarithData → ℕ
LinarithData.maxVar
<$>
get: {σ : outParam (Type ?u.10485)} → {m : Type ?u.10485 → Type ?u.10484} → [self : MonadState σ m] → m σ
get
/-- Return the current comparison set. -/ def
getPCompSet: LinarithM PCompSet
getPCompSet
:
LinarithM: Type → Type
LinarithM
PCompSet: Type
PCompSet
:=
LinarithData.comps: LinarithData → PCompSet
LinarithData.comps
<$>
get: {σ : outParam (Type ?u.11133)} → {m : Type ?u.11133 → Type ?u.11132} → [self : MonadState σ m] → m σ
get
/-- Throws an exception if a contradictory `PComp` is contained in the current state. -/ def
validate: LinarithM Unit
validate
:
LinarithM: Type → Type
LinarithM
Unit: Type
Unit
:= do match
(← getPCompSet): ?m.11868
(←
getPCompSet: LinarithM PCompSet
getPCompSet
(← getPCompSet): ?m.11868
)
.
toList: {α : Type ?u.11870} → {cmp : α → α → Ordering} → RBSet α cmp → List α
toList
.
find?: {α : Type ?u.11879} → (α → Bool) → List α → Option α
find?
(fun p :
PComp: Type
PComp
=> p.
isContr: PComp → Bool
isContr
) with |
none: {α : Type ?u.11892} → Option α
none
=> return
(): Unit
()
|
some: {α : Type ?u.11820} → α → Option α
some
c =>
throw: {ε : outParam (Type ?u.11991)} → {m : Type ?u.11990 → Type ?u.11989} → [self : MonadExcept ε m] → {α : Type ?u.11990} → ε → m α
throw
c /-- Updates the current state with a new max variable and comparisons, and calls `validate` to check for a contradiction. -/ def
update: ℕ → PCompSet → LinarithM Unit
update
(
maxVar: ℕ
maxVar
:
ℕ: Type
ℕ
) (
comps: PCompSet
comps
:
PCompSet: Type
PCompSet
) :
LinarithM: Type → Type
LinarithM
Unit: Type
Unit
:= do
StateT.set: {σ : Type ?u.13123} → {m : Type ?u.13123 → Type ?u.13122} → [inst : Monad m] → σ → StateT σ m PUnit
StateT.set
⟨
maxVar: ℕ
maxVar
,
comps: PCompSet
comps
⟩
validate: LinarithM Unit
validate
/-- `splitSetByVarSign a comps` partitions the set `comps` into three parts. * `pos` contains the elements of `comps` in which `a` has a positive coefficient. * `neg` contains the elements of `comps` in which `a` has a negative coefficient. * `notPresent` contains the elements of `comps` in which `a` has coefficient 0. Returns `(pos, neg, notPresent)`. -/ def
splitSetByVarSign: ℕ → PCompSet → PCompSet × PCompSet × PCompSet
splitSetByVarSign
(a :
ℕ: Type
ℕ
) (
comps: PCompSet
comps
:
PCompSet: Type
PCompSet
) :
PCompSet: Type
PCompSet
×
PCompSet: Type
PCompSet
×
PCompSet: Type
PCompSet
:=
comps: PCompSet
comps
.
foldl: {σ : Sort ?u.13483} → {α : Type ?u.13482} → {cmp : α → α → Ordering} → (σ → α → σ) → σ → RBSet α cmp → σ
foldl
(fun ⟨pos, neg,
notPresent: PCompSet
notPresent
⟩
pc: ?m.13497
pc
=> let
n: ?m.13537
n
:=
pc: ?m.13497
pc
.
c: PComp → Comp
c
.
coeffOf: Comp → ℕ → ℤ
coeffOf
a if
n: ?m.13537
n
>
0: ?m.13542
0
then ⟨pos.
insert: {α : Type ?u.13621} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert
pc: ?m.13497
pc
, neg,
notPresent: PCompSet
notPresent
⟩ else if
n: ?m.13537
n
<
0: ?m.13644
0
then ⟨pos, neg.
insert: {α : Type ?u.13730} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert
pc: ?m.13497
pc
,
notPresent: PCompSet
notPresent
⟩ else ⟨pos, neg,
notPresent: PCompSet
notPresent
.
insert: {α : Type ?u.13755} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert
pc: ?m.13497
pc
⟩) ⟨
RBSet.empty: {α : Type ?u.13999} → {cmp : α → α → Ordering} → RBSet α cmp
RBSet.empty
,
RBSet.empty: {α : Type ?u.14016} → {cmp : α → α → Ordering} → RBSet α cmp
RBSet.empty
,
RBSet.empty: {α : Type ?u.14021} → {cmp : α → α → Ordering} → RBSet α cmp
RBSet.empty
⟩ /-- `elimVarM a` performs one round of Fourier-Motzkin elimination, eliminating the variable `a` from the `linarith` state. -/ def
elimVarM: ℕ → LinarithM Unit
elimVarM
(a :
ℕ: Type
ℕ
) :
LinarithM: Type → Type
LinarithM
Unit: Type
Unit
:= do let
vs: ?m.15604
vs
←
getMaxVar: LinarithM ℕ
getMaxVar
if (a ≤
vs: ?m.15604
vs
) then (do let ⟨pos, neg,
notPresent: PCompSet
notPresent
⟩ :=
splitSetByVarSign: ℕ → PCompSet → PCompSet × PCompSet × PCompSet
splitSetByVarSign
a
(← getPCompSet): ?m.15676
(←
getPCompSet: LinarithM PCompSet
getPCompSet
(← getPCompSet): ?m.15676
)
update: ℕ → PCompSet → LinarithM Unit
update
(
vs: ?m.15604
vs
-
1: ?m.15721
1
) (pos.
foldl: {σ : Sort ?u.15776} → {α : Type ?u.15775} → {cmp : α → α → Ordering} → (σ → α → σ) → σ → RBSet α cmp → σ
foldl
(fun
s: ?m.15787
s
p: ?m.15790
p
=>
s: ?m.15787
s
.
union: {α : Type ?u.15792} → {cmp : α → α → Ordering} → RBSet α cmp → RBSet α cmp → RBSet α cmp
union
(
elimWithSet: ℕ → PComp → PCompSet → PCompSet
elimWithSet
a
p: ?m.15790
p
neg))
notPresent: PCompSet
notPresent
)) else
pure: {f : Type ?u.15910 → Type ?u.15909} → [self : Pure f] → {α : Type ?u.15910} → α → f α
pure
(): Unit
()
/-- `elimAllVarsM` eliminates all variables from the linarith state, leaving it with a set of ground comparisons. If this succeeds without exception, the original `linarith` state is consistent. -/ def
elimAllVarsM: LinarithM Unit
elimAllVarsM
:
LinarithM: Type → Type
LinarithM
Unit: Type
Unit
:= do for
i: ?m.17475
i
in (
List.range: ℕ → List ℕ
List.range
((←
getMaxVar: LinarithM ℕ
getMaxVar
) +
1: ?m.17353
1
)).
reverse: {α : Type ?u.17405} → List α → List α
reverse
do
elimVarM: ℕ → LinarithM Unit
elimVarM
i: ?m.17475
i
/-- `mkLinarithData hyps vars` takes a list of hypotheses and the largest variable present in those hypotheses. It produces an initial state for the elimination monad. -/ def
mkLinarithData: List Comp → ℕ → LinarithData
mkLinarithData
(
hyps: List Comp
hyps
:
List: Type ?u.19152 → Type ?u.19152
List
Comp: Type
Comp
) (
maxVar: ℕ
maxVar
:
ℕ: Type
ℕ
) :
LinarithData: Type
LinarithData
:= ⟨
maxVar: ℕ
maxVar
,
.ofList: {α : Type ?u.19162} → List α → (cmp : α → α → Ordering) → RBSet α cmp
.ofList
(
hyps: List Comp
hyps
.
enum: {α : Type ?u.19164} → List α → List (ℕ × α)
enum
.
map: {α : Type ?u.19168} → {β : Type ?u.19167} → (α → β) → List α → List β
map
$ fun ⟨n,
cmp: Comp
cmp
⟩ =>
PComp.assump: Comp → ℕ → PComp
PComp.assump
cmp: Comp
cmp
n)
_: ?m.19163 → ?m.19163 → Ordering
_
⟩ /-- `produceCertificate hyps vars` tries to derive a contradiction from the comparisons in `hyps` by eliminating all variables ≤ `maxVar`. If successful, it returns a map `coeff : ℕ → ℕ` as a certificate. This map represents that we can find a contradiction by taking the sum `∑ (coeff i) * hyps[i]`. -/ def
FourierMotzkin.produceCertificate: CertificateOracle
FourierMotzkin.produceCertificate
:
CertificateOracle: Type
CertificateOracle
:= fun
hyps: ?m.19652
hyps
maxVar: ?m.19655
maxVar
=> match
ExceptT.run: {ε : Type ?u.19658} → {m : Type ?u.19658 → Type ?u.19657} → {α : Type ?u.19658} → ExceptT ε m α → m (Except ε α)
ExceptT.run
(
StateT.run: {σ : Type ?u.19663} → {m : Type ?u.19663 → Type ?u.19662} → {α : Type ?u.19663} → StateT σ m α → σ → m (α × σ)
StateT.run
(do
validate: LinarithM Unit
validate
;
elimAllVarsM: LinarithM Unit
elimAllVarsM
:
LinarithM: Type → Type
LinarithM
Unit: Type
Unit
) (
mkLinarithData: List Comp → ℕ → LinarithData
mkLinarithData
hyps: ?m.19652
hyps
maxVar: ?m.19655
maxVar
)) with | (
Except.ok: {ε : Type ?u.19774} → {α : Type ?u.19773} → α → Except ε α
Except.ok
_) =>
failure: {f : Type ?u.19795 → Type ?u.19794} → [self : Alternative f] → {α : Type ?u.19795} → f α
failure
| (
Except.error: {ε : Type ?u.19817} → {α : Type ?u.19816} → ε → Except ε α
Except.error
contr: PComp
contr
) => return
contr: PComp
contr
.
src: PComp → CompSource
src
.flatten end Linarith