/-
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.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.4
u)) (_: Q(Semiring «$α»)
_ : Q(Semiring: Type ?u.17 → Type ?u.17
SemiringSemiring $α: ?m.4
 $α: Type u
α)) (n: ℕ
n : ℕ: Type
ℕ) : Q($α: Type u
α) :=
  match n: ℕ
n with
  | 0: ℕ
0 => q(0: ?m.60
0 : $α: Type u
α)
  | 1: ℕ
1 => q(1: ?m.246
1 : $α: Type u
α)
  | k: ℕ
k+2 =>
    have lit: Q(ℕ)
lit : Q(ℕ: Type
ℕ) := mkRawNatLit: ℕ → Expr
mkRawNatLit n: ℕ
n
    let k: Q(ℕ)
k : Q(ℕ: Type
ℕ) := mkRawNatLit: ℕ → Expr
mkRawNatLit k: ℕ
k
    let _x: Q(Nat.AtLeastTwo «$lit»)
_x : Q(Nat.AtLeastTwo: ℕ → Prop
Nat.AtLeastTwo $lit: ℕ
lit) :=
      (q(instAtLeastTwoHAddNatInstHAddInstAddNatOfNat: ∀ {n : ℕ}, Nat.AtLeastTwo (n + 2)
instAtLeastTwoHAddNatInstHAddInstAddNatOfNat (n := $k: ℕ
k)) : Expr: Type
Expr)
    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.927
u)} (inst: Q(Semiring «$α»)
inst : Q(Semiring: Type ?u.943 → Type ?u.943
SemiringSemiring $α: ?m.927
 $α: Type u
α)) (e: Q(«$α»)
e : Q($α: Type u
α)) : Q($α: Type u
α) :=
if n: ℕ
n = 1: ?m.967
1 then e: Q(«$α»)
e else
  let n: ?m.1006
n := 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 Expr
mulExpr (n: ℕ
n : ℕ: Type
ℕ) (e: Expr
e : Expr: Type
Expr) : MetaM: Type → Type
MetaM Expr: Type
Expr := 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: Expr
e
  let inst: Q(Semiring «$α»)
inst : Q(Semiring: Type ?u.1611 → Type ?u.1611
SemiringSemiring $α: Level
 $α: Type fst✝
α) ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«$α»)
synthInstanceQ q(Semiring: Type ?u.1628 → Type ?u.1628
SemiringSemiring $α: 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.2441
u)} (_inst: Q(AddMonoid «$α»)
_inst : Q(AddMonoid: Type ?u.2454 → Type ?u.2454
AddMonoidAddMonoid $α: ?m.2441
 $α: Type u
α)) : List: Type ?u.2458 → Type ?u.2458
List Q($α: Type u
α) → Q($α: Type u
α)
| []   => q(0: Level
0)
| 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.2490
List 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 Expr
addExprs : List: Type ?u.4712 → Type ?u.4712
List Expr: Type
Expr → MetaM: Type → Type
MetaM Expr: Type
Expr
| [] => return q(0: ?m.4782
0) -- This may not be of the intended type; use with caution.
| L: List Expr
L@(h: Expr
h::_) => do
  let ⟨_: Level
_, α: let u := fst✝;
Q(Type fst✝)
α, _⟩ ← inferTypeQ': Expr →
  MetaM
    ((u : Level) ×
      (α :
        let u := u;
        Q(Type u)) ×
        Q(«$α»))
inferTypeQ' h: Expr
h
  let inst: Q(AddMonoid «$α»)
inst : Q(AddMonoid: Type ?u.5090 → Type ?u.5090
AddMonoidAddMonoid $α: Level
 $α: Type fst✝
α) ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«$α»)
synthInstanceQ q(AddMonoid: Type ?u.5106 → Type ?u.5106
AddMonoidAddMonoid $α: 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)} →
    Q(AddMonoid «$α») → List Q(«$α») → Q(«$α»)
addExprs' inst: Q(AddMonoid «$α»)
inst L: List Expr
L

