## Stream: general

### Topic: Request for review of a leftpad proof

#### Yufan Lou (Feb 24 2020 at 05:26):

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

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

#### 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



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

#### Scott Morrison (Feb 24 2020 at 05:37):

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

#### 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?

#### 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

#### 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!

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

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

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

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

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

#### Yufan Lou (Feb 24 2020 at 05:52):

wow that can definitely go in README too

#### 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?

#### Yufan Lou (Feb 24 2020 at 05:54):

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

#### Yufan Lou (Feb 24 2020 at 05:55):

not today :sleepy:

#### Alex J. Best (Feb 24 2020 at 06:05):

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

#### Scott Morrison (Feb 24 2020 at 06:05):

Which online editor are you using?

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

#### Yufan Lou (Feb 24 2020 at 06:07):

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

#### 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

#### 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!

That's ... wow

#### Simon Hudon (Feb 24 2020 at 06:44):

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

#### Simon Hudon (Feb 24 2020 at 06:50):

Yours look pretty good :)

#### 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