Request for review of a leftpad proof

Stream: general

[Yufan Lou]

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

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

[Scott Morrison]

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.

[Alex J. Best]

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.

[Scott Morrison]

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

[Alex J. Best]

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

[Yufan Lou]

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

[Alex J. Best]

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!

[Scott Morrison]

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).

[Scott Morrison]

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."

[Yufan Lou]

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

[Yufan Lou]

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.

[Scott Morrison]

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. :-)

[Yufan Lou]

wow that can definitely go in README too

[Yufan Lou]

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?

[Yufan Lou]

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

[Yufan Lou]

not today :sleepy:

[Alex J. Best]

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

[Scott Morrison]

Which online editor are you using?

[Scott Morrison]

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

[Yufan Lou]

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

[Bryan Gin-ge Chen]

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

[Yufan Lou]

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!

[Yufan Lou]

That's ... wow

[Simon Hudon]

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

[Simon Hudon]

Yours look pretty good :)

[Yufan Lou]

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