3
$\begingroup$
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.

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

4 Answers 4

2
$\begingroup$

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.
  repeat rewrite Nat.mul_add_distr_l.
  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.

$\endgroup$
2
  • $\begingroup$ Thank you! I finished it off using the ring tactic $\endgroup$ Apr 18 at 22:41
  • $\begingroup$ @NovaSczerin If this answers your question, please accept the answer $\endgroup$
    – Couchy
    Apr 19 at 3:02
9
$\begingroup$

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.

$\endgroup$
2
$\begingroup$
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 add_zero. reflexivity.
  + 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 *)
    rewrite add_zero. rewrite add_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 *)
    rewrite add_zero. rewrite add_zero. rewrite add_zero. simpl.
    (* 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 *)
    admit.
    (* Too tired to finish *)
Admitted.

This is how far I got, using only intro, induction, simpl, reflexivity AND rewrite (as without rewrite you get nowhere). Not sure if that was an optimal way of doing this, but... And then I resigned.

The task isn't for humans to do, as it is very frustrating - manually manipulate expressions using lots of rewrites. This is why lia, ring and similar tactics are made - to allow humans skip the boring part.

$\endgroup$
2
  • $\begingroup$ wow thats a lot of rewrites! can ring be implemented instead somewhere? $\endgroup$ Apr 18 at 21:55
  • $\begingroup$ FYI you can use repeat rewrite ... to repeat the rewrite until the goal no longer changes $\endgroup$
    – Couchy
    Apr 18 at 21:59
1
$\begingroup$

It comes out quite concisely with the use of ArithRing.

Require Import Arith.

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.
  intro. induction n; simpl sum_n2.
  - ring.
  - ring_simplify. rewrite IHn. ring.
Qed.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.