Logical congruence or weakening tactic

Stream: mathlib4

[Patrick Massot]

Something that comes up from time is I don' t think we have a tactic that will allow to prove a goal with a complicated logical structure using an expression with the same structure but not quite matching. For instance consider

import Mathlib.Tactic

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  - n := sorry

I want to run a single tactic bringing me to a tactic state with data x y ε N n, assumptions ε > 0 and n ≥ N and goal x + n = y + ε ↔ x - ε = y - n or, even better, goal x + n = y + ε → x - ε = y - n. Various ways of not really achieving this goal are:

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
     ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  -n := by
  convert h using 6

  constructor
  all_goals { intro ; linarith}

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  -n := by
  revert h
  apply Iff.mp
  congrm ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, ?_

  constructor
  all_goals { intro ; linarith}

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  -n := by
  refine forall_imp ?_ h
  intro
  apply forall_imp
  intro
  apply Exists.imp
  intro
  apply forall_imp
  intro
  apply forall_imp
  intro
  intro
  linarith

An example where the deep goal is not an equivalence would be

lemma inv_succ_lt_all : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε := by
  convert Metric.tendsto_atTop.mp tendsto_one_div_add_atTop_nhds_0_nat using 0
  simp only [Real.dist_0_eq_abs, fun n : ℕ ↦ abs_of_pos (Nat.one_div_pos_of_nat (α := ℝ) (n := n))]

lemma inv_succ_lt_all' : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := sorry

Proving the second lemma from the first one is extremely frustrating for students (this happened to @Claus Clausen this morning for instance). Of course it's doable, but it's frustrating. A principled way to do it is again

lemma inv_succ_lt_all' : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := by
  refine forall_imp ?_ inv_succ_lt_all
  intro
  apply forall_imp
  intro
  apply Exists.imp
  intro
  apply forall_imp
  intro
  apply forall_imp
  intro
  intro

  exact LT.lt.le ‹_›

But I think this deserves a tactic. One tricky part is to generate names without being too unhygienic.

[Kevin Buzzard]

This reminds me of the question I ask every January.

[Patrick Massot]

Indeed this is not the first time we have this conversation. I don't know if you remember but back in the old days of the perfectoid spaces project I cooked up a broken version of this tactic.

[Kevin Buzzard]

@Jireh Loreaux what do you think of this challenge? :-)

[Patrick Massot]

If found it! https://github.com/leanprover-community/lean-perfectoid-spaces/blob/95a6520ce578b30a80b4c36e36ab2d559a842690/src/for_mathlib/uniform_space/group_basis.lean#L13-L25

[Kevin Buzzard]

Great, now run it through mathport :-) </joke>

[Patrick Massot]

I want a non-broken one, just for a change.

[Jireh Loreaux]

I'll give it a shot.

[Eric Wieser]

Is this something that could be in the realm of gcongr?

[Patrick Massot]

It is similar in spirit but formally doesn't fit.

[Eric Wieser]

Even under the viewpoint that implication is "just" ≤ on propositions?

[Jireh Loreaux]

@Patrick Massot This is my first real foray into metaprogramming on my own, so I'm sure this has bugs or missing features, and is poorly written, but it seems to work on the examples you provided (find them at the end of the snippet). I can already see a few places for improvement, but I wanted to get your feedback first.

import Mathlib.Tactic

open Lean Expr Meta Qq

lemma and_imp_left_of_imp_imp {p q r : Prop} (h : r → p → q) : r ∧ p → r ∧ q := by tauto

