what's the difference between Lean 4's simpa and simp tactics?

Question

I am having some difficulty understanding the simpa tactic in the example below (and in general).

The documentation says that

simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

My understanding is that it is a variant of the simp tactic, but I can't see precisely what was added (w.r.t. simp). In the example:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

noncomputable section

open Real

/-- The sin function has derivative 1 at 0. -/
example : HasDerivAt sin 1 0 := by
  simpa using hasDerivAt_sin 0
  -- simp [hasDerivAt_sin 0]; exact hasDerivAt_sin 0

end

The simpa line works. But if I break it into a simp and something else, it fails (at the simp step).

My questions are:

How can one simulate simpa with simp and more basic tactics?

Why is it useful as advertised in the documentation?

Answer 1

What simpa does

simpa [] using hasDerivAt_sin 0 is more-or-less equivalent to the following:

  /-
  ⊢ HasDerivAt sin 1 0
  -/

  -- add fact to the context
  have myfact := hasDerivAt_sin 0
  /-
  myfact : HasDerivAt sin (cos 0) 0
  ⊢ HasDerivAt sin 1 0
  -/

  -- simplify the goal
  try simp []
  /-
  myfact : HasDerivAt sin (cos 0) 0
  ⊢ HasDerivAt sin 1 0
  -/

  -- simplify the fact we are using
  try simp [] at myfact
  /-
  myfact : HasDerivAt sin 1 0
  ⊢ HasDerivAt sin 1 0
  -/

  -- apply the fact we are using to the current goal
  exact myfact
  /- No goals! -/

(The trys are because simp normally fails if it doesn't make any progress.)

Why you need simpa

To see why simpa is needed in this case, let's look the exact simp lemmas being used. If you instead use

simpa? [] using hasDerivAt_sin 0

(with a ?), Lean will tell you that you can replace this with

simpa only [cos_zero] using hasDerivAt_sin 0

Here cos_zero is just the theorem cos 0 = 1.

However, if we do

simp only [cos_zero, hasDerivAt_sin 0]

it will repeatedly rewrite the goal with each lemma, but the goal doesn't have a cos 0 in it. It only has a 1. The cos 0 is in the lemma we want to apply, namely hasDerivAt_sin 0 which has type HasDerivAt sin (cos 0) 0. simp doesn't try to simplify the simp lemmas, just the goal.

An alternative in this case using pure simp

Now, in your particular case, you could use

simp [<-cos_zero, hasDerivAt_sin 0]

and it would work since it would replace the only 1 with cos 0, and then the goal and the other simp lemma would match, closing the goal. (<-cos_zero uses the reversed equality 1 = cos 0.) You could also just rewrite with rw [<-cos_zero] to be even more specific. (To see why you typically don't want simp to apply a lemma in both directions, consider sin 0 = 0. If you replace every 0 with sin 0 repeatedly, it could blow up the expression.)

But I think simpa is nice here since it makes what is going on clear (once you understand what simpa does).

Answer 2

To add to Jason Rute's answer: the reason why simpa exists is that, even though it can be pretty easily be simulated with simps, there is a policy in Mathlib not to use simp in non-terminal positions, for maintainability reasons. Indeed, when simp is used in a non-terminal position (that is, it does not close the current goal, and therefore an other tactic is used afterwards), improving simp (that is, making it more powerful at simplifying the goal) could break the code, by making the next tactic not applicable (for instance, if the better version of simp is capable of closing that goal at once). This means that adding lemmas to simp's database of known simplification rules could break a lot of code, which would make adding stuff to Mathlib harder.

This is where simpa kicks in: it can be simulated by non-terminal simps, but can only itself be used in a terminal position (as it tries to close the goal), so having simpa allows one to use simp where this would break Mathlib's policy of "only terminal simps".

Of course, besides this, it happens that simpa becomes more convenient than simp even if you don't care about this "only terminal simps" policy.