splitConjunctions

Mathlib.Tactic.Linarith.Preprocessing

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

Lean4

/-- Processor that recursively replaces `P ∧ Q` hypotheses with the pair `P` and `Q`. -/
partial def splitConjunctions : Preprocessor
    where
  description := "split conjunctions"
  transform := aux
where/-- Implementation of the `splitConjunctions` preprocessor. -/
   aux (proof : Expr) : MetaM (List Expr) := do
    match (← instantiateMVars (← inferType proof)).getAppFnArgs with
    | (``And, #[_, _]) =>
      pure ((← aux (← mkAppM ``And.left #[proof])) ++ (← aux (← mkAppM ``And.right #[proof])))
    | _ =>
      pure [proof]

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

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

Разделы

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

Аффилиация

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