Rename bound variable inside a quantifier

Stream: lean4

[tau]

I proved divergence of an identity sequence as an exercise, and there's one thing bothering me:

  -- ¬∃ a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |(fun x => ↑x) n - a| < ε
  simp
  -- ∀ (x : ℝ), ∃ x_1, 0 < x_1 ∧ ∀ (x_2 : ℕ), ∃ x_3, x_2 ≤ x_3 ∧ x_1 ≤ |↑x_3 - x|

simp here loses the original names and introduces new x x_1 x_2 x_3, and so does push_neg. Is it possible to keep the original names?

[Kenny Lau]

simp just applies the lemmas, and for example the lemma for the first step involves:
not_exists : (¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x
and simp just sees this and thinks, I see the LHS in the current expression, so I replace it with the RHS

it wouldn't be a good thing to have simp additionally think "I see a bounded variable in the LHS and also the RHS so I should keep the name" because in a general theorem, the bounded variables don't have to be related at all

[tau]

Kenny Lau said:

simp just applies the lemmas, and for example the lemma for the first step involves:
not_exists : (¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x
and simp just sees this and thinks, I see the LHS in the current expression, so I replace it with the RHS

Yeah, I figured out that much. Still, is it possible to change the names to the original names without retyping the whole goal?

[Kenny Lau]

it is undoubtedly possible to have a specialised tactic to keep bvar names but then by being specialised its code is by definition not very maintainable, as if you go to the docstring for push_neg, you see that it is a special case of the more general push tactic

[Kenny Lau]

tau said:

Still, is it possible to change the names to the original names without retyping the whole goal?

it's possible to write a tactic to do that but I don't think I've seen it yet

[Kenny Lau]

oh wow, it exists!

[Kenny Lau]

but it has very few functionalities and it's literally never been used

[tau]

Kenny Lau said:

oh wow, it exists!

Thanks! Unfortunately, it doesn't seem to work the way I expect: rename_bvar x → a changes the goal to ∀ (a : ℝ), ∃ a_1, 0 < a_1 ∧ ∀ (a_2 : ℕ), ∃ a_3, a_2 ≤ a_3 ∧ a_1 ≤ |↑a_3 - a|, and the other variables can't be renamed. From my understanding, these variables all have the same internal name as well as distinct indices to protect against clashing, and rename_bvar ignores these indices.

[Kenny Lau]

import Mathlib

example (h : ∀ x : ℕ, ∃ y : ℕ, x = y) : ∀ x : ℕ, ∃ y : ℕ, x = y := by
  rename_bvar y → z at h
  rename_bvar y → a₁

@tau please include #mwe

[Kenny Lau]

ah I read your message again, yeah I guess this is what I meant by that it has very few functionalities and wasn't really tested much

[Kenny Lau]

for example, I would add a feature to be able to refer to the old variable by index

[tau]

Sure, sorry.

import Mathlib

def isLimit (f : ℕ → ℝ) (a: ℝ): Prop := ∀ ε>0, ∃ N: ℕ, ∀ n ≥ N, |f n - a| < ε
def convergent (f: ℕ → ℝ): Prop := ∃ a, isLimit f a
def divergent (f: ℕ → ℝ): Prop := ¬convergent f

def line: ℕ → ℝ := λx ↦ x

example: divergent line := by
  unfold divergent line convergent isLimit
  -- ¬∃ a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |(fun x => ↑x) n - a| < ε
  simp
  -- ∀ (x : ℝ), ∃ x_1, 0 < x_1 ∧ ∀ (x_2 : ℕ), ∃ x_3, x_2 ≤ x_3 ∧ x_1 ≤ |↑x_3 - x|
  rename_bvar x → a
  rename_bvar a_1 → ε
  sorry

[Aaron Liu]

Kenny Lau said:

it wouldn't be a good thing to have simp additionally think "I see a bounded variable in the LHS and also the RHS so I should keep the name" because in a general theorem, the bounded variables don't have to be related at all

Wasn't there a gadget to tell simp which bounds variables on the lhs corresponding to which ones on the rhs?

[Patrick Massot]

@Jovan Gerbscheid this is a huge regression from push_neg. It was a core requirement of this tactic. Can you fix that in push very soon or should we revert that refactor to get back a working push_neg?

[Patrick Massot]

It’s crazy that we didn’t have unit tests catching this.

[Michael Rothgang]

In some lemmas (e.g., rewriting sums), you definitely want to keep the names of bound variables. (Not all lemmas, as Kenny points out.) There's a lean gadget binderHint (or so, don't remember exactly) which helps here, but IIRC is hardly used in practice.

[Michael Rothgang]

@Joachim Breitner was working on this: what's the status of that feature? Would it be wise to go ahead and tag lots if mathlib with it.

[Patrick Massot]

This is completely independent from new features in Lean. There was a complete failure of the reviewing process which broke a crucial teaching tactic and we simply need to revert that commit if it’s complicated to fix.

[Michael Rothgang]

Agreed; we are talking about two different issues here. I think both bear fixing, but regressions go first.

[Michael Rothgang]

Do you have an example of the old push_neg syntax that is broken now/a pointer to one?

[Patrick Massot]

#lean4 > Rename bound variable inside a quantifier @ 💬 is now a mwe.

[Patrick Massot]

You can see it in the playground (replace the simp with push_neg).

[tau]

Should I create a GitHub issue for this?

[Patrick Massot]

Thanks, but I hope it’s not necessary. We’ll learn very soon whether there is an easy fix, and otherwise the commit which introduced the bug will be reverted within a few days.

[Jovan Gerbscheid]

There are two issues with our tests: They were supposed to use guard_target =ₛ instead of guard_target =. And there is a bug in the implementation of guard_target =ₛ so that it doesn't actually check that the binder names are the same (but the doc-string says that it does)

In the meantime, here is a quickfix for the problem: #31212

[Michael Rothgang]

Thanks a lot! Is there a way to test this, aside from locally (or waiting for the Lean bug to get fixed)?

[Jovan Gerbscheid]

I think that you are required to eta reduce the LHS of your simp lemma to guarantee that the binderNameHint works. In the lemma that I fixed, the binderNameHint does work in rw, but in simp, it picks up the name of the bound variable in the LHS of the lemma. A long while ago I tried to fix this discrepancy with lean#8155

[Damiano Testa]

Michael Rothgang said:

Thanks a lot! Is there a way to test this, aside from locally (or waiting for the Lean bug to get fixed)?

I think that #guard_msging a logInfo of the goal would include the actual binder names.

[Jovan Gerbscheid]

Thanks, I've added a #guard_msgs test to the above PR

[Patrick Massot]

Thanks Jovan! I’m a bit worried that the fix seems so specific to Exists.

[Jovan Gerbscheid]

The only two cases where the name preservation is done in push_neg is for pushing through forall and exists. And the forall case is still special cased as it was before. It's only the exists case that is relying on the binderNameHint

[Patrick Massot]

Ok, I don’t remember how I did it in the Lean 3 version anyway.