[Merged by Bors] - feat: add peel tactic

[j-loreaux]

As requested on Zulip.

Given p q : ℕ → Prop, h : ∀ x, p x, and a goal ⊢ : ∀ x, q x, the tactic peel h with h' x 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.

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_peel ε hε N n hn 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.

Co-authored-by: Kyle Miller kmill31415@gmail.com

---

Note: I am completely open to renaming the tactic if a consensus is reached about a better name.

[robertylewis]

This looks awesome!

Could you add some tests that involve type class arguments?

[j-loreaux]

(EDIT: I have added two examples like the one below to the test suite)

@robertylewis can you give an example of what you're looking for? Several of the tests already have expressions that include type classes (e.g., Add, Sub, TopologicalSpace, etc.).

Maybe something like this is what you mean?

example {α : Type*} [CommRing α] (h : ∀ x : α, ∃ y : α, x + y = 2) :
    ∀ x : α, ∃ y : α, (x + y) ^ 2 = 4 := by
  peel 2 h
  rw [this]
  ring

[robertylewis]

@j-loreaux your examples are exactly what I meant, thanks 😄

@PatrickMassot mentioned that typeclass-heavy examples have gotten him into trouble in similar situations. To confirm, Patrick, do Jireh's new tests cover what you were thinking?

[PatrickMassot]

@robertylewis , I think you are referring to the widget issue that was pretty different.

@j-loreaux I think that what is missing are tests that would catch a missing withContext. All your test have peel at the very beginning. We need examples where there are intro before peel and several goals at the time when peel is called.

[kmill]

Here are a few comments

[kmill]

Looks good to me

[PatrickMassot]

Thanks a lot Jireh and Kyle! This is really great.
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style