Lean4
/-- Given a list `hyps` of proofs of comparisons, `runLinarith cfg hyps prefType`
preprocesses `hyps` according to the list of preprocessors in `cfg`.
This results in a list of branches (typically only one),
each of which must succeed in order to close the goal.
In each branch, we partition the list of hypotheses by type, and run `linarith` on each class
in the partition; one of these must succeed in order for `linarith` to succeed on this branch.
If `prefType` is given, it will first use the class of proofs of comparisons over that type.
-/
-- If it succeeds, the passed metavariable should have been assigned.
def runLinarith (cfg : LinarithConfig) (prefType : Option Expr) (g : MVarId) (hyps : List Expr) : MetaM Unit := do
let singleProcess (g : MVarId) (hyps : List Expr) : MetaM Expr :=
g.withContext
(do
linarithTraceProofs (s! "after preprocessing, linarith has {hyps.length} facts:") hyps
let mut hyp_set ← partitionByType hyps
trace[linarith]"hypotheses appear in {hyp_set.size} different types"
let pref : MetaM _ ←
do
if let some t := prefType then
let (i, vs) ← hyp_set.find t
hyp_set := hyp_set.eraseIdxIfInBounds i
pure <|
withTraceNode `linarith (return m!"{(exceptEmoji ·)} running on preferred type {t}") <|
proveFalseByLinarith cfg.transparency cfg.oracle cfg.discharger g vs
else
pure failure
pref <|> findLinarithContradiction cfg g hyp_set.toList)
let mut preprocessors := cfg.preprocessors
if cfg.splitNe then
preprocessors := Linarith.removeNe :: preprocessors
if cfg.splitHypotheses then
preprocessors := Linarith.splitConjunctions.globalize.branching :: preprocessors
let branches ← preprocess preprocessors g hyps
for (g, es) in branches do
let r ← singleProcess g es
g.assign r
(Expr.mvar g).ensureHasNoMVars
