applyIdRule — Mathlib

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

For example, `e = q(Continuous fun x => x)` and `funPropDecl` is `FunPropDecl` for `Continuous`.
-/
def applyIdRule (funPropDecl : FunPropDecl) (e : Expr) (funProp : Expr → FunPropM (Option Result)) :
    FunPropM (Option Result) := do
  let thms ← getLambdaTheorems funPropDecl.funPropName .id
  if thms.size = 0 then
    let msg := s!"missing identity 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
Похожие утверждения