/--
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 × Ineq
addIneq : Ineq: Type
Ineq → Ineq: Type
Ineq → (Name: Type
Name × Ineq: Type
Ineq)
| eq: Ineq
eq, eq: Ineq
eq => (``Linarith.eq_of_eq_of_eq: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a = 0 → b = 0 → a + b = 0
Linarith.eq_of_eq_of_eq, eq: Ineq
eq)
| eq: Ineq
eq, le: Ineq
le => (``Linarith.le_of_eq_of_le: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a = 0 → b ≤ 0 → a + b ≤ 0
Linarith.le_of_eq_of_le, le: Ineq
le)
| eq: Ineq
eq, lt: Ineq
lt => (``Linarith.lt_of_eq_of_lt: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a = 0 → b < 0 → a + b < 0
Linarith.lt_of_eq_of_lt, lt: Ineq
lt)
| le: Ineq
le, eq: Ineq
eq => (``Linarith.le_of_le_of_eq: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a ≤ 0 → b = 0 → a + b ≤ 0
Linarith.le_of_le_of_eq, le: Ineq
le)
| le: Ineq
le, le: Ineq
le => (``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 ≤ 0
add_nonpos, le: Ineq
le)
| le: Ineq
le, lt: Ineq
lt => (``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 < c
add_lt_of_le_of_neg, lt: Ineq
lt)
| lt: Ineq
lt, eq: Ineq
eq => (``Linarith.lt_of_lt_of_eq: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, a < 0 → b = 0 → a + b < 0
Linarith.lt_of_lt_of_eq, lt: Ineq
lt)
| lt: Ineq
lt, le: Ineq
le => (``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 < c
add_lt_of_neg_of_le, lt: Ineq
lt)
| lt: Ineq
lt, lt: Ineq
lt => (``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 < 0
Left.add_neg, lt: Ineq
lt)

