有限個の要素を持つSetについて

# 概要

`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` もまたサクッと定義してみます:

```coq
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` の同型性を証明するための道具立てがほとんどそろっているのでさくっと証明できます。

```coq
(** 標準ライブラリを使えば 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` の同型性を示します:

```coq
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の形で表現すると:

```coq
Goal. forall (x:fin 2), x = F1 \/ x = FS F1.
```

となります。それ以外の要素はあり得ないことはCoqが構成的道具立てで選言特性が成立する（`A\/B`が成立するならAかBかのどちらかは成立する）ことからわかります。


```coq
(** 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は導けそうな気がしますがここではこれ以上深堀りしません）。


```coq
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.
```


# まとめ
有限個の集合を表す型３つを定義し、それらの間の同型性を示しました。またそれらの型が有限であることを要素を明示的に書き下すことにより確かめました。依存型の場合分けに追加の公理を使用しませんでした。