Zulip Chat Archive

Stream: general

Topic: Request for review of a leftpad proof


view this post on Zulip Yufan Lou (Feb 24 2020 at 05:26):

https://github.com/hwayne/lets-prove-leftpad/pull/29

Submission of Lean to Hillel's challenge to prove a formal leftpad

view this post on Zulip Scott Morrison (Feb 24 2020 at 05:37):

I think your text leaves out a critical point, namely that the reason why your proofs just consist of rw leftpad, simp, is because the theorems you're trying to prove have already been proved in mathlib! It's not like any magic is happening, beyond that simp is good at pulling out relevant lemmas from the library.

view this post on Zulip Alex J. Best (Feb 24 2020 at 05:37):

What you wrote looks great! The only thing I would say is that add_comm actually is a simp lemma (see the example below), the mechanism that stops it from looping however is possibly what makes it not solve your goal there outright, but it can do so in some instances,

lemma is_add_comm_simp (n m : ) : n + m = m + n :=
begin
simp,
end

#print is_add_comm_simp

in this example simp changes m+n to n+m but not the other way round so the goal is proved.

view this post on Zulip Scott Morrison (Feb 24 2020 at 05:37):

(add_comm will not be a simp lemma for much longer, btw)

view this post on Zulip Alex J. Best (Feb 24 2020 at 05:38):

Sure, but the reason isn't because it loops, just that its a bit arbitrary where you end up right?

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:42):

Scott Morrison said:

I think your text leaves out a critical point, namely that the reason why your proofs just consist of rw leftpad, simp, is because the theorems you're trying to prove have already been proved in mathlib! It's not like any magic is happening, beyond that simp is good at pulling out relevant lemmas from the library.

Let me specify that simp is pulling out theorem from mathlib

view this post on Zulip Alex J. Best (Feb 24 2020 at 05:42):

Actually if you do simp [-add_comm] for your proof of leftpad_length you won't need to rewrite again after, so in this case it is actually the fact that add_comm is (currently) a simp lemma that is slowing you down!

view this post on Zulip Scott Morrison (Feb 24 2020 at 05:46):

Alex J. Best said:

Sure, but the reason isn't because it loops, just that its a bit arbitrary where you end up right?

Yes. It's arbitrary and non-deterministic (or rather, possibly dependent on things you'd really like to be irrelevant).

view this post on Zulip Scott Morrison (Feb 24 2020 at 05:47):

I'm not sure what this Hillel leftpad thing is about, but I wonder if it would be more interesting to actually show direct proofs of these facts, in Lean canonical style, and then point out as an extra: "of course, since all these theorems already exist in mathlib, and simp is awesome, we can prove all these facts with a uniform proof rw leftpad, simp."

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:49):

That would definitely be awesome, but out of my depth. I might add when I study a bit more about mathlib.

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:51):

This leftpad thing is a half-joke referring to when leftpad got removed from npm and sabotaged the building of half of all javascript apps. Hillel is promoting formal methods to be more mainstream so it is a way to ride the meme machine kinda.

view this post on Zulip Scott Morrison (Feb 24 2020 at 05:51):

One solution is just to replace simp with squeeze_simp, see which lemma it's using, look them up, and copy and paste the proofs. :-)

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:52):

wow that can definitely go in README too

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:53):

Alex J. Best said:

Actually if you do simp [-add_comm] for your proof of leftpad_length you won't need to rewrite again after

Didn't work when I tried in the online editor. Is it something new?

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:54):

squeeze_simp is not in online editor either. Ah I need to actually start my vscode.

view this post on Zulip Yufan Lou (Feb 24 2020 at 05:55):

not today :sleepy:

view this post on Zulip Alex J. Best (Feb 24 2020 at 06:05):

I don't think it's new, thats weird.

view this post on Zulip Scott Morrison (Feb 24 2020 at 06:05):

Which online editor are you using?

view this post on Zulip Scott Morrison (Feb 24 2020 at 06:06):

You should definitely use Bryan's one, at https://leanprover-community.github.io/lean-web-editor/, not the original one.

view this post on Zulip Yufan Lou (Feb 24 2020 at 06:07):

Oh, I've been using the original one all this time

view this post on Zulip Bryan Gin-ge Chen (Feb 24 2020 at 06:23):

Nice work! Did you see @Simon Hudon's PR to that repository? https://github.com/hwayne/lets-prove-leftpad/pull/8

view this post on Zulip Yufan Lou (Feb 24 2020 at 06:37):

Bryan Gin-ge Chen said:

Nice work! Did you see Simon Hudon's PR to that repository? https://github.com/hwayne/lets-prove-leftpad/pull/8

Oh no I did not! Thanks!

view this post on Zulip Yufan Lou (Feb 24 2020 at 06:38):

That's ... wow

view this post on Zulip Simon Hudon (Feb 24 2020 at 06:44):

I should really finish up that presentation. I've been procrastinating two years on that

view this post on Zulip Simon Hudon (Feb 24 2020 at 06:50):

Yours look pretty good :)

view this post on Zulip Yufan Lou (Feb 24 2020 at 06:52):

Thank you! Yours is way up there for me to study :nerd:


Last updated: May 13 2021 at 00:41 UTC