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
import Mathlib.Tactic.Zify
import Mathlib.Tactic.CancelDenoms
import Mathlib.Lean.Exception
import Std.Data.RBMap.Basic
import Mathlib.Data.HashMap

/-!
# Linarith preprocessing

This file contains methods used to preprocess inputs to `linarith`.

In particular, `linarith` works over comparisons of the form `t R 0`, where `R ∈ {<,≤,=}`.
It assumes that expressions in `t` have integer coefficients and that the type of `t` has
well-behaved subtraction.

## Implementation details

A `GlobalPreprocessor` is a function `List Expr → TacticM (List Expr)`. Users can add custom
preprocessing steps by adding them to the `LinarithConfig` object. `Linarith.defaultPreprocessors`
is the main list, and generally none of these should be skipped unless you know what you're doing.
-/

namespace Linarith

/-! ### Preprocessing -/

open Lean Elab Tactic Meta
open Qq

/-- Processor that recursively replaces `P ∧ Q` hypotheses with the pair `P` and `Q`. -/
partial def 
splitConjunctions: Preprocessor
splitConjunctions : 
Preprocessor: Type
Preprocessor where
  name := 
"split conjunctions": String
"split conjunctions"
  transform := 
aux: Expr → MetaM (List Expr)
aux
where
  /-- Implementation of the `splitConjunctions` preprocessor. -/
  
aux: Expr → MetaM (List Expr)
aux (
proof: Expr
proof : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM (
List: Type ?u.6 → Type ?u.6
List 
Expr: Type
Expr) := do
    match 
(← instantiateMVars (← inferType proof)): ?m.190
(← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
(← instantiateMVars (← inferType proof)): ?m.190
 
(← inferType proof): ?m.104
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType proof): ?m.104
 
proof: Expr
proof
(← inferType proof): ?m.104
)
(← instantiateMVars (← inferType proof)): ?m.190
).
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
    | (
``And: Name
``
And: Prop → Prop → Prop
And, #[_, _]) =>
      
pure: {f : Type ?u.478 → Type ?u.477} → [self : Pure f] → {α : Type ?u.478} → α → f α
pure (
(← aux (← mkAppM ``And.left #[proof])) ++
        (← aux (← mkAppM ``And.right #[proof])): ?m.526
(← 
aux: Expr → MetaM (List Expr)
aux
(← aux (← mkAppM ``And.left #[proof])) ++
        (← aux (← mkAppM ``And.right #[proof])): ?m.526
 
(← mkAppM ``And.left #[proof]): ?m.304
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``And.left #[proof]): ?m.304
 ``
And.left: ∀ {a b : Prop}, a ∧ b → a
And.left
(← mkAppM ``And.left #[proof]): ?m.304
 #[
proof: Expr
proof
(← mkAppM ``And.left #[proof]): ?m.304
])
(← aux (← mkAppM ``And.left #[proof])) ++
        (← aux (← mkAppM ``And.right #[proof])): ?m.526
) ++
        (← 
aux: Expr → MetaM (List Expr)
aux
(← aux (← mkAppM ``And.left #[proof])) ++
        (← aux (← mkAppM ``And.right #[proof])): ?m.526
 
(← mkAppM ``And.right #[proof]): ?m.420
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``And.right #[proof]): ?m.420
 ``
And.right: ∀ {a b : Prop}, a ∧ b → b
And.right
(← mkAppM ``And.right #[proof]): ?m.420
 #[
proof: Expr
proof
(← mkAppM ``And.right #[proof]): ?m.420
])
(← aux (← mkAppM ``And.left #[proof])) ++
        (← aux (← mkAppM ``And.right #[proof])): ?m.526
))
    | _ => 
pure: {f : Type ?u.623 → Type ?u.622} → [self : Pure f] → {α : Type ?u.623} → α → f α
pure [
proof: Expr
proof]

/--
Removes any expressions that are not proofs of inequalities, equalities, or negations thereof.
-/
partial def 
filterComparisons: Preprocessor
filterComparisons : 
Preprocessor: Type
Preprocessor where
  name := 
"filter terms that are not proofs of comparisons": String
"filter terms that are not proofs of comparisons"
  transform 
h: ?m.4019
h := do
    let 
tp: ?m.4235
tp ← 
whnfR: Expr → MetaM Expr
whnfR 
(← instantiateMVars (← inferType h)): ?m.4180
(← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
(← instantiateMVars (← inferType h)): ?m.4180
 
(← inferType h): ?m.4094
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType h): ?m.4094
 
h: ?m.4019
h
(← inferType h): ?m.4094
)
(← instantiateMVars (← inferType h)): ?m.4180
)
    if 
(← isProp tp): ?m.4290
(← 
isProp: Expr → MetaM Bool
isProp
(← isProp tp): ?m.4290
 
tp: ?m.4235
tp
(← isProp tp): ?m.4290
) && 
(← aux tp): ?m.4345
(← 
aux: Expr → MetaM Bool
aux
(← aux tp): ?m.4345
 
tp: ?m.4235
tp
(← aux tp): ?m.4345
) then 
pure: {f : Type ?u.4440 → Type ?u.4439} → [self : Pure f] → {α : Type ?u.4440} → α → f α
pure [
h: ?m.4019
h]
    else 
pure: {f : Type ?u.4514 → Type ?u.4513} → [self : Pure f] → {α : Type ?u.4514} → α → f α
pure 
[]: List ?m.4539
[]
where
  /-- Implementation of the `filterComparisons` preprocessor. -/
  
aux: Expr → MetaM Bool
aux (
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Bool: Type
Bool := do
  match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``Eq: Name
``
Eq: {α : Sort u_1} → α → α → Prop
Eq, _) | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, _) | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, _) => 
pure: {f : Type ?u.2548 → Type ?u.2547} → [self : Pure f] → {α : Type ?u.2548} → α → f α
pure 
true: Bool
true
  | (
``Not: Name
``
Not: Prop → Prop
Not, #[
e: Expr
e]) => match 
(← whnfR e): ?m.2720
(← 
whnfR: Expr → MetaM Expr
whnfR
(← whnfR e): ?m.2720
 
e: Expr
e
(← whnfR e): ?m.2720
).
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
    | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, _) | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, _) => 
pure: {f : Type ?u.2746 → Type ?u.2745} → [self : Pure f] → {α : Type ?u.2746} → α → f α
pure 
true: Bool
true
    | _ => 
pure: {f : Type ?u.2834 → Type ?u.2833} → [self : Pure f] → {α : Type ?u.2834} → α → f α
pure 
false: Bool
false
  | _ => 
pure: {f : Type ?u.3276 → Type ?u.3275} → [self : Pure f] → {α : Type ?u.3276} → α → f α
pure 
false: Bool
false

section removeNegations

/--
If `prf` is a proof of `¬ e`, where `e` is a comparison,
`flipNegatedComparison prf e` flips the comparison in `e` and returns a proof.
For example, if `prf : ¬ a < b`, ``flipNegatedComparison prf q(a < b)`` returns a proof of `a ≥ b`.
-/
def 
flipNegatedComparison: Expr → Expr → MetaM Expr
flipNegatedComparison (
prf: Expr
prf : 
Expr: Type
Expr) (
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Expr: Type
Expr :=
  match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, #[_, _, _, _]) => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
lt_of_not_ge: ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a < b
lt_of_not_ge #[
prf: Expr
prf]
  | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, #[_, _, _, _]) => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
le_of_not_gt: ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a > b → a ≤ b
le_of_not_gt #[
prf: Expr
prf]
  | _ => throwError "Not a comparison (flipNegatedComparison): {
e: Expr
e}"

/--
Replaces proofs of negations of comparisons with proofs of the reversed comparisons.
For example, a proof of `¬ a < b` will become a proof of `a ≥ b`.
-/
def 
removeNegations: Preprocessor
removeNegations : 
Preprocessor: Type
Preprocessor where
  name := 
"replace negations of comparisons": String
"replace negations of comparisons"
  transform 
h: ?m.9646
h := do
    let 
t: Q(Prop)
t : Q(
Prop: Type
Prop) ← 
whnfR: Expr → MetaM Expr
whnfR 
(← inferType h): ?m.9721
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType h): ?m.9721
 
h: ?m.9646
h
(← inferType h): ?m.9721
)
    match 
t: Q(Prop)
t with
    | ~q(¬ $p) =>
      trace[linarith] "removing negation in {
h: ?m.9646
h}"
      return 
[← flipNegatedComparison h (← whnfR p)]: List ?m.11212
[← 
flipNegatedComparison: Expr → Expr → MetaM Expr
flipNegatedComparison
[← flipNegatedComparison h (← whnfR p)]: List ?m.11212
 
h: ?m.9646
h
[← flipNegatedComparison h (← whnfR p)]: List ?m.11212
 
(← whnfR p): ?m.11129
(← 
whnfR: Expr → MetaM Expr
whnfR
(← whnfR p): ?m.11129
 
p: Q(Prop)
p
(← whnfR p): ?m.11129
)
[← flipNegatedComparison h (← whnfR p)]: List ?m.11212
]
    | _        => return [
h: ?m.9646
h]

end removeNegations

section natToInt

open Mathlib.Tactic.Zify

/--
`isNatProp tp` is true iff `tp` is an inequality or equality between natural numbers
or the negation thereof.
-/
partial def 
isNatProp: Expr → Bool
isNatProp (
e: Expr
e : 
Expr: Type
Expr) : 
Bool: Type
Bool :=
  match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``Eq: Name
``
Eq: {α : Sort u_1} → α → α → Prop
Eq, #[
.const: Name → List Level → Expr
.const 
``Nat: Name
``
Nat: Type
Nat [], _, _]) => 
true: Bool
true
  | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, #[
.const: Name → List Level → Expr
.const 
``Nat: Name
``
Nat: Type
Nat [], _, _, _]) => 
true: Bool
true
  | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, #[
.const: Name → List Level → Expr
.const 
``Nat: Name
``
Nat: Type
Nat [], _, _, _]) => 
true: Bool
true
  | (
``GE.ge: Name
``
GE.ge: {α : Type u} → [inst : LE α] → α → α → Prop
GE.ge, #[
.const: Name → List Level → Expr
.const 
``Nat: Name
``
Nat: Type
Nat [], _, _, _]) => 
true: Bool
true
  | (
``GT.gt: Name
``
GT.gt: {α : Type u} → [inst : LT α] → α → α → Prop
GT.gt, #[
.const: Name → List Level → Expr
.const 
``Nat: Name
``
Nat: Type
Nat [], _, _, _]) => 
true: Bool
true
  | (
``Not: Name
``
Not: Prop → Prop
Not, #[
e: Expr
e]) => 
isNatProp: Expr → Bool
isNatProp 
e: Expr
e
  | _ => 
false: Bool
false

/-- If `e` is of the form `((n : ℕ) : ℤ)`, `isNatIntCoe e` returns `n : ℕ`. -/
def 
isNatIntCoe: Expr → Option Expr
isNatIntCoe (
e: Expr
e : 
Expr: Type
Expr) : 
Option: Type ?u.24476 → Type ?u.24476
Option 
Expr: Type
Expr :=
  match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``Nat.cast: Name
``
Nat.cast: {R : Type u} → [inst : NatCast R] → ℕ → R
Nat.cast, #[
.const: Name → List Level → Expr
.const 
``Int: Name
``
Int: Type
Int [], _, 
n: Expr
n]) => 
some: {α : Type ?u.24544} → α → Option α
some 
n: Expr
n
  | _ => 
none: {α : Type ?u.24554} → Option α
none

/--
`getNatComparisons e` returns a list of all subexpressions of `e` of the form `((t : ℕ) : ℤ)`.
-/
partial def 
getNatComparisons: Expr → List Expr
getNatComparisons (
e: Expr
e : 
Expr: Type
Expr) : 
List: Type ?u.26456 → Type ?u.26456
List 
Expr: Type
Expr :=
  match 
isNatIntCoe: Expr → Option Expr
isNatIntCoe 
e: Expr
e with
  | 
some: {α : Type ?u.26460} → α → Option α
some 
n: Expr
n => [
n: Expr
n]
  | 
none: {α : Type ?u.26481} → Option α
none => match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
    | (
``HAdd.hAdd: Name
``
HAdd.hAdd: {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAdd α β γ] → α → β → γ
HAdd.hAdd, #[_, _, _, _, 
a: Expr
a, 
b: Expr
b]) => 
getNatComparisons: Expr → List Expr
getNatComparisons 
a: Expr
a ++ 
getNatComparisons: Expr → List Expr
getNatComparisons 
b: Expr
b
    | (
``HMul.hMul: Name
``
HMul.hMul: {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HMul α β γ] → α → β → γ
HMul.hMul, #[_, _, _, _, 
a: Expr
a, 
b: Expr
b]) => 
getNatComparisons: Expr → List Expr
getNatComparisons 
a: Expr
a ++ 
getNatComparisons: Expr → List Expr
getNatComparisons 
b: Expr
b
    | _ => 
[]: List ?m.26745
[]

/-- If `e : ℕ`, returns a proof of `0 ≤ (e : ℤ)`. -/
def 
mk_coe_nat_nonneg_prf: Expr → MetaM Expr
mk_coe_nat_nonneg_prf (
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Expr: Type
Expr :=
  
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
Int.coe_nat_nonneg: ∀ (n : ℕ), 0 ≤ ↑n
Int.coe_nat_nonneg #[
e: Expr
e]

open Std

/-- Ordering on `Expr`. -/
-- We only define this so we can use `RBSet Expr`. Perhaps `HashSet` would be more appropriate?
def 
Expr.compare: Expr → Expr → Ordering
Expr.compare (
a: Expr
a 
b: Expr
b : 
Expr: Type
Expr) : 
Ordering: Type
Ordering :=
  if 
