removeNegations

Mathlib.Tactic.Linarith.Preprocessing

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

Lean4

/-- 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
    where
  description := "replace negations of comparisons"
  transform
    h := do
    let t : Q(Prop) ← whnfR (← inferType h)
    match t with
    | ~q(¬$p) =>
      match ← flipNegatedComparison h (← whnfR p) with
      | some h' =>
        trace[linarith]"removing negation in {h}"
        return [h']
      | _ =>
        return [h]
    | _ =>
      return [h]

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

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

Разделы

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

Аффилиация

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