## Stream: new members

### Topic: Achievement: multiply convergent sequences

#### Pedro Minicz (May 26 2020 at 22:20):

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 (May 26 2020 at 22:21):

Nice! This is much trickier than the sum statement

#### Pedro Minicz (May 26 2020 at 22:21):

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 (May 26 2020 at 22:21):

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

#### Kevin Buzzard (May 26 2020 at 22:21):

you have a non-terminal simp

#### Pedro Minicz (May 26 2020 at 22:22):

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

#### Kevin Buzzard (May 26 2020 at 22:23):

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

I mean line 186

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

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

#### Kevin Buzzard (May 26 2020 at 22:25):

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

#### Pedro Minicz (May 26 2020 at 22:26):

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

#### Pedro Minicz (May 26 2020 at 22:26):

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

#### Kevin Buzzard (May 26 2020 at 22:28):

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 (May 26 2020 at 22:29):

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 (May 26 2020 at 22:30):

Oh, I see! Thank you!

#### Kevin Buzzard (May 26 2020 at 22:33):

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

#### Pedro Minicz (May 26 2020 at 22:33):

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

#### Kevin Buzzard (May 26 2020 at 22:34):

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

#### Kevin Buzzard (May 26 2020 at 22:34):

You are allowed simp, ring but not too much else

#### Pedro Minicz (May 26 2020 at 22:35):

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 (May 26 2020 at 22:37):

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

#### Mario Carneiro (May 26 2020 at 22:41):

It's usually longer than just exact h

#### Jalex Stark (May 26 2020 at 22:41):

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 (May 26 2020 at 22:42):

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

#### Mario Carneiro (May 26 2020 at 22:42):

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 (May 26 2020 at 22:42):

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

#### Mario Carneiro (May 26 2020 at 22:43):

so you could write exact ‹_› instead of assumption

#### Pedro Minicz (May 26 2020 at 22:43):

Mario Carneiro said:

It's usually longer than just exact h

Indeed.

#### Mario Carneiro (May 26 2020 at 22:44):

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

#### Mario Carneiro (May 26 2020 at 22:44):

same for contradiction?

#### Mario Carneiro (May 26 2020 at 22:45):

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

#### Kevin Buzzard (May 26 2020 at 22:52):

It takes even longer to type assumption?!

#### Pedro Minicz (May 26 2020 at 22:54):

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

#### Alex J. Best (May 26 2020 at 23:04):

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 (May 26 2020 at 23:10):

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.

Last updated: May 18 2021 at 16:25 UTC