Zulip Chat Archive

Stream: new members

Topic: Achievement: multiply convergent sequences


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

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:21):

Nice! This is much trickier than the sum statement

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

view this post on Zulip Pedro Minicz (May 26 2020 at 22:21):

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:21):

you have a non-terminal simp

view this post on Zulip Pedro Minicz (May 26 2020 at 22:22):

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

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:23):

I mean line 186

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

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

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

view this post on Zulip Pedro Minicz (May 26 2020 at 22:26):

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

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

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

view this post on Zulip Pedro Minicz (May 26 2020 at 22:30):

Oh, I see! Thank you!

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:33):

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

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

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:34):

You are allowed simp, ring but not too much else

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

view this post on Zulip Pedro Minicz (May 26 2020 at 22:37):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 22:41):

It's usually longer than just exact h

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:42):

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

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

view this post on Zulip Mario Carneiro (May 26 2020 at 22:42):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 22:43):

so you could write exact ‹_› instead of assumption

view this post on Zulip Pedro Minicz (May 26 2020 at 22:43):

Mario Carneiro said:

It's usually longer than just exact h

Indeed.

view this post on Zulip Mario Carneiro (May 26 2020 at 22:44):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 22:44):

same for contradiction?

view this post on Zulip Mario Carneiro (May 26 2020 at 22:45):

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 22:52):

It takes even longer to type assumption?!

view this post on Zulip Pedro Minicz (May 26 2020 at 22:54):

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

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

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