Expr.lt: Expr → Expr → Bool
Expr.lt 
a: Expr
a 
b: Expr
b then 
.lt: Ordering
.lt else if 
a: Expr
a.
equal: Expr → Expr → Bool
equal 
b: Expr
b then 
.eq: Ordering
.eq else 
.gt: Ordering
.gt

/--
If `h` is an equality or inequality between natural numbers,
`natToInt` lifts this inequality to the integers.
It also adds the facts that the integers involved are nonnegative.
To avoid adding the same nonnegativity facts many times, it is a global preprocessor.
 -/
def 
natToInt: GlobalBranchingPreprocessor
natToInt : 
GlobalBranchingPreprocessor: Type
GlobalBranchingPreprocessor where
  name := 
"move nats to ints": String
"move nats to ints"
  transform 
g: ?m.28767
g 
l: ?m.28770
l := do
    let 
l: ?m.30112
l ← 
l: ?m.28770
l.
mapM: {m : Type ?u.28835 → Type ?u.28834} →
  [inst : Monad m] → {α : Type ?u.28833} → {β : Type ?u.28835} → (α → m β) → List α → m (List β)
mapM $ fun 
h: ?m.28874
h => do
      let 
t: ?m.29091
t ← 
whnfR: Expr → MetaM Expr
whnfR 
(← instantiateMVars (← inferType h)): ?m.29036
(← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
(← instantiateMVars (← inferType h)): ?m.29036
 
(← inferType h): ?m.28950
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType h): ?m.28950
 
h: ?m.28874
h
(← inferType h): ?m.28950
)
(← instantiateMVars (← inferType h)): ?m.29036
)
      if 
isNatProp: Expr → Bool
isNatProp 
t: ?m.29091
t then
        let (
some: {α : Type ?u.29285} → α → Option α
some (
h': Expr
h', 
t': Expr
t'), _) ← 
Term.TermElabM.run': {α : Type} →
  TermElabM α →
    optParam Term.Context
        { declName? := none, auxDeclToFullName := ∅, macroStack := [], mayPostpone := true, errToSorry := true,
          autoBoundImplicit := false,
          autoBoundImplicits :=
            { root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
              tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
              shift := PersistentArray.initShift, tailOff := 0 },
          autoBoundImplicitForbidden := fun x => false, sectionVars := ∅, sectionFVars := ∅, implicitLambda := true,
          isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none,
          saveRecAppSyntax := true, holesAsSyntheticOpaque := false } →
      optParam Term.State
          { levelNames := [], syntheticMVars := ∅, pendingMVars := ∅, mvarErrorInfos := ∅, letRecsToLift := [] } →
        MetaM α
Term.TermElabM.run' (
run_for: {α : Type} → MVarId → TacticM α → TermElabM (Option α × List MVarId)
run_for 
g: ?m.28767
g (
zifyProof: Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",") → Expr → Expr → TacticM (Expr × Expr)
zifyProof 
none: {α : Type ?u.29252} → Option α
none 
h: ?m.28874
h 
t: ?m.29091
t))
          | throwError "zifyProof failed on {
h: ?m.28874
h}"
        if ← 
filterComparisons.aux: Expr → MetaM Bool
filterComparisons.aux 
t': Expr
t' then
          
pure: {f : Type ?u.29451 → Type ?u.29450} → [self : Pure f] → {α : Type ?u.29451} → α → f α
pure 
h': Expr
h'
        else
          -- `zifyProof` turned our comparison into something that wasn't a comparison
          -- probably replacing `n = n` with `True`, because of
          -- https://github.com/leanprover-community/mathlib4/issues/741
          -- so we just keep the original hypothesis.
          
pure: {f : Type ?u.29520 → Type ?u.29519} → [self : Pure f] → {α : Type ?u.29520} → α → f α
pure 
h: ?m.28874
h
      else
        
pure: {f : Type ?u.30005 → Type ?u.30004} → [self : Pure f] → {α : Type ?u.30005} → α → f α
pure 
h: ?m.28874
h
    let 
nonnegs: ?m.30848
nonnegs ← 
l: ?m.30112
l.
foldlM: {m : Type ?u.30158 → Type ?u.30157} →
  [inst : Monad m] → {s : Type ?u.30158} → {α : Type ?u.30156} → (s → α → m s) → s → List α → m s
foldlM (init := 
∅: ?m.30789
∅) fun (
es: RBSet Expr Expr.compare
es : 
RBSet: (α : Type ?u.30201) → (α → α → Ordering) → Type ?u.30201
RBSet 
Expr: Type
Expr 
Expr.compare: Expr → Expr → Ordering
Expr.compare) 
h: ?m.30206
h => do
      try
        let (
a: Expr
a, 
b: Expr
b) ← 
getRelSides: Expr → MetaM (Expr × Expr)
getRelSides 
(← inferType h): ?m.30288
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType h): ?m.30288
 
h: ?m.30206
h
(← inferType h): ?m.30288
)
        
pure: {f : Type ?u.30372 → Type ?u.30371} → [self : Pure f] → {α : Type ?u.30372} → α → f α
pure <| (
es: RBSet Expr Expr.compare
es.
insertList: {α : Type ?u.30396} → {cmp : α → α → Ordering} → RBSet α cmp → List α → RBSet α cmp
insertList (
getNatComparisons: Expr → List Expr
getNatComparisons 
a: Expr
a)).
insertList: {α : Type ?u.30409} → {cmp : α → α → Ordering} → RBSet α cmp → List α → RBSet α cmp
insertList (
getNatComparisons: Expr → List Expr
getNatComparisons 
b: Expr
b)
      catch 
_: ?m.30512
_ => 
pure: {f : Type ?u.30515 → Type ?u.30514} → [self : Pure f] → {α : Type ?u.30515} → α → f α
pure 
es: RBSet Expr Expr.compare
es
    
pure: {f : Type ?u.30954 → Type ?u.30953} → [self : Pure f] → {α : Type ?u.30954} → α → f α
pure [(
g: ?m.28767
g, ((← 
nonnegs: ?m.30848
nonnegs.
toList: {α : Type ?u.30892} → {cmp : α → α → Ordering} → RBSet α cmp → List α
toList.
mapM: {m : Type ?u.30899 → Type ?u.30898} →
  [inst : Monad m] → {α : Type ?u.30897} → {β : Type ?u.30899} → (α → m β) → List α → m (List β)
mapM 
mk_coe_nat_nonneg_prf: Expr → MetaM Expr
mk_coe_nat_nonneg_prf) ++ 
l: ?m.30112
l : 
List: Type ?u.30987 → Type ?u.30987
List 
Expr: Type
Expr))]

end natToInt

section strengthenStrictInt

/--
`isStrictIntComparison tp` is true iff `tp` is a strict inequality between integers
or the negation of a weak inequality between integers.
-/
def 
isStrictIntComparison: Expr → Bool
isStrictIntComparison (
e: Expr
e : 
Expr: Type
Expr) : 
Bool: Type
Bool :=
  match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, #[
