Tactic to collapse quantifiers between hyp and goal

Stream: new members

[Ricardo Prado Cunha]

Is there a tactic that can make use of repeated intro+specialize and cases+use to get rid of identical quantifiers ($\forall$ and $\exists$) between a hypothesis and the goal?

For example, in the tutorial problem 78

lemma continuous_opposite {f : ℝ → ℝ} {x₀ : ℝ} (h : continuous_at_pt f x₀) :
  continuous_at_pt (λ x, -f x) x₀ :=

you start with the state (after some unfolding and omitting unecessary context)

h : ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : ℝ), | x - x₀ | ≤ δ → | f x - f x₀ | ≤ ε)
⊢ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : ℝ), | x - x₀ | ≤ δ → | - f x - - f x₀ | ≤ ε)

I'm looking for some tactic to condense the operations

intros ε hε,
specialize h ε hε,
rcases h with ⟨δ, hδ, h⟩,
use [δ, hδ],
intros x hx,
specialize h x hx,

since these just serve to eliminate the common beginning between h and ⊢ (∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : ℝ),).

[Kevin Buzzard]

What does convert h using 3 do?

[Kevin Buzzard]

(if it's easy to make a #mwe then this would make the question easier to answer)

[Kevin Buzzard]

Maybe some variant of

  revert h,
  refine iff.mp _,
  rw iff_iff_eq,
  apply pi_congr (λ _, _),
  apply pi_congr (λ _, _),
  congr,
  apply funext (λ _, _),
  apply pi_congr (λ _, _),
  apply pi_congr (λ _, _),
  congr' 1,

etc etc could be turned into a tactic.

[Jireh Loreaux]

In this particular case, the answer is just to use simp_rw

[Kevin Buzzard]

The problem with this approach is that you have to manually write suffices : \forall x x₀, | f x - f x₀ | = | - f x - - f x₀ |, by simp_rw [this] rather than letting the computer work it out.

[Kyle Miller]

Kevin Buzzard said:

What does convert h using 3 do?

I think I made mathlib4's convert tactic be able to do this, but the mathlib3 one doesn't know how.

[Kyle Miller]

@Ricardo Prado Cunha I had the same question and wrote a tactic to do some of that, but I never polished it for mathlib because after I did the tutorials I didn't really have so many of these nested quantifiers to deal with anymore in my own work.

[Kyle Miller]

This doesn't really answer your question Ricardo since this is for Lean 4, but I wanted to check that mathlib4's convert does work here:

import Mathlib.Data.Real.Basic

example (f : ℝ → ℝ)
    (h : ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε)) :
    ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : ℝ), |x - x₀| ≤ δ → |(- f x - - f x₀)| ≤ ε) := by
  convert h using 9 with ε hε δ hδ x hx
  sorry
/-
x₀: ℝ
f: ℝ → ℝ
h: ∀ (ε : ℝ), ε > 0 → ∃ δ H, ∀ (x : ℝ), abs (x - x₀) ≤ δ → abs (f x - f x₀) ≤ ε
ε: ℝ
hε: ε > 0
δ: ℝ
hδ: δ > 0
x: ℝ
hx: abs (x - x₀) ≤ δ
⊢ abs (-f x - -f x₀) = abs (f x - f x₀)
-/

[Pedro Sánchez Terraf]

Kyle Miller said:

Ricardo Prado Cunha I had the same question and wrote a tactic to do some of that, but I never polished it for mathlib because after I did the tutorials I didn't really have so many of these nested quantifiers to deal with anymore in my own work.

Off-rails comment: Natural examples rarely involve more than four (exposed) alternated quantifiers $\forall\exists\forall\exists$ or $\exists\forall\exists\forall$. At the same time, it is paradoxical that one of the first formal definitions (that of limit) already involves three. A neat pedagogical issue.

[Moritz Doll]

Kevin Buzzard said:

Maybe some variant of

  revert h,
  refine iff.mp _,
  rw iff_iff_eq,
  apply pi_congr (λ _, _),
  apply pi_congr (λ _, _),
  congr,
  apply funext (λ _, _),
  apply pi_congr (λ _, _),
  apply pi_congr (λ _, _),
  congr' 1,

etc etc could be turned into a tactic.

this should be a good application of congrm (without the first two lines)

[Moritz Doll]

adding the first two lines could be a macro if this appears more often

[Ricardo Prado Cunha]

Kevin Buzzard said:

What does convert h using 3 do?

Changes the goal to (λ (x : ℝ), - f x) = f (i.e., -f = f). Changing the 3 to different values doesn't seem to help.

Also will try to make the MWE in a bit.

[Ricardo Prado Cunha]

Kyle Miller said:

Ricardo Prado Cunha I had the same question and wrote a tactic to do some of that, but I never polished it for mathlib because after I did the tutorials I didn't really have so many of these nested quantifiers to deal with anymore in my own work.

Makes since. I did try to look for other questions asking the same thing before posting this but I missed yours. I guess if this doesn't really show up that much in practice then it's not that pressing of a problem, and if it's available in mathlib4 that's probably good enough.

[Ricardo Prado Cunha]

Moritz Doll said:

Kevin Buzzard said:

Maybe some variant of

  revert h,
  refine iff.mp _,
  rw iff_iff_eq,
  apply pi_congr (λ _, _),
  apply pi_congr (λ _, _),
  congr,
  apply funext (λ _, _),
  apply pi_congr (λ _, _),
  apply pi_congr (λ _, _),
  congr' 1,

etc etc could be turned into a tactic.

this should be a good application of congrm (without the first two lines)

congrm (after reverting and refining into an iff) does work, but it requires writing out the entire common part of the goal, which is quite cumbersome for this usecase.

[Ricardo Prado Cunha]

Here is the MWE

import data.real.basic

def continuous_at_pt (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

example {f : ℝ → ℝ} {x₀ : ℝ} (h : continuous_at_pt f x₀) :
  continuous_at_pt (λ x, -f x) x₀ :=
begin
  intros ε hε,
  specialize h ε hε,
  rcases h with ⟨δ, hδ, h⟩,
  use [δ, hδ],
  intros x hx,
  specialize h x hx,
  simp,
  rwa abs_sub_comm,
end

(definition of continuous_at_pt taken from the tutorial). Basically I'm looking for an easier way to do those first 6 tactics (up to the last specialize), as I've found this to be a recurring pattern when dealing with limits and the like.