Zulip Chat Archive

Stream: lean4

Topic: repeat automatically does refl?


Matt Yan (Feb 06 2022 at 03:15):

I have a goal which can be closed byrw lemma, rw lemma, rw lemma, refl,, it turns out repeat {rw lemma}, also does the refl for me. Is it built in to all combinators?

Julian Berman (Feb 06 2022 at 03:21):

Is this actually Lean 4 or 3?

Matt Yan (Feb 06 2022 at 03:28):

Then one used in Buzzard's natural number game, I noticed that both rwa and repeat does the refl for you. And thus the shortest proof in world 3 level 5 being

induction c with n hn,
repeat {rw mul_zero}, -- does 3 rewrites followed by a refl

rw mul_succ,
rwa [hn, mul_succ, mul_add], -- followed by a refl

If this is not version dependent behavior @Kevin Buzzard you might want to update the notes a bit

Arthur Paulino (Feb 06 2022 at 03:54):

@Matt Yan you might have a better chance finding your answer on #new members. The natural numbers game uses Lean 3 and this stream is more specific to Lean 4

Matt Yan (Feb 06 2022 at 03:57):

Thanks!

Matt Yan (Feb 06 2022 at 03:58):

What version is the reference manual based on? https://leanprover.github.io/reference/index.html

Arthur Paulino (Feb 06 2022 at 04:00):

That's Lean 3

Arthur Paulino (Feb 06 2022 at 04:04):

Also keep in mind that the NNG uses a certain version of Lean 3 that might differ from the version that's largely used by the community in some aspects. I tried searching for the source code of repeat on my smartphone but I had no success

Julian Berman (Feb 06 2022 at 04:05):

Yes, the answer I believe will have to do with the fact that NNG specifically uses a simplified version of rw.

Julian Berman (Feb 06 2022 at 04:05):

Normally rw will call refl, but NNG's does not (for pedagogical reasons).

Julian Berman (Feb 06 2022 at 04:05):

But probably it doesn't similarly cripple repeat or rwa, so you get the normal behavior.

Matt Yan (Feb 06 2022 at 04:06):

I see...I do find lean 4 and relevant docs on GitHub and github io, Is there any plan to migrate NNG to lean 4? @Kevin Buzzard

Julian Berman (Feb 06 2022 at 04:06):

This is probably already documented somewhere, but yeah NNG is also a very old version of Lean 3.

Julian Berman (Feb 06 2022 at 04:06):

Yes I believe it eventually will. But it's still early, Lean 4 is still changing often, and mathlib, the major library for Lean 3, is still not very close to ported to Lean 4, so that will likely happen first.

Matt Yan (Feb 06 2022 at 04:08):

Julian Berman said:

This is probably already documented somewhere, but yeah NNG is also a very old version of Lean 3.

In which case it would still be better if NNG uses the latest stable Lean 3

Julian Berman (Feb 06 2022 at 04:14):

It's definitely been discussed before, see e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Adding.20logging.20for.20cases.20where.20oleans.20are.20not.20picked.20up/near/259862000 -- I don't know if there's a status update but I'd guess Kevin certainly wouldn't mind if someone sent a PR doing so, it likely will involve some fixes it sounds like though.

Notification Bot (Feb 06 2022 at 04:27):

This topic was moved by Kyle Miller to #new members > repeat automatically does refl?


Last updated: Dec 20 2023 at 11:08 UTC