simp messes up names

Stream: general

[Patrick Massot]

In

import logic.basic

example (P : ℕ → Prop) (h : ¬ ∃ n, P n) : ¬ P 0 :=
begin
  simp only [not_exists] at h,
  exact h 0
end

The goal after the simp line is ∀ (x : ℕ), ¬P x, whereas I'm expecting ∀ (n : ℕ), ¬P n. Is there any way to prevent simp from messing up names like this? In a more complicated proof it becomes very confusing for students

[Patrick Massot]

I'm blaming simp but rw does the same

[Patrick Massot]

Is it possible to write a tactic that fixes the names after invoking simp only [not_exists] or simp only [not_forall]? It looks non trivial because the structure of the expr is not the same, but it still sounds feasible by de Bruijn indices gurus.

[Simon Hudon]

I think simp and rw use the same names used in the lemma. In your situation, there seems to be a different obviously correct behavior but if you look at a lemma like (∀ a, _) ∧ (∀ b, _) ↔ (∀ c, _) ∨ (∀ d, _) ∨ (∀ e, _), it's not obvious what names to use after rewrite

[Patrick Massot]

I understand why there is no good general solution. I'm looking for a solution specific to these not_* lemmas (including not_le and not_lt) where a tactic both calls simp only and fixes names

[Simon Hudon]

Now that I think of it, I may have an idea on how to do it in general. I'm not overly enthusiastic about doing it for specific lemmas because when the wheels fall off, people get even more confused.

[Kevin Buzzard]

I guess you could always teach the students that ∀ (x : ℕ), ¬P x and ∀ (n : ℕ), ¬P n are syntactically equal...

[Chris Hughes]

Is it really that confusing?

[Mario Carneiro]

I think it's best to just not worry about the names of binders that are not open. Lean control over this is limited

[Mario Carneiro]

you can always name it when you use it in intros or anything else that actually puts a name in your context

[Mario Carneiro]

(incidentally, Metamath has great support for this - since the variables are named the same in the original lemma, they get renamed in tandem when you apply the theorem)

[Patrick Massot]

Since nobody else seemed interested, I wrote a tactic doing that at https://gist.github.com/PatrickMassot/58b2c3e557e7010db0fb8ab5057dfd47 (you can put that file in mathlib or any project using it). Remember the goal is to push negations through quantifiers and logical connective without renaming variables. This tactic is based on @Jeremy Avigad 's finish code, and help from Simon who told me about eta-reduction messing up with my Exists. The two test cases at the end show the tactic in action. The first one goes from

h : ∃ (p : ℕ), ¬∀ (n : ℕ), n > p,
h' : ∃ (p : ℕ), ¬∃ (n : ℕ), n < p
⊢ ¬∀ (n : ℕ), n = 0

to

h : ∃ (p n : ℕ), n ≤ p,
h' : ∃ (p : ℕ), ∀ (n : ℕ), p ≤ n
⊢ ∃ (n : ℕ), n ≠ 0

The second transforms

h : ¬∀ (ε : ℤ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε)

into

h : ∃ (ε : ℤ), ε > 0 ∧ ∀ (N : ℕ), ∃ (n : ℕ), n ≥ N ∧ ε ≤ |a n - l|

(I used integers instead of real numbers to avoid importing real numbers)

[Patrick Massot]

I'm inordinately proud of this tactic. I think it's really relevant to teaching, but actually I also think it should be in mathlib

[Patrick Massot]

https://github.com/leanprover-community/mathlib/pull/853