def peelQuantifier (goal : MVarId) (e : Expr) (n : Option Name := none) : MetaM MVarId := do
  goal.withContext do
    let ty : Q(Prop) ← whnfR (← inferType e)
    let target : Q(Prop) ← whnfR (← goal.getType)
    unless (← isProp ty) && (← isProp target) do
      return goal
    match ty, target with
      | .forallE _ t₁ b₁ _, .forallE n₂ t₂ b₂ c => do
        unless ← isDefEq (← whnfR t₁) (← whnfR t₂) do
          return goal
        let all_imp ← mkFreshExprMVar <| ← withoutModifyingState <| withLocalDecl n₂ c t₂ fun x => do
          let type₁ := b₁.instantiate1 x
          let type₂ := b₂.instantiate1 x
          mkForallFVars #[x] (← mkArrow type₁ type₂)
        goal.assign (← mkAppM ``forall_imp #[all_imp, e])
        let (_, new_goal) ← all_imp.mvarId!.intro (n.getD n₂)
        return new_goal
      | ~q(∃ x : $t₁, $p x), ~q(∃ x : $t₂, $q x) => do
        unless ← isDefEq (← whnfR t₁) (← whnfR t₂) do
          return goal
        let q : Q($t₁ → Prop) := q
        let all_imp : Q(Prop) ← mkFreshExprMVar q(∀ x : $t₁, $p x → $q x)
        goal.assign (← mkAppM ``Exists.imp #[all_imp, e])
        let (_, new_goal) ← all_imp.mvarId!.intro (n.getD `_)
        return new_goal
      | ~q($r ∧ $p), ~q($r' ∧ $q) => do
        unless ← isDefEq q($r) q($r') do
          return goal
        let and_imp ← mkFreshExprMVar q($r' → $p → $q)
        goal.assign (← mkAppM ``and_imp_left_of_imp_imp #[and_imp, e])
        let (_, new_goal) ← and_imp.mvarId!.intro (n.getD `_)
        return new_goal
      | _, _ => do
        return goal

def peelTacAux (e : TSyntax `ident) (n : Option (TSyntax `ident)) : Elab.Tactic.TacticM Unit :=
  Elab.Tactic.withMainContext do
    let e ← Elab.Term.elabTerm e none
    match n with
    | .some n =>
    Elab.Tactic.liftMetaTactic (fun g ↦ return [(← peelQuantifier g e (n := .some n.getId))])
    | .none => Elab.Tactic.liftMetaTactic (fun g ↦ return [(← peelQuantifier g e)])

syntax (name := peel) "peel" ident (colGt ident)? : tactic
@[tactic peel] def peelTac : Elab.Tactic.Tactic := fun stx => do
  match stx with
  | `(tactic| peel $e:ident) => peelTacAux e none
  | `(tactic| peel $e:ident $n:ident) => peelTacAux e (.some n)
  | _ => Elab.throwUnsupportedSyntax

syntax (name := zoom) "zoom" ident ((colGt ident)*)? : tactic
macro_rules
  | `(tactic| zoom $h:ident) => `(tactic| peel $h; intro h'; try (replace $h := h'; clear h'))
  | `(tactic| zoom $h:ident $n:ident) => `(tactic| peel $h $n; intro h'; try (replace $h := h'; clear h'))
  | `(tactic| zoom $h:ident $n:ident $ns:ident*) => `(tactic| zoom $h $n; zoom $h $ns:ident*)

example (p q : Nat → Prop) (h : ∀ y, p y) (h₁ : ∀ z, p z → q z) : ∀ x, q x := by
  zoom h n
  exact h₁ n h
  done

example (p q : Nat → Prop) (h : ∃ y, p y) (h₁ : ∀ z, p z → q z) : ∃ x, q x := by
  zoom h x
  exact h₁ x h
  done

example (p q : Nat → Prop) (h : ∀ y, p y) (h₁ : ∀ z, p z → q z) : ∀ x, q x := by
  zoom h x
  exact h₁ x h
  done

example (p q : ℝ → ℝ → Prop) (h : ∀ ε > 0, ∃ δ > 0, p ε δ)
    (hpq : ∀ x y, x > 0 → y > 0 → p x y → q x y) :
    ∀ ε > 0, ∃ δ > 0, q ε δ := by
  zoom h ε hε δ hδ
  exact hpq ε δ hε hδ h

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  - n := by
  zoom h ε hε N n hn
  linarith

lemma inv_succ_lt_all : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε := by
  convert Metric.tendsto_atTop.mp tendsto_one_div_add_atTop_nhds_0_nat using 0
  simp only [Real.dist_0_eq_abs, fun n : ℕ ↦ abs_of_pos (Nat.one_div_pos_of_nat (α := ℝ) (n := n))]

lemma inv_succ_lt_all' : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := by
  have h := inv_succ_lt_all -- right now `zoom` only accepts `ident`s, not a supplied `term`.
  zoom h ε hε N n hn
  exact h.le

[Patrick Massot]

This is fantastic! Thanks a lot for working on this.

[Patrick Massot]

I think the syntax is not consistent with other tactics. I would expect the with token to introduce the name lists. This will probably make it easier to take in an arbitrary expression instead of the name of a local declaration.

[Jireh Loreaux]

Hold on, I think I can do that in a few seconds. Meh, my janky replace business was getting in the way, may take me a bit longer.

[Jireh Loreaux]

Okay, I plan to clean it up and add the following features:

1. use with, and then allow terms instead of just idents
2. proper handling of userName by making fresh ones
3. take an optional numeric argument which allows for setting the depth without specifying variable names

[Jireh Loreaux]

Let me know if there's anything else you want it to do.

[Patrick Massot]

I don't feel confident enough in meta-programming to review meta-code written by others. But I want to point out a potential trap since you are not yet an expert. I think it's fine in your case, but I always get nervous when I see nested nested actions as in your code. Do you understand why the two functions myFun and myFun' do not return the same result in the code below?

abbrev M := StateT Nat Id

def f : M Nat → M Nat := fun n ↦ do
  set 5
  return ← n

def g : Nat → M Nat := fun n ↦ do
  return n + (← get)

def myFun : M Nat := do
  return ← f <| g (← get)

#eval myFun.run' 0  -- says 5

def myFun' : M Nat := do
  return ← f <| do g (← get)

#eval myFun'.run' 0  -- says 10

[Patrick Massot]

Let me tag @David Thrane Christiansen since I don't remember if #fpil warns about that specific version of this footgun.

[Vincent Beffara]

This zoom tactic seems very useful! It would probably feel more natural to have roughly the same syntax as filter_upwards though (zoom [h] with n or something of that kind). And possibly make zoom accept eventually as a quantifier ?

[Patrick Massot]

I don't understand the last sentence.

[Vincent Beffara]

That's because I don't understand filters :-)

[Patrick Massot]

Could you give an example of what you would like to see as tactic state before and after applying the tactic?

[Vincent Beffara]

The way zoom treats \forall feels a lot like the way filter_upwards treats eventually

[Patrick Massot]

Oh I see, you want a version that handle eventually and frequently where the current one handles forall and exists?

[Vincent Beffara]

Yes, exactly. They seem to fill the same purpose, might as well be the same tactic

[Vincent Beffara]

(I don't "want" it, I am just wondering if it would make sense.)

[Vincent Beffara]

example {x y : ℝ} {f : ℝ → ℝ} (h : ∀ x : ℝ, ∀ᶠ y in 𝓝 x, |f y - f x| ≤ |y - x|) :
    ∀ x : ℝ, ∀ᶠ y in 𝓝 x, |(f y - f x) ^ 2| ≤ |y - x| ^ 2 := by
  zoom h x y
/-
f: ℝ → ℝ
x y: ℝ
h: |f y - f x| ≤ |y - x|
⊢ |(f y - f x) ^ 2| ≤ |y - x| ^ 2
-/

[Patrick Massot]

Yes, I think this would be a nice extension.

[Patrick Massot]

However it would not really replace filter_upwards which can take several arguments.

[Vincent Beffara]

zoom [h1, h2] with x ? As in

example (p q : Nat → Prop) (h : ∀ y, p y) (h₁ : ∀ z, p z → q z) : ∀ x, q x := by
  zoom [h, h₁] with x h h₁ using h₁ h
  done

[Joachim Breitner]

Judging from the examples, this tactic looks like a variant of intro that also specializes a bunch of hypothesea using the intro'ed terms. Is that correct? I wonder if there is a name other than zoom that conveys this intuition better (or conveys the right intuition if this one is wrong).
Maybe something along the lines of

intros x y specializing h1 h2

Hmm, I guess it does more than just intro, and supports other quantifiers as well. Nevermind that particular suggestion then .

[Vincent Beffara]

To be even more similar to filter_upwards, the zoom [h, h₁] with x h h₁ using h₁ h case would feel like this:

example (p q : Nat → Prop) (h : ∀ y, p y) (h₁ : ∀ z, p z → q z) : ∀ x, q x := by
  rw [← Filter.eventually_top] at h h₁ ⊢
  filter_upwards [h, h₁] with x h h₁ using h₁ h

[Patrick Massot]

I also think the name isn't great, but I didn't to derail the conversation into bike shedding before we agree on the technical core.

[Jireh Loreaux]

Yeah, the zoom name was just a placeholder.

[Jireh Loreaux]

Patrick, thanks for that example and warning. I understand why the results are what they are, but I don't yet feel it deep enough in my bones that I would have spotted it without prompting. Do you have a suggestion for how I should be de-nestifying my dos? Just one example of how the code should be transformed would be enough.

[Jireh Loreaux]

Adding support for ∀ᶠ and ∃ᶠ should be relatively straightforward.

[Patrick Massot]

I don't know if we should de-nestify. You should simply know that if you find an incomprehensible bug where Lean seems to ignore a withWhatever or withoutModifyingWhatever then this issue is probably the cause.

[Patrick Massot]

If you want to explicitly say "I know where this nested action will bubble up" then you can simply bubble it yourself, as in:

def myFun : M Nat := do
  let x ← get
  return ← f <| g x

which is what myFun was doing in my example.

[Patrick Massot]

The problem is that what you usually want it the opposite behavior. For this I don't know any alternative to insert the missing do.

[Patrick Massot]

Maybe @Kyle Miller wants to comment on this since we hit that issue several times while coding together.

[Jireh Loreaux]

I'm mostly happy with this now, so let the bikeshedding begin.

peel tactic

import Mathlib.Tactic

open Lean Expr Meta Qq Elab Tactic

lemma and_imp_left_of_imp_imp {p q r : Prop} (h : r → p → q) : r ∧ p → r ∧ q := by tauto

def peelQuantifier (goal : MVarId) (e : Expr) (n : Option Name := none) (n' : Option Name := none) :
    MetaM (List MVarId) := goal.withContext do
  let ty : Q(Prop) ← whnfR (← inferType e)
  let target : Q(Prop) ← whnfR (← goal.getType)
  let freshName ← mkFreshUserName `h_peel
  unless (← isProp ty) && (← isProp target) do
    return [goal]
  match ty, target with
    | .forallE _ t₁ b₁ _, .forallE n₂ t₂ b₂ c => do
      unless ← isDefEq (← whnfR t₁) (← whnfR t₂) do
        return [goal]
      let all_imp ← mkFreshExprMVar <| ← withoutModifyingState <| withLocalDecl n₂ c t₂ fun x => do
        mkForallFVars #[x] (← mkArrow (b₁.instantiate1 x) (b₂.instantiate1 x))
      goal.assign (← mkAppM ``forall_imp #[all_imp, e])
      let (_, new_goal) ← all_imp.mvarId!.introN 2 [n.getD n₂, n'.getD freshName]
      return [new_goal]
    | ~q(∃ x : $α₁, $p x), ~q(∃ x : $α₂, $q x) => do
      unless ← isDefEq (← whnfR α₁) (← whnfR α₂) do
        return [goal]
      let p : Q($α₂ → Prop) := p
      let e : Q(∃ x : $α₂, $p x) := e
      let all_imp : Q(∀ x : $α₂, $p x → $q x) ← mkFreshExprMVar q(∀ x : $α₂, $p x → $q x)
      goal.assign q(Exists.imp $all_imp $e)
      let (_, new_goal) ← all_imp.mvarId!.introN 2 [n.getD `_, n'.getD freshName]
      return [new_goal]
    | ~q($r ∧ $p), ~q($r' ∧ $q) => do
      unless ← isDefEq q($r) q($r') do
        return [goal]
      let and_imp : Q($r' → $p → $q) ← mkFreshExprMVar q($r' → $p → $q)
      let e : Q($r' ∧ $p) := e
      goal.assign q(and_imp_left_of_imp_imp $and_imp $e)
      let (_, new_goal) ← and_imp.mvarId!.introN 2 [n.getD `_, n'.getD freshName]
      return [new_goal]
    | ~q(∀ᶠ (x : $α₁) in $f₁, $p x), ~q(∀ᶠ (x : $α₂) in $f₂, $q x) => do
      unless (← isDefEq (← whnfR α₁) (← whnfR α₂)) && (← isDefEq (← whnfR f₁) (← whnfR f₂)) do
        return [goal]
      let p : Q($α₂ → Prop) := p
      let e : Q(∀ᶠ (x : $α₂) in $f₂, $p x) := e
      let all_imp : Q(∀ x : $α₂, $p x → $q x) ← mkFreshExprMVar q(∀ x : $α₂, $p x → $q x)
      goal.assign q(Filter.Eventually.mp $e (Filter.eventually_of_forall $all_imp))
      let (_, new_goal) ← all_imp.mvarId!.introN 2 [n.getD `_, n'.getD freshName]
      return [new_goal]
    | ~q(∃ᶠ (x : $α₁) in $f₁, $p x), ~q(∃ᶠ (x : $α₂) in $f₂, $q x) => do
      unless (← isDefEq (← whnfR α₁) (← whnfR α₂)) && (← isDefEq (← whnfR f₁) (← whnfR f₂)) do
        return [goal]
      let p : Q($α₂ → Prop) := p
      let e : Q(∃ᶠ (x : $α₂) in $f₂, $p x) := e
      let all_imp : Q(∀ x : $α₂, $p x → $q x) ← mkFreshExprMVar q(∀ x : $α₂, $p x → $q x)
      goal.assign q(Filter.Frequently.mp $e (Filter.eventually_of_forall $all_imp))
      let (_, new_goal) ← all_imp.mvarId!.introN 2 [n.getD `_, n'.getD freshName]
      return [new_goal]
    | _, _ => do
      return [goal]

def peelTacAux (e : TSyntax `term) (n : Option (TSyntax `ident)) (n' : Option (TSyntax `ident)) :
    TacticM Unit := withMainContext do
  let e ← Elab.Term.elabTerm e none
  match n, n' with
    | .some n₁, .some n₂ => liftMetaTactic (peelQuantifier · e (.some n₂.getId) (.some n₁.getId))
    | .none, .some n₂ => liftMetaTactic (peelQuantifier · e (.some n₂.getId))
    | .some n₁, .none => liftMetaTactic (peelQuantifier · e (n' := .some n₁.getId))
    | .none, .none => liftMetaTactic (peelQuantifier · e)

syntax (name := peel) "peel" (ppSpace num)? term (Mathlib.Tactic.withArgs)? : tactic
@[tactic peel] def peelTac : Tactic := fun stx => do
  match stx with
    | `(tactic| peel $e:term) => peelTacAux e .none .none
    | `(tactic| peel $e:term with $n₁:ident) => peelTacAux e (.some n₁) .none
    | `(tactic| peel $e:term with $n₁:ident $n₂:ident) => peelTacAux e (.some n₁) (.some n₂)
    | `(tactic| peel $e:term with $n₁:ident $n₂:ident $n₃:ident*) =>
      evalTactic (← `(tactic| peel $e:term with $n₁ $n₂; have h' := $n₁; clear $n₁; peel h' with $n₁ $n₃:ident*; clear h'))
    | `(tactic| peel $n:num $e:term with $h₁:ident) =>
      match n.getNat with
        | 0 => pure ()
        | 1 => evalTactic (← `(tactic| peel $e:term with $h₁))
        | k + 2 =>
          let j := Syntax.mkNumLit <| toString (k + 1)
          evalTactic (← `(tactic| peel $e:term with $h₁; have h' := $h₁; clear $h₁; peel $j h' with $h₁; clear h'))
    | `(tactic| peel $n:num $h:ident) => evalTactic (← `(tactic| peel $n $h with $h))
    | _ => Elab.throwUnsupportedSyntax

open Filter Topology

example {f : ℝ → ℝ} (h : ∀ x : ℝ, ∀ᶠ y in 𝓝 x, |f y - f x| ≤ |y - x|) :
    ∀ x : ℝ, ∀ᶠ y in 𝓝 x, |f y - f x| ^ 2 ≤ |y - x| ^ 2 := by
  peel h with h_peel x y
  gcongr

example (α : Type*) (f g : Filter α) (p q : α → α → Prop) (h : ∀ᶠ x in f, ∃ᶠ y in g, p x y)
    (h₁ : ∀ x y, p x y → q x y) : ∀ᶠ x in f, ∃ᶠ y in g, q x y := by
  peel h with h_peel x y
  exact h₁ x y h_peel

example (α : Type*) (f : Filter α) (p q : α → Prop) (h : ∀ᶠ x in f, p x) (h₁ : ∀ x, p x → q x) :
    ∀ᶠ x in f, q x := by
  peel h with h_peel x
  exact h₁ x h_peel

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  - n := by
  peel 5 h
  linarith

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  - n := by
  peel h with h_peel ε hε N n hn
  linarith

lemma inv_succ_lt_all : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) < ε := by
  convert Metric.tendsto_atTop.mp tendsto_one_div_add_atTop_nhds_0_nat using 0
  simp only [Real.dist_0_eq_abs, fun n : ℕ ↦ abs_of_pos (Nat.one_div_pos_of_nat (α := ℝ) (n := n))]

example : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := by
  peel inv_succ_lt_all with h ε hε N n hn
  exact h.le

example : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := by
  peel 5 inv_succ_lt_all with h_peel
  exact h_peel.le

example : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := by
  intro ε hε
  peel 3 inv_succ_lt_all ε hε with h_peel
  exact h_peel.le

example : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1 / (n + 1 : ℝ) ≤ ε := by
  intro ε hε
  peel inv_succ_lt_all ε hε with h N n hn
  exact h.le

example (p q : Nat → Prop) (h : ∀ y, p y) (h₁ : ∀ z, p z → q z) : ∀ x, q x := by
  peel h
  exact h₁ _ <| by assumption

example (p q : Nat → Prop) (h : ∃ y, p y) (h₁ : ∀ z, p z → q z) : ∃ x, q x := by
  peel h with h x
  exact h₁ x h

example (p q : ℝ → ℝ → Prop) (h : ∀ ε > 0, ∃ δ > 0, p ε δ)
    (hpq : ∀ x y, x > 0 → y > 0 → p x y → q x y) :
    ∀ ε > 0, ∃ δ > 0, q ε δ := by
  peel h with h ε hε δ hδ
  exact hpq ε δ hε hδ h

Note that:

1. the temporary name is now peel
2. it supports ∀ᶠ and ∃ᶠ now.
3. It uses with and accepts terms
4. It allows for a numeric argument and hypotheses will be named automatically, for situations in which the names don't matter.

This means that we can simplify one of the original examples to:

example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y  - n := by
  peel 5 h
  linarith

[Jireh Loreaux]

Oh, and for some reason using Qq really makes compiling the peelQuantifier declaration slow. I'm not sure why though. Perhaps I'm doing something wrong.

[Vincent Beffara]

Very nice! So how hard would it be to add

• possibility to add using h x y at the end to close the goal in one line?
• support for several inputs peel [h1, h2]?

[Maybe I'm seeing too much similarity with filter_upwards but in fact it seems that merging the two would make sense. From an end-user's point of view.]

[Jireh Loreaux]

I'm not sure what several inputs would mean? using is probably easy.

[Joachim Breitner]

There could be multiple hypotheses around that you want to peel stuff off together?

[Jireh Loreaux]

(deleted)

[Timo Carlin-Burns]

If it's given multiple hypotheses to peel stuff off of and they both have have existentials, how would it choose which hypothesis to use the witness from?

example (p : ℝ → ℝ → Prop) (h : ∀ ε > 0, ∃ δ > 0, p ε δ) (h2 : ∀ ε > 0, ∃ δ > 0, p ε δ → q ε δ) :
    ∀ ε > 0, ∃ δ > 0, q ε δ :=
  by peel [h, h2] -- ??
  -- this doesn't make sense because there are two conflicting witnesses for δ

[Patrick Massot]

The situation is much clearer for the filter version since one of the axioms defining filters precisely adresses this question.

[Patrick Massot]

What the filter technology would do here is to choose the minimum of the two witnesses. But of course in the general case there is no clear choice to make.

[Patrick Massot]

More explicitly, docs#Filter.Eventually.and is a wrapper around docs#Filter.inter_mem and when you prove that neighborhood of zero form a filter, taking this min is exactly what ensures this axiom.

[Patrick Massot]

So I guess my answer is: for serious uses you need filters anyway and for teaching purposes the current peel is good enough.

[Patrick Massot]

And of course the current peel with one argument is also great as a general purpose tool, even in serious contexts.

[Patrick Massot]

And note that I know "serious" is not the right word. Teaching is also serious.

[Jireh Loreaux]

What about the name? I'm open to suggestions. peel, peel_quantifier, match_quantifier, qcongr, telescope?

[Vincent Beffara]

qconvert?

[Jireh Loreaux]

#7685

[Utensil Song]

peel seems to be a very vivid and encouraging name, matching its semantic, I love it.

[Joachim Breitner]

I agree. Although I see the merit of the more sober qconvert, it works a bit like convert with implication rather than equality, doesn't it?