rw and refl

Stream: general

[Dan Velleman]

My understanding is that the rw tactic tries to apply refl at the end. Is that right? Is there any way to tell it not to do that? I'm writing a tactic that calls rw, and it is a bit inconvenient for me to have rw call refl.

[Kevin Buzzard]

Just write a new tactic which is the same as tactic.interactive.rw but removes the line which calls refl at the end. That's what I did in the natural number game.

[Reid Barton]

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/tactic/modded.lean#L27

[Reid Barton]

compare
https://github.com/leanprover-community/lean/blob/4887d8a30621941c883f208e151e61ab268c006d/library/init/meta/interactive.lean#L352
where the original rw_core does try (reflexivity reducible)

[Dan Velleman]

I thought of that, but when I look at tactic.interactive.rw, it just says propagate_tags (rw_core q l cfg), and when I look at tactic.rewrite_core, it says meta constant, and there's no code. Am I looking in the wrong place?

[Dan Velleman]

I don't see where the call to refl is happening.

[Kevin Buzzard]

Compare the definitions of rw_core in the two links above.

[Dan Velleman]

Oh wait, are tactic.rewrite_core and tactic.rw_core different?

[Kevin Buzzard]

import tactic

example : tactic.rewrite_core = tactic.rw_core := rfl -- unknown identifier 'tactic.rw_core'

One exists and the other doesn't?

[Reid Barton]

It's private but yes, it's different from rewrite_core.

[Dan Velleman]

I see, thanks.