ふと、3つのコンストラクタをもつ帰納型を有限型 (finType) として扱いたくなったのだが、どうやればいいのか調べるのにけっこう苦労した。
結局、以下のようにすれば可能なようだ。
From mathcomp Require Import all_ssreflect.
From HB Require Import structures.
Inductive mytype :=
| C1 : bool -> mytype
| C2 : bool -> mytype
| C3 : bool -> mytype.
Lemma sum_of_mytypeK : cancel
(fun (v : mytype) =>
match v with
| C1 b => inl (inl b)
| C2 b => inl (inr b)
| C3 b => inr b
end)
(fun (v : bool + bool + bool) =>
match v with
| inl (inl b) => C1 b
| inl (inr b) => C2 b
| inr b => C3 b
end).
Proof. by case; case. Qed.
HB.instance Definition _ := Finite.copy mytype (can_type sum_of_mytypeK).
Check mytype : choiceType.
Check mytype : countType.
Check mytype : eqType.
Check mytype : finType.
ここでは、bool + bool + bool 型 (つまり sum (sum bool bool) bool 型) と mytype が同型であることを証明して、それにより mytype が有限型であることを登録している。
これをやると、finType の継承元 (choiceType, countType, eqType) としても mytype が自動的に登録されるようだ。 (登録されるので、mytype : choiceType のようなキャストが通る。このキャストは型を、登録された choiceType の値からその型を取り出す式に変換している。)
もちろん、mytype などというものは定義せずに、bool + bool + bool 型を使うという方法もあるが、 そうすると inl (inr b) みたいなわかりにくい表現を使わないといけない。 (inl (inr b) を呼び出す関数として C1 を定義して、Arguments C1 : simpl never. とすればかなり inl (inr b) という内部表現を隠せるが、それでも出てきてしまうことはあって、change で修正しなければいけないので面倒くさい )
まぁ、Notation で inl (inr b) を C1 b にみせかければよかったのかもしれない。 でも、sum 型を他の用途でも使っているとそっちにも影響するし、分解を [a|b|c] と書きたいところを [[a|b]|c] と書かなければならない問題は残る。
なお、環境は Rocq 9.0.0 と rocq-mathcomp-ssreflect 2.4.0 である。
[latest]