solveByElim

Mathlib.Tactic.Propose

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Propose.solveByElim

Lean4

/-- Shortcut for calling `solveByElim`. -/
def solveByElim (orig : MVarId) (goals : Array MVarId) (use : Array Expr) (required : Array Expr) (depth) := do
  let cfg : SolveByElimConfig := { maxDepth := depth, exfalso := true, symm := true, intro := false }
  let cfg :=
    if !required.isEmpty then
      cfg.testSolutions
        (fun _ => do
          let r ← instantiateMVars (.mvar orig)
          pure <| required.all fun e => e.occurs r)
    else cfg
  let cfg := cfg.synthInstance
  _ ← SolveByElim.solveByElim cfg (use.toList.map pure) (fun _ => return (← getLocalHyps).toList) goals.toList

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

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

Разделы

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

Аффилиация

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