Anarchy Proof - Sum of Natural Numbers

最近全然Coqを触ってなかったので、久々にやってみました。

示さないといけないのは、0からnまでの和の2倍が n * (n + 1)に等しいっていうやつで、まぁ何も考えずにnについて帰納法で示せばよいです。ただ、autoとかringとかomegaとかを使うとなぜか負けた気分になるので、使わずに地道に頑張りました。

golfしないといけないのに、全くgolfしてない・・・
後半の方は、a + b + c + d = c + b + a + dみたいな等式を書き換えしてるだけなので、もうちょっと縮むかもしれないですね。

Require Import Definitions.
Require Import Arith.

Theorem Sum_of_nat: forall (n: nat), 2 * sum n = n * (n + 1).
Proof.
induction n.
simpl; reflexivity.
assert (sum (S n) = (S n) + sum n).
induction n; simpl; reflexivity.
assert (S n = 1 + n).
induction n; simpl; reflexivity.
rewrite H.
rewrite H0.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_l.
rewrite IHn.
rewrite mult_plus_distr_l.
rewrite mult_1_l.
rewrite mult_1_r.
assert (1 + n + 1 = n + 2).
rewrite plus_assoc_reverse; rewrite plus_permute.
simpl; reflexivity.
rewrite H1; rewrite mult_plus_distr_l.
rewrite mult_plus_distr_l.
rewrite mult_comm with (m:=2).
do 2 rewrite plus_comm with (m:=(2*n)).
rewrite plus_comm with (n:=(n*n)).
rewrite mult_1_r.
do 2 rewrite plus_assoc_reverse.
do 2 rewrite plus_permute with (m:=2*n).
rewrite plus_permute with (n:=2).
reflexivity.
Qed.

はてな記法には、Coqのシンタックスハイライトないんですね、残念