Achievement: multiply convergent sequences

Stream: new members

[Pedro Minicz]

Hey, I just want to share a cool achievement. I just formalized a proof that the limit of the product of two sequences is the product of the limits! You can view the proof on Github.

[Kevin Buzzard]

Nice! This is much trickier than the sum statement

[Pedro Minicz]

Not sure whether or not this kind of topic fits this stream (or any stream, for that matter). Please tell me if that is the case.

[Pedro Minicz]

Also, any and all suggestions about my code are welcome!

[Kevin Buzzard]

you have a non-terminal simp

[Pedro Minicz]

You mean the @[simp] annotation? Or a use of the tactic?

[Kevin Buzzard]

You're probably supposed to run the simp, look at the new goal, replace simp with suffices : <new goal>, and then prove it with simpa using this

[Kevin Buzzard]

I mean line 186

[Kevin Buzzard]

Maybe just write simp [limit_neg_iff, limit_mul_const const_limit], and close the goal in one line

[Kevin Buzzard]

Maybe limit_neg_iff could even be tagged with @[simp] and then you wouldn't have to explicitly include it

[Pedro Minicz]

Yes, simp [limit_neg_iff, limit_mul_const const_limit] does close the goal in one line, thank you!

[Pedro Minicz]

I don't get how to use the suffices idiom in this case, though.

[Kevin Buzzard]

If you really wanted to run simp to change ⊢ limit (-c₁ * c₂) (-l₁ * l₂) into ⊢ limit (-(c₁ * c₂)) (-(l₁ * l₂)) in the middle of a proof, the mathlib-approved way is

    suffices : limit (-(c₁ * c₂)) (-(l₁ * l₂)),
      simpa using this,
    rw limit_neg_iff (etc etc)

[Kevin Buzzard]

The idea is that when in 1 year's time someone decides to tag limit_neg_iff as a simp lemma, then your proof won't break

[Pedro Minicz]

Oh, I see! Thank you!

[Kevin Buzzard]

similarly for line 171 you could write simpa [abs_sub] using hN,

[Pedro Minicz]

Non-terminal simps are kind everywhere in my code. I'll keep that in mind going forward.

[Kevin Buzzard]

It's the way I started too, but be warned, they won't like it when you start PR'ing :-)

[Kevin Buzzard]

You are allowed simp, ring but not too much else

[Pedro Minicz]

I see, good thing I'm allowed to do that. Typing simp at w, ring at w at the end of the proof while watching the goal state was the best experience I had with Lean thus far! :grinning_face_with_smiling_eyes:

[Pedro Minicz]

From what I have observed, the assumption tactic isn't used often, why is that?

[Mario Carneiro]

It's usually longer than just exact h

[Jalex Stark]

because whenever you're using assumption, you probably actually know the name of the thing that assumption finds? so writing exact h gives a more readable proof
assumption also probably takes a tiny bit longer to run

[Kevin Buzzard]

and exact h is probably quicker too! We need a good abbreviation for assumption.

[Mario Carneiro]

it's also potentially much slower, this can happen sometimes when there is another assumption that looks really similar to h and comes first, and lean starts unfolding everything to find out if it is really the same

[Mario Carneiro]

There is a nice term mode abbreviation for assumption, ‹_›

[Mario Carneiro]

so you could write exact ‹_› instead of assumption

[Pedro Minicz]

Mario Carneiro said:

It's usually longer than just exact h

Indeed.

[Mario Carneiro]

An assumption? would also be cool (producing a Try this: exact h)

[Mario Carneiro]

same for contradiction?

[Mario Carneiro]

which could produce Try this: cases h or Try this: cases h1 h2

[Kevin Buzzard]

It takes even longer to type assumption?!

[Pedro Minicz]

Making those tactics could be a good exercise for a tutorial on writing tactics

[Alex J. Best]

Pedro Minicz said:

Non-terminal simps are kind everywhere in my code. I'll keep that in mind going forward.

The other alternative to using suffices is to change simp to squeeze_simp and lean will tell you exactly what simp lemmas are used so you can change the line to simp only [lemma1,lemma2]. This is also more resistant to breakage than a bare simp, but can be less readable than a good suffices

[Yury G. Kudryashov]

Or if you want your code to broke once a new lemma is added to the simp set (so that you'll have to fix your proof but probably make it simpler/shorter), you can use guard_target https://leanprover-community.github.io/mathlib_docs/tactics.html#guard_target right after simp.