.const: Name → List Level → Expr
.const 
``Int: Name
``
Int: Type
Int [], _, _, _]) => 
true: Bool
true
  | (
``GT.gt: Name
``
GT.gt: {α : Type u} → [inst : LT α] → α → α → Prop
GT.gt, #[
.const: Name → List Level → Expr
.const 
``Int: Name
``
Int: Type
Int [], _, _, _]) => 
true: Bool
true
  | (
``Not: Name
``
Not: Prop → Prop
Not, #[
e: Expr
e]) => match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
    | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, #[
.const: Name → List Level → Expr
.const 
``Int: Name
``
Int: Type
Int [], _, _, _]) => 
true: Bool
true
    | (
``GE.ge: Name
``
GE.ge: {α : Type u} → [inst : LE α] → α → α → Prop
GE.ge, #[
.const: Name → List Level → Expr
.const 
``Int: Name
``
Int: Type
Int [], _, _, _]) => 
true: Bool
true
    | _ => 
false: Bool
false
  | _ => 
false: Bool
false

/--
If `pf` is a proof of a strict inequality `(a : ℤ) < b`,
`mkNonstrictIntProof pf` returns a proof of `a + 1 ≤ b`,
and similarly if `pf` proves a negated weak inequality.
-/
def 
mkNonstrictIntProof: Expr → MetaM Expr
mkNonstrictIntProof (
pf: Expr
pf : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Expr: Type
Expr := do
  match 
(← inferType pf): ?m.44282
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType pf): ?m.44282
 
pf: Expr
pf
(← inferType pf): ?m.44282
).
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, #[_, _, 
a: Expr
a, 
b: Expr
b]) =>
    return 
mkApp: Expr → Expr → Expr
mkApp 
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.44621
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.44621
 ``
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.44621
 
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.44610
#[← 
mkAppOptM: Name → Array (Option Expr) → MetaM Expr
mkAppOptM
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.44610
 ``
Int.add_one_le_iff: ∀ {a b : ℤ}, a + 1 ≤ b ↔ a < b
Int.add_one_le_iff
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.44610
 #[
a: Expr
a
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.44610
, 
b: Expr
b
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.44610
]]
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.44621
) 
pf: Expr
pf
  | (
``GT.gt: Name
``
GT.gt: {α : Type u} → [inst : LT α] → α → α → Prop
GT.gt, #[_, _, 
a: Expr
a, 
b: Expr
b]) =>
    return 
mkApp: Expr → Expr → Expr
mkApp 
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45014
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45014
 ``
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45014
 
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45003
#[← 
mkAppOptM: Name → Array (Option Expr) → MetaM Expr
mkAppOptM
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45003
 ``
Int.add_one_le_iff: ∀ {a b : ℤ}, a + 1 ≤ b ↔ a < b
Int.add_one_le_iff
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45003
 #[
b: Expr
b
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45003
, 
a: Expr
a
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45003
]]
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45014
) 
pf: Expr
pf
  | (
``Not: Name
``
Not: Prop → Prop
Not, #[
P: Expr
P]) => match 
P: Expr
P.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
    | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, #[_, _, 
a: Expr
a, 
b: Expr
b]) =>
      return 
mkApp: Expr → Expr → Expr
mkApp 
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45403
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45403
 ``
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45403
 
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45392
#[← 
mkAppOptM: Name → Array (Option Expr) → MetaM Expr
mkAppOptM
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45392
 ``
Int.add_one_le_iff: ∀ {a b : ℤ}, a + 1 ≤ b ↔ a < b
Int.add_one_le_iff
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45392
 #[
b: Expr
b
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45392
, 
a: Expr
a
#[← mkAppOptM ``Int.add_one_le_iff #[b, a]]: Array ?m.45392
]]
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[b, a]]): ?m.45403
)
        
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45464
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45464
 ``
lt_of_not_ge: ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a < b
lt_of_not_ge
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45464
 #[
pf: Expr
pf
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45464
])
    | (
``GE.ge: Name
``
GE.ge: {α : Type u} → [inst : LE α] → α → α → Prop
GE.ge, #[_, _, 
a: Expr
a, 
b: Expr
b]) =>
      return 
mkApp: Expr → Expr → Expr
mkApp 
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.45823
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.45823
 ``
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.45823
 
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.45812
#[← 
mkAppOptM: Name → Array (Option Expr) → MetaM Expr
mkAppOptM
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.45812
 ``
Int.add_one_le_iff: ∀ {a b : ℤ}, a + 1 ≤ b ↔ a < b
Int.add_one_le_iff
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.45812
 #[
a: Expr
a
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.45812
, 
b: Expr
b
#[← mkAppOptM ``Int.add_one_le_iff #[a, b]]: Array ?m.45812
]]
(← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[a, b]]): ?m.45823
)
        
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45884
(← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45884
 ``
lt_of_not_ge: ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, ¬a ≥ b → a < b
lt_of_not_ge
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45884
 #[
pf: Expr
pf
(← mkAppM ``lt_of_not_ge #[pf]): ?m.45884
])
    | _ => 
throwError "mkNonstrictIntProof failed: proof is not an inequality": ?m.45944 ?m.45945
throwError
throwError "mkNonstrictIntProof failed: proof is not an inequality": ?m.45944 ?m.45945
 "mkNonstrictIntProof failed: proof is not an inequality"
  | _ => 
throwError "mkNonstrictIntProof failed: proof is not an inequality": ?m.47051 ?m.47052
throwError
throwError "mkNonstrictIntProof failed: proof is not an inequality": ?m.47051 ?m.47052
 "mkNonstrictIntProof failed: proof is not an inequality"


/-- `strengthenStrictInt h` turns a proof `h` of a strict integer inequality `t1 < t2`
into a proof of `t1 ≤ t2 + 1`. -/
def 
strengthenStrictInt: Preprocessor
strengthenStrictInt : 
Preprocessor: Type
Preprocessor where
  name := 
"strengthen strict inequalities over int": String
"strengthen strict inequalities over int"
  transform 
h: ?m.51506
h := do
    if 
isStrictIntComparison: Expr → Bool
isStrictIntComparison 
(← inferType h): ?m.51581
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType h): ?m.51581
 
h: ?m.51506
h
(← inferType h): ?m.51581
) then
      return 
[← mkNonstrictIntProof h]: List ?m.51756
[← 
mkNonstrictIntProof: Expr → MetaM Expr
mkNonstrictIntProof
[← mkNonstrictIntProof h]: List ?m.51756
 
h: ?m.51506
h
[← mkNonstrictIntProof h]: List ?m.51756
]
    else
      return [
h: ?m.51506
h]

end strengthenStrictInt

section compWithZero

