読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqで同値関係

同値関係 実務 Function Defined Extract Inductive

最近仕事でlistの要素を仲間分けしてリストのリストを返す 次のような関数をOCamlで定義した。

let rec classify rel l =
  match l with
  | [] -> []
  | x::xs ->
     let (ys,zs) = List.partition (fun y -> rel x y) xs in
     (x, ys) :: classify rel zs

この関数はlistの先頭要素をみてそれと仲間のものをlistから抽出する。そして残ったものに対して再帰的に処理を行うといった感じだ。
引数で与えられる rel は仲間かどうかの判定関数で、 x と y が仲間なときにだけ rel x y は true となる。

この関数は数学の世界で言う同値関係(equivalence relation)による類別(classification)を求める関数になっていてほしい。
つまり分類されたどのクラスに対してもそのクラスに属する任意の二元は仲間同士であることが成り立ってほしい。

この関数はサービスの根幹となる部分で使われていたので、同様の関数をCoqで定義して証明してみた。

まずは関数の定義:

Function classify (rel: A -> A -> bool) (l: list A) {measure length l} : list (A * list A) :=
  match l with
  | nil => nil
  | x::xs =>
     let (ys,zs) := List.partition (fun y => rel x y) xs in
     (x, ys) :: classify rel zs
  end.
(*  停止性の証明  *)
Defined.

この関数は再帰関数になっているが、再帰呼び出しで与えるリストが小さくなっているかどうかが明らかでないため、停止性が自明ではない。
しかし、よく考えると l の尻尾である xs を partition分けした一方に対して再帰呼び出しをしているので、停止するのは明らかだ。
明らかならば証明しよう。Functionコマンドを使うと関数の素直な実装と停止性の証明を分けて書けるので非常に便利である。

次にこの関数がさっき述べた性質を満たしているかどうか証明した。

Theorem t : forall (a x y: A) (clas: list A)
  (lst: list A) (rel: A -> A -> bool),
  Equivalence_bool rel -> In x clas -> In y clas ->
     In (a, clas) (classify rel lst) -> rel x y = true.

ただし、与えられる関係relが同値関係の公理を満たしていることが前提として必要である。Equivalence_bool relという
前提がそのことを表している。この定理を証明するために一つ簡単なLemmaを証明してそれを使った。ソースコードの全体は以下である。

Require Import List.

Section ListClassification.
Variable A: Set.

Lemma partition_length
     : forall  (f : A -> bool) (l yess nos: list A),
         (yess, nos) = partition f l ->
         length l = length yess + length nos.
Proof.
intros f l; induction l.
 intros.
   inversion H.
   simpl in |- *; reflexivity.
simpl in |- *.
  case (f a).
 generalize IHl.
   case (partition f l).
   intros ys ns IHl'.
   intros.
   inversion H.
   simpl in |- *.
   rewrite (IHl' ys ns) in |- *.
  reflexivity.
 reflexivity.
generalize IHl.
  case (partition f l).
  intros ys ns IHl'.
  intros.
  inversion H.
  simpl in |- *.
  rewrite <- plus_n_Sm in |- *.
  rewrite (IHl' ys ns) in |- *; reflexivity.
Qed.


Require Import Recdef.

Function classify (rel: A -> A -> bool) (l: list A) {measure length l} : list (A * list A) :=
  match l with
  | nil => nil
  | x::xs =>
     let (ys,zs) := List.partition (rel x) xs in
     (x, ys) :: classify rel zs
  end.
intros.
simpl in |- *.
rewrite (partition_length (rel x) xs ys zs) in |- *.
 apply Lt.le_lt_n_Sm.
   apply Plus.le_plus_r.
rewrite teq0 in |- *; reflexivity.
Defined.

(* equivalence relations bool ============== *)
Definition R r (x y:A) : Prop := r x y = true.
Definition Reflexive_bool (r:A->A->bool) : Prop := forall x:A, R r x x.
Definition Transitive_bool (r:A->A->bool): Prop :=
  forall x y z:A, R r x y -> R r y z -> R r x z.
Definition Symmetric_bool (r:A->A->bool) : Prop :=
  forall x y:A, R r x y -> R r y x.
Inductive Equivalence_bool (r:A->A->bool) : Prop :=
  Def_of_Equiv_bool : Reflexive_bool r -> Transitive_bool r -> Symmetric_bool r -> Equivalence_bool r.
(* ========================================= *)


Lemma partition_spec : forall (f : A -> bool) (l : list A) x ys ns,
   (ys, ns) = partition f l -> In x ys -> f x = true.
Proof.
   intros f l; induction l.
 simpl in |- *; intros.
   inversion H.
   rewrite H2 in H0; elim H0.
simpl in |- *.
  elim (Bool.bool_dec (f a) true).
 intros eq; rewrite eq in |- *.
   generalize IHl.
   case (partition f l).
   intros yys nns IHl'.
   intros.
   inversion H.
   rewrite H2 in H0.
   elim (in_inv H0).
  intros eq2; rewrite <- eq2 in |- *; apply eq.
 apply (IHl' x yys nns).
   reflexivity.
intros neq.
  generalize IHl.
  case (partition f l).
  intros yys nns IHl'.
  rewrite (Bool.not_true_is_false (f a) neq) in |- *.
  intros.
   eapply IHl'.
   reflexivity.
  inversion H.
  rewrite H2 in H0; apply H0.
Qed.


Lemma classify_lem : forall a c r l,
  In (a, c) (classify r l) -> (forall x, In x c -> r a x = true).
Proof.
intros a c r l.
apply
 (classify_ind r
    (fun l cl => In (a, c) cl -> forall x : A, In x c -> r a x = true)).
 intros.
   elim H.
intros.
  elim (in_inv H0).
 intros eq; inversion eq.
    eapply (partition_spec (r a) xs x0 ys zs).
  rewrite <- e0 in |- *; rewrite H3 in |- *; reflexivity.
 rewrite H4 in |- *; apply H1.
intro H2; apply H.
 apply H2.
apply H1.
Qed.


Theorem t : forall (a x y: A) (clas: list A)
  (lst: list A) (rel: A -> A -> bool),
  Equivalence_bool rel -> In x clas -> In y clas ->
     In (a, clas) (classify rel lst) -> rel x y = true.
Proof.
intros.
elim H.
unfold Transitive_bool.
unfold Symmetric_bool.
unfold R in |- *.
intros.
apply (H4 x a y).
  apply H5.
  apply (classify_lem _ _ _ _ H2 x H0).
apply (classify_lem _ _ _ _ H2 y H1).
Qed.

End ListClassification.

(*
    (* optional for Coq 8.2 *)
    Extract Inductive list => list [ "[]" "(::)" ].
    Extract Inductive prod => "(*)" [ "(,)" ].
    Extract Inductive bool => "bool" [ "true" "false" ].
*)

Extraction "listClassification.ml" classify.