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.
```/-
Authors: Robert Y. Lewis
Ported by: Scott Morrison
-/

import Mathlib.Tactic.Linarith.Elimination
import Mathlib.Tactic.Linarith.Parsing
import Mathlib.Util.Qq

/-!
# Deriving a proof of false

`linarith` uses an untrusted oracle to produce a certificate of unsatisfiability.
It needs to do some proof reconstruction work to turn this into a proof term.
This file implements the reconstruction.

## Main declarations

The public facing declaration in this file is `proveFalseByLinarith`.
-/

open Lean Elab Tactic Meta

namespace Qq

/-- Typesafe conversion of `n : ℕ` to `Q(\$α)`. -/
def ofNatQ: {u : Level} →
(α :
let u := u;
Q(Type u)) →
Q(Semiring «\$α») → ℕ → Q(«\$α»)ofNatQ (α: let u := u;
Q(Type u)α : Q(Type \$u: ?m.4u)) (_: Q(Semiring «\$α»)_ : Q(Semiring: Type ?u.17 → Type ?u.17SemiringSemiring \$α: ?m.4 \$α: Type uα)) (n: ℕn : ℕ: Typeℕ) : Q(\$α: Type uα) :=
match n: ℕn with
| 0: ℕ0 => q(0: ?m.600 : \$α: Type uα)
| 1: ℕ1 => q(1: ?m.2461 : \$α: Type uα)
| k: ℕk+2 =>
have lit: Q(ℕ)lit : Q(ℕ: Typeℕ) := mkRawNatLit: ℕ → ExprmkRawNatLit n: ℕn
let k: Q(ℕ)k : Q(ℕ: Typeℕ) := mkRawNatLit: ℕ → ExprmkRawNatLit k: ℕk
let _x: Q(Nat.AtLeastTwo «\$lit»)_x : Q(Nat.AtLeastTwo: ℕ → PropNat.AtLeastTwo \$lit: ℕlit) :=
q(OfNat.ofNat: {α : Type ?u.381} → (x : ℕ) → [self : OfNat α x] → αOfNat.ofNatOfNat.ofNat \$lit: Level \$lit: ℕlit)

end Qq

namespace Linarith

open Ineq
open Qq

/-! ### Auxiliary functions for assembling proofs -/

/-- A typesafe version of `mulExpr`. -/
def mulExpr': {u : Level} →
ℕ →
{α :
let u := u;
Q(Type u)} →
Q(Semiring «\$α») → Q(«\$α») → Q(«\$α»)mulExpr' (n: ℕn : ℕ: Typeℕ) {α: let u := u;
Q(Type u)α : Q(Type \$u: ?m.927u)} (inst: Q(Semiring «\$α»)inst : Q(Semiring: Type ?u.943 → Type ?u.943SemiringSemiring \$α: ?m.927 \$α: Type uα)) (e: Q(«\$α»)e : Q(\$α: Type uα)) : Q(\$α: Type uα) :=
if n: ℕn = 1: ?m.9671 then e: Q(«\$α»)e else
let n: ?m.1006n := ofNatQ: {u : Level} →
(α :
let u := u;
Q(Type u)) →
Q(Semiring «\$α») → ℕ → Q(«\$α»)ofNatQ α: let u := u;
Q(Type u)α inst: Q(Semiring «\$α»)inst n: ℕn
q(\$n: «\$α»nn * \$e: Level * \$e: «\$α»e)

/--
`mulExpr n e` creates an `Expr` representing `n*e`.
When elaborated, the coefficient will be a native numeral of the same type as `e`.
-/
def mulExpr: ℕ → Expr → MetaM ExprmulExpr (n: ℕn : ℕ: Typeℕ) (e: Expre : Expr: TypeExpr) : MetaM: Type → TypeMetaM Expr: TypeExpr := do
let ⟨_: Level_, α: let u := fst✝;
Q(Type fst✝)α, e: Q(«\$α»)e⟩ ← inferTypeQ': Expr →
MetaM
((u : Level) ×
(α :
let u := u;
Q(Type u)) ×
Q(«\$α»))inferTypeQ' e: Expre
let inst: Q(Semiring «\$α»)inst : Q(Semiring: Type ?u.1611 → Type ?u.1611SemiringSemiring \$α: Level \$α: Type fst✝α) ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ q(Semiring: Type ?u.1628 → Type ?u.1628SemiringSemiring \$α: Level \$α: Type fst✝α)
return mulExpr': {u : Level} →
ℕ →
{α :
let u := u;
Q(Type u)} →
Q(Semiring «\$α») → Q(«\$α») → Q(«\$α»)mulExpr' n: ℕn inst: Q(Semiring «\$α»)inst e: Q(«\$α»)e

/-- A type-safe analogue of `addExprs`. -/
def addExprs': {u : Level} →
{α :
let u := u;
Q(Type u)} →
Q(AddMonoid «\$α») → List Q(«\$α») → Q(«\$α»)addExprs' {α: let u := u;
Q(Type u)α : Q(Type \$u: ?m.2441u)} (_inst: Q(AddMonoid «\$α»)_inst : Q(AddMonoid: Type ?u.2454 → Type ?u.2454AddMonoidAddMonoid \$α: ?m.2441 \$α: Type uα)) : List: Type ?u.2458 → Type ?u.2458List Q(\$α: Type uα) → Q(\$α: Type uα)
| []   => q(0: Level0)
| h: Q(«\$α»)h::t: List Q(«\$α»)t => go: Q(«\$α») → List Q(«\$α») → Q(«\$α»)go h: Q(«\$α»)h t: List Q(«\$α»)t
where
/-- Inner loop for `addExprs'`. -/
go: Q(«\$α») → List Q(«\$α») → Q(«\$α»)go (p: Q(«\$α»)p : Q(\$α: Type uα)) : List: Type ?u.2490 → Type ?u.2490List Q(\$α: Type uα) → Q(\$α: Type uα)
| [] => p: Q(«\$α»)p
| [q: Q(«\$α»)q] => q(\$p: «\$α»pp + \$q: Level + \$q: «\$α»q)
| q: Q(«\$α»)q::t: List Q(«\$α»)t => go: Q(«\$α») → List Q(«\$α») → Q(«\$α»)go q(\$p: «\$α»pp + \$q: Level + \$q: «\$α»q) t: List Q(«\$α»)t

