Lean4
/-- Try to prove `e = q(P (fun x => let y := φ x; ψ x y)`.
For example,
- `funPropDecl` is `FunPropDecl` for `Continuous`
- `e = q(Continuous fun x => let y := φ x; ψ x y)`
- `f = q(fun x => let y := φ x; ψ x y)`
-/
def letCase (funPropDecl : FunPropDecl) (e : Expr) (f : Expr) (funProp : Expr → FunPropM (Option Result)) :
FunPropM (Option Result) := do
match f with
| .lam xName xType (.letE yName yType yValue yBody _) xBi =>
do
let yType := yType.consumeMData
let yValue := yValue.consumeMData
let yBody := yBody.consumeMData
let yType := yType.headBeta
if (yType.hasLooseBVar 0) then
throwError "dependent type encountered {← ppExpr (Expr.forallE xName xType yType default)}"
if ¬(yValue.hasLooseBVar 0) then
let body := yBody.swapBVars 0 1
let e' := mkLet yName yType yValue (e.setArg (funPropDecl.funArgId) (.lam xName xType body xBi))
return ← funProp e'
match (yBody.hasLooseBVar 0), (yBody.hasLooseBVar 1) with
| true, true =>
let f ← mkUncurryFun 2 (Expr.lam xName xType (.lam yName yType yBody default) xBi)
let g :=
Expr.lam xName xType (binderInfo := default)
(mkAppN (← mkConstWithFreshMVarLevels ``Prod.mk) #[xType, yType, .bvar 0, yValue])
applyCompRule funPropDecl e f g funProp
| true, false =>
let f := Expr.lam yName yType yBody default
let g := Expr.lam xName xType yValue default
applyCompRule funPropDecl e f g funProp
| false, _ =>
let f := Expr.lam xName xType (yBody.lowerLooseBVars 1 1) xBi
funProp (e.setArg (funPropDecl.funArgId) f)
| _ =>
throwError"expected expression of the form `fun x => lam y := ..; ..`"
