Zulip Chat Archive

Stream: general

Topic: simp messes up names


view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 18 2019 at 22:06):

I'm blaming simp but rw does the same

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Chris Hughes (Mar 18 2019 at 23:42):

Is it really that confusing?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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