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.