# How do I prove this theorem with induction in COQ

Require Import Arith.

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

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

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

Fixpoint sum_odd_n (n:nat) : nat :=
match n with
|  0 => 0
| S p => 1 + 2 * p + sum_odd_n p
end.


(* You may use the following lemma. *)

Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.
Proof.
induction n; simpl; try reflexivity.
replace (S (n + n * S n)) with (S (n + n * n + n)) by ring;
rewrite <- IHn; ring.
Qed.


Question 1 :

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.


Question 2 :

Lemma sum_cube_p : forall n, sum_n3 n = (sum_n n) * (sum_n n).
Proof.
intros. induction n; simpl sum_n3.

Qed.


and

Question 3:

Lemma odd_sum : forall n, sum_odd_n n = n * n.
Proof.

Qed.

• Do you have more context? Why do you define sum_n2? Apr 12 at 1:18
• I guess sum_n2 is wrong. It looks like there should be p * p in the body, instead of n * n. Apr 12 at 1:18
• I edited the post. Apr 12 at 2:01
• I’m voting to close this question because we do not solve homework problems. Apr 12 at 11:04
• I am asking for help not to solve my homework problem smh. I showed what I could figure out so far. Apr 12 at 11:17

You can take advantage of the ring tactic that can prove equality modulo associativity and commutativity

Require Import Arith.

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

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

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

Fixpoint sum_odd_n (n:nat) : nat :=
match n with
|  0 => 0
| S p => 1 + 2 * p + sum_odd_n p
end.

Lemma sum_n_p : forall n, 2 * sum_n n = n * (n + 1).
Proof.
now induction n as [|n IH]; simpl; try ring [IH].
Qed.

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1).
Proof.
now induction n as [|n IH]; simpl; try ring [IH].
Qed.

Lemma sum_cube_p : forall n, sum_n3 n = (sum_n n) * (sum_n n).
Proof.
intro n.
apply (Nat.mul_cancel_l _ _ 4); auto with arith.
now induction n as [|n IH]; simpl; try ring[IH (sum_n_p n)].
Qed.

Lemma odd_sum : forall n, sum_odd_n n = n * n.
Proof.
now induction n as [|n IH]; simpl; try ring [IH].
Qed.