/--
`rearrangeComparison e` takes a proof `e` of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`, where `R ∈ {=, ≤, <}`.
 -/
partial def 
rearrangeComparison: Expr → MetaM Expr
rearrangeComparison (
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Expr: Type
Expr := do
  
aux: Expr → Expr → MetaM Expr
aux 
e: Expr
e 
(← instantiateMVars (← inferType e)): ?m.138506
(← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
(← instantiateMVars (← inferType e)): ?m.138506
 
(← inferType e): ?m.138420
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType e): ?m.138420
 
e: Expr
e
(← inferType e): ?m.138420
)
(← instantiateMVars (← inferType e)): ?m.138506
)
where
  /-- Implementation of `rearrangeComparison`, after type inference. -/
  
aux: Expr → Expr → MetaM Expr
aux (
proof: Expr
proof 
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Expr: Type
Expr :=
    match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
    | (
``LE.le: Name
``
LE.le: {α : Type u} → [self : LE α] → α → α → Prop
LE.le, #[_, _, 
a: Expr
a, 
b: Expr
b]) => match 
a: Expr
a.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs, 
b: Expr
b.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
      | _, (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]) => return 
proof: Expr
proof
      | (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]), _ => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
neg_nonpos_of_nonneg: ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, 0 ≤ a → -a ≤ 0
neg_nonpos_of_nonneg #[
proof: Expr
proof]
      | _, _                                          => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
sub_nonpos_of_le: ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ b → a - b ≤ 0
sub_nonpos_of_le #[
proof: Expr
proof]
    | (
``LT.lt: Name
``
LT.lt: {α : Type u} → [self : LT α] → α → α → Prop
LT.lt, #[_, _, 
a: Expr
a, 
b: Expr
b]) => match 
a: Expr
a.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs, 
b: Expr
b.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
      | _, (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]) => return 
proof: Expr
proof
      | (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]), _ => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
neg_neg_of_pos: ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, 0 < a → -a < 0
neg_neg_of_pos #[
proof: Expr
proof]
      | _, _                                          => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
sub_neg_of_lt: ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a < b → a - b < 0
sub_neg_of_lt #[
proof: Expr
proof]
    | (
``Eq: Name
``
Eq: {α : Sort u_1} → α → α → Prop
Eq, #[_, 
a: Expr
a, 
b: Expr
b]) => match 
a: Expr
a.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs, 
b: Expr
b.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
      | _, (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]) => return 
proof: Expr
proof
      | (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]), _ => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
Eq.symm: ∀ {α : Sort u} {a b : α}, a = b → b = a
Eq.symm #[
proof: Expr
proof]
      | _, _                                          => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
sub_eq_zero_of_eq: ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, a = b → a - b = 0
sub_eq_zero_of_eq #[
proof: Expr
proof]
    | (
``GT.gt: Name
``
GT.gt: {α : Type u} → [inst : LT α] → α → α → Prop
GT.gt, #[_, _, 
a: Expr
a, 
b: Expr
b]) => match 
a: Expr
a.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs, 
b: Expr
b.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
      | _, (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]) => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
neg_neg_of_pos: ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, 0 < a → -a < 0
neg_neg_of_pos #[
proof: Expr
proof]
      | (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]), _ => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
lt_zero_of_zero_gt: ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LT α] {a : α}, 0 > a → a < 0
lt_zero_of_zero_gt #[
proof: Expr
proof]
      | _, _                                          => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
sub_neg_of_lt: ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a < b → a - b < 0
sub_neg_of_lt #[
proof: Expr
proof]
    | (
``GE.ge: Name
``
GE.ge: {α : Type u} → [inst : LE α] → α → α → Prop
GE.ge, #[_, _, 
a: Expr
a, 
b: Expr
b]) => match 
a: Expr
a.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs, 
b: Expr
b.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
      | _, (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]) => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
neg_nonpos_of_nonneg: ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, 0 ≤ a → -a ≤ 0
neg_nonpos_of_nonneg #[
proof: Expr
proof]
      | (
``OfNat.ofNat: Name
``
OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat, #[_, 
.lit: Literal → Expr
.lit (
.natVal: ℕ → Literal
.natVal 
0: ℕ
0), _]), _ => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
le_zero_of_zero_ge: ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LE α] {a : α}, 0 ≥ a → a ≤ 0
le_zero_of_zero_ge #[
proof: Expr
proof]
      | _, _                                          => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
sub_nonpos_of_le: ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ b → a - b ≤ 0
sub_nonpos_of_le #[
proof: Expr
proof]
    | (
``Not: Name
``
Not: Prop → Prop
Not, #[
a: Expr
a]) => do
      let 
nproof: ?m.136098
nproof ← 
flipNegatedComparison: Expr → Expr → MetaM Expr
flipNegatedComparison 
proof: Expr
proof 
a: Expr
a
      
aux: Expr → Expr → MetaM Expr
aux 
nproof: ?m.136098
nproof 
(← inferType nproof): ?m.136153
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType nproof): ?m.136153
 
nproof: ?m.136098
nproof
(← inferType nproof): ?m.136153
)
    | 
a: Name × Array Expr
a => throwError "couldn't rearrange comparison {
a: Name × Array Expr
a}"

/--
`compWithZero h` takes a proof `h` of an equality, inequality, or negation thereof,
and turns it into a proof of a comparison `_ R 0`, where `R ∈ {=, ≤, <}`.
 -/
def 
compWithZero: Preprocessor
compWithZero : 
Preprocessor: Type
Preprocessor where
  name := 
"make comparisons with zero": String
"make comparisons with zero"
  transform 
e: ?m.337040
e := try
    
pure: {f : Type ?u.337134 → Type ?u.337133} → [self : Pure f] → {α : Type ?u.337134} → α → f α
pure 
[← rearrangeComparison e]: List ?m.337159
[← 
rearrangeComparison: Expr → MetaM Expr
rearrangeComparison
[← rearrangeComparison e]: List ?m.337159
 
e: ?m.337040
e
[← rearrangeComparison e]: List ?m.337159
]
  catch 
e: ?m.337217
e =>
    if ← 
e: ?m.337217
e.
isFailedToSynthesize: Exception → IO Bool
isFailedToSynthesize then
      
pure: {f : Type ?u.337715 → Type ?u.337714} → [self : Pure f] → {α : Type ?u.337715} → α → f α
pure 
[]: List ?m.337740
[]
    else
      
throw: {ε : outParam (Type ?u.337748)} →
  {m : Type ?u.337747 → Type ?u.337746} → [self : MonadExcept ε m] → {α : Type ?u.337747} → ε → m α
throw 
e: ?m.337217
e

end compWithZero

section cancelDenoms

theorem 
without_one_mul: ∀ {M : Type u_1} [inst : MulOneClass M] {a b : M}, 1 * a = b → a = b
without_one_mul [
MulOneClass: Type ?u.339407 → Type ?u.339407
MulOneClass 
M: ?m.339404
M] {
a: M
a 
b: M
b : 
M: ?m.339404
M} (
h: 1 * a = b
h : 
1: ?m.339419
1 * 
a: M
a = 
b: M
b) : 
a: M
a = 
b: M
b := 
Goals accomplished! 🐙
M: Type u_1

inst✝: MulOneClass M

a, b: M

h: 1 * a = b

a = b
M: Type u_1

inst✝: MulOneClass M

a, b: M

h: 1 * a = b

a = b
M: Type u_1

inst✝: MulOneClass M

a, b: M

h: a = b

a = b
M: Type u_1

inst✝: MulOneClass M

a, b: M

h: a = b

a = b
Goals accomplished! 🐙


/--
`normalizeDenominatorsLHS h lhs` assumes that `h` is a proof of `lhs R 0`.
It creates a proof of `lhs' R 0`, where all numeric division in `lhs` has been cancelled.
-/
def 
normalizeDenominatorsLHS: Expr → Expr → MetaM Expr
normalizeDenominatorsLHS (
h: Expr
h 
lhs: Expr
lhs : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM 
Expr: Type
Expr := do
  let mut (
v: ℕ
v, 
lhs': Expr
lhs') ← 
CancelDenoms.derive: Expr → MetaM (ℕ × Expr)
CancelDenoms.derive 
lhs: Expr
lhs
  if 
v: ℕ
v = 
1: ?m.340831
1 then
    -- `lhs'` has a `1 *` out front, but `mkSingleCompZeroOf` has a special case
    -- where it does not produce `1 *`. We strip it off here:
    
lhs': Expr
lhs' ← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
without_one_mul: ∀ {M : Type u_1} [inst : MulOneClass M] {a b : M}, 1 * a = b → a = b
without_one_mul #[
lhs': Expr
lhs']
  let (_, 
h'': Expr
h'') ← 
mkSingleCompZeroOf: ℕ → Expr → MetaM (Ineq × Expr)
mkSingleCompZeroOf 
v: ℕ
v 
h: Expr
h
  try
    
h'': Expr
h''.
rewriteType: Expr → Expr → MetaM Expr
rewriteType 
lhs': Expr
lhs'
  catch 
e: ?m.341293
e =>
    dbg_trace
      
s!"Error in Linarith.normalizeDenominatorsLHS: {← e.toMessageData.toString}": ?m.341474
s!
s!"Error in Linarith.normalizeDenominatorsLHS: {← e.toMessageData.toString}": ?m.341474
"Error in Linarith.normalizeDenominatorsLHS: {← 
e: ?m.341293
e
s!"Error in Linarith.normalizeDenominatorsLHS: {← e.toMessageData.toString}": ?m.341474
.
toMessageData: Exception → MessageData
toMessageData
s!"Error in Linarith.normalizeDenominatorsLHS: {← e.toMessageData.toString}": ?m.341474
.
toString: MessageData → IO String
toString
s!"Error in Linarith.normalizeDenominatorsLHS: {← e.toMessageData.toString}": ?m.341474
}"
    
throw: {ε : outParam (Type ?u.341492)} →
  {m : Type ?u.341491 → Type ?u.341490} → [self : MonadExcept ε m] → {α : Type ?u.341491} → ε → m α
throw 
e: ?m.341293
e

/--
`cancelDenoms pf` assumes `pf` is a proof of `t R 0`. If `t` contains the division symbol `/`,
it tries to scale `t` to cancel out division by numerals.
-/
def 
cancelDenoms: Preprocessor
cancelDenoms : 
Preprocessor: Type
Preprocessor where
  name := 
"cancel denominators": String
"cancel denominators"
  transform := fun 
pf: ?m.344688
pf => (do
      let (_, 
lhs: Expr
lhs) ← 
parseCompAndExpr: Expr → MetaM (Ineq × Expr)
parseCompAndExpr 
(← inferType pf): ?m.344827
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType pf): ?m.344827
 
pf: ?m.344688
pf
(← inferType pf): ?m.344827
)
      
