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