Proof Party の問題をCoqで挑戦してみた。

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。

東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん

自然数(エンコーディングは問わず)ã®åŠ ç®—ã®å¯æ›æ³•å‰‡ã€çµåˆæ³•å‰‡ã€åˆ†é…æ³•å‰‡ã‚’è¨¼æ˜Žã€‚

自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。

まず、自然数全体の型 nat を定義する。

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

次にこの自然数上での足し算を計算する plus 関数を定義する。

Fixpoint plus x y :=
  match x with
  | O => y
  | S x => S (plus x y)
  end
where "x + y" := (plus x y).

まず一番簡単な足し算の結合則を証明する。

Proposition p01_plus_assoc :
  forall x y z, x + (y + z) = (x + y) + z.
Proof.
intros x y z; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

次に足し算の可換性を証明しようと思うが、そのために次の2つの補題を証明しておく。
ちなみに O+x = x と S x + y = S (x + y) は定義より明らかに成り立つことなので、あえて補題を用意することはしない。

Lemma plus_O : forall x, x + O = x.
Proof.
intro x; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

Lemma plus_Sy : forall x y, x + S y = S (x + y).
Proof.
intros x y; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

そして、足し算の可換性。

Proposition p01_plus_comm :
  forall x y, x + y = y + x.
Proof.
intros x y; induction x; simpl.
 rewrite plus_O in |- *; reflexivity.
 rewrite IHx in |- *; rewrite plus_Sy in |- *.
 reflexivity.
Qed.

あとは分配法則だが、これには掛け算が必要なので掛け算を定義する。

Fixpoint mult x y :=
  match x with
  | O => O
  | S x => y + mult x y
  end
where "x * y" := (mult x y).

左からの分配法則は簡単である。上で証明した足し算の結合則や可換性をバリバリ使っているのがわかるだろう。

Proposition p01_distr_l :
  forall x y k, k * (x + y) = k * x + k * y.
Proof.
intros x y k; induction k; simpl in |- *.
 reflexivity.
 
 rewrite IHk in |- *.
 rewrite <- (p01_plus_assoc x y _) in |- *.
 rewrite (p01_plus_assoc y (k * x) (k * y)) in |- *.
 rewrite (p01_plus_comm y (k * x)) in |- *.
 rewrite <- (p01_plus_assoc (k * x) y (k * y)) in |- *.
 rewrite (p01_plus_assoc x (k * x) _) in |- *.
 reflexivity.
Qed.

掛け算の可換性があれば右からの分配法則も示せるので、掛け算の可換性を証明。足し算の可換性と同様にいくつかの補題を証明して使った。

Lemma mult_O :
  forall x, x * O = O.
Proof.
intros x; induction x; simpl in |- *.
 reflexivity.
 apply IHx.
Qed.

Lemma mult_Sy :
  forall x y, x * S y = x + x * y.
Proof.
intros x y; induction x; simpl in |- *.
 reflexivity.
 
 rewrite IHx in |- *.
 rewrite (p01_plus_assoc y x (x * y)) in |- *.
 rewrite (p01_plus_comm y x) in |- *.
 rewrite <- (p01_plus_assoc x y (x * y)) in |- *.
 reflexivity.
Qed.

Lemma mult_comm :
  forall x y, x * y = y * x.
Proof.
intros x y; induction x; simpl in |- *.
 rewrite mult_O in |- *; reflexivity.
 
 rewrite mult_Sy in |- *.
 rewrite IHx in |- *.
 reflexivity.
Qed.

右からの分配法則。

Proposition p01_distr_r :
  forall x y k, (x + y) * k = x * k + y * k.
Proof.
intros x y k.
rewrite (mult_comm (x + y) k) in |- *.
rewrite (mult_comm x k) in |- *.
rewrite (mult_comm y k) in |- *.
apply p01_distr_l.
Qed.