guard: {f : Type → Type ?u.344953} → [inst : Alternative f] → (p : Prop) → [inst : Decidable p] → f Unit
guard $ 
lhs: Expr
lhs.
containsConst: Expr → (Name → Bool) → Bool
containsConst (fun 
n: ?m.344971
n => 
n: ?m.344971
n = ``
HDiv.hDiv: {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HDiv α β γ] → α → β → γ
HDiv.hDiv || 
n: ?m.344971
n = ``
Div.div: {α : Type u} → [self : Div α] → α → α → α
Div.div)
      
pure: {f : Type ?u.345186 → Type ?u.345185} → [self : Pure f] → {α : Type ?u.345186} → α → f α
pure 
[← normalizeDenominatorsLHS pf lhs]: List ?m.345211
[← 
normalizeDenominatorsLHS: Expr → Expr → MetaM Expr
normalizeDenominatorsLHS
[← normalizeDenominatorsLHS pf lhs]: List ?m.345211
 
pf: ?m.344688
pf
[← normalizeDenominatorsLHS pf lhs]: List ?m.345211
 
lhs: Expr
lhs
[← normalizeDenominatorsLHS pf lhs]: List ?m.345211
])
    <|> return [
pf: ?m.344688
pf]
end cancelDenoms

section nlinarith
/--
`findSquares s e` collects all terms of the form `a ^ 2` and `a * a` that appear in `e`
and adds them to the set `s`.
A pair `(a, true)` is added to `s` when `a^2` appears in `e`,
and `(a, false)` is added to `s` when `a*a` appears in `e`.  -/
partial def 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares (
s: HashSet (Expr × Bool)
s : 
HashSet: (α : Type ?u.346629) → [inst : BEq α] → [inst : Hashable α] → Type ?u.346629
HashSet (
Expr: Type
Expr × 
Bool: Type
Bool)) (
e: Expr
e : 
Expr: Type
Expr) : 
MetaM: Type → Type
MetaM (
HashSet: (α : Type ?u.346683) → [inst : BEq α] → [inst : Hashable α] → Type ?u.346683
HashSet (
Expr: Type
Expr × 
Bool: Type
Bool)) :=
  match 
e: Expr
e.
getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs with
  | (
``HPow.hPow: Name
``
HPow.hPow: {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HPow α β γ] → α → β → γ
HPow.hPow, #[_, _, _, _, 
a: Expr
a, 
b: Expr
b]) => match 
b: Expr
b.
numeral?: Expr → Option ℕ
numeral? with
    | 
some: {α : Type ?u.346794} → α → Option α
some 
2: ℕ
2 => do
      let 
s: ?m.346889
s ← 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares 
s: HashSet (Expr × Bool)
s 
a: Expr
a
      return (
s: ?m.346889
s.
insert: {α : Type ?u.346916} → {x : BEq α} → {x_1 : Hashable α} → HashSet α → α → HashSet α
insert (
a: Expr
a, 
true: Bool
true))
    | _ => 
e: Expr
e.
foldlM: {α : Type} → {m : Type → Type ?u.346994} → [inst : Monad m] → (α → Expr → m α) → α → Expr → m α
foldlM 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares 
s: HashSet (Expr × Bool)
s
  | (
``HMul.hMul: Name
``
HMul.hMul: {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HMul α β γ] → α → β → γ
HMul.hMul, #[_, _, _, _, 
a: Expr
a, 
b: Expr
b]) => if 
a: Expr
a.
equal: Expr → Expr → Bool
equal 
b: Expr
b then do
      let 