/-- `addExprs L` creates an `Expr` representing the sum of the elements of `L`, associated left. -/
def addExprs: List Expr → MetaM ExpraddExprs : List: Type ?u.4712 → Type ?u.4712List Expr: TypeExpr → MetaM: Type → TypeMetaM Expr: TypeExpr
| [] => return q(0: ?m.47820) -- This may not be of the intended type; use with caution.
| L: List ExprL@(h: Exprh::_) => do
let ⟨_: Level_, α: let u := fst✝;
Q(Type fst✝)α, _⟩ ← inferTypeQ': Expr →
MetaM
((u : Level) ×
(α :
let u := u;
Q(Type u)) ×
Q(«\$α»))inferTypeQ' h: Exprh
let inst: Q(AddMonoid «\$α»)inst : Q(AddMonoid: Type ?u.5090 → Type ?u.5090AddMonoidAddMonoid \$α: Level \$α: Type fst✝α) ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ q(AddMonoid: Type ?u.5106 → Type ?u.5106AddMonoidAddMonoid \$α: Level \$α: Type fst✝α)
-- This is not type safe; we just assume all the `Expr`s in the tail have the same type:
return addExprs': {u : Level} →
{α :
let u := u;
Q(Type u)} →

/--
If our goal is to add together two inequalities `t1 R1 0` and `t2 R2 0`,
`addIneq R1 R2` produces the strength of the inequality in the sum `R`,
along with the name of a lemma to apply in order to conclude `t1 + t2 R 0`.
-/
def addIneq: Ineq → Ineq → Name × IneqaddIneq : Ineq: TypeIneq → Ineq: TypeIneq → (Name: TypeName × Ineq: TypeIneq)
| eq: Ineqeq, eq: Ineqeq => (``Linarith.eq_of_eq_of_eq: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a = 0 → b = 0 → a + b = 0Linarith.eq_of_eq_of_eq, eq: Ineqeq)
| eq: Ineqeq, le: Ineqle => (``Linarith.le_of_eq_of_le: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a = 0 → b ≤ 0 → a + b ≤ 0Linarith.le_of_eq_of_le, le: Ineqle)
| eq: Ineqeq, lt: Ineqlt => (``Linarith.lt_of_eq_of_lt: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a = 0 → b < 0 → a + b < 0Linarith.lt_of_eq_of_lt, lt: Ineqlt)
| le: Ineqle, eq: Ineqeq => (``Linarith.le_of_le_of_eq: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a ≤ 0 → b = 0 → a + b ≤ 0Linarith.le_of_le_of_eq, le: Ineqle)
| le: Ineqle, le: Ineqle => (``add_nonpos: ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0add_nonpos, le: Ineqle)
| le: Ineqle, lt: Ineqlt => (``add_lt_of_le_of_neg: ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, b ≤ c → a < 0 → b + a < cadd_lt_of_le_of_neg, lt: Ineqlt)
| lt: Ineqlt, eq: Ineqeq => (``Linarith.lt_of_lt_of_eq: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a < 0 → b = 0 → a + b < 0Linarith.lt_of_lt_of_eq, lt: Ineqlt)
| lt: Ineqlt, le: Ineqle => (``add_lt_of_neg_of_le: ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a < 0 → b ≤ c → a + b < cadd_lt_of_neg_of_le, lt: Ineqlt)
| lt: Ineqlt, lt: Ineqlt => (``Left.add_neg: ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a < 0 → b < 0 → a + b < 0Left.add_neg, lt: Ineqlt)

