はじめに
本記事はTPP2024で発表した内容になります。
リストlistの型は通常nilとconsの2つのコンストラクタから定義されますが、
型変数Aに対し、cons A型をA -> list A -> list AではなくA -> list (list A) -> list Aに変更した型をHaskellやCoq/SSreflectで定義する方法について記述します。
ソースはこちら
Haskellで定義する
まず、この型の名前をSSeqとしてHaskellで実装したものは以下のようになります。
data SSeq a = SNil | SCons a (SSeq (SSeq a))
まずはHaskellでこの型について見てみます。
SSeqはどんな型？(Haskell編)
まず、任意のa型に対し、の値SNilはSSeq a型の値になります。
snil :: SSeq a
snil = SNil
特にSNil :: SSeq (SSeq a)であるので、以下の例のように、任意のx :: aに対し、SCons x snilもSSeq a型になります。
s0 :: SSeq Int
s0 = SCons 0 SNil
さらにSNil :: SSeq (SSeq (SSeq a))でもあることからsnil :: SSeq aを含む任意のs0 :: SSeq aと組み合わせてSCons s0 SNil :: SSeq (SSeq a)を作ることができます。
snil' :: SSeq (SSeq a)
snil' = SCons SNil SNil
s0' :: SSeq (SSeq Int)
s0' = SCons s0 SNil
{- = SCons (SCons 0 SNil) SNil -}
つまり以下のような値も作ることができます。
s1' :: SSeq Int
s1' = SCons 1 snil'
{- = SCons 1 (SCons SNil SNil) -}
s10 :: SSeq Int
s10 = SCons 1 s0'
{- = SCons 1 (SCons (SCons 0 SNil) SNil) -}
このように非自明な値が無限に存在するのがSSeqという型になります。
Functor則等は満たす？
このSSeqがFunctorやApplicative、Monadになるかどうか調べるために、とりあえずFunctorを定義してみます。
instance Functor SSeq where
fmap _ SNil = SNil
fmap f (SCons x s) = SCons (f x) $ fmap (fmap f) s
しかしながら、これは本当にFunctor則を満たすのでしょうか？
そこで形式検証するためにCoqを用いてSSeqを再定義するのが本記事の目的です。
Coqではそのまま定義できない
上記のようにHaskellではコンパイルが通るのですが、Coqではそのまま定義できません。
Inductive sseq : Type -> Type :=
| snil T: sseq T
| scons T: T -> sseq (sseq T) -> sseq T.
(* Error: Universe inconsistency *)
そこで、これと同型の型を定義して、その同値性を示していきます。
代わりにsseqnを定義する
アイデアとしてはsseqの代わりに以下の条件を満たすsseqn : Type -> nat -> Typeを定義することを考えます。
sseqn T 0 = T
sseqn T n.+1 = sseq (sseqn T n)
つまり、任意の自然数nに対し、sseqn T n = iter n sseq Tを満たすような型という意味です。
このときsseq T 1 = sseq Tを満たすので、これを用いてsseq Tを定義するというのが本方針です。
sseqnの2通りの定義
私はsseqnを2通りで定義してみました。
sseqの定義をそのまま書き換える方法
1つ目はsseqの定義をそのままsseqnで書き換える方法です。
sseqの元の定義
Inductive sseq : Type -> Type :=
| snil T: sseq T
| scons T: T -> sseq (sseq T) -> sseq T.
(* Error: Universe inconsistency *)
に対して、sseqn' T n = iter n sseq Tとなるように書き換えると以下のようになります。
Inductive sseqn' (T:Type) : nat -> Type :=
| sseqn'0 : T -> sseqn' T 0
| sseqn'Nil d: sseqn' T d.+1
| sseqn'Cons d: sseqn' T d -> sseqn' T d.+2 -> sseqn' T d.+1.
ここでコンストラクタが3つに増えているのは、元の型引数Tの値がsseq (...(sseq T)...)になる場合があり、0次元のTの場合と区別する必要があるからです。
3つ目のsconsに対応するコンストラクタはd次元とd.+2次元の引数からd次元の引数が作れることを表しています。
ただしnatの依存型になるので、この定義だと場合分け等の証明が多少ややこしくなるのがネックです。
二分木を使う方法
もう1つは二分木を使う方法です。
どういうことかというと、sseqの2つコンストラクタのうち、snilは二分木の葉、sconsはT型とsseq (sseq T)型の2つの木から新たな木を作っているように見え、全体としての構造は二分木に似ています。
そこで、sseqを二分木に対して帰納的に定義するという方針です。
まずは二分木を定義しておきます。
Inductive bitree (T:Type) : Type :=
| BiLeaf : bitree T
| BiNode of T & bitree T & bitree T.
この二分木に対し、sseq_rec : Type -> nat -> bitree unit -> Typeを以下のように定義します。
Fixpoint sseq_rec (A:Type) (d:nat) (t:bitree unit) : Type :=
if d is d'.+1
then if t is BiNode _ tl tr
then sseq_rec A d' tl * sseq_rec A d'.+2 tr else unit
else if t is BiNode _ _ _ then empty else A.
これはt:bitree unitに対して帰納的な定義になっています。
注意が必要なのはd = 0の時ですが、これはsseqの定義からコンストラクタはsconsにはなり得ないので、二分木tがBiLeafでないときは空集合empty := Empty_setを返しています。
またsnilに対応するのがt > 0, b = BiLeafのときで、1点集合unitを返します。
このとき、sseqnは以下のように、これを満たす二分木tが存在することで定義できます。
Definition sseqn (A:Type) (d:nat) := sigT (sseq_rec A d).
(*
Inductive sigT (A:Type) (P:A -> Type) : Type :=
existT : forall x : T, P x -> {x : A & P x}.
*)
sseqn'とsseqnの同値性
上記2つの方法で定義したsseqn'とsseqnは同値になります。
まず、sseqn' A d -> sseqn A d型とsseqn A d -> sseqn' A d型の2つの変換関数を定義します。(内部に登場する関数の詳細はソースにて)
Fixpoint sseqn'_sseqn (A:Type) (d:nat) (x:sseqn' A d) : sseqn A d :=
match x with
| sseqn'0 a => to_sseq0 a
| sseqn'Nil d => sseqnNil _ _
| sseqn'Cons d a s => sseqnCons (sseqn'_sseqn a) (sseqn'_sseqn s)
end.
Definition sseqn_sseqn' (A:Type) (d:nat) (x:sseqn A d) : sseqn' A d :=
match x with
| existT _ t => sseq_rec_sseqn' t
end.
これらがそれぞれcancelできることを示します。
Lemma sseqn_sseqn'_sseqn (A:Type) (d:nat):
cancel (@sseqn_sseqn' A d) (@sseqn'_sseqn _ _).
Lemma sseqn'_sseqn_sseqn' (A:Type) (d:nat):
cancel (@sseqn'_sseqn A d) (@sseqn_sseqn' _ _).
これで同値性が示せたので、以降はsseqnのみを用いて議論していきます。
まず、sseqnの重要な性質を見ていきます。
sseqnの性質
sseqnのいくつかの性質を見ていきます。
sseqnのFunctor性
sseqnが関手になることを示します。
細かい定義は省略しますが、map関数とこれが満たすべき性質を示します。
Definition sseqn_map (A B:Type) (d:nat) (f:A -> B) (x:sseqn A d) :
sseqn B d :=
match x with
| existT t p => existT _ t (sseq_rec_map f p)
end.
Lemma sseqn_map_id (A:Type) (d:nat) (x:sseqn A d): sseqn_map id x = x.
Lemma sseqn_map_comp (A B C:Type) (d:nat) (f:A -> B) (g:B -> C) (x:sseqn A d):
sseqn_map (g \o f) x = sseqn_map g (sseqn_map f x).
Lemma eq_sseqn_map (A B:Type) (d:nat) (f g:A -> B) :
f =1 g -> @sseqn_map _ _ d f =1 sseqn_map g.
sseqn (sseqn T d) kとsseqn T (k + d)の同値性
後にsseqを定義し、任意の自然数nに対し、sseqn T nとiter n sseq Tの同値性を示すのですが、
特にiter (k + d) sseq T = iter k sseq (iter d sseq T)が成り立つことからsseqn (sseqn T d) kとsseqn T (k + d)が同値でなければいけません。
これを先に示しておきます。
まずはこれらの間の変換関数を定義します。
まずはsseqn (sseqn A d) k -> sseqn A (k + d)の変換関数sseqn_liftを定義します。(詳細は省略します)
Definition sseqn_lift (A:Type) (k d:nat) :
sseqn (sseqn A d) k -> sseqn A (k + d) :=
fun x => match x with
| existT _ x => sseqn_lift_rec x
end.
次のその逆関数sseqn_unlift : sseqn A (k + d) -> sseqn (sseqn A d) kも定義します。
Definition sseqn_unlift (A:Type) (k d:nat):
sseqn A (k + d) -> sseqn (sseqn A d) k :=
fun x => match x with
| existT _ x => sseqn_unlift_rec x
end.
これらが互いに逆関数になっていることは以下からわかります。
Lemma sseqn_lift_unlift (A:Type) (k d:nat):
cancel (@sseqn_unlift A k d) (@sseqn_lift _ _ _).
Lemma sseqn_unlift_lift (A:Type) (k d:nat):
cancel (@sseqn_lift A k d) (@sseqn_unlift _ _ _).
sseqn T 0とTの同値性
sseqnを定義しましたが、欲しい性質を再掲すると以下の通りです。
sseqn T 0 = T
sseqn T n.+1 = sseq (sseqn T n)
まずは1つ目のsseqn T 0とTの同値性を示します。
まずfrom_sseq0 : sseqn T 0 -> Tとto_sseq0 : T -> sseqn T 0を定義します。
Definition from_sseq0 (A:Type) (x:sseqn A 0) : A :=
match x with
| existT t s => let f : sseq_rec A 0 t -> A :=
match t return sseq_rec A 0 t -> A with
| BiLeaf => id
| BiNode _ _ _ => fun x => match x with end
end
in f s
end.
Definition to_sseq0 (A:Type) : A -> sseqn A 0 := existT _ (BiLeaf _).
これらがcancelできることを示します。
Lemma to_from_sseq0 (A:Type) : cancel (@from_sseq0 A) (@to_sseq0 _).
Proof. by case =>[[|? ? ? []]]. Qed.
Lemma from_to_sseq0 (A:Type) : cancel (@to_sseq0 A) (@from_sseq0 _).
Proof. done. Qed.
sseqを定義する
sseqnが定義できたので本題であるsseqを定義していきます。
Definition sseq (A:Type) : Type := sseqn A 1.
もちろん、そのコンストラクタに対応するsseqNilとsseqConsも定義します。
まずはsseqnの世界でnilとconsを定義します。
Definition sseqnNil (A:Type) (d:nat) : sseqn A d.+1 := existT _ (BiLeaf _) tt.
Definition sseqnCons (A:Type) (d:nat) :
sseqn A d -> sseqn A d.+2 -> sseqn A d.+1 :=
fun a s =>
match a, s with
| existT tl xl, existT tr xr => existT _ (BiNode tt tl tr) (pair xl xr)
end.
これをsseqで書き直します。
Definition sseqNil (A:Type) : sseq A := sseqnNil _ 0.
Definition sseqCons (A:Type) : A -> sseq (sseq A) -> sseq A :=
fun a s => sseqnCons (to_sseq0 a) (sseqn_lift s).
これらがhaskellのSSeqと同値になることを示していきます。
HaskellのSSeqとCoqのsseqの同値性
この2つの同値性ですが、CoqではHaskellと同じ方法でSSeqを定義することができず、単純に同値性を記述することができません。
そこで、代わりにsseqがInductiveに定義された型の公理を満たすことを示します。
Inductiveで定義される型の公理
自然数におけるペアノの公理を見て分かる通り、Inductiveに定義される型が満たすべき公理は以下の通りです。
- コンストラクタの存在
- 各コンストラクタの単射性
- コンストラクタの一位性
- 帰納原理
この4つうち、sseqのコンストラクタの存在性はすでにsseqNilとsseqConsを定義したことから示していますので、残りの3つを示していきます。
各コンストラクタの単射性
sseqの2つのコンストラクタsseqNilとsseqConsのうち、sseqNilは引数を取らないのではsseqConsの単射性の証明は以下の通りです。
Lemma sseqCons_inj (A:Type) (x x':A) (s s':sseq (sseq A)):
sseqCons x s = sseqCons x' s' -> x = x' /\ s = s'.
Proof.
rewrite -(from_to_sseq0 x) -(from_to_sseq0 x') /sseqCons !to_from_sseq0.
rewrite -(sseqn_unlift_lift s) -(sseqn_unlift_lift s') !sseqn_lift_unlift.
case : (to_sseq0 x) (to_sseq0 x') =>[t p][t' p'].
case : (sseqn_lift s) (sseqn_lift s') =>[tr xr][tr' xr'] H.
case : H (H) => Ht Htr. move : Ht Htr p' xr' =><-<- p' xr' H.
suff : (p, xr) = (p', xr') by case =>->->.
apply /Eqdep_dec.inj_pair2_eq_dec : H => y y'.
by case : (@bitree_eqP _ y y'); [left|right].
Qed.
ここでEqdep_dec.inj_pair2_eq_decが出てきますが、これは依存型に対してcaseするときに出てきます。実際にsseqnは二分木bitree型に依存する型になります。
ちなみに
Eqdep_dec.inj_pair2_eq_dec
: forall A:Type,
(forall x y:A, {x = y} + {x <> y}) ->
forall (P:A -> Type) (p:A) (x y:P p),
existT P p x = existT P p y -> x = y
なので、これがAが決定可能な型、特にeqtypeならば問題なく場合分けができます。
今回はAがbitreeだったので問題なく証明できます。
コンストラクタの一位性
ここでいう一位性とはsseqの各要素は高々1つのコンストラクタでしか表現できないという性質です。
今回のケースでは以下のように任意のa, xに対してsseqCons a x <> sseqNilを示せばいいです。
Lemma sseq_neqcons (A:Type) (a:A) x: sseqCons a x <> sseqNil _.
Proof.
rewrite /sseqCons/sseqNil. case : (to_sseq0 a) (sseqn_lift x) =>[t0 p0].
case =>[t p]. by case.
Qed.
ここでは高々1つと言いましたが、その存在性、つまりsseqの各要素はあるコンストラクタで表現できるという性質は以下の定理から示せます。
Lemma sseq_case (A:Type) (s:sseq A) :
s = sseqNil _ \/ exists a s', s = sseqCons a s'.
Proof.
case : s =>[[[]|[] tl tr /=[xl xr]]]; [by left|right].
exists (from_sseq0 (existT _ tl xl)),
(@sseqn_unlift _ 1 _ (existT _ tr xr)). rewrite /sseqCons to_from_sseq0.
by rewrite sseqn_lift_unlift.
Qed.
しかしながらこの性質は基本的には以下の公理である次の帰納原理から示せます。
帰納原理
示したい帰納原理は以下の通りです。
Proposition sseq_ind (A:Type) (P:forall d, sseq (iter _ d sseq A) -> Prop) :
(forall d, P _ (sseqNil (iter _ d sseq A))) ->
(forall (a:A) (s:sseq (sseq A)), P 1 s -> P 0 (sseqCons a s)) ->
(forall d (a:sseq (iter _ d sseq A))
(s:sseq (sseq (sseq (iter _ d sseq A)))),
P d a -> P d.+2 s -> P d.+1 (sseqCons a s)) ->
forall d (s:sseq (iter _ d sseq A)), P _ s.
ここでポイントなのは、述語Pの型がsseq A -> Propではなくforall d, sseq (iter _ d sseq A) -> Propつまりforall d, iter _ d.+1 sseq A -> Propであるということと
sseqConsに対応する帰納法の仮定がd = 0の時とd > 0の時の2つ必要だということです。
これはsseqCons : A -> sseq (sseq A) -> sseq Aと次元の高い引数が必要になるため、高次元のiter _ d sseq Aにおける帰納法の仮定が必要になるためです。
またd = 0のとき, iter _ d sseq A = Aであり帰納法の仮定が使えなくなるため、d > 0の場合と区別する必要が出てきます。
sseqn上で帰納原理を示す
さてこの命題を示すためにまずはsseqnの世界のこの帰納原理を示します。
Lemma sseq_ind' (A:Type) (P:forall d, sseqn A d.+1 -> Prop) :
(forall d, P _ (sseqnNil A d)) ->
(forall (a:sseqn A 0) (s:sseqn A 2),
P _ s -> P _ (sseqnCons a s)) ->
(forall d (a:sseqn A d.+1) (s:sseqn A d.+3),
P _ a -> P _ s -> P _ (sseqnCons a s)) ->
forall d (s:sseqn A d.+1), P _ s.
Proof.
move => Hnil Hcons0 Hcons d [t].
elim : t d =>[|[] tl IHl tr IHr][|d]/=[]; try exact /Hnil.
- move => a b. exact /(Hcons0 (existT _ _ a) (existT _ _ b))/IHr.
- move => a b. exact : Hcons (IHl _ a) (IHr _ b).
Qed.
しかしながら、ここからsseqの世界への変換がまだうまくいってません。
理由としては証明に以下のような可換図式が必要になるのですが、
sseqn A (1 + n + m) -> sseqn (sseqn A m) (1 + n)
↓ ↓
sseqn (sseqn A (n + m)) 1 -> sseqn (sseqn (sseqn A m) n) 1
ここでsseqnのnat型の第二引数は単調減少するわけではなく増加することもあるので、これを示すために結果的に1をlに一般化して
sseqn A (l + n + m) -> sseqn (sseqn A m) (l + n)
↓ ↓
sseqn (sseqn A (n + m)) l -> sseqn (sseqn (sseqn A m) n) l
を示す必要があります。しかしながらl + n + m = l + (n + m)は自明な命題ではないので、この可換図式はそのままではCoqにおいて型エラーで通らないです。
ですので、本当に示すべき可換図式は以下の通りになります。
sseqn A (l + n + m) -> sseqn (sseqn A m) (l + n)
↓ ↓
sseqn A (l + (n + m)) ↓
↓ ↓
sseqn (sseqn A (n + m)) l -> sseqn (sseqn (sseqn A m) n) l
sseqn A (l + n + m) -> sseqn A (l + (n + m))の型変換にはcast関数を作る必要があるのですが、これにはl + n + m = l + (n + m)の証明を引数として渡さないといけなくなります。
この証明を渡すという扱いが非常に大変なので、まだ私は証明できていないです。
Definition cast_sseqn (A:Type) (d e:nat) (H:d = e) (x:sseqn A d) :
sseqn A e := match x with
| existT _ y => existT _ _ (cast_sseq_rec H y)
end.
まとめ
list型のconsをA -> list (list A) -> list Aに変更した型をHaskellとCoqで(ほとんど)定義しました。
Haskellにおいてはそのまま定義できますが、Coqにおいては直接定義できないこと、しかしながら同値な定義ならできそうなことがわかりました。