findContradictionWithNle

Mathlib.Tactic.Order

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Order.findContradictionWithNle

Lean4

/-- Using the `≤`-graph `g`, find a contradiction with some `≰`-fact. -/
def findContradictionWithNle (g : Graph) (idxToAtom : Std.HashMap ℕ Expr) (facts : Array AtomicFact) :
    MetaM <| Option Expr := do
  for fact in facts do
    if let .nle lhs rhs proof := fact then
      let some pf ← g.buildTransitiveLeProof idxToAtom lhs rhs |
        continue
      return some <| mkApp proof pf
  return none

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

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

Разделы

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

Аффилиация

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