conventions regarding combining simp and rw

Stream: new members

[Paul Nelson]

Are there general reasons to prefer one of the following over the other? (Assuming that both work.)

  simp only [ha, hb]
  rw [hc]

  simp only [ha, hb, hc]

I might have guessed that the first would generally be preferred because rw should be more direct than simp: applying one rewrite rule in one way rather than applying a bunch of them in all ways. But maybe there are other reasons to prefer the second.

More generally, are there reasons to prefer fewer lines of code, at the possible expense of clarity? For instance:

  have : a = b := thm1
  have := thm2 this

vs.

  have := thm2 (thm1 : a = b)

[Johan Commelin]

I think this mostly a matter of taste, and there is quite some variance, also in mathlib. But there is an unmistakable tendency towards short proofs.

[Kevin Buzzard]

My guess is that the one tactic option takes fewer milliseconds than the two tactic option so the computer scientists argue that it's preferred. What benefit is the two tactic option giving you? It's not clear to me that it's any clearer in this case.

[Paul Nelson]

no real benefit, just a wild guess that rw might be efficient than simp. It also feels a tad clearer since it says in which order the hypotheses are applied; for a more extreme example, compare rw [ha, hb, hc] to simp only [ha, hb, hc].

[Kevin Buzzard]

I guess I'm used to mathematicians saying "and now this follows from lemmas 3.2, 3.4 and proposition 4.1"

[Eric Wieser]

rw is easier to repair if the proof breaks, since it records the order the lemmas are used in

[Ruben Van de Velde]

simp_rw then :)

[Joachim Breitner]

As a reader, to me simp only […] can indicate an important suble difference from rw:

• simp (often) means “transform the full goal into some particular form, everywhere”. There is often a high-level semantic intention behind it (achieving a normal form, unfolding a function everywhere, moving from one level of abstractions to another).
• rw (often) means “we do equational reasoning, and apply an important, carefully chosen rewrite at exactly one step”

But I am perfectly aware that this is mostly a theoretical ideal, and in practice I use the tactic that works… :-)

[Kevin Buzzard]

@Paul Nelson I think that at the end of the day mathlib has decided that the culture is "proofs as small as possible and hang readability". 95% of the lemmas in mathlib are mathematically trivial anyway (they are API for definitions, it's surprisingly rare that a lemma has any kind of nontrivial content, this is because it's important to write down all the trivialities) and for mathematically trivial lemmas nobody is going to read the proofs anyway because they don't need to.

The issue has been raised before that mangling proofs intentionally might not be the best idea all the time, but actually for longer proofs there has been a movement to get people to document what's actually going on. The counterargument is that if you read the code in VS Code rather than just looking at a printout or a static web page, then you can usually figure out what's going on anyway.