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.

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

4 Answers 4

Reset to default
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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you! I finished it off using the ring tactic $\endgroup$
    – Nova Sczerin
    Commented Apr 18, 2022 at 22:41
  • $\begingroup$ @NovaSczerin If this answers your question, please accept the answer $\endgroup$
    – Couchy
    Commented Apr 19, 2022 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.

Improve this answer
$\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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ wow thats a lot of rewrites! can ring be implemented instead somewhere? $\endgroup$
    – Nova Sczerin
    Commented Apr 18, 2022 at 21:55
  • $\begingroup$ FYI you can use repeat rewrite ... to repeat the rewrite until the goal no longer changes $\endgroup$
    – Couchy
    Commented Apr 18, 2022 at 21:59
2
$\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.
Improve this answer
$\endgroup$

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