Documentation

Mathlib.Tactic.Peel

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.

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

    The list of constants that are regarded as being quantifiers.

    Equations
    Instances For

      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

        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

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

          Equations
          Instances For

            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

              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

                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
                Instances For

                  Similar to peelArgs but peels arbitrarily many quantifiers. Returns whether or not any quantifiers were peeled.

                  Peel off a single quantifier from an .

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Peel off quantifiers from an and assign the names given in l to the introduced variables.

                    Equations
                    Instances For