Massot Exercise 0037

Stream: Berkeley Lean Seminar

[Calvin McPhail-Snyder]

I had a question about exercise 0037 in the Massot tutorial. The solution is

-- A sequence admits at most one limit
-- 0037
example : seq_limit u l → seq_limit u l' → l = l' :=
begin
  intros hyp,
  intros hyp',
  apply eq_of_abs_sub_le_all,
  intros ε ε_pos,
  cases hyp (ε/2) (by linarith) with N hN,
  cases hyp' (ε/2) (by linarith) with N' hN',
  calc |l - l'| = |(l - u (max N N')) + (u (max N N') - l')| : by ring
            ... ≤ |l - u (max N N')| + |u (max N N') - l'| : by apply abs_add
            ... ≤ |u (max N N') - l| + |u (max N N') - l'| : by rw abs_sub
            ... ≤ ε : by linarith [hN (max N N') (le_max_left _ _), hN' (max N N') (le_max_right _ _)]
end

I mostly get why this works, but I don't really understand what's happening in the last line here: what's that syntax?

I think I would better understand a solution along the lines of

-- A sequence admits at most one limit
-- 0037
example : seq_limit u l → seq_limit u l' → l = l' :=
begin
  intros hyp,
  intros hyp',
  apply eq_of_abs_sub_le_all,
  intros ε ε_pos,
  cases hyp (ε/2) (by linarith) with N hN,
  cases hyp' (ε/2) (by linarith) with N' hN',
  let n := max N N'
  calc |l - l'| = |(l - u n) + (u n) - l')| : by ring
            ... ≤ |l - u n| + |u n - l'| : by apply abs_add
            ... ≤ |u n - l| + |u n - l'| : by rw abs_sub
            ... ≤ ε/2 + ε/2 : by linarith [ ??? ]
            ... ≤ ε : by ring
end

but I couldn't get this working: you need to add lemmas that n is bigger than N and N', and I got lost doing this; I'm also not quite sure how to feed those lemmas to linarith or similar. Is the awkwardness of carrying around these extra lemmas why the solution is in that form? Or is that a valid style and I just don't know quite how to do it?

[Pedro Minicz]

Its not inconvenient at all to have those extra hypothesis imo. Specially because they are just specialized versions of hN and hN'.

example : seq_limit u l → seq_limit u l' → l = l' :=
begin
  intros hyp,
  intros hyp',
  apply eq_of_abs_sub_le_all,
  intros ε ε_pos,
  cases hyp (ε/2) (by linarith) with N hN,
  cases hyp' (ε/2) (by linarith) with N' hN',
  let n := max N N',
  specialize hN n (le_max_left _ _),
  specialize hN' n (le_max_right _ _),
  calc |l - l'| = |(l - u n) + ((u n) - l')| : by ring
            ... ≤ |l - u n| + |u n - l'| : by apply abs_add
            ... ≤ |u n - l| + |u n - l'| : by rw abs_sub
            ... ≤ ε/2 + ε/2 : by linarith
            ... ≤ ε : by ring
end

[Pedro Minicz]

You could have also given them directly to linarith:

example : seq_limit u l → seq_limit u l' → l = l' :=
begin
  intros hyp,
  intros hyp',
  apply eq_of_abs_sub_le_all,
  intros ε ε_pos,
  cases hyp (ε/2) (by linarith) with N hN,
  cases hyp' (ε/2) (by linarith) with N' hN',
  let n := max N N',
  calc |l - l'| = |(l - u n) + ((u n) - l')| : by ring
            ... ≤ |l - u n| + |u n - l'| : by apply abs_add
            ... ≤ |u n - l| + |u n - l'| : by rw abs_sub
            ... ≤ ε/2 + ε/2 : by linarith [hN n (le_max_left _ _), hN' n (le_max_right _ _)]
            ... ≤ ε : by ring
end

[Pedro Minicz]

You can give extra lemmas for linarith to work with by listing them inside [].

[Pedro Minicz]

linarith will then use these extra lemmas as if they were in the context.

[Pedro Minicz]

Essentially: have h := ..., linarith is effectively the same as linarith [...].

[Pedro Minicz]

Note that this is the case with multiple tactics. For example, simp by itself it will only simplify a handful of lemmas, however, if you want to to use more you can use simp [lemma_1, lemma_2].

[Patrick Lutz]

Part of what's going on here is also that linarith is capable of doing a small amount of arithmetic, like knowing that if $a < \epsilon / 2$ and $b < \epsilon / 2$ then $a + b < \epsilon$. So the ring on the last line is not necessary

[Calvin McPhail-Snyder]

Thanks! That clarified things.

[Calvin McPhail-Snyder]

Here the underscore syntax is some sort of anonymous function?

[Pedro Minicz]

Lean will try to figure out what to put _. I could have also been explicit: le_max_left N N'.

[Pedro Minicz]

I find that in some cases its way better to use _, and if you do too I think you will also eventually become frustrated that Lean can't infer even more!

[Pedro Minicz]

A notable example I recently ran into was and_not_self (mk (quotient s) * mk ↥s ≤ mk (quotient s) * mk ↥s), which (in my context) could be reduced to the much more legible and_not_self _

[Kevin Buzzard]

@Calvin McPhail-Snyder you can switch between term and tactic mode at any time. I think set can be easier to use than let sometimes. Here is the solution you posted with set instead of let, and your ??? replaced by some sorrys:

example : seq_limit u l → seq_limit u l' → l = l' :=
begin
  intros hyp,
  intros hyp',
  apply eq_of_abs_sub_le_all,
  intros ε ε_pos,
  cases hyp (ε/2) (by linarith) with N hN,
  cases hyp' (ε/2) (by linarith) with N' hN',
  set n := max N N' with hn,
  calc |l - l'| = |(l - u n) + (u n - l')| : by ring
            ... ≤ |l - u n| + |u n - l'| : by apply abs_add
            ... ≤ |u n - l| + |u n - l'| : by rw abs_sub
            ... ≤ ε/2 + ε/2 : by linarith [hN n begin sorry end, hN' n begin sorry end ]
            ... ≤ ε : by ring
end

You can just fill in those sorrys in tactic mode, they're independent little puzzles. The advantage of set is that the hypothesis n = max N N' has a name now. It's true by definition, but this can be intimidating for beginners.

[Kevin Buzzard]

Once you've convinced yourself that exact le_max left _ _ solves the first sorry, you can replace begin exact X end with X, and this is what Patrick did.

[Kyle Miller]

Kevin Buzzard said:

The advantage of set is that the hypothesis n = max N N' has a name now. It's true by definition, but this can be intimidating for beginners.

One thread I've been slowly trying to pull is to understand why let definitions aren't picked up by linarith. Mario mentioned it was only recently that a tactic could even see the definition of something, so there's that. I could see there being some sort of performance penalty, but not in the adding of the equalities to the context: rfl of definitionally equal things should be basically free. From perusing the code, linarith looks for all inequalities and breaks them up into linear factors ("atoms"), and by default it doesn't try too hard to check whether different atoms are the same.

While I'm somewhat willing to make Lean happy, I'd rather it be the other way around.

(I thought I read that there was going to be a big change to linarith in the next few weeks, once someone got back, but I can't find it again.)

[Kevin Buzzard]

I'm not a computer scientist, but my impression is the following. I don't understand what linarith is doing, but I know for sure that if you just give it straight hypotheses h1 : a < b h2 : b < c h3 : c < 5 and then have goal a < 10 then linarith just works. And then you start wondering why it can't solve a <= max a b because that's also some trivial linear inequality, right? Or why it can't see through let bindings. So I went through a phase of basically reporting "bug reports" of the form "linarith should do this, right? It's trivial" and believe you me, the CS community here has bent over backwards to accommodate my requests for tactics to make life easier for mathematicians -- but when it came to requests like this, it was explained to me that what I was doing was basically asking for "mission creep". linarith does what it does, and does it well, but it doesn't do things like digging into let bindings or applying le_max_left or abs_le etc -- there is some sort of basic principle of computer science I think, and these requests to start asking for extra functionality are somehow going against this principle.

[Kevin Buzzard]

import tactic

example (a b : ℕ) (h : a ≤ b) : a ≤ b :=
begin
  let n := a,
  change n ≤ b, -- n = a by definition so `change` works
  linarith -- still works
end

It does seem to be able to see through let binders. It's stuff like le_max_left and abs_le which it doesn't know.

[Kyle Miller]

I think I've already accepted linarith not being able to prove anything like a <= max a b. I also know that mission creep is exactly "why can't it just do this one extra thing?" But, this is "in the current context, turn the definitions into equalities as if you had used set."

[Kyle Miller]

It doesn't seem to see things like that if its let n := a + 1 rather than just a variable. I'll have to check again.

[Kevin Buzzard]

Can you show me the explicit example where let is failing and set fixes it? linarith is doing great with random simple examples obfuscated by let, for me

[Kevin Buzzard]

There are changes to linarith on the cards -- go to the mathlib github page, click on "pull requests" and then search for linarith. You can see the current state of the pull requests and what people are saying about them. Rob Lewis is the guy who wrote it and who was away for a while recently.

[Kyle Miller]

example (a b : ℤ) (h : a ≤ b) : a ≤ b :=
begin
  let n := a,
  have h : n ≤ b + 1, linarith, -- OK
end

example (a b : ℤ) (h : a ≤ b) : a ≤ b :=
begin
  let n := a + 1,
  have h : n ≤ b + 1, linarith, -- not OK
end

example (a b : ℤ) (h : a ≤ b) : a ≤ b :=
begin
  set n := a + 1 with eq,
  have h : n ≤ b + 1, linarith, -- OK
end

[Kyle Miller]

Kevin Buzzard said:

There are changes to linarith on the cards -- go to the mathlib github page

Thanks for directing me to the PRs. I'll keep an eye open, and once it's in maybe I'll try to figure out how to modify linarith to deal with let definitions and see if it causes anything to go wrong.

[Kyle Miller]

Here are the examples, a bit less contrived:

example (a b : ℤ) (h : a ≤ b) : a ≤ b :=
begin
  let n := a,
  change n ≤ b,
  linarith, -- OK
end

example (a b : ℤ) (h : a ≤ b) : a + 1 ≤ b + 1 :=
begin
  let n := a + 1,
  change n ≤ b + 1,
  linarith, -- not OK
end

example (a b : ℤ) (h : a ≤ b) : a + 1 ≤ b + 1 :=
begin
  set n := a + 1 with eq,
  change n ≤ b + 1,
  linarith, -- OK
end

[Kevin Buzzard]

Because I don't understand let, I fear that asking Rob/Mario to make this work is precisely one of these "just one more thing" requests. It's not even clear to me that a PR would be welcome. If you understand more about computers than I do then feel free to engage them on the topic over in #maths, they'll happily try and explain the issues to you I'm sure. For all I know it is a reasonable request. Once when this came up Rob wrote set for me, and I've been using set ever since.

[Kyle Miller]

Thanks for pushing for set -- it's definitely a nice quality of life improvement.

I think the reason we've been noticing this is because of all the limit proofs in Massot's tutorials. You frequently need to specialize some limit at some particular epsilon, and before we knew about set we would avoid let definitions altogether because linarith wouldn't be able to fill in the positivity proof:

set ε := (u n - l)/2 with εeq,
specialize h ε (by linarith),

[Kevin Buzzard]

A lot of the enhancements made by Rob and Mario and people Rob has supervised have come from people just trying to do maths in #maths, running into problems, asking for help, and then these people have selflessly made tools for us. We have norm_num because I was whinging that I couldn't solve (4 : real) < 5. Then I started getting undergraduates interested and they ran into problems with algebra, so Mario wrote ring, and then they ran into problems with moving freely from nat to int and so Rob supervised a student to write norm_cast. I have had an extremely positive experience with these CS people. Whenever we run into problems, they try to help us out. This is one of the reasons that I've stuck around -- we run into problems when trying to do mathematics, and they solve them for us. I think one of the reasons it works like this is that writing tactics in Lean is perhaps not too hard to do if you know what you're doing -- or perhaps these people are looking for publications -- who knows. But if you are trying to do mathematics and running into problems, #maths is the place to go.

[Calvin McPhail-Snyder]

@Kevin Buzzard I didn't know about set and I think my frustration was caused by trying to use let instead. Thanks!

[Patrick Lutz]

I think set was written after the tutorials were made right?

[Patrick Lutz]

At some point when I was doing the tutorials I kept writing things like have : \exists N, N \ge N1 \and N \ge N2 := begin use max N1 N2, .... and then doing cases with the resulting statement to get around this issue

[Patrick Lutz]

learning about set was pretty nice after that