## Stream: new members

### Topic: More automatic unfolding

#### Pedro Minicz (May 24 2020 at 18:07):

Lean should do more automatic unfolding by default. It is rather unreasonable (imho) for the following to fail:

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

example (u : ℕ → ℝ) (l l' : ℝ) : seq_limit u l → seq_limit u l' → l = l' :=
begin
intros hl hl',
by_contra h,
change l ≠ l' at h,
have h₁ : 0 < |l - l'|,
{ apply abs_pos_of_ne_zero,
apply sub_ne_zero_of_ne,
assumption },
let ε := |l - l'| / 4,
cases hl ε (by linarith) with N hN,
cases hl' ε (by linarith) with N' hN',
sorry
end


#### Pedro Minicz (May 24 2020 at 18:12):

Which imports affect this and how exactly?

#### Alex J. Best (May 24 2020 at 18:12):

If we copy paste your code it doesn't know what | is for instance

#### Kevin Buzzard (May 24 2020 at 18:14):

Just make it so that other people can cut and paste

#### Pedro Minicz (May 24 2020 at 18:14):

It's notation |x| := abs x from tuto_lib. Just fixed it.

#### Kevin Buzzard (May 24 2020 at 18:15):

If I cut and paste it doesn't work. Please just make it work

#### Alex J. Best (May 24 2020 at 18:16):

Now i get an invalid expression at the le

#### Johan Commelin (May 24 2020 at 18:17):

@Pedro Minicz Which part is failing, and what would you expect? If you change def to abbreviation, lean will be more eagerly unfolding.

#### Johan Commelin (May 24 2020 at 18:17):

But usually def should be fine.

#### Pedro Minicz (May 24 2020 at 18:18):

(by linarith) fails. I'd expect it to be able to "see through" let ε := ....

#### Pedro Minicz (May 24 2020 at 18:19):

Uncommenting have ε_pos : ... and chancing (by linarith) to ε_pos works. Which is frustrating considering that it is pretty much the same thing.

#### Pedro Minicz (May 24 2020 at 18:20):

I'd expect Lean to automatically unfold those.

#### Pedro Minicz (May 24 2020 at 18:22):

On another note, I found the use of lemmas like one_eq_succ_zero weird in the Natural Number Game, I'd expect those to unfold naturally. It could be something to do with the Natural Number Game in particular (like rw not solving reflexivity) or something to do how Lean has has_one among many other such type classes, probably the latter.

#### Johan Commelin (May 24 2020 at 18:22):

@Pedro Minicz Does it help to use set instead of let?

#### Kevin Buzzard (May 24 2020 at 18:23):

one_eq_succ_zero can be proved by refl but I don't tell people that, because I am trying to teach mathematicians and mathematicians don't understand the concept of definitional equality because their concept of a definition is more fluid than the computer science definition

#### Pedro Minicz (May 24 2020 at 18:24):

@Kevin Buzzard I see, indeed that makes perfect sense.

#### Pedro Minicz (May 24 2020 at 18:24):

@Johan Commelin No, set is appears so behave exactly like let in this situation.

#### Kevin Buzzard (May 24 2020 at 18:26):

 set ε := |l - l'| / 4 with hε, is what you want

#### Pedro Minicz (May 24 2020 at 18:27):

I haven't encountered many situation like one_eq_succ_zero outside the Natural Number Game. Lean automatically unfold (or replace by definitional equality, I don't know which expression is more appropriate) definitions in these (definitional equality) cases, I'd hope.

#### Kevin Buzzard (May 24 2020 at 18:27):

The point of set is that if you use it with with then it adds the hypothesis which is stopping linarith from working into the context.

#### Pedro Minicz (May 24 2020 at 18:27):

I see! Thank you!

#### Kevin Buzzard (May 24 2020 at 18:27):

  set ε := |l - l'| / 4 with hε,
cases hl ε (by linarith) with N hN,
cases hl' ε (by linarith) with N' hN',
...


#### Pedro Minicz (May 24 2020 at 18:28):

Any particular reason why tactics can't "see through" := definitions? I'd imagine it may be a performance concern.

#### Pedro Minicz (May 24 2020 at 18:28):

But then, making theorems and lemmas short and opaque should solve the deal while letting local let definitions be transparent.

#### Alex J. Best (May 24 2020 at 18:28):

Kevin Buzzard said:

  set ε := |l - l'| / 4 with hε,
cases hl ε (by linarith) with N hN,
cases hl' ε (by linarith) with N' hN',
...


Doesn't work for me :confused:

#### Kevin Buzzard (May 24 2020 at 18:29):

import data.real.basic

notation |x| := abs x

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

example (u : ℕ → ℝ) (l l' : ℝ) : seq_limit u l → seq_limit u l' → l = l' :=
begin
intros hl hl',
by_contra h,
change l ≠ l' at h,
have h₁ : 0 < |l - l'|,
{ apply abs_pos_of_ne_zero,
apply sub_ne_zero_of_ne,
assumption },
set ε := |l - l'| / 4 with hε,
cases hl ε (by linarith) with N hN,
cases hl' ε (by linarith) with N' hN',
sorry
end


#### Pedro Minicz (May 24 2020 at 18:29):

As far as I have seen mathlib already mostly tends to the "short lemmas" side.

#### Reid Barton (May 24 2020 at 18:41):

Some tactics seem to see through local let bindings while others don't, I never figured out why.

#### Pedro Minicz (May 24 2020 at 19:16):

@Reid Barton Could you list such tactics? I'd be interested to see them.

#### Reid Barton (May 24 2020 at 19:18):

I think rw does for example

#### Reid Barton (May 25 2020 at 15:30):

Oddly enough I just needed this exact combination (linarith with the equality hypothesis generated by set)

Last updated: May 13 2021 at 06:15 UTC