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 else if
a: Expr
a
.
equal: Expr β†’ Expr β†’ Bool
equal
b: Expr
b
then .eq else .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: 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: (Ξ± : 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.
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
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), _]) => 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), _]), _ =>
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), _]) => 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), _]), _ =>
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), _]) => 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), _]), _ =>
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), _]) =>
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), _]), _ =>
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), _]) =>
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), _]), _ =>
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 => throwError "couldn't rearrange comparison {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,
lhs': Expr
lhs'
) ←
CancelDenoms.derive: Expr β†’ MetaM (β„• Γ— Expr)
CancelDenoms.derive
lhs: Expr
lhs
if 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
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: (Ξ± : 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 => do let
s: ?m.346889
s
←
findSquares: HashSet (Expr Γ— Bool) β†’ Expr β†’ MetaM (HashSet (Expr Γ— Bool))
findSquares
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 | (
``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
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 | _ =>
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 /-- `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.
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.
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,
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: Type ?u.366783 β†’ Type ?u.366783
List
GlobalBranchingPreprocessor: Type
GlobalBranchingPreprocessor
) (g :
MVarId: Type
MVarId
) (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.
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
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
,
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
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
l
(← ls.mapM fun (g, l) => do pp.process g l): ?m.366965
)
.
join: {Ξ± : Type ?u.366992} β†’ List (List Ξ±) β†’ List Ξ±
join
) [(g, l)] end Linarith