The ring tactic

On the occasion, the goal is a Leibniz equality is a first-degree equation that involves literals (Peano numbers), names (variables), additions, and multiplications. For example, consider proving the twice_S lemma:

Lemma twice_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
  intro n.

The *goals* window reads:

n : nat
============================
2 * S n = S (S (2 * n))

To ease the life of their users, the CPA designers provided a ring tactic that

• simplifies the LHS and the RHS into a sum of products, using the associativity, commutativity, and distributivity of addition and multiplication and computing constant expressions;
• reorders the resulting products (using the commutativity of multiplication) so that the constant (if there is one) occurs first and then variables occur in the same order; and
• reorders the resulting sums (using the commutativity of addition) so that the constant (if there is one) occurs first and then the products occur in the same order.

The resulting LHS and RHS are said to be in “normal form”, i.e., they cannot be simplified any further.

As it happens, such normal forms are unique, and so the ring tactic compares their structure. If the two normal forms are structurally equal, the original Leibniz equality holds, and if they are not structurally equal, the original Leibniz equality does not hold.

And so the proof of twice_S is completed using the ring tactic:

  ring.
Qed.

Interlude

Bong-sun: Wait a minute.

Dana: Er, sure?

Bong-sun: But then all the exercises from Chapter Formalizing a proof with the Coq Proof Assistant...

Dana: Yes. They can be solved using the intros tactic and then the ring tactic.

Pablito: Let me try, let me try:

Proposition binomial_expansion_2 :
  forall x y : nat,
    (x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Proof.
  intros x y.
  ring.
Qed.

Anton: Harrumph.

Resources

• The .v file for the present lecture note (latest version: 05 Jun 2025).

Version

Factored out the present chapter from Chapter More tactics in Week 10 [05 Jun 2025]