findLinarithContradiction — Mathlib

Lean4

/-- Given a list `ls` of lists of proofs of comparisons, `findLinarithContradiction cfg ls` will try to
prove `False` by calling `linarith` on each list in succession. It will stop at the first proof of
`False`, and fail if no contradiction is found with any list.
-/
def findLinarithContradiction (cfg : LinarithConfig) (g : MVarId) (ls : List (Expr × List Expr)) : MetaM Expr :=
  try
    ls.firstM
        (fun ⟨α, L⟩ =>
          withTraceNode `linarith (return m!"{(exceptEmoji ·)} running on type {α}") <|
            proveFalseByLinarith cfg.transparency cfg.oracle cfg.discharger g L)
  catch e =>
    throwError "linarith failed to find a contradiction\n{g }\n{e.toMessageData}"

Похожие утверждения