Lean4
/-- Prove function property of using *morphism theorems*. -/
def applyMorRules (funPropDecl : FunPropDecl) (e : Expr) (fData : FunctionData)
(funProp : Expr → FunPropM (Option Result)) : FunPropM (Option Result) := do
trace[Debug.Meta.Tactic.fun_prop]"applying morphism theorems to {← ppExpr e}"
match ← fData.isMorApplication with
| .none =>
throwError "fun_prop bug: invalid use of mor rules on {← ppExpr e}"
| .underApplied =>
applyPiRule funPropDecl e funProp
| .overApplied =>
let some (f, g) ← fData.peeloffArgDecomposition |
return none
applyCompRule funPropDecl e f g funProp
| .exact =>
let candidates ← getMorphismTheorems e
trace[Meta.Tactic.fun_prop]"candidate morphism theorems: {← candidates.mapM fun c => ppOrigin (.decl c.thmName)}"
for c in candidates do
if let some r← tryTheorem? e (.decl c.thmName) funProp then
return r
trace[Debug.Meta.Tactic.fun_prop]"no theorem matched"
return none
