simp and calc

In this post, I will summarize what I have learned about the simp tactic. Short for "simplification," simp is a tactic that automatically transforms expressions into a simpler form, just as its name suggests. The learning material I am using continues to be "Introduction to the Lean Language from Scratch: Hands-on Learning of Formal Mathematics Library Development".

Registering Theorems with attribute [simp]

The simp tactic does not automatically rewrite just anything. It only uses theorems that have been explicitly given the attribute [simp] as rewriting rules. Conversely, if the theorems required for the expression you want to prove do not yet have the simp attribute, simp alone will not make any progress in the proof.

Let's take a look at the following practical example.

example (n : MyNat) : 0 + (n + 0) = n := by
  fail_if_success simp

  rw [MyNat.add_zero, MyNat.zero_add]


attribute [simp] MyNat.add_zero MyNat.zero_add

example (n : MyNat) : 0 + (n + 0) = n := by
  simp

The fail_if_success tactic is used to verify that the tactic written immediately after it fails. Here, writing fail_if_success simp explicitly confirms that "at this point, the proof should not be complete using simp alone." Indeed, because MyNat.add_zero and MyNat.zero_add do not have the simp attribute at this stage, simp alone cannot prove 0 + (n + 0) = n, and we must explicitly rewrite it using rw [MyNat.add_zero, MyNat.zero_add].

However, after adding and registering the simp attribute to these two theorems using attribute [simp] MyNat.add_zero MyNat.zero_add, the exact same proposition can now be proved using only simp. Since simp automatically selects applicable rules from the set of registered theorems and repeatedly rewrites the goal, registering the necessary theorems beforehand makes the proof significantly more concise.

Passing Theorems Temporarily with []

Even without permanently registering a theorem via attribute [simp], you can pass theorem names inside [] when calling simp to use them as rewriting rules for that specific instance only.

theorem MyNat.ctor_eq_zero : MyNat.zero = 0 := by
  rfl

example : MyNat.zero = 0 := by
  simp [MyNat.ctor_eq_zero]

In this case, although MyNat.ctor_eq_zero itself is not given the simp attribute, using simp [MyNat.ctor_eq_zero] allows it to be used as an additional rewriting rule exclusively within this proof. If auxiliary theorems that aren't meant to be used everywhere are registered globally using attribute [simp], it could alter the behavior of simp in other proofs. Therefore, I found this capability to specify temporary rules to be a very helpful mechanism.

simp at and simp_all

While the examples so far have focused on simplifying the goal, simp can be applied to hypotheses as well. To specify the target of the rewriting, you use simp at.

example (m n : MyNat) (h : m + n + 0 = n + m) : m + n = n + m := by
  simp at h
  rw [h]

In this example, by applying simp at h to the hypothesis h : m + n + 0 = n + m, the hypothesis h itself is simplified to m + n = n + m using theorems that have the simp attribute (such as MyNat.add_zero in this case). Since the simplified h becomes identical to the goal, the proof is completed simply by running rw [h].

Additionally, if you want to simplify all hypotheses in the local context along with the goal all at once, you can write simp at *. Furthermore, if the goal can be completely solved as a result of the simplification, you can use simp_all to perform both the simplification and the completion of the proof in a single step. Writing simp at individually for multiple hypotheses can be tedious, so learning this all-in-one approach felt highly practical.

@[simp] theorem and Verification with simp?

If you want to attach the simp attribute at the same time you prove a theorem, you can declare it using the @[simp] theorem syntax instead of writing attribute [simp] later.

@[simp] theorem MyNat.succ_add (m n : MyNat) : .succ m + n = .succ (m + n) := by
  induction n
  case zero =>
    rfl
  case succ n' ih =>
    simp [ih]

This example uses simp [ih] in the succ case of the induction. If you want to check which theorems simp actually used to perform the rewriting, you can write simp? [ih] instead of simp [ih]. Doing so will cause Lean to display a message like the following:

Try this: [apply] simp only [MyNat.add_succ, ih]

This informs you that simp [ih] actually completed the proof using only two rewriting rules: MyNat.add_succ and ih. By rewriting the code to simp only [MyNat.add_succ, ih] as suggested, you can make the proof explicit and restrict it to only the specified theorems and hypotheses.

Making Expression Transformations Explicit with the calc Tactic

Lastly, although it has a slightly different flavor than simp, I'd like to mention the calc tactic that I learned during the proof process. Using calc, you can advance a proof by writing down the step-by-step transformations of an expression. In contrast to tactics like simp or rw, where it can be difficult to see what is happening under the hood, calc stands out because the transformation process itself serves as documentation for the proof.

example (m n : MyNat) : .succ m + n = .succ (m + n) := by
  induction n with
  | zero => rfl
  | succ n' ih => calc
    _ = (m.succ + n').succ := by rw [MyNat.add_succ]
    _ = (m + n').succ.succ := by rw [MyNat.succ_add]
    _ = (m + n'.succ).succ := by rw [MyNat.add_succ]

In this example, the induction n with syntax is used to write both the zero and succ n' ih cases together, separated by |. Inside the calc block used in the succ case, the underscore _ inherits the right-hand side of the previous line. It explicitly shows line-by-line which theorem was used to rewrite the expression—from (m.succ + n').succ to (m + n').succ.succ, and finally to (m + n'.succ).succ. While proving everything at once with simp hides the intermediate steps, using calc allows you to read the proof while following the path of the transformation. I felt this is an especially valuable way of writing code when proving complex equations or when re-reading proofs later on.

Conclusion

In this post, I learned about the simp tactic, including registering theorems with attribute [simp], temporary specifications using [], targeting with simp at and simp_all, verification methods via @[simp] theorem and simp?, and finally the calc tactic for making expression transformations explicit. My biggest takeaway this time was understanding that while simp is a powerful tactic that automates proofs, a registration system governing "which theorems are allowed to be used as rewriting rules" operates behind the scenes, and its role contrasts beautifully with tactics like calc that carefully write out the entire process.