applyPiRule — Mathlib

Lean4
/-- Try to prove `e` using *pi lambda theorem*.

For example, `e = q(Continuous fun x y => f x y)` and `funPropDecl` is `FunPropDecl` for
`Continuous`
-/
def applyPiRule (funPropDecl : FunPropDecl) (e : Expr) (funProp : Expr → FunPropM (Option Result)) :
    FunPropM (Option Result) := do
  let thms ← getLambdaTheorems funPropDecl.funPropName .pi
  if thms.size = 0 then
    let msg := s!"missing pi rule to prove `{← ppExpr e}`"
    logError msg
    trace[Meta.Tactic.fun_prop]
    return none
  for thm in thms do
    if let some r← tryTheoremWithHint? e (.decl thm.thmName) #[] funProp then
      return r
  return none
Похожие утверждения