(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というのがあり、有理数も標準的に扱うことができる。

実数の構成について

Coqでの実数は9つの項と17の公理で定義されている。項の型と意味はだいたい次の様な感じ。

Parameter R : Set. (* 実数全体 *)

Parameter R0 : R. (* 実数の0 *)
Parameter R1 : R. (* 実数の1 *)
Parameter Rplus : R -> R -> R. (* 実数上での足し算 *)
Parameter Rmult : R -> R -> R. (* 実数上での掛け算 *)
Parameter Ropp : R -> R. (* 足し算に関する逆元 *)
Parameter Rinv : R -> R. (* 掛け算に関する逆元 *)
Parameter Rlt : R -> R -> Prop. (* 実数上の"より大きい"を表す述語 *)
Parameter up : R -> Z. (* up x はx以上の最小の整数 *)

17の公理は、大きく見て4つの部分に分けられる。

• 実数Rは非自明な体である

Axiom Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
Axiom Rplus_opp_r : forall r:R, r + - r = 0.
Axiom Rplus_0_l : forall r:R, 0 + r = r.
Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
Axiom Rmult_1_l : forall r:R, 1 * r = r.
Axiom R1_neq_R0 : 1 <> 0.
Axiom Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.

• 実数Rは全順序集合である

Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
Axiom Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
Axiom Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
Axiom Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
Axiom Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.

• アルキメデスの原理(いかなる実数に対してもそれより大きい整数が存在する。)

up xは天井関数、IZRは整数Zからの包含写像

Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.

• 実数Rの連続性(上に有界な領域 E ⊂ R には常に上限が存在する)。

Axiom
  completeness :
    forall E:R -> Prop,
      bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.

Bolzano & Weierstrassの定理(有界な数列は収束する部分列を持つ)

Bolzano Weierstrass の定理はCoqではもう既に証明されていて、しかもそれは標準ライブラリに備わっている！
Rtopology.vというライブラリのソースを見ればこの定理を見つけることができる。

Theorem Bolzano_Weierstrass :
  forall (un:nat -> R) (X:R -> Prop),
    compact X -> (forall n:nat, X (un n)) ->  exists l : R, ValAdh un l.

実数列unは nat -> R 型で、領域 X ⊂ R はR -> Prop 型で表現しているようだ。

ValAdh un lの定義は以下のとおりで、lに収束するunの部分列が存在することと同等の命題みたいだ。

Definition ValAdh (un:nat -> R) (x:R) : Prop :=
  forall (V:R -> Prop) (N:nat),
    neighbourhood V x ->  exists p : nat, (N <= p)%nat /\ V (un p).

中間値の定理(The Intermediate Value Theorem)

中間値の定理もCoqの標準ライブラリに存在する。Rsqrt_def.vの中にIVTという名前で見つけることができる。

Lemma IVT :
  forall (f:R -> R) (x y:R),
    continuity f ->
    x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.

ただ、中間値が f x と f y の間の任意の値というわけではなく、0固定だったので、そこを任意の値が取れるように改良した。

Require Import Reals.
Require Import FunctionalExtensionality.
Open Scope R_scope.

Proposition p05 :
  forall (f:R -> R) a b y,
    continuity f ->
    a < b ->
    f a < y ->
    y < f b ->
    (exists c, a <= c <= b /\ f c = y).
Proof.
intros.
elim (IVT (fun x => f x - y) a b).
 intros c H3; elim H3; intros; exists c.
 split.
  apply H4.
  
  apply (Rplus_eq_reg_l (- y)).
  rewrite Rplus_opp_l in |- *.
  rewrite Rplus_comm in |- *.
  apply H5.
  
 rewrite
  (functional_extensionality (fun x : R => f x - y) (f - (fun _ => y))%F)
  in |- *.
  apply continuity_minus.
   apply H.
   
   apply continuity_const.
   intros p q; reflexivity.
   
  intro x; reflexivity.
  
 apply H0.
 
 apply (Rlt_minus (f a) y H1).
 
 apply (Rlt_Rminus y (f b) H2).
Qed.

リストの結合関数 ++ の結合則 l1 ++ (l2 ++ l3) == (l1 ++ l2) ++ l3

リストのappendの結合則は非常に便利だが、証明は簡単だ。こういった性質はテストでは網羅的にチェックできないため、証明という検証方法がプログラムの品質を高める上で非常に有効だと思う。

Require Import List.

Proposition p06 :
  forall {A} (l1 l2 l3: list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Proof.
intros A l1 l2 l3; induction l1; simpl in |- *.
 reflexivity.
 
 rewrite IHl1 in |- *.
 reflexivity.
Qed.

reverse (reverse list) == listとなる事を示す

http://d.hatena.ne.jp/yoshihiro503/20090708 で証明した。

あるソート関数がちゃんとソートする事を証明

以前Merge Sort を実装して証明した。
http://d.hatena.ne.jp/yoshihiro503/20090923

ソースコード全体は以下。
http://bitbucket.org/yoshihiro503/mergesort/

1階命題論理でresolutionが成り立つ事を示す

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。

Proposition p09 :
  forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C.
Proof.
intros A B C H; elim H; intros.
elim H0.
 elim H1.
  intros H2 H3; elim H2.
    apply H3.
 intros H2 _; right; apply H2.
intro H2; left; apply H2.
Qed.

直観主義論理での二重否定除去と排中律の同値性

同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。

Lemma p10_left :
  (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)).
Proof.
intros.
apply H.
intro.
elim (H0 H2).
apply H1.
Qed.

Lemma p10_right :
  (forall A B, (~B -> ~A) -> (A -> B)) -> (forall A, ~~A -> A).
Proof.
intros.
apply (H True A).
 intro.
   intro.
   elim H0.
   apply H1.
apply I.
Qed.