s: ?m.347420
s ← 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares 
s: HashSet (Expr × Bool)
s 
a: Expr
a
      return (
s: ?m.347420
s.
insert: {α : Type ?u.347447} → {x : BEq α} → {x_1 : Hashable α} → HashSet α → α → HashSet α
insert (
a: Expr
a, 
false: Bool
false))
    else
      
e: Expr
e.
foldlM: {α : Type} → {m : Type → Type ?u.347518} → [inst : Monad m] → (α → Expr → m α) → α → Expr → m α
foldlM 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares 
s: HashSet (Expr × Bool)
s
  | _ => 
e: Expr
e.
foldlM: {α : Type} → {m : Type → Type ?u.347588} → [inst : Monad m] → (α → Expr → m α) → α → Expr → m α
foldlM 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares 
s: HashSet (Expr × Bool)
s

/--
`nlinarithExtras` is the preprocessor corresponding to the `nlinarith` tactic.

* For every term `t` such that `t^2` or `t*t` appears in the input, adds a proof of `t^2 ≥ 0`
  or `t*t ≥ 0`.
* For every pair of comparisons `t1 R1 0` and `t2 R2 0`, adds a proof of `t1*t2 R 0`.

This preprocessor is typically run last, after all inputs have been canonized.
-/
def 
nlinarithExtras: GlobalPreprocessor
nlinarithExtras : 
GlobalPreprocessor: Type
GlobalPreprocessor where
  name := 
"nonlinear arithmetic extras": String
"nonlinear arithmetic extras"
  transform 
ls: ?m.351878
ls := do
    let 
s: ?m.352257
s ← 
ls: ?m.351878
ls.
foldrM: {m : Type ?u.351943 → Type ?u.351942} →
  [inst : Monad m] → {s : Type ?u.351943} → {α : Type ?u.351941} → (α → s → m s) → s → List α → m s
foldrM (fun 
h: ?m.351983
h 
s': ?m.351986
s' => do 
findSquares: HashSet (Expr × Bool) → Expr → MetaM (HashSet (Expr × Bool))
findSquares 
s': ?m.351986
s' 
(← instantiateMVars (← inferType h)): ?m.352133
(← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars
(← instantiateMVars (← inferType h)): ?m.352133
 
(← inferType h): ?m.352047
(← 
inferType: Expr → MetaM Expr
inferType
(← inferType h): ?m.352047
 
h: ?m.351983
h
(← inferType h): ?m.352047
)
(← instantiateMVars (← inferType h)): ?m.352133
))
      
HashSet.empty: {α : Type ?u.352165} → [inst : BEq α] → [inst_1 : Hashable α] → HashSet α
HashSet.empty
    let 
new_es: ?m.352367
new_es ← 
s: ?m.352257
s.
foldM: {α : Type ?u.352302} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {δ : Type ?u.352301} →
        {m : Type ?u.352301 → Type ?u.352301} → [inst : Monad m] → (δ → α → m δ) → δ → HashSet α → m δ
foldM (fun 
new_es: ?m.352346
new_es (⟨
e: Expr
e, 
is_sq: Bool
is_sq⟩ : Expr × Bool) =>
      ((do
        let 
p: ?m.353890
p ← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM (if 
is_sq: Bool
is_sq then ``
sq_nonneg: ∀ {R : Type u_1} [inst : LinearOrderedRing R] (a : R), 0 ≤ a ^ 2
sq_nonneg else ``
mul_self_nonneg: ∀ {α : Type u} [inst : LinearOrderedRing α] (a : α), 0 ≤ a * a
mul_self_nonneg) #[
e: Expr
e]
        
pure: {f : Type ?u.353893 → Type ?u.353892} → [self : Pure f] → {α : Type ?u.353893} → α → f α
pure $ 
p: ?m.353890
p::
new_es: ?m.352346
new_es) <|> 
pure: {f : Type ?u.353673 → Type ?u.353672} → [self : Pure f] → {α : Type ?u.353673} → α → f α
pure 
new_es: ?m.352346
new_es)) (
[]: List ?m.352360
[] : 
List: Type ?u.352358 → Type ?u.352358
List 
Expr: Type
Expr)
    let 
new_es: ?m.352422
new_es ← 
compWithZero: Preprocessor
compWithZero.
globalize: Preprocessor → GlobalPreprocessor
globalize.
transform: GlobalPreprocessor → List Expr → MetaM (List Expr)
transform 
new_es: ?m.352367
new_es
    trace[linarith] "nlinarith preprocessing found squares"
    trace[linarith] "{
s: ?m.352257
s.
toList: {α : Type ?u.353612} → {x : BEq α} → {x_1 : Hashable α} → HashSet α → List α
toList}"
    
linarithTraceProofs: {α : Type} → [inst : ToMessageData α] → α → List Expr → MetaM Unit
linarithTraceProofs 
"so we added proofs": String
"so we added proofs" 
new_es: ?m.352422
new_es
    let 
with_comps: ?m.355192
with_comps ← (
new_es: ?m.352422
new_es ++ 
ls: ?m.351878
ls).
mapM: {m : Type ?u.354710 → Type ?u.354709} →
  [inst : Monad m] → {α : Type ?u.354708} → {β : Type ?u.354710} → (α → m β) → List α → m (List β)
mapM (fun 
e: ?m.354749
e => do
      let 
tp: ?m.354809
tp ← 
inferType: Expr → MetaM Expr
inferType 
e: ?m.354749
e
      try
        let ⟨
ine: Ineq
ine, _⟩ ← 
parseCompAndExpr: Expr → MetaM (Ineq × Expr)
parseCompAndExpr 
tp: ?m.354809
tp
        
pure: {f : Type ?u.354909 → Type ?u.354908} → [self : Pure f] → {α : Type ?u.354909} → α → f α
pure (
ine: Ineq
ine, 
e: ?m.354749
e)
      catch 
_: ?m.355001
_ => 
pure: {f : Type ?u.355004 → Type ?u.355003} → [self : Pure f] → {α : Type ?u.355004} → α → f α
pure (
Ineq.lt: Ineq
Ineq.lt, 
e: ?m.354749
e))
    let 
products: ?m.355294
products ← 
with_comps: ?m.355192
with_comps.
mapDiagM: {m : Type ?u.355238 → Type ?u.355237} →
  {α : Type ?u.355236} → {β : Type ?u.355238} → [inst : Monad m] → (α → α → m β) → List α → m (List β)
mapDiagM $ fun (⟨
posa: Ineq
posa, 
a: Expr
a⟩ : Ineq × Expr) ⟨
posb: Ineq
posb, 
b: Expr
b⟩ =>
      try
        (
some: {α : Type ?u.355472} → α → Option α
some <$> match 
posa: Ineq
posa, 
posb: Ineq
posb with
          | 
Ineq.eq: Ineq
Ineq.eq, _ => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
zero_mul_eq: ∀ {α : Type u_1} {R : α → α → Prop} [inst : Semiring α] {a b : α}, a = 0 → R b 0 → a * b = 0
zero_mul_eq #[
a: Expr
a, 
b: Expr
b]
          | _, 
