Closed-expression of a sum with proof in Coq

Pretty obsessed with chess lately, but this weekend I had some fun with mathematics after spotting this tweet.

One well known fact is the sum $1 + 2 + \ldots + n = \frac {n(n + 1)} {2}$ . Let’s try to prove this fact in Coq. Some time ago, I wrote a similar post but using the Idris programming language.

The code

I will not walk through the code I wrote, I’ll just post it here:

Fixpoint sum (n : nat) : nat :=
  match n with
  | 0   => 0
  | S n => sum n + S n
  end.

Lemma lemma1 : forall n m o : nat,
  m = o -> n + m = n + o.
Proof.
  intros n m o.
  intros H1.
  rewrite H1.
  reflexivity.
Qed.

Lemma sum_closed_expr_basic : forall n : nat, 2 * sum n = n * (n + 1).
Proof.
  intros. induction n.
  - reflexivity.
  - simpl.
    rewrite <- mult_n_Sm.
    rewrite <- IHn.
    rewrite <- plus_n_O. simpl.
    rewrite (plus_comm (sum n) (S n)).
    simpl.
    apply f_equal.
    rewrite <- plus_n_O.
    rewrite <- plus_assoc. rewrite <- plus_assoc.
    apply lemma1.
    simpl.
    rewrite plus_comm. simpl.
    apply f_equal.
    rewrite <- (plus_comm (sum n) (n + sum n)).
    rewrite <- (plus_comm (sum n) n). rewrite plus_assoc.
    reflexivity.
Qed.

It’s pretty dirty, manually tweaking the equation until reflexivity is reached. Of course, I’m not an expert with the Coq programming language, so I thought there must be a cleaner way of doing this 🙂

The magical solution

After googling, I found a very neat solution:

Lemma sum_closed_expr : forall n : nat, 2 * sum n = n * (n + 1).
  intros.
  induction n.
  trivial.
  cbv [sum].
  rewrite mult_plus_distr_l.
  fold sum.
  rewrite IHn.
  ring.
Qed.

Woot! Magic. What caught my eye is the ring tactic; how did it just manage to prove $n \cdot (n + 1) + 2 \cdot S n = S n \cdot (S n + 1)$ ?

To make it more explicit, instead of ring we can try using ring_simplify. It produces the following equation: $n \cdot n + 3 \cdot n + 2 = n \cdot n + 3 \cdot n + 2$ which easily follows with reflexivity.

Digging a little bit more, I found in the docs that ring tactic normalizes polynomials over any ring or semiring structure. But what does that mean? Well, it’s basically a solver for ring polynomial equations, but we cannot just use it on any equation. So what are polynomial ring equations?

Polynomial rings?!

We’ll paste some definitions here, according to this script by Open University:

Let R be a set and let + and $\cdot$ be binary operations on R. Then (R,+, $\cdot$ ) is a ring if the following axioms hold: closure (+ and $\cdot$ ), associativity (+ and $\cdot$ ), additive and multiplicative identity, additive inverses, commutativity (+ and $\cdot$ ), distributivity

And for the field:

A (commutative) ring R is a field if the additive and multiplicative identities are distinct, and every non-zero element is a unit.

Now we finally get to polynomial rings:

Let F be a field. Then a polynomial over F with the variable x is a polynomial of the form $f(x) = a_0 + a_1x + a_2x^2 + \ldots + a_nx^n$ , where $a_0, a_1, a_2, \ldots, a_n \in F$ and $n \geq 0$ , where $x^0$ is defined to be 1.
The polynomial ring over F is
$F[x] = {a_0 + a_1x + \ldots + a_nx^n : a_0, a_1, \ldots, a_n \in F, n \geq 0}$ .

The tactic in Coq works on naturals, so everywhere you see R you can replace with $\mathbb{N}$ , and the operators are the usual addition and multiplication.