simp/simpa vs rw/rwa

Stream: general

[Damiano Testa]

Could simpa be changed so that if simp closes a goal, then simpa closes it as well, instead of giving an error?
I am thinking of something like rwa which performs the rewrite even when the a(ssumption) is not available.

import tactic

example : 0 = 0 := by simp --works
example : 0 = 0 := by simpa --simpa failed  state: no goals

Maybe there is a reason why this behaviour is unwanted/problematic?

[Anne Baanen]

I like this because simpa lets you know when a plain simp would have worked. How about keeping an error or at least a message, but replacing the message with "try this: simp"?

[Damiano Testa]

I like the "Try this" idea!

[Eric Wieser]

I'd assumed that this thread was going to be the complaint that simpa using foo bar works but rwa [some_lemma] using foo bar doesn't

[Damiano Testa]

Ah, I probably named it wrong: i had more an "simp is to simpa as rw is to rwa" in mind.

[Johan Commelin]

So there are two improvements: (i) make rwa more like simpa by having rwa ... using .... and (ii) make both of them output Try this: if a rw or simp would already have closed the goal.

[Eric Rodriguez]

I'd find rwa usingsuper helpful. I've used simpa only using too many times for that.

[Damiano Testa]

Johan, thank you for the more thorough disambiguation: I failed at communication! :face_palm:

[Reid Barton]

Isn't rwa using not actually useful though? Isn't rw, exact the same length even?

[Filippo A. E. Nuccio]

Well, but you might need rw, exacts which is one character longer :smiley:

[Anne Baanen]

If we're following simpa using, rwa [eqs] using hyp would mean something more like have this := hyp, rw [eqs] at this ⊢, exact this

[Eric Wieser]

As a compromise, maybe rwa [eqs] using hyp should mean have this := hyp, rw [eqs] at this, exact this (that is, without rewriting at the goal)

[Eric Wieser]

Because rw [eqs] at this ⊢ is rarely going to be useful, because every lemma in eqs has to match both this and ⊢ at every step

[Anne Baanen]

Good point, I always forget whether it succeeds if any of the lemmas matches this or all of them.

[Reid Barton]

I don't really see the gain from any of this... just another non-compositional thing to learn.

[Eric Wieser]

have := foo bar,
rw baz at this,
exact this

feels awfully verbose, and often leads to ugly golfs with the frustrating triangle that would be more readable as:

rwa baz at foo bar

I guess the other way of looking at it is that we shouldn't have rwa either, as rw foo, assumption works fine and is compositional.

[Arthur Paulino]

Novice input: I think it's easier to learn when things have more structure. Making rwa more similar to simpa would probably turn it into less things to learn

[Reid Barton]

it's not real structure though

[Anne Baanen]

How about an almost term tac tactic that works like exact term except it applies tac to term first?

[Alex J. Best]

Eric Wieser said:

have := foo bar,
rw baz at this,
exact this

feels awfully verbose, and often leads to ugly golfs with the frustrating triangle that would be more readable as:

rwa baz at foo bar

I guess the other way of looking at it is that we shouldn't have rwa either, as rw foo, assumption works fine and is compositional.

Doesn't

have := foo bar,
rwa baz at this,

work for your example though? so its not that long?

[Anne Baanen]

So simpa [eqs] using term = almost term { simp [eqs] } and rwa [eqs] using term = almost term { rw [eqs] }

[Eric Wieser]

Are you proposing an almost tactic, @Anne Baanen?

[Anne Baanen]

I would prefer having a tactic like that over duplicate logic in rwa/simpa.

[Eric Rodriguez]

simpa simplifies both the using term and the goal, so I'm not too sure that almost would work

[Eric Rodriguez]

I feel like it's mostly useful for one-liners to have this sort of thing, as rwa ... using flows a lot better than let x := ... in by rwa ... at this

[Anne Baanen]

Another example of a simpa-like tactic: tactic#exact_mod_cast