リストのconsの型をA -> list A -> list AではなくA -> list (list A) -> list Aにした型をHaskellとCoq/SSReflectで定義したい

# はじめに

本記事は[TPP2024](https://www.math.nagoya-u.ac.jp/~garrigue/tpp2024/)で発表した内容になります。

リスト`list`の型は通常`nil`と`cons`の2つのコンストラクタから定義されますが、
型変数`A`に対し、`cons A`型を`A -> list A -> list A`ではなく`A -> list (list A) -> list A`に変更した型をHaskellやCoq/SSreflectで定義する方法について記述します。

ソースは[こちら](https://github.com/nekonistyle/Qiita_example/blob/main/sseq/sseq.v)


# Haskellで定義する

まず、この型の名前を`SSeq`としてHaskellで実装したものは以下のようになります。

```haskell
data SSeq a = SNil | SCons a (SSeq (SSeq a))
```

まずはHaskellでこの型について見てみます。

## `SSeq`はどんな型？(Haskell編)

まず、任意の`a`型に対し、の値`SNil`は`SSeq a`型の値になります。

```haskell
snil :: SSeq a
snil = SNil
```

特に`SNil :: SSeq (SSeq a)`であるので、以下の例のように、任意の`x :: a`に対し、`SCons x snil`も`SSeq a`型になります。

```haskell
s0 :: SSeq Int
s0 = SCons 0 SNil
```

さらに`SNil :: SSeq (SSeq (SSeq a))`でもあることから`snil :: SSeq a`を含む任意の`s0 :: SSeq a`と組み合わせて`SCons s0 SNil :: SSeq (SSeq a)`を作ることができます。

```haskell
snil' :: SSeq (SSeq a)
snil' = SCons SNil SNil

s0' :: SSeq (SSeq Int)
s0' = SCons s0 SNil
{-  = SCons (SCons 0 SNil) SNil -}
```

つまり以下のような値も作ることができます。

```haskell
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`を定義してみます。

```haskell
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ではそのまま定義できません。

```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`を定義することを考えます。

```coq
sseqn T 0 = T
```

```coq
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`の元の定義

```coq
  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`となるように書き換えると以下のようになります。

```coq
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`を二分木に対して帰納的に定義するという方針です。

まずは二分木を定義しておきます。

```coq
  Inductive bitree (T:Type) : Type :=
  | BiLeaf : bitree T
  | BiNode of T & bitree T & bitree T.
```

この二分木に対し、`sseq_rec : Type -> nat -> bitree unit -> Type`を以下のように定義します。

```coq
  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`が存在することで定義できます。

```coq
  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つの変換関数を定義します。(内部に登場する関数の詳細はソースにて)

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

```coq
  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`できることを示します。

```coq
  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`関数とこれが満たすべき性質を示します。

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

```coq
  Lemma sseqn_map_id (A:Type) (d:nat) (x:sseqn A d): sseqn_map id x = x.
```

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

```coq
  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`を定義します。(詳細は省略します)

```coq
  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`も定義します。

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

これらが互いに逆関数になっていることは以下からわかります。

```coq
  Lemma sseqn_lift_unlift (A:Type) (k d:nat):
    cancel (@sseqn_unlift A k d) (@sseqn_lift _ _ _).
```

```coq
  Lemma sseqn_unlift_lift (A:Type) (k d:nat):
    cancel (@sseqn_lift A k d) (@sseqn_unlift _ _ _).
```


## `sseqn T 0`と`T`の同値性

`sseqn`を定義しましたが、欲しい性質を再掲すると以下の通りです。

```coq
sseqn T 0 = T
```

```coq
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`を定義します。

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

```coq
  Definition to_sseq0 (A:Type) : A -> sseqn A 0 := existT _ (BiLeaf _).
```

これらが`cancel`できることを示します。

```coq
  Lemma to_from_sseq0 (A:Type) : cancel (@from_sseq0 A) (@to_sseq0 _).
  Proof. by case =>[[|? ? ? []]]. Qed.
```

```coq
  Lemma from_to_sseq0 (A:Type) : cancel (@to_sseq0 A) (@from_sseq0 _).
  Proof. done. Qed.
```


# `sseq`を定義する

`sseqn`が定義できたので本題である`sseq`を定義していきます。

```coq
  Definition sseq (A:Type) : Type := sseqn A 1.
```

もちろん、そのコンストラクタに対応する`sseqNil`と`sseqCons`も定義します。

まずは`sseqn`の世界で`nil`と`cons`を定義します。

```coq
  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`で書き直します。

```coq
  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`の単射性の証明は以下の通りです。

```coq
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`型に依存する型になります。

ちなみに
```coq
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`を示せばいいです。

```coq
  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`の各要素はあるコンストラクタで表現できるという性質は以下の定理から示せます。

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


しかしながらこの性質は基本的には以下の公理である次の帰納原理から示せます。


## 帰納原理

示したい帰納原理は以下の通りです。

```coq
  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`の世界のこの帰納原理を示します。

```coq
  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)`の証明を引数として渡さないといけなくなります。
この証明を渡すという扱いが非常に大変なので、まだ私は証明できていないです。

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