何かを読む会 という社内勉強会が発足されました。読んだ本の内容を共有しよう。一人で勉強していてもダレるので共有することで無理やり進捗を出そう。他の人の発表を聞いて読んだ気になろう。っていう緩めの会です。途中まで読んで放置していたプログラミング Coq の続きを読んでまとめました。

挿入ソートを証明する。

証明したいことは次の二点。

挿入前と挿入後で要素に変化がないこと(isort_permutation)
挿入後に要素が整列されていること(isort_sorted)

上記を型で示すと以下のようになる。

isort_permutation : forall (l : list nat), Permutation l (insertion_sort l)
isort_sorted      : forall (l : list nat), LocallySorted le (insertion_sort l)

実装

Require Import List.
Require Import Arith.

Fixpoint insert (a : nat) (l : list nat) : list nat :=
  match l with
  | nil => a :: nil
  | x :: xs => if leb a x then a :: l else x :: insert a xs
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | nil => nil
  | x :: xs => insert x (insertion_sort xs)
  end.

要素の変化がないこと

あるリストがあるリストと同じ要素で成り立っているのは以下のモジュールで定義されている。

Inductive Permutation : list A -> list A -> Prop :=
  | perm_nil: Permutation [] []
  | perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
  | perm_swap x y l : Permutation (y::x::l) (x::y::l)
  | perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''.

nil と nil は同じ要素から成り立つ
l と l' が同じ要素から成り立つならば x :: l と x :: l' も同じ要素から成り立つ
y :: x :: l と x :: y :: l は同じ要素から成り立つ
(l と l' が同じ要素から成り立ち、l' と l'‘ が同じ要素から成り立つ) ならば l と l’‘ も同じ要素から成り立つ

isort_permutation の証明

isort_permutation の型

forall (l : list nat), Permutation l (insertion_sort l)

帰納法を使う。 l が nil の時は insertion_sort l は nil なので Permutation nil nil となり自明。

帰納法のため、nの場合にあたる仮定は

forall (l : list nat), Permutation xs (insertion_sort xs)

n + 1 に当たる命題は

forall (l : list nat), Permutation x :: xs (insertion_sort x::xs)

となり、

forall (l : list nat), Permutation x :: xs (insert x (insertion_sort xs)

と変形できる。

つまり

forall (l : list nat), Permuation x :: xs (x :: insertion_sort xs)

と

forall (l : lsit nat), Permutation (x :: insertion_sort xs) (insert x (insertion_sort xs)

を示すことで perm_trans から

forall l l' l'' , Permutation l l' -> Permutation l' l'' -> Permutation l l''

Permutation (x :: xs) (x :: insertion_sort xs) ->
  Permutation (x :: insertion_sort xs) (insert x (insertion_sort xs)) ->
    Permutation (x :: xs) (insert x (insertion_sort xs))

となり、導ける。

A については仮定と Permutation のコンストラクタ

perm_skip : forall x l l', Permutation l l' -> Permutation (x :: l) (x :: l')

から導ける。

まず B を補題として証明する。

isort_permutaiton の証明は以下。

命令	説明
intros	forall などから変数を仮定へ移動する
simpl	簡約
apply	仮定や定理などを適用
destruct	条件分岐しているものなどを subgoal に分ける
induction	帰納法を実施するために subgoal に分ける

どういうふうに証明が進むかは coq ide や proof-general 使って見てください。

Require Import List.
Require Import Arith.
Require Import Sorting.Permutation.
Require Import Sorting.Sorted.

(* isort_permutation *)

Lemma insert_perm : forall (x : nat)(l : list nat), Permutation (x :: l) (insert x l).
  induction l.
  intros.
  simpl.
  apply Permutation_refl.

  intros.
  simpl.
  destruct (leb x a).

  apply Permutation_refl.

  apply perm_trans with (a :: x :: l).
  apply perm_swap.

  apply perm_skip.
  apply IHl.
Qed.

Theorem isort_permutation : forall (l : list nat), Permutation l (insertion_sort l).
  induction l.
  apply perm_nil.
  simpl.
  apply perm_trans with (a :: insertion_sort l).
  apply perm_skip.
  apply IHl.
  apply insert_perm.
Qed.

整列の定義

リスト l が整列されていることはSorting.Sortedモジュールで定義されている.

Induction LocallySorted (A : Type) (R : A -> A -> Prop) : list A :=
  | LSorted_nil : LocallySorted R nil
  | LSorted_cons1 : forall a : A, LocallySorted R (a :: nil)
  | LSorted_consn : forall (a b : A) (l : list A),
    LocallySorted R (b :: l) ->
      R a b -> LocallySorted R (a :: b :: l)

上の定義は次のような意味です。 R a b は a < b のようなものです。

nil は整列している
x :: nil は整列している
b :: l が整列しているとき, R a b ならば a :: b :: l は整列している

整列されていることの証明

こちらでも帰納法で考える。まず l が nil の場合は insertion_sort nil = nil となり、LSorted_nil : LocallySorted le nil から明らか。

LocallySort le (insertion_sort l) -> LocallySort le (insertion_sort (a :: l)) の場合を考える。 LocallySort le (insertion_sort (a ::l) は LocallySort le (insert a (insertion_sort l))と変形できる。この時、insertion_sort l は仮定より整列しているため、

insert_sorted : forall (a : nat) (l : list a), LocallySort le l -> LocallySorted le (insert a l)

を示すことができれば証明できる。

これを補題として証明をすすめる。

整列の証明

Lemma insert_sorted : forall (a : nat) (l : list nat),
    LocallySorted le l -> LocallySorted le (insert a l).
  induction l.
  constructor.

  intro.
  simpl.
  remember (leb a a0).
  destruct b.

  apply LSorted_consn.
  apply H.
  apply leb_complete.
  congruence.

  inversion H.
  simpl.
  apply LSorted_consn.
  apply LSorted_cons1.
  apply lt_le_weak.
  apply leb_complete_conv.
  congruence.

  subst.
  simpl.
  simpl in IHl.
  remember (leb a b).

  destruct b0.
  apply LSorted_consn.
  apply IHl.
  apply H2.

  apply lt_le_weak.
  apply leb_complete_conv.
  congruence.

  apply LSorted_consn.
  apply IHl.
  apply H2.
  apply H3.
Qed.

Theorem isort_sorted : forall (l : list nat) , LocallySorted le (insertion_sort l).
  induction l.
  constructor.

  simpl.

  apply insert_sorted.
  apply IHl.
Qed.

これで isertion_sort はソートの前後で要素が変わらないことと、ソート後に整列されていることが証明できた。

(wat-aro)

生きてます

プログラミング Coq 証明駆動開発(1)