(1 + 2 + ... + n) = n*(n+1) / 2の証明

この問題はCoqの自然数ライブラリを使った。まずを計算するsum関数を定義した。

Require Import Arith.

Fixpoint sum n :=
  match n with
  | O => O
  | S n => S n + sum n
  end.

自然数では割り算が難しいので、全体に2を掛けた次の形をまず証明する。

Lemma p02_aux : forall n, 2 * sum n = n * (n + 1).
Proof.
intro n; induction n.
 reflexivity.
 
 unfold sum in |- *; fold sum in |- *.
 rewrite mult_plus_distr_l in |- *.
 rewrite IHn in |- *.
 ring.
Qed.

自然数では割り算が自由にできないが、次のdiv2 という関数が標準ライブラリにあったのでそれを使った。

Require Import Div2.

Proposition p02 : forall n, sum n = div2 (n * (n + 1)).
Proof.
intros.
rewrite <- p02_aux in |- *.
rewrite div2_double in |- *; reflexivity.
Qed.

今回は自然数の範囲で証明したが、有理数上で証明した方がきれいだったかもしれない。Coqの標準ライブラリにはQArithというのがあり、有理数も標準的に扱うことができる。