/--
`mkLTZeroProof coeffs pfs` takes a list of proofs of the form `tᵢ Rᵢ 0`,
paired with coefficients `cᵢ`.
It produces a proof that `∑cᵢ * tᵢ R 0`, where `R` is as strong as possible.
-/
def mkLTZeroProof: List (Expr × ℕ) → MetaM ExprmkLTZeroProof : List: Type ?u.6965 → Type ?u.6965List (Expr: TypeExpr × ℕ: Typeℕ) → MetaM: Type → TypeMetaM Expr: TypeExpr
| [] => throwError "no linear hypotheses found": ?m.7429 ?m.7430throwErrorthrowError "no linear hypotheses found": ?m.7429 ?m.7430 "no linear hypotheses found"
| [(h: Exprh, c: ℕc)] => do
let (_, t: Exprt) ← mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)mkSingleCompZeroOf c: ℕc h: Exprh
return t: Exprt
| ((h: Exprh, c: ℕc)::t: List (Expr × ℕ)t) => do
let (iq: Ineqiq, h': Exprh') ← mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)mkSingleCompZeroOf c: ℕc h: Exprh
let (_, t: Exprt) ← t: List (Expr × ℕ)t.foldlM: {m : Type ?u.8092 → Type ?u.8091} →
[inst : Monad m] → {s : Type ?u.8092} → {α : Type ?u.8090} → (s → α → m s) → s → List α → m sfoldlM (λ pr: ?m.8132pr ce: ?m.8135ce => step: Ineq → Expr → Expr → ℕ → MetaM (Ineq × Expr)step pr: ?m.8132pr.1: {α : Type ?u.8143} → {β : Type ?u.8142} → α × β → α1 pr: ?m.8132pr.2: {α : Type ?u.8147} → {β : Type ?u.8146} → α × β → β2 ce: ?m.8135ce.1: {α : Type ?u.8231} → {β : Type ?u.8230} → α × β → α1 ce: ?m.8135ce.2: {α : Type ?u.8235} → {β : Type ?u.8234} → α × β → β2) (iq: Ineqiq, h': Exprh')
return t: Exprt
where
/--
`step c pf npf coeff` assumes that `pf` is a proof of `t1 R1 0` and `npf` is a proof
of `t2 R2 0`. It uses `mkSingleCompZeroOf` to prove `t1 + coeff*t2 R 0`, and returns `R`
along with this proof.
-/
step: Ineq → Expr → Expr → ℕ → MetaM (Ineq × Expr)step (c: Ineqc : Ineq: TypeIneq) (pf: Exprpf npf: Exprnpf : Expr: TypeExpr) (coeff: ℕcoeff : ℕ: Typeℕ) : MetaM: Type → TypeMetaM (Ineq: TypeIneq × Expr: TypeExpr) := do
let (iq: Ineqiq, h': Exprh') ← mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)mkSingleCompZeroOf coeff: ℕcoeff npf: Exprnpf
let (nm: Namenm, niq: Ineqniq) := addIneq: Ineq → Ineq → Name × IneqaddIneq c: Ineqc iq: Ineqiq
return (niq: Ineqniq, ←mkAppM: Name → Array Expr → MetaM ExprmkAppM nm: Namenm #[pf: Exprpf, h': Exprh'])

/-- If `prf` is a proof of `t R s`, `leftOfIneqProof prf` returns `t`. -/
def leftOfIneqProof: Expr → MetaM ExprleftOfIneqProof (prf: Exprprf : Expr: TypeExpr) : MetaM: Type → TypeMetaM Expr: TypeExpr := do
let (t: Exprt, _) ← getRelSides: Expr → MetaM (Expr × Expr)getRelSides (← inferType prf): ?m.10731(← inferType: Expr → MetaM ExprinferType(← inferType prf): ?m.10731 prf: Exprprf(← inferType prf): ?m.10731)
return t: Exprt

/-- If `prf` is a proof of `t R s`, `typeOfIneqProof prf` returns the type of `t`. -/
def typeOfIneqProof: Expr → MetaM ExprtypeOfIneqProof (prf: Exprprf : Expr: TypeExpr) : MetaM: Type → TypeMetaM Expr: TypeExpr := do
inferType: Expr → MetaM ExprinferType (← leftOfIneqProof prf): ?m.11482(← leftOfIneqProof: Expr → MetaM ExprleftOfIneqProof(← leftOfIneqProof prf): ?m.11482 prf: Exprprf(← leftOfIneqProof prf): ?m.11482)

/--
`mkNegOneLtZeroProof tp` returns a proof of `-1 < 0`,
where the numerals are natively of type `tp`.
-/
def mkNegOneLtZeroProof: Expr → MetaM ExprmkNegOneLtZeroProof (tp: Exprtp : Expr: TypeExpr) : MetaM: Type → TypeMetaM Expr: TypeExpr := do
let zero_lt_one: ?m.11850zero_lt_one ← mkAppOptM: Name → Array (Option Expr) → MetaM ExprmkAppOptM ``zero_lt_one: ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1zero_lt_one #[tp: Exprtp, none: {α : Type ?u.11823} → Option αnone, none: {α : Type ?u.11828} → Option αnone, none: {α : Type ?u.11832} → Option αnone, none: {α : Type ?u.11836} → Option αnone, none: {α : Type ?u.11840} → Option αnone]
mkAppM: Name → Array Expr → MetaM ExprmkAppM `neg_neg_of_pos: Name`neg_neg_of_pos #[zero_lt_one: ?m.11850zero_lt_one]

/--
`addNegEqProofs l` inspects the list of proofs `l` for proofs of the form `t = 0`. For each such
proof, it adds a proof of `-t = 0` to the list.
-/
def addNegEqProofs: List Expr → MetaM (List Expr)addNegEqProofs : List: Type ?u.12074 → Type ?u.12074List Expr: TypeExpr → MetaM: Type → TypeMetaM (List: Type ?u.12076 → Type ?u.12076List Expr: TypeExpr)
| [] => return []: List ?m.12137[]
| (h: Exprh::tl: List Exprtl) => do
let (iq: Ineqiq, t: Exprt) ← parseCompAndExpr: Expr → MetaM (Ineq × Expr)parseCompAndExpr (← inferType h): ?m.12267(← inferType: Expr → MetaM ExprinferType(← inferType h): ?m.12267 h: Exprh(← inferType h): ?m.12267)
match iq: Ineqiq with
| Ineq.eq: IneqIneq.eq => do
let nep: ?m.12569nep := mkAppN: Expr → Array Expr → ExprmkAppN (← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]): ?m.12566(← mkAppM: Name → Array Expr → MetaM ExprmkAppM(← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]): ?m.12566 `Iff.mpr: Name`Iff.mpr(← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]): ?m.12566 #[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555#[← mkAppOptM: Name → Array (Option Expr) → MetaM ExprmkAppOptM#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555 ``neg_eq_zero: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, -a = 0 ↔ a = 0neg_eq_zero#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555 #[none: {α : Type ?u.12406} → Option αnone#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555, none: {α : Type ?u.12411} → Option αnone#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555, t: Exprt#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555]](← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]): ?m.12566) #[h: Exprh]
let tl: ?m.12630tl ← addNegEqProofs: List Expr → MetaM (List Expr)addNegEqProofs tl: List Exprtl
return h: Exprh::nep: ?m.12569nep::tl: ?m.12630tl

