Zulip Chat Archive

Stream: new members

Topic: More automatic unfolding


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

view this post on Zulip Bryan Gin-ge Chen (May 24 2020 at 18:10):

Could you include your imports?

view this post on Zulip Pedro Minicz (May 24 2020 at 18:12):

Which imports affect this and how exactly?

view this post on Zulip Alex J. Best (May 24 2020 at 18:12):

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

view this post on Zulip Kevin Buzzard (May 24 2020 at 18:14):

Just make it so that other people can cut and paste

view this post on Zulip Pedro Minicz (May 24 2020 at 18:14):

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

view this post on Zulip Kevin Buzzard (May 24 2020 at 18:15):

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

view this post on Zulip Alex J. Best (May 24 2020 at 18:16):

Now i get an invalid expression at the le

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

view this post on Zulip Johan Commelin (May 24 2020 at 18:17):

But usually def should be fine.

view this post on Zulip Pedro Minicz (May 24 2020 at 18:18):

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

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

view this post on Zulip Pedro Minicz (May 24 2020 at 18:20):

I'd expect Lean to automatically unfold those.

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

view this post on Zulip Johan Commelin (May 24 2020 at 18:22):

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

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

view this post on Zulip Pedro Minicz (May 24 2020 at 18:24):

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

view this post on Zulip Pedro Minicz (May 24 2020 at 18:24):

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

view this post on Zulip Kevin Buzzard (May 24 2020 at 18:26):

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

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

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

view this post on Zulip Pedro Minicz (May 24 2020 at 18:27):

I see! Thank you!

view this post on Zulip Kevin Buzzard (May 24 2020 at 18:27):

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

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

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

view this post on Zulip Alex J. Best (May 24 2020 at 18:28):

Kevin Buzzard said:

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

Doesn't work for me :confused:

view this post on Zulip 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 ,
  cases hl ε (by linarith) with N hN,
  cases hl' ε (by linarith) with N' hN',
  sorry
end

view this post on Zulip Pedro Minicz (May 24 2020 at 18:29):

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

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

view this post on Zulip Pedro Minicz (May 24 2020 at 19:16):

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

view this post on Zulip Reid Barton (May 24 2020 at 19:18):

I think rw does for example

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