When `rw` tactic in Lean completes the proof?

user_19418717 0
Viewed 89

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?

lean
1 Answers

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.

user_18221640
Related