/--
`proveEqZeroUsing tac e` tries to use `tac` to construct a proof of `e = 0`.
-/
def proveEqZeroUsing: TacticM Unit → Expr → MetaM ExprproveEqZeroUsing (tac: TacticM Unittac : TacticM: Type → TypeTacticM Unit: TypeUnit) (e: Expre : Expr: TypeExpr) : MetaM: Type → TypeMetaM Expr: TypeExpr := do
let ⟨u: Levelu, α: let u := u;
Q(Type u)α, e: Q(«\$α»)e⟩ ← inferTypeQ': Expr →
MetaM
((u : Level) ×
(α :
let u := u;
Q(Type u)) ×
Q(«\$α»))inferTypeQ' e: Expre
let _h: Q(Zero «\$α»)_h : Q(Zero: Type ?u.14694 → Type ?u.14694ZeroZero \$α: Level \$α: Type uα) ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ q(Zero: Type ?u.14698 → Type ?u.14698ZeroZero \$α: Level \$α: Type uα)
synthesizeUsing': Expr → TacticM Unit → MetaM ExprsynthesizeUsing' q(\$e: «\$α»ee = 0: Level = 0: ?m.147130) tac: TacticM Unittac

/-! #### The main method -/

/--
`proveFalseByLinarith` is the main workhorse of `linarith`.
Given a list `l` of proofs of `tᵢ Rᵢ 0`,
it tries to derive a contradiction from `l` and use this to produce a proof of `False`.

