## Stream: general

### Topic: simp messes up names

#### Patrick Massot (Mar 18 2019 at 22:05):

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 (Mar 18 2019 at 22:06):

I'm blaming simp but rw does the same

#### Patrick Massot (Mar 18 2019 at 22:09):

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 (Mar 18 2019 at 22:12):

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 (Mar 18 2019 at 22:14):

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 (Mar 18 2019 at 22:27):

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 (Mar 18 2019 at 22:53):

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

#### Chris Hughes (Mar 18 2019 at 23:42):

Is it really that confusing?

#### Mario Carneiro (Mar 18 2019 at 23:43):

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 (Mar 18 2019 at 23:44):

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

#### Mario Carneiro (Mar 18 2019 at 23:45):

(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 (Mar 25 2019 at 20:33):

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 (Mar 25 2019 at 20:34):

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 (Mar 26 2019 at 21:15):

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

Last updated: May 10 2021 at 00:31 UTC