/--
`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 Expr
mkLTZeroProof : List: Type ?u.6965 → Type ?u.6965
List (Expr: Type
Expr × ℕ: Type
ℕ) → MetaM: Type → Type
MetaM Expr: Type
Expr
| [] => throwError "no linear hypotheses found": ?m.7429 ?m.7430
throwErrorthrowError "no linear hypotheses found": ?m.7429 ?m.7430
 "no linear hypotheses found"
| [(h: Expr
h, c: ℕ
c)] => do
     let (_, t: Expr
t) ← mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)
mkSingleCompZeroOf c: ℕ
c h: Expr
h
     return t: Expr
t
| ((h: Expr
h, c: ℕ
c)::t: List (Expr × ℕ)
t) => do
     let (iq: Ineq
iq, h': Expr
h') ← mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)
mkSingleCompZeroOf c: ℕ
c h: Expr
h
     let (_, t: Expr
t) ← 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 s
foldlM (λ pr: ?m.8132
pr ce: ?m.8135
ce => step: Ineq → Expr → Expr → ℕ → MetaM (Ineq × Expr)
step pr: ?m.8132
pr.1: {α : Type ?u.8143} → {β : Type ?u.8142} → α × β → α
1 pr: ?m.8132
pr.2: {α : Type ?u.8147} → {β : Type ?u.8146} → α × β → β
2 ce: ?m.8135
ce.1: {α : Type ?u.8231} → {β : Type ?u.8230} → α × β → α
1 ce: ?m.8135
ce.2: {α : Type ?u.8235} → {β : Type ?u.8234} → α × β → β
2) (iq: Ineq
iq, h': Expr
h')
     return t: Expr
t
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: Ineq
c : Ineq: Type
Ineq) (pf: Expr
pf npf: Expr
npf : Expr: Type
Expr) (coeff: ℕ
coeff : ℕ: Type
ℕ) : MetaM: Type → Type
MetaM (Ineq: Type
Ineq × Expr: Type
Expr) := do
    let (iq: Ineq
iq, h': Expr
h') ← mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)
mkSingleCompZeroOf coeff: ℕ
coeff npf: Expr
npf
    let (nm: Name
nm, niq: Ineq
niq) := addIneq: Ineq → Ineq → Name × Ineq
addIneq c: Ineq
c iq: Ineq
iq
    return (niq: Ineq
niq, ←mkAppM: Name → Array Expr → MetaM Expr
mkAppM nm: Name
nm #[pf: Expr
pf, h': Expr
h'])

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

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

/--
`mkNegOneLtZeroProof tp` returns a proof of `-1 < 0`,
where the numerals are natively of type `tp`.
-/
def mkNegOneLtZeroProof: Expr → MetaM Expr
mkNegOneLtZeroProof (tp: Expr
tp : Expr: Type
Expr) : MetaM: Type → Type
MetaM Expr: Type
Expr := do
  let zero_lt_one: ?m.11850
zero_lt_one ← mkAppOptM: Name → Array (Option Expr) → MetaM Expr
mkAppOptM ``zero_lt_one: ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
  [inst_4 : NeZero 1], 0 < 1
zero_lt_one #[tp: Expr
tp, 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 Expr
mkAppM `neg_neg_of_pos: Name
`neg_neg_of_pos #[zero_lt_one: ?m.11850
zero_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.12074
List Expr: Type
Expr → MetaM: Type → Type
MetaM (List: Type ?u.12076 → Type ?u.12076
List Expr: Type
Expr)
| [] => return []: List ?m.12137
[]
| (h: Expr
h::tl: List Expr
tl) => do
  let (iq: Ineq
iq, t: Expr
t) ← parseCompAndExpr: Expr → MetaM (Ineq × Expr)
parseCompAndExpr (← inferType h): ?m.12267
(← inferType: Expr → MetaM Expr
inferType(← inferType h): ?m.12267
 h: Expr
h(← inferType h): ?m.12267
)
  match iq: Ineq
iq with
  | Ineq.eq: Ineq
Ineq.eq => do
    let nep: ?m.12569
nep := mkAppN: Expr → Array Expr → Expr
mkAppN (← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]): ?m.12566
(← mkAppM: Name → Array Expr → MetaM Expr
mkAppM(← 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 Expr
mkAppOptM#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555
 ``neg_eq_zero: ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, -a = 0 ↔ a = 0
neg_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: Expr
t#[← mkAppOptM ``neg_eq_zero #[none, none, t]]: Array ?m.12555
]](← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]): ?m.12566
) #[h: Expr
h]
    let tl: ?m.12630
tl ← addNegEqProofs: List Expr → MetaM (List Expr)
addNegEqProofs tl: List Expr
tl
    return h: Expr
h::nep: ?m.12569
nep::tl: ?m.12630
tl
  | _ => return h: Expr
h :: (← addNegEqProofs tl): ?m.12751
(← addNegEqProofs: List Expr → MetaM (List Expr)
addNegEqProofs(← addNegEqProofs tl): ?m.12751
 tl: List Expr
tl(← addNegEqProofs tl): ?m.12751
)

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

/-! #### 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 Expr
proveFalseByLinarith (cfg: LinarithConfig
cfg : LinarithConfig: Type
LinarithConfig) : MVarId: Type
MVarId → List: Type ?u.15554 → Type ?u.15554
List Expr: Type
Expr → MetaM: Type → Type
MetaM Expr: Type
Expr
| _, [] => throwError "no args to linarith": ?m.15584 ?m.15585
throwErrorthrowError "no args to linarith": ?m.15584 ?m.15585
 "no args to linarith"
| g: MVarId
g, l: List Expr
l@(h: Expr
h::_) => 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.16826
l' ← addNegEqProofs: List Expr → MetaM (List Expr)
addNegEqProofs l: List Expr
l
    trace[linarith.detail] "... finished `addNegEqProofs`."
    let inputs: ?m.17308
inputs := (← mkNegOneLtZeroProof (← typeOfIneqProof h)): ?m.17305
(← mkNegOneLtZeroProof: Expr → MetaM Expr
mkNegOneLtZeroProof(← mkNegOneLtZeroProof (← typeOfIneqProof h)): ?m.17305
 (← typeOfIneqProof h): ?m.17250
(← typeOfIneqProof: Expr → MetaM Expr
typeOfIneqProof(← typeOfIneqProof h): ?m.17250
 h: Expr
h(← typeOfIneqProof h): ?m.17250
)(← mkNegOneLtZeroProof (← typeOfIneqProof h)): ?m.17305
)::l': ?m.16826
l'.reverse: {α : Type ?u.17311} → List α → List α
reverse
    trace[linarith.detail] "... finished `mkNegOneLtZeroProof`."
    trace[linarith.detail] (← inputs.mapM inferType): ?m.17944
(← inputs: ?m.17308
inputs(← 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 Expr
inferType(← inputs.mapM inferType): ?m.17944
)
    let (comps: List Comp
comps, max_var: ℕ
max_var) ← linearFormsAndMaxVar: TransparencyMode → List Expr → MetaM (List Comp × ℕ)
linearFormsAndMaxVar cfg: LinarithConfig
cfg.transparency: LinarithConfig → TransparencyMode
transparency inputs: ?m.17308
inputs
    trace[linarith.detail] "... finished `linearFormsAndMaxVar`."
    trace[linarith.detail] "{comps: List Comp
comps}"
    let oracle: ?m.19099
oracle := cfg: LinarithConfig
cfg.oracle: LinarithConfig → Option CertificateOracle
oracle.getD: {α : Type ?u.19100} → Option α → α → α
getD FourierMotzkin.produceCertificate: CertificateOracle
FourierMotzkin.produceCertificate
    -- perform the elimination and fail if no contradiction is found.
    let certificate: ?m.19129
certificate : Std.HashMap Nat Nat ← try
      oracle: ?m.19099
oracle comps: List Comp
comps max_var: ℕ
max_var
    catch e: ?m.19206
e =>
      trace[linarith] e: ?m.19206
e.toMessageData: Exception → MessageData
toMessageData
      throwError "linarith failed to find a contradiction": ?m.19576 ?m.19577
throwErrorthrowError "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.19129
certificate.toList: {α : Type ?u.20070} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.20069} → Std.HashMap α β → List (α × β)
toList}"
    let enum_inputs: ?m.20263
enum_inputs := inputs: ?m.17308
inputs.enum: {α : Type ?u.20264} → List α → List (ℕ × α)
enum
    -- construct a list pairing nonzero coeffs with the proof of their corresponding comparison
    let zip: ?m.20270
zip := enum_inputs: ?m.20263
enum_inputs.filterMap: {α : Type ?u.20272} → {β : Type ?u.20271} → (α → Option β) → List α → List β
filterMap fun ⟨n: ℕ
n, e: Expr
e⟩ => (certificate: ?m.19129
certificate.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: Expr
e, ·)
    let mls: ?m.20383
mls ← zip: ?m.20270
zip.mapM: {m : Type ?u.20330 → Type ?u.20329} →
  [inst : Monad m] → {α : Type ?u.20328} → {β : Type ?u.20330} → (α → m β) → List α → m (List β)
mapM fun ⟨e: Expr
e, n: ℕ
n⟩ => do mulExpr: ℕ → Expr → MetaM Expr
mulExpr n: ℕ
n (← leftOfIneqProof e): ?m.20912
(← leftOfIneqProof: Expr → MetaM Expr
leftOfIneqProof(← leftOfIneqProof e): ?m.20912
 e: Expr
e(← leftOfIneqProof e): ?m.20912
)
    -- `sm` is the sum of input terms, scaled to cancel out all variables.
    let sm: ?m.20438
sm ← addExprs: List Expr → MetaM Expr
addExprs mls: ?m.20383
mls
    -- let sm ← instantiateMVars sm
    trace[linarith] "The expression\n  {sm: ?m.20438
sm}\nshould be both 0 and negative"
    -- we prove that `sm = 0`, typically with `ring`.
    let sm_eq_zero: ?m.21630
sm_eq_zero ← proveEqZeroUsing: TacticM Unit → Expr → MetaM Expr
proveEqZeroUsing cfg: LinarithConfig
cfg.discharger: LinarithConfig → TacticM Unit
discharger sm: ?m.20438
sm
    -- we also prove that `sm < 0`
    let sm_lt_zero: ?m.21685
sm_lt_zero ← mkLTZeroProof: List (Expr × ℕ) → MetaM Expr
mkLTZeroProof zip: ?m.20270
zip
    -- this is a contradiction.
    let pftp: ?m.21740
pftp ← inferType: Expr → MetaM Expr
inferType sm_lt_zero: ?m.21685
sm_lt_zero
    let ⟨_, nep: Expr
nep, _⟩ ← g: MVarId
g.rewrite: MVarId →
  Expr →
    Expr →
      optParam Bool false →
        optParam Occurrences Occurrences.all →
          optParam Rewrite.Config { transparency := TransparencyMode.reducible, offsetCnstrs := true } →
            MetaM RewriteResult
rewrite pftp: ?m.21740
pftp sm_eq_zero: ?m.21630
sm_eq_zero
    let pf': ?m.21893
pf' ← mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``Eq.mp: {α β : Sort u} → α = β → α → β
Eq.mp #[nep: Expr
nep, sm_lt_zero: ?m.21685
sm_lt_zero]
    mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``Linarith.lt_irrefl: ∀ {α : Type u} [inst : Preorder α] {a : α}, ¬a < a
Linarith.lt_irrefl #[pf': ?m.21893
pf']

end Linarith