0
$\begingroup$

Just practicing some induction proofs and was wondering what would be the fastest and most effective way to solve this proof and proofs similar to this?

Lemma randompractice : forall n : nat,
    sum_n_random n * 30 + n * (n + 1) * (2 * n + 1) = n * (n + 1) * (2 * n + 1) * (3 * n * n + 3 * n).
Proof.
Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

The proof is a bit clumsy because you don't have proper subtraction in nat. One way to go is to suppose first that n is not zero.

Lemma randompractice : forall n : nat,
    sum_n_random n * 30 + n * (n + 1) * (2 * n + 1) = n * (n + 1) * (2 * n + 1) * (3 * n * n + 3 * n).
Proof.
destruct n as [|n]; [trivial|].
assert (H : sum_n_random (S n) * 30 =
              S n * (S n + 1) * (2 * S n + 1) * (3 * S n * S n + 3 * n + 2));
    [|rewrite H; ring].
induction n as [|n IH]; [trivial|].
replace (sum_n_random (S (S n)) * 30) with 
             ((S (S n)) * (S (S n)) * (S (S n)) * (S (S n)) * 30 
               + sum_n_random (S n) * 30) by (simpl; ring).
rewrite IH; ring.
Qed.
Improve this answer
$\endgroup$
6
  • $\begingroup$ you really did this! Impressive!! $\endgroup$
    – Lolo
    May 15 at 21:28
  • $\begingroup$ Are you trying to get solution to some class exercises? $\endgroup$
    – Lolo
    May 15 at 23:43
  • $\begingroup$ I think editing a question to ask another question is not in the idea of stack exchange..... $\endgroup$
    – Lolo
    May 15 at 23:51
  • $\begingroup$ Yep but you want other people to be able to keep track of what is going on.too.... $\endgroup$
    – Lolo
    May 15 at 23:55
  • $\begingroup$ Anyway if you are a beginner in Coq and you've managed to solve the inital question. Congrat! $\endgroup$
    – Lolo
    May 15 at 23:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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