An oracle is used to search for a certificate of unsatisfiability.
In the current implementation, this is the Fourier Motzkin elimination routine in
`Elimination.lean`, but other oracles could easily be swapped in.

The returned certificate is a map `m` from hypothesis indices to natural number coefficients.
If our set of hypotheses has the form  `{tᵢ Rᵢ 0}`,
then the elimination process should have guaranteed that
1.\ `∑ (m i)*tᵢ = 0`,
with at least one `i` such that `m i > 0` and `Rᵢ` is `<`.

We have also that
2.\ `∑ (m i)*tᵢ < 0`,
since for each `i`, `(m i)*tᵢ ≤ 0` and at least one is strictly negative.
So we conclude a contradiction `0 < 0`.

It remains to produce proofs of (1) and (2). (1) is verified by calling the `discharger` tactic
of the `LinarithConfig` object, which is typically `ring`. We prove (2) by folding over the
set of hypotheses.
-/
def proveFalseByLinarith: LinarithConfig → MVarId → List Expr → MetaM ExprproveFalseByLinarith (cfg: LinarithConfigcfg : LinarithConfig: TypeLinarithConfig) : MVarId: TypeMVarId → List: Type ?u.15554 → Type ?u.15554List Expr: TypeExpr → MetaM: Type → TypeMetaM Expr: TypeExpr
| _, [] => throwError "no args to linarith": ?m.15584 ?m.15585throwErrorthrowError "no args to linarith": ?m.15584 ?m.15585 "no args to linarith"
| g: MVarIdg, l: List Exprl@(h: Exprh::_) => do
trace[linarith.detail] "Beginning work in `proveFalseByLinarith`."
-- for the elimination to work properly, we must add a proof of `-1 < 0` to the list,
-- along with negated equality proofs.
let l': ?m.16826l' ← addNegEqProofs: List Expr → MetaM (List Expr)addNegEqProofs l: List Exprl
let inputs: ?m.17308inputs := (← mkNegOneLtZeroProof (← typeOfIneqProof h)): ?m.17305(← mkNegOneLtZeroProof: Expr → MetaM ExprmkNegOneLtZeroProof(← mkNegOneLtZeroProof (← typeOfIneqProof h)): ?m.17305 (← typeOfIneqProof h): ?m.17250(← typeOfIneqProof: Expr → MetaM ExprtypeOfIneqProof(← typeOfIneqProof h): ?m.17250 h: Exprh(← typeOfIneqProof h): ?m.17250)(← mkNegOneLtZeroProof (← typeOfIneqProof h)): ?m.17305)::l': ?m.16826l'.reverse: {α : Type ?u.17311} → List α → List αreverse
trace[linarith.detail] "... finished `mkNegOneLtZeroProof`."
trace[linarith.detail] (← inputs.mapM inferType): ?m.17944(← inputs: ?m.17308inputs(← inputs.mapM inferType): ?m.17944.mapM: {m : Type ?u.17892 → Type ?u.17891} →
[inst : Monad m] → {α : Type ?u.17890} → {β : Type ?u.17892} → (α → m β) → List α → m (List β)mapM(← inputs.mapM inferType): ?m.17944 inferType: Expr → MetaM ExprinferType(← inputs.mapM inferType): ?m.17944)
let (comps: List Compcomps, max_var: ℕmax_var) ← linearFormsAndMaxVar: TransparencyMode → List Expr → MetaM (List Comp × ℕ)linearFormsAndMaxVar cfg: LinarithConfigcfg.transparency: LinarithConfig → TransparencyModetransparency inputs: ?m.17308inputs
trace[linarith.detail] "... finished `linearFormsAndMaxVar`."
trace[linarith.detail] "{comps: List Compcomps}"
let oracle: ?m.19099oracle := cfg: LinarithConfigcfg.oracle: LinarithConfig → Option CertificateOracleoracle.getD: {α : Type ?u.19100} → Option α → α → αgetD FourierMotzkin.produceCertificate: CertificateOracleFourierMotzkin.produceCertificate
-- perform the elimination and fail if no contradiction is found.
let certificate: ?m.19129certificate : Std.HashMap Nat Nat ← try
oracle: ?m.19099oracle comps: List Compcomps max_var: ℕmax_var
catch e: ?m.19206e =>
trace[linarith] e: ?m.19206e.toMessageData: Exception → MessageDatatoMessageData
throwError "linarith failed to find a contradiction": ?m.19576 ?m.19577throwErrorthrowError "linarith failed to find a contradiction": ?m.19576 ?m.19577 "linarith failed to find a contradiction"
trace[linarith] "linarith has found a contradiction: {certificate: ?m.19129certificate.toList: {α : Type ?u.20070} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.20069} → Std.HashMap α β → List (α × β)toList}"
let enum_inputs: ?m.20263enum_inputs := inputs: ?m.17308inputs.enum: {α : Type ?u.20264} → List α → List (ℕ × α)enum
-- construct a list pairing nonzero coeffs with the proof of their corresponding comparison
let zip: ?m.20270zip := enum_inputs: ?m.20263enum_inputs.filterMap: {α : Type ?u.20272} → {β : Type ?u.20271} → (α → Option β) → List α → List βfilterMap fun ⟨n: ℕn, e: Expre⟩ => (certificate: ?m.19129certificate.find?: {α : Type ?u.20721} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.20720} → Std.HashMap α β → α → Option βfind? n: ℕn).map: {α : Type ?u.20733} → {β : Type ?u.20732} → (α → β) → Option α → Option βmap (e: Expre, ·)
let mls: ?m.20383mls ← zip: ?m.20270zip.mapM: {m : Type ?u.20330 → Type ?u.20329} →
[inst : Monad m] → {α : Type ?u.20328} → {β : Type ?u.20330} → (α → m β) → List α → m (List β)mapM fun ⟨e: Expre, n: ℕn⟩ => do mulExpr: ℕ → Expr → MetaM ExprmulExpr n: ℕn (← leftOfIneqProof e): ?m.20912(← leftOfIneqProof: Expr → MetaM ExprleftOfIneqProof(← leftOfIneqProof e): ?m.20912 e: Expre(← leftOfIneqProof e): ?m.20912)
-- `sm` is the sum of input terms, scaled to cancel out all variables.
let sm: ?m.20438sm ← addExprs: List Expr → MetaM ExpraddExprs mls: ?m.20383mls
-- let sm ← instantiateMVars sm
trace[linarith] "The expression\n  {sm: ?m.20438sm}\nshould be both 0 and negative"
-- we prove that `sm = 0`, typically with `ring`.
let sm_eq_zero: ?m.21630sm_eq_zero ← proveEqZeroUsing: TacticM Unit → Expr → MetaM ExprproveEqZeroUsing cfg: LinarithConfigcfg.discharger: LinarithConfig → TacticM Unitdischarger sm: ?m.20438sm
-- we also prove that `sm < 0`
let sm_lt_zero: ?m.21685sm_lt_zero ← mkLTZeroProof: List (Expr × ℕ) → MetaM ExprmkLTZeroProof zip: ?m.20270zip