Lean4
/-- 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
where
description := "move nats to ints"
transform g
l := do
let l ←
l.mapM fun h => do
let t ← whnfR (← instantiateMVars (← inferType h))
if ← isNatProp t then
let (some (h', t'), _) ← Term.TermElabM.run' (run_for g (zifyProof none h t)) |
throwError "zifyProof failed on {h}"
if ← succeeds t'.ineqOrNotIneq? then
pure 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 h
else
pure h
withNewMCtxDepth <|
AtomM.run .reducible <| do
let nonnegs ←
l.foldlM (init := ∅) fun (es : TreeSet (Nat × Nat) lexOrd.compare) h => do
try
let (_, _, a, b) ← (← inferType h).ineq?
let getIndices (p : Expr × Expr) : AtomM (ℕ × ℕ) := do
return ((← AtomM.addAtom p.1).1, (← AtomM.addAtom p.2).1)
let indices_a ← (getNatComparisons a).mapM getIndices
let indices_b ← (getNatComparisons b).mapM getIndices
pure <| (es.insertMany indices_a).insertMany indices_b
catch _ =>
pure es
let atoms : Array Expr := (← get).atoms
let nonneg_pfs : List Expr ←
nonnegs.toList.filterMapM fun p => do
mk_natCast_nonneg_prf (atoms[p.1]!, atoms[p.2]!)
pure [(g, nonneg_pfs ++ l)]
