The `peel` tactic #

peel h with h' idents* tries to apply forall_imp (or Exists.imp, or Filter.Eventually.mp, Filter.Frequently.mp and Filter.eventually_of_forall) with the argument h and uses idents* to introduce variables with the supplied names, giving the "peeled" argument the name h'.

One can provide a numeric argument as in peel 4 h which will peel 4 quantifiers off the expressions automatically name any variables not specifically named in the with clause.

In addition, the user may supply a term e via ... using e in order to close the goal immediately. In particular, peel h using e is equivalent to peel h; exact e. The using syntax may be paired with any of the other features of peel.

source

def Mathlib.Tactic.Peel.peel :

Lean.ParserDescr

Peels matching quantifiers off of a given term and the goal and introduces the relevant variables.

peel e peels all quantifiers (at reducible transparency), using this for the name of the peeled hypothesis.
peel e with h is peel e but names the peeled hypothesis h. If h is _ then uses this for the name of the peeled hypothesis.
peel n e peels n quantifiers (at default transparency).
peel n e with x y z ... h peels n quantifiers, names the peeled hypothesis h, and uses x, y, z, and so on to name the introduced variables; these names may be _. If h is _ then uses this for the name of the peeled hypothesis. The length of the list of variables does not need to equal n.
peel e with x₁ ... xₙ h is peel n e with x₁ ... xₙ h.

There are also variants that apply to an iff in the goal:

peel n peels n quantifiers in an iff.
peel with x₁ ... xₙ peels n quantifiers in an iff and names them.

Given p q : ℕ → Prop, h : ∀ x, p x, and a goal ⊢ : ∀ x, q x, the tactic peel h with x h' will introduce x : ℕ, h' : p x into the context and the new goal will be ⊢ q x. This works with ∃, as well as ∀ᶠ and ∃ᶠ, and it can even be applied to a sequence of quantifiers. Note that this is a logically weaker setup, so using this tactic is not always feasible.

For a more complex example, given a hypothesis and a goal:

h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
⊢ ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε

(which differ only in </≤), applying peel h with ε hε N n hn h_peel will yield a tactic state:

h : ∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε
ε : ℝ
hε : 0 < ε
N n : ℕ
hn : N ≤ n
h_peel : 1 / (n + 1 : ℝ) < ε
⊢ 1 / (n + 1 : ℝ) ≤ ε

and the goal can be closed with exact h_peel.le. Note that in this example, h and the goal are logically equivalent statements, but peel cannot be immediately applied to show that the goal implies h.

In addition, peel supports goals of the form (∀ x, p x) ↔ ∀ x, q x, or likewise for any other quantifier. In this case, there is no hypothesis or term to supply, but otherwise the syntax is the same. So for such goals, the syntax is peel 1 or peel with x, and after which the resulting goal is p x ↔ q x. The congr! tactic can also be applied to goals of this form using congr! 1 with x. While congr! applies congruence lemmas in general, peel can be relied upon to only apply to outermost quantifiers.

Finally, the user may supply a term e via ... using e in order to close the goal immediately. In particular, peel h using e is equivalent to peel h; exact e. The using syntax may be paired with any of the other features of peel.

This tactic works by repeatedly applying lemmas such as forall_imp, Exists.imp, Filter.Eventually.mp, Filter.Frequently.mp, and Filter.eventually_of_forall.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Mathlib.Tactic.Peel.quantifiers :

List Lean.Name

The list of constants that are regarded as being quantifiers.

Equations

Mathlib.Tactic.Peel.quantifiers = [`Exists, `And, `Filter.Eventually, `Filter.Frequently]

Instances For

source

def Mathlib.Tactic.Peel.whnfQuantifier (p : Lean.Expr) (unfold : Bool) :

Lean.MetaM Lean.Expr

If unfold is false then do whnfR, otherwise unfold everything that's not a quantifier, according to the quantifiers list.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Mathlib.Tactic.Peel.throwPeelError {α : Type} (ty : Lean.Expr) (target : Lean.Expr) :

Lean.MetaM α

Throws an error saying ty and target could not be matched up.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Mathlib.Tactic.Peel.mkFreshBinderName (f : Lean.Expr) :

Lean.MetaM Lean.Name

If f is a lambda then use its binding name to generate a new hygienic name, and otherwise choose a new hygienic name.

Equations

Mathlib.Tactic.Peel.mkFreshBinderName f = liftM (Lean.mkFreshUserName (match f with | Lean.Expr.lam n binderType body binderInfo => n | x => `a))

Instances For

source

def Mathlib.Tactic.Peel.applyPeelThm (thm : Lean.Name) (goal : Lean.MVarId) (e : Lean.Expr) (ty : Lean.Expr) (target : Lean.Expr) (n : Lean.Name) (n' : Lean.Name) :

Lean.MetaM (Lean.FVarId × List Lean.MVarId)

Applies a "peel theorem" with two main arguments, where the first is the new goal and the second can be filled in using e. Then it intros two variables with the provided names.

If, for example, goal : ∃ y : α, q y and thm := Exists.imp, the metavariable returned has type q x where x : α has been introduced into the context.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Mathlib.Tactic.Peel.peelCore (goal : Lean.MVarId) (e : Lean.Expr) (n? : Option Lean.Name) (n' : Lean.Name) (unfold : Bool) :

Lean.MetaM (Lean.FVarId × List Lean.MVarId)

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 δ.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Mathlib.Tactic.Peel.peelArgs (e : Lean.Expr) (num : ℕ) (l : List Lean.Name) (n? : Option Lean.Name) (unfold : optParam Bool true) :

Lean.Elab.Tactic.TacticM Unit

Given a list l of names, this peels num quantifiers off of the expression e and the main goal and introduces variables with the provided names until the list of names is exhausted. Note: the name n? (with default this) is used for the name of the expression e with quantifiers peeled.

Equations