Search code examples
lean

When `rw` tactic in Lean completes the proof?

I'm learning Theorem proving with Lean in Natural number game, and I have difficulty in understanding the behavior of rw tactic.

In Level 1/17 in Inequality world, I wrote the following code:

use 1,
rw add_comm,

Then Lean completes the proof. Here I've not used refl tactic. On the other hand, in Level 2/17 in Inequality world, a similar code

use 0,
rw add_zero,

doesn't complete the proof. I suspected that the following code would work:

use 0,
symmetry,
rw add_zero,

but this code again doesn't complete the proof; I needed to use refl tactic in these cases. How should I understand the difference of these?

Solution

  • This is likely a bug in NNG; the rw tactic in normal Lean always tries (a weak version of) refl after you finish all your rewrites, but this behaviour was disabled in NNG because it's not great for teaching. However, turning this behaviour off isn't easy, and sometimes it will slip through the cracks.