Lean4
/-- Try to prove `e` using *composition lambda theorem*.
For example, `e = q(Continuous fun x => f (g x))` and `funPropDecl` is `FunPropDecl` for
`Continuous`
You also have to provide the functions `f` and `g`. -/
def applyCompRule (funPropDecl : FunPropDecl) (e f g : Expr) (funProp : Expr → FunPropM (Option Result)) :
FunPropM (Option Result) := do
let thms ← getLambdaTheorems funPropDecl.funPropName .comp
if thms.size = 0 then
let msg := s!"missing composition rule to prove `{← ppExpr e}`"
logError msg
trace[Meta.Tactic.fun_prop]
return none
for thm in thms do
let .comp id_f id_g := thm.thmArgs |
return none
if let some r← tryTheoremWithHint? e (.decl thm.thmName) #[(id_f, f), (id_g, g)] funProp then
return r
return none
