How can I prove this theorem with induction in Coq?

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1).


where sum_n2 is defined

Fixpoint sum_n2 n := match n with 0 => 0 | S p => n*n + sum_n2 p end.


after applying these tactics:

- intros.
- induction n.
- simpl.
- reflexivity.


I get here:

1 subgoal
n : nat
IHn : 6 * sum_n2 n = n * (n + 1) * (2 * n + 1)

______________________________________(1/1)

6 * sum_n2 (S n) = S n * (S n + 1) * (2 * S n + 1)


My goal is almost identical to my hypothesis but instead of just n's, every instance of n is S n and I do not know where I can go from here.

• You could try simpl (sum_n2 (S n)).
– Couchy
Apr 18 at 2:06
• Also, the lia tactic (for linear arithmetic) is your best friend here, use Require Import Lia.
– Couchy
Apr 18 at 4:12
• is there a way to go about this without using the lia tactic? Apr 18 at 6:40
• How would you prove it on paper? Apr 18 at 7:47

The beginning of the proof looks as follows:

Require Import Coq.Arith.PeanoNat.
Fixpoint sum_n2 n := match n with 0 => 0 | S p => n*n + sum_n2 p end.
Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1).
Proof.
intros n.
induction n.
- simpl. reflexivity.
- simpl (sum_n2 (S n)).
rewrite Nat.mul_succ_r.
rewrite IHn.


there you obtain the goal

6 * n + 6 * (n * S n) + n * (n + 1) * (2 * n + 1) + 6 =
(S n * S n + S n * 1) * (2 * S n) + (S n * S n + S n * 1) * 1


This can be finished off with the linear arithmetic lia tactic. You can try to prove this without lia (it is at least a good exercise in understanding the Coq standard library), but you will quickly realize it is not worth your time and sanity.

• Thank you! I finished it off using the ring tactic Apr 18 at 22:41
– Couchy
Apr 19 at 3:02

There have been several good answers to this question, so I'm not trying to compete with them, but rather offer a peculiar angle on this problem as food for thought and potential for a useful library contribution.

I would not prove the lemma by induction. I would simply test that it holds for 0, 1, 2 and 3. The fact that those tests pass is sufficient to show that the lemma holds universally.

But how do I obtain the proof by mere testing? I need to observe that the degree of the formulae on both sides of the equation is three: the left sums over a quadratic, and summation increments degree; the right is the product of three linear forms.

Of course, the proof that degree n formulae agree everywhere if they agree on 0..n requires induction on n. It's a rather amusing exercise. The trick is to ensure that your language of formulae is closed under taking the forward difference, i.e., that given some f, you can always compute df such that for all n, f(n+1) = f(n) + df(n). (The point is that df inverts the summation operator.) Then you prove that when f has nonzero degree, df has degree one less. Now, f agrees with g on 0..n+1 if and only if f(0) = g(0) and df agrees with dg on 0..n.

Fixpoint sum_n2 n := match n with 0 => 0 | S p => n*n + sum_n2 p end.

Theorem sum_n2_S n: sum_n2 (S n) = (S n) * (S n) + sum_n2 n.
Proof.
reflexivity.
Qed.

Theorem add_zero a: a + 0 = a.
Proof.
induction a.
+ simpl. reflexivity.
+ simpl. rewrite IHa. reflexivity.
Qed.

Theorem sum_S a b: S (a + b) = a + S b.
Proof.
induction a.
+ simpl. reflexivity.
+ simpl. rewrite IHa. reflexivity.
Qed.

Theorem sum_comm a b: a + b = b + a.
Proof.
induction a.
+ simpl. rewrite IHa. rewrite sum_S. reflexivity.
Qed.

Theorem sum_assoc a b c: a + (b + c) = (a + b) + c.
Proof.
induction a.
+ simpl. auto.
+ simpl. rewrite IHa. reflexivity.
Qed.

Theorem aux0 a b c: a * (b + c) = a * b + a * c.
Proof.
induction a.
+ simpl. reflexivity.
+ simpl. rewrite IHa. rewrite <- (sum_assoc b c (a * b + a * c)).
rewrite <- (sum_assoc b (a * b) (c + a * c)).
rewrite (sum_assoc c (a * b) (a * c)).
rewrite (sum_comm c (a * b)).
rewrite <- (sum_assoc (a * b) c (a * c)).
reflexivity.
Qed.

Theorem aux1 n m: n + S m = S (n + m).
Proof.
induction n.
+ simpl. reflexivity.
+ simpl. rewrite IHn. reflexivity.
Qed.

Theorem aux2 n m: n * S m = n + n * m.
Proof.
induction n.
+ simpl. reflexivity.
+ simpl. rewrite IHn. rewrite sum_assoc. rewrite (sum_comm m n).
rewrite <- sum_assoc. reflexivity.
Qed.

Theorem mult_zero n: n * 0 = 0.
Proof.
induction n.
+ simpl. reflexivity.
+ simpl. rewrite IHn. reflexivity.
Qed.

Theorem mult_comm n m: n * m = m * n.
Proof.
induction n.
+ simpl. rewrite mult_zero. reflexivity.
+ simpl. rewrite aux2. rewrite IHn. reflexivity.
Qed.

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1).
Proof.
induction n.
+ simpl. reflexivity.
+ rewrite sum_n2_S. rewrite aux0. rewrite IHn. simpl.
(* remove all additions of zero *)
(* try to move all S to the start of the expression *)
rewrite aux1. rewrite aux1. rewrite aux1. rewrite aux1.
rewrite aux1. rewrite aux1. rewrite aux1. rewrite aux1.
rewrite aux1. rewrite aux1. rewrite aux1. rewrite aux1.
rewrite aux1. rewrite aux1. rewrite aux1. rewrite aux1.
rewrite aux1. rewrite aux1. rewrite aux1.
(* again remove all additions of zero *)
(* keep moving S to the start *)
rewrite aux1. rewrite aux1. rewrite aux1.
(* transform all a * S b to a + a * b *)
rewrite aux2. rewrite aux2. rewrite aux2. rewrite aux2.
rewrite aux2. rewrite aux2. rewrite aux2.
(* try to move all n * n to start *)
rewrite (sum_comm n (n * n)).
(* simplify (?) a bit using associativity of addition *)
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
(* *)
rewrite aux0. rewrite aux0.
rewrite (mult_comm (n * n + n) n).
rewrite (mult_comm (n + n + n * n + n) n).
rewrite (sum_comm n (n * n)).
rewrite sum_assoc. rewrite sum_assoc.
rewrite aux0. rewrite aux0. rewrite aux0. rewrite aux0.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc. rewrite sum_assoc.
rewrite sum_assoc. rewrite sum_assoc.
(* ok, let's move n * (n * n) to start or smth like that *)

• FYI you can use repeat rewrite ... to repeat the rewrite until the goal no longer changes