More automatic unfolding

Stream: new members

[Pedro Minicz]

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

[Bryan Gin-ge Chen]

Could you include your imports?

[Pedro Minicz]

Which imports affect this and how exactly?

[Alex J. Best]

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

[Kevin Buzzard]

Just make it so that other people can cut and paste

[Pedro Minicz]

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

[Kevin Buzzard]

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

[Alex J. Best]

Now i get an invalid expression at the le

[Johan Commelin]

@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]

But usually def should be fine.

[Pedro Minicz]

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

[Pedro Minicz]

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

[Pedro Minicz]

I'd expect Lean to automatically unfold those.

[Pedro Minicz]

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]

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

[Kevin Buzzard]

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]

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

[Pedro Minicz]

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

[Kevin Buzzard]

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

[Pedro Minicz]

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]

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]

I see! Thank you!

[Kevin Buzzard]

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

[Pedro Minicz]

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

[Pedro Minicz]

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

[Alex J. Best]

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]

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]

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

[Reid Barton]

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

[Pedro Minicz]

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

[Reid Barton]

I think rw does for example

[Reid Barton]

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