【Coq】掛け算の交換法則を証明してみた。

●はじめに

たまに物議を醸す掛け算の順番について。

「掛け算の定義より自明」なんて説明じゃ学校の先生は納得してくれなそうなので、定理証明支援系のプログラミング言語であるCoqを用いて証明をしてみました。以前軽く紹介したペアノ自然数を用いています。

●証明

(* 自然数の定義 *)
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.


(* 足し算と掛け算の定義 *)
Fixpoint add (m n : nat) : nat :=
  match m with
  | O    => n
  | S m' => S (add m' n)
  end.

Fixpoint mul (m n : nat) : nat :=
  match m with
  | O    => O
  | S m' => n + (mul m' n)
  end.

(* シンタックスシュガーみたいなヤツの定義 *)
Notation "m + n" := (add m n) (at level 50, left associativity).
Notation "m * n" := (mul m n) (at level 40, left associativity).


(* 各種証明 *)
Theorem add_identity_l (n : nat) : n + O = n.
Proof.
  induction n.
  + reflexivity.
  + simpl.
    rewrite IHn.
    reflexivity.
Qed.

Theorem add_assoc : forall m n l : nat, (m + n) + l = m + (n + l).
Proof.
  induction m.
  + reflexivity.
  + intros n l.
    simpl.
    rewrite IHm.
    reflexivity.
Qed.

Theorem add_suc_r (m n : nat) : m + S n = S (m + n).
Proof.
induction m.
  + reflexivity.
  + simpl.
    rewrite IHm.
    reflexivity.
Qed.

Theorem add_comm (m n : nat) : m + n = n + m.
Proof.
  induction n.
  + apply add_identity_l.
  + rewrite add_suc_r.
    rewrite IHn.
    reflexivity.
Qed.

Theorem mul_univ_r (n : nat) : n * O = O.
Proof.
induction n.
  + reflexivity.
  + simpl.
    apply IHn.
Qed.

Theorem mul_suc_r (n m : nat) : n * S m = n + n * m.
Proof.
  induction n.
  + reflexivity.
  + simpl.
    rewrite IHn.
    rewrite <- (add_assoc m n (n * m)).
    rewrite (add_comm m n).
    rewrite <- (add_assoc n m (n * m)).
    reflexivity.
Qed.
   
Theorem mul_comm (n m : nat) : n * m = m * n.
Proof.
  induction n.
  + symmetry.
    apply mul_univ_r.
  + rewrite mul_suc_r.
    simpl.
    rewrite IHn.
    reflexivity.
Qed.

●おわりに

これで小学生も安心して掛け算の交換法則を使えますね。

めでたしめでたし。