概要
unit は１つの要素 tt を持ち、 bool は２つの要素 true と false を持ちます。一般に、nつの要素を持つ Set を表現する型として、標準ライブラリに型 Fin.t が存在します。unitやboolがそうであるように Fin.t もまた Inductive に定義されます。一方、 Recursive に定義する方法もあるはずで、それを ffin と呼びましょう。また、subset type を使った型 forall n, {k | k < n} で定義する方法も思いつき、これを iset と呼びましょう。
本稿ではまず、ffin, iset を定義してそれらが Fin.t と（集合として）同型であることを示します。特にiset nの要素数は直観的に n だとわかるので Fin.t, ffin の要素数も意図通りに n だという確証が得られ、ひと安心できるわけです。
続いて、より具体的な例として、Fin.t 2 の要素が F1 と FS F1 の２つしかないことなどをPropで表現して証明してみます。依存型の場合分けを含むので、テクニカルには少し難しいです。追加の公理をつかった方法――例えばJMeqを使うdependent destruction――を使うのもよいですが、今回は追加の公理なしでやってみます。
1. ３つの型
前述のとおり Fin.t が標準ライブラリにありますが、これに fin という別名をつけましょう。Recursiveに定義する ffin, subset type で定義する iset もまたサクッと定義してみます:
Require Fin.
(** fin は既存のを利用 *)
Notation fin := Fin.t.
Notation F1 := Fin.F1.
Notation FS := Fin.FS.
(** ffin は Recursive に定義 *)
Fixpoint ffin (n:nat) : Set := match n with
| O => Empty_set
| S n' => option(ffin n')
end.
(** iset は subset type *)
Definition iset (n:nat): Set := {k | k < n}.
ffin に関しては少し補足が必要かもしれません。ffin 3 の要素は None, Some None, Some (Some None) の３つしかないというわけです。ffin 0 は Empty_set なので要素を持ちません。
2. 集合としての同型性
fin, ffin, iset どれも全順序がありますが細かいことを忘れて、集合としての同型性をしめします。つまり f:fin n -> ffin n と g: ffin n -> fin n で fg, gf がともに恒等関数であるようなものを構成すればよいです。
標準ライブラリの Fin には fin と iset の同型性を証明するための道具立てがほとんどそろっているのでさくっと証明できます。
(** 標準ライブラリを使えば fin が iset と同型だという証明は簡単 *)
Definition fin2iset n: fin n -> iset n := Fin.to_nat.
Definition iset2fin n: iset n -> fin n := fun p =>
match p with exist _ k pk => Fin.of_nat_lt pk end.
Lemma rid_fi: forall n (x:iset n), fin2iset (iset2fin x) = x.
Proof. unfold fin2iset, iset2fin. intros n [k pk].
rewrite Fin.to_nat_of_nat. reflexivity. Qed.
Lemma lid_fi: forall n (x:fin n), iset2fin (fin2iset x) = x.
Proof. unfold fin2iset, iset2fin. intros. rewrite <-Fin.of_nat_to_nat_inv.
now destruct (Fin.to_nat x). Qed.
fin と ffin の同型性を示します:
Fixpoint f2ff {n} (c: fin n): ffin n := match c with
| F1 => None
| FS c' => Some (f2ff c')
end.
Fixpoint ff2f {n}: ffin n -> fin n := match n with
| O => fun e => match e with end
| S n' => fun fc => match fc with
| None => F1
| Some fc' => FS (ff2f fc')
end
end.
Lemma rid_fff: forall n (x:ffin n) , f2ff (ff2f x) = x.
Proof. induction n. intros []. intros []. simpl. now rewrite IHn. reflexivity. Qed.
Lemma lid_fff: forall n (x:fin n) , ff2f (f2ff x) = x.
Proof. induction n as [|n'].
intros X; inversion X.
intros. pattern x. apply Fin.caseS'. reflexivity.
intros y. simpl. now rewrite IHn'.
Qed.
3. 要素の列挙
定義から要素は慣れれば自明ですが、明示的に表してみるのもよいでしょう。例えば fin 2 の要素は F1, FS F1 のただ２つですが、これをPropの形で表現すると:
Goal. forall (x:fin 2), x = F1 \/ x = FS F1.
となります。それ以外の要素はあり得ないことはCoqが構成的道具立てで選言特性が成立する（A\/Bが成立するならAかBかのどちらかは成立する）ことからわかります。
(** fin 1 / ffin 1/ iset 1 は要素が１つ*)
Lemma fin1_elem: forall x: fin 1, x = F1.
Proof. intros. pattern x. apply Fin.caseS'. reflexivity. intros C. inversion C. Qed.
Lemma ffin1_elem: forall x: ffin 1, x = None.
Proof. intros []. inversion f. reflexivity. Qed.
Lemma iset1_elem: forall x: iset 1, proj1_sig x = 0.
Proof. intros []. simpl. lia. Qed.
(** fin 2 / ffin 2/ iset 2 は要素が2つ *)
Lemma fin2_elem: forall x:fin 2, x = F1 \/ x = FS F1.
Proof. intros. pattern x; apply Fin.caseS'. now left. intros y.
right. now rewrite (fin1_elem y). Qed.
Lemma ffin2_elem: forall x:ffin 2, x = None \/ x = Some None.
Proof. intros []. right. now rewrite (ffin1_elem f). now left. Qed.
Lemma iset2_elem: forall x: iset 2, proj1_sig x = 0 \/ proj1_sig x = 1.
Proof. intros []. simpl. lia. Qed.
4. 要素の列挙（応用）
前章の結果をもう少し一般化してみます。任意のnを与えたとき、fin n, ffin n の要素を全て含むリストを返す関数 elem_f, elem_ff を実装し、その正しさを証明してみます。正しいとは、すべての要素が含まれていること (elem_f_correct1)、要素数が n であること(elem_f_correct2）、要素に重複がないこと （elem_f_correct3）としてみます（なんとなく1と2から3は導けそうな気がしますがここではこれ以上深堀りしません）。
Fixpoint elem_f n: list (fin n) := match n with
| O => []
| S n' => F1:: (map FS (elem_f n'))
end.
Fixpoint elem_ff n: list (ffin n) := match n with
| O => []
| S n' => None:: (map Some (elem_ff n'))
end.
Lemma elemf_correct1: forall n (a:fin n), In a (elem_f n).
Proof. induction n. intros. inversion a.
simpl. intros. pattern a. apply Fin.caseS'. now left.
intros b. right. apply in_map. apply IHn. Qed.
Lemma elemff_correct1: forall n (a:ffin n), In a (elem_ff n).
Proof. induction n. intros. inversion a.
simpl. intros []. right. now apply in_map. now left. Qed.
Lemma elemf_correct2: forall n, n = length (elem_f n).
Proof. induction n; auto.
simpl. rewrite map_length. now rewrite <- IHn. Qed.
Lemma in_map_FS: forall n (l:list (fin n)) a, In (FS a) (map FS l) -> In a l.
Proof. induction l; [auto|]. simpl; intros. destruct H. left. now apply Fin.FS_inj.
right. now apply IHl. Qed.
Lemma elemf_correct3: forall n, NoDup (elem_f n).
Proof. intros. induction n. constructor.
simpl. remember (elem_f n) as l. clear Heql. induction IHn.
- constructor; [auto|constructor].
- simpl. inversion IHIHn. subst. constructor.
+ apply not_in_cons. split; [discriminate|assumption].
+ constructor;auto. intro. destruct H. now apply in_map_FS.
Qed.
Lemma in_map_some: forall (A:Type) (l:list A) a, In (Some a) (map Some l) -> In a l.
Proof. induction l. intros _ [].
simpl; intros ? []. left;inversion H;auto. right. now apply IHl. Qed.
Lemma elemff_correct3: forall n, NoDup (elem_ff n).
Proof. intros. induction n. constructor.
simpl. remember (elem_ff n) as l. clear Heql. induction IHn.
- constructor; [auto|constructor].
- simpl. inversion IHIHn. subst. constructor.
+ apply not_in_cons. split; [discriminate|assumption].
+ constructor;auto. intro. destruct H. now apply in_map_some.
Qed.
まとめ
有限個の集合を表す型３つを定義し、それらの間の同型性を示しました。またそれらの型が有限であることを要素を明示的に書き下すことにより確かめました。依存型の場合分けに追加の公理を使用しませんでした。