addNegEqProofs

Mathlib.Tactic.Linarith.Verification

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.addNegEqProofs

Lean4

/-- `addNegEqProofs l` inspects the list of proofs `l` for proofs of the form `t = 0`. For each such
proof, it adds a proof of `-t = 0` to the list.
-/
def addNegEqProofs : List Expr → MetaM (List Expr)
  | [] => return []
  | (h :: tl) => do
    let (iq, t) ← parseCompAndExpr (← inferType h)
    match iq with
    | Ineq.eq =>
      do
        let nep := mkAppN (← mkAppM `Iff.mpr #[← mkAppOptM ``neg_eq_zero #[none, none, t]]) #[h]
        let tl ← addNegEqProofs tl
        return h :: nep :: tl
    | _ =>
      return h :: (← addNegEqProofs tl)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru