mkHigherOrderType — Mathlib

Lean4
/-- From a lemma of the shape `∀ x, f (g x) = h x`
derive an auxiliary lemma of the form `f ∘ g = h`
for reasoning about higher-order functions.
-/
partial def mkHigherOrderType (e : Expr) : MetaM Expr := do
  if not e.isForall then
    throwError"not a forall"
  withLocalDecl e.bindingName! e.binderInfo e.bindingDomain! fun fvar => do
      let body := instantiate1 e.bindingBody! fvar
      if body.isForall then
        let exp ← mkHigherOrderType body
        mkForallFVars #[fvar] exp (binderInfoForMVars := e.binderInfo)
      else
        let some (_, lhs, rhs) ← matchEq? body |
          throwError "not an equality {← ppExpr body}"
        mkEq (← mkComp fvar lhs) (← mkComp fvar rhs)
Похожие утверждения