Zulip Chat Archive

Stream: new members

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 here from #lean4 > repeat automatically does refl? by Kyle Miller

Kyle Miller (Feb 06 2022 at 04:46):

docs#tactic.repeat is the core for the repeat tactic, but it doesn't do refl.

If I were to guess, what's going on is that repeat accidentally circumvents whatever the mechanism is that makes rw become the special NNG tactic.interactive.rw'

(@Rob Lewis Do you have any idea why rw in a repeat would use the non-NNG rw, if that's what's happening? Just pinging you because your name is at the top of this file)

Mario Carneiro (Feb 06 2022 at 06:13):

@Kyle Miller Yes, your guess is correct. The rw inside repeat is the regular one, not the NNG one. It is because repeat takes a tactic block in the regular tactic class, and it hasn't been overridden in NNG to take NNG tactics instead

Kevin Buzzard (Feb 06 2022 at 08:22):

I'm reluctant to fiddle with NNG because it works and I'm in the middle of a heavy term of teaching


Last updated: Dec 20 2023 at 11:08 UTC