Lean4
/-- This is the core to the `peel` tactic.
It tries to match `e` and `goal` as quantified statements (using `∀` and the quantifiers in
the `quantifiers` list), then applies "peel theorems" using `applyPeelThm`.
We treat `∧` as a quantifier for sake of dealing with quantified statements
like `∃ δ > (0 : ℝ), q δ`, which is notation for `∃ δ, δ > (0 : ℝ) ∧ q δ`. -/
def peelCore (goal : MVarId) (e : Expr) (n? : Option Name) (n' : Name) (unfold : Bool) : MetaM (FVarId × List MVarId) :=
goal.withContext
(do
let ty ← whnfQuantifier (← inferType e) unfold
let target ← whnfQuantifier (← goal.getType) unfold
if ty.isForall && target.isForall then
applyPeelThm ``forall_imp goal e ty target (← n?.getDM (mkFreshUserName target.bindingName!)) n'
else if ty.getAppFn.isConst && ty.getAppNumArgs == target.getAppNumArgs && ty.getAppFn == target.getAppFn then
match target.getAppFnArgs with
| (``Exists, #[_, p]) =>
applyPeelThm ``Exists.imp goal e ty target (← n?.getDM (mkFreshBinderName p)) n'
| (``And, #[_, _]) =>
applyPeelThm ``and_imp_left_of_imp_imp goal e ty target (← n?.getDM (mkFreshUserName `p)) n'
| (``Filter.Eventually, #[_, p, _]) =>
applyPeelThm ``eventually_imp goal e ty target (← n?.getDM (mkFreshBinderName p)) n'
| (``Filter.Frequently, #[_, p, _]) =>
applyPeelThm ``frequently_imp goal e ty target (← n?.getDM (mkFreshBinderName p)) n'
| _ =>
throwPeelError ty target
else
throwPeelError ty target)
