rw or simp only

Stream: general

[Filippo A. E. Nuccio]

Quite often a long list of rw works equally well with a simp only tactic: for instance, in my code, I have

simp only [minor_map, minor_minor, equiv.self_comp_symm, minor_id_id, map_map],

and I can equally well write

rw [minor_map, minor_minor, equiv.self_comp_symm, equiv.self_comp_symm, minor_id_id, map_map],

to obtain the same result. I wonder which is considered nicer: on a one hand, rw seems (to me) more basic a tactic than simp only, so it looks more elegant; on the other, to make the rw work I have to repeat equiv.self_comp_symm twice, and it makes it less elegant... :thinking: :tie:

[Yaël Dillies]

Yet another alternative is simp_rw, which is basically rw on steroids. But, as opposed to simp only, it will try the lemmas in order, and ,not cycle.

[Filippo A. E. Nuccio]

Well, I normally use simp_rw when I need to rw inside binders, which simp_rw can do and rw can't. But you're right, one more option...

[Eric Wieser]

The advantage of rw is you can stick your cursor in the proof to see how the goal evolves after each step

[Eric Rodriguez]

I personally prefer rw until I have to start repeating, and then I'll just use simp only (I've never tried simp_rw with repeats...)

[Damiano Testa]

I think simp_rw also needs repeats.

[Filippo A. E. Nuccio]

Eric Wieser said:

The advantage of rw is you can stick your cursor in the proof to see how the goal evolves after each step

Oh, yes, this seems a very good point. OK, I'll stick to rw as long as I can, and only switch to simp only when repetitions arise.