Ineq.eq: Ineq
Ineq.eq => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
mul_zero_eq: ∀ {α : Type u_1} {R : α → α → Prop} [inst : Semiring α] {a b : α}, R a 0 → b = 0 → a * b = 0
mul_zero_eq #[
a: Expr
a, 
b: Expr
b]
          | 
Ineq.lt: Ineq
Ineq.lt, 
Ineq.lt: Ineq
Ineq.lt => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
mul_pos_of_neg_of_neg: ∀ {α : Type u} [inst : StrictOrderedRing α] {a b : α}, a < 0 → b < 0 → 0 < a * b
mul_pos_of_neg_of_neg #[
a: Expr
a, 
b: Expr
b]
          | 
Ineq.lt: Ineq
Ineq.lt, 
Ineq.le: Ineq
Ineq.le => do
              let 
a: ?m.355635
a ← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
le_of_lt: ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt #[
a: Expr
a]
              
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
mul_nonneg_of_nonpos_of_nonpos: ∀ {α : Type u} [inst : OrderedRing α] {a b : α}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b
mul_nonneg_of_nonpos_of_nonpos #[
a: ?m.355635
a, 
b: Expr
b]
          | 
Ineq.le: Ineq
Ineq.le, 
Ineq.lt: Ineq
Ineq.lt => do
              let 
b: ?m.355734
b ← 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
le_of_lt: ∀ {α : Type u} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt #[
b: Expr
b]
              
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
mul_nonneg_of_nonpos_of_nonpos: ∀ {α : Type u} [inst : OrderedRing α] {a b : α}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b
mul_nonneg_of_nonpos_of_nonpos #[
a: Expr
a, 
b: ?m.355734
b]
          | 
Ineq.le: Ineq
Ineq.le, 
Ineq.le: Ineq
Ineq.le => 
mkAppM: Name → Array Expr → MetaM Expr
mkAppM ``
mul_nonneg_of_nonpos_of_nonpos: ∀ {α : Type u} [inst : OrderedRing α] {a b : α}, a ≤ 0 → b ≤ 0 → 0 ≤ a * b
mul_nonneg_of_nonpos_of_nonpos #[
a: Expr
a, 
b: Expr
b])
      catch 
_: ?m.355985
_ => 
pure: {f : Type ?u.355988 → Type ?u.355987} → [self : Pure f] → {α : Type ?u.355988} → α → f α
pure 
none: {α : Type ?u.356012} → Option α
none
    let 
products: ?m.355354
products ← 
compWithZero: Preprocessor
compWithZero.
globalize: Preprocessor → GlobalPreprocessor
globalize.
transform: GlobalPreprocessor → List Expr → MetaM (List Expr)
transform 
products: ?m.355294
products.
reduceOption: {α : Type ?u.355343} → List (Option α) → List α
reduceOption
    return (
new_es: ?m.352422
new_es ++ 
ls: ?m.351878
ls ++ 
products: ?m.355354
products)

end nlinarith

-- TODO the `removeNe` preprocesor
section removeNe
-- /--
-- `remove_ne_aux` case splits on any proof `h : a ≠ b` in the input,
-- turning it into `a < b ∨ a > b`.
-- This produces `2^n` branches when there are `n` such hypotheses in the input.
-- -/
-- meta def remove_ne_aux : list expr → tactic (list branch) :=
-- λ hs,
-- (do e ← hs.mfind (λ e : expr, do e ← infer_type e, guard $ e.is_ne.is_some),
--     [(_, ng1), (_, ng2)] ← to_expr ``(or.elim (lt_or_gt_of_ne %%e)) >>= apply,
--     let do_goal : expr → tactic (list branch) := λ g,
--       do set_goals [g],
--          h ← intro1,
--          ls ← remove_ne_aux $ hs.remove_all [e],
--          return $ ls.map (λ b : branch, (b.1, h::b.2)) in
--     (++) <$> do_goal ng1 <*> do_goal ng2)
-- <|> do g ← get_goal, return [(g, hs)]

-- /--
-- `remove_ne` case splits on any proof `h : a ≠ b` in the input, turning it into `a < b ∨ a > b`,
-- by calling `linarith.remove_ne_aux`.
-- This produces `2^n` branches when there are `n` such hypotheses in the input.
-- -/
-- meta def remove_ne : global_branching_preprocessor :=
-- { name := "remove_ne",
--   transform := remove_ne_aux }
end removeNe


/--
The default list of preprocessors, in the order they should typically run.
-/
def 
defaultPreprocessors: List GlobalBranchingPreprocessor
defaultPreprocessors : 
List: Type ?u.366111 → Type ?u.366111
List 
GlobalBranchingPreprocessor: Type
GlobalBranchingPreprocessor :=
  [
filterComparisons: Preprocessor
filterComparisons, 
removeNegations: Preprocessor
removeNegations, 
natToInt: GlobalBranchingPreprocessor
natToInt, 
strengthenStrictInt: Preprocessor
strengthenStrictInt,
    
compWithZero: Preprocessor
compWithZero, 
cancelDenoms: Preprocessor
cancelDenoms]

/--
`preprocess pps l` takes a list `l` of proofs of propositions.
It maps each preprocessor `pp ∈ pps` over this list.
The preprocessors are run sequentially: each receives the output of the previous one.
Note that a preprocessor may produce multiple or no expressions from each input expression,
so the size of the list may change.
-/
def 
preprocess: List GlobalBranchingPreprocessor → MVarId → List Expr → MetaM (List Branch)
preprocess (
pps: List GlobalBranchingPreprocessor
pps : 
List: Type ?u.366783 → Type ?u.366783
List 
GlobalBranchingPreprocessor: Type
GlobalBranchingPreprocessor) (
g: MVarId
g : 
MVarId: Type
MVarId) (
l: List Expr
l : 
List: Type ?u.366788 → Type ?u.366788
List 
Expr: Type
Expr) :
    
MetaM: Type → Type
MetaM (
List: Type ?u.366791 → Type ?u.366791
List 
Branch: Type
Branch) :=
  
pps: List GlobalBranchingPreprocessor
pps.
foldlM: {m : Type ?u.366801 → Type ?u.366800} →
  [inst : Monad m] → {s : Type ?u.366801} → {α : Type ?u.366799} → (s → α → m s) → s → List α → m s
foldlM (fun 
ls: ?m.366841
ls 
pp: ?m.366844
pp => return 
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
(← 
ls: ?m.366841
ls
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
.
mapM: {m : Type ?u.366909 → Type ?u.366908} →
  [inst : Monad m] → {α : Type ?u.366907} → {β : Type ?u.366909} → (α → m β) → List α → m (List β)
mapM
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
 
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
fun
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
 (
g: MVarId
g
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
, 
l: List Expr
l
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
) => 
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
do
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
 
pp: ?m.366844
pp
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
.
process: GlobalBranchingPreprocessor → MVarId → List Expr → MetaM (List Branch)
process
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
 
g: MVarId
g
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
 
l: List Expr
l
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
).
join: {α : Type ?u.366992} → List (List α) → List α
join) [(
g: MVarId
g, 
l: List Expr
l)]

end Linarith