はじめに
本記事は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においては直接定義できないこと、しかしながら同値な定義ならできそうなことがわかりました。