repeat automatically does refl?

Stream: new members

[Matt Yan]

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]

Is this actually Lean 4 or 3?

[Matt Yan]

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]

@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]

Thanks!

[Matt Yan]

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

[Arthur Paulino]

That's Lean 3

[Arthur Paulino]

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]

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

[Julian Berman]

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

[Julian Berman]

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

[Matt Yan]

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]

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

[Julian Berman]

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]

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]

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]

This topic was moved here from #lean4 > repeat automatically does refl? by Kyle Miller

[Kyle Miller]

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]

@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]

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