Lean4
/-- Try to remove applied argument i.e. prove `P (fun x => f x y)` from `P (fun x => f x)`.
For example
- `funPropDecl` is `FunPropDecl` for `Continuous`
- `e = q(Continuous fun x => foo (bar x) y)`
- `fData` contains info on `fun x => foo (bar x) y`
This tries to prove `Continuous fun x => foo (bar x) y` from `Continuous fun x => foo (bar x)`
-/
def removeArgRule (funPropDecl : FunPropDecl) (e : Expr) (fData : FunctionData)
(funProp : Expr → FunPropM (Option Result)) : FunPropM (Option Result) := do
match h : fData.args.size with
| 0 =>
throwError "fun_prop bug: invalid use of remove arg case {← ppExpr e}"
| n + 1 =>
let arg := fData.args[n]
if arg.coe.isSome then
-- if have to apply morphisms rules if we deal with morphisms
return ← applyMorRules funPropDecl e fData funProp
else
let some (f, g) ← fData.peeloffArgDecomposition |
return none
applyCompRule funPropDecl e f g funProp
