refutationFor

Mathlib.Tactic.CC

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCState.refutationFor

Lean4

/-- `refutationFor cc e` constructs a proof for `Not e` if it is equivalent to `False` in `CCState`
-/
def refutationFor (ccs : CCState) (e : Expr) : MetaM Expr := do
  let (some r, _) ← CCM.run (CCM.getEqProof e (.const ``False [])) { ccs with } |
    throwError"CCState.refutationFor failed to build proof"
  mkAppM ``of_eq_false #[r]

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

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

Разделы

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

Аффилиация

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