Coq/SSReflectでコンストラクタ数や構造が引数に依存して変化するInductive型を定義する

# はじめに

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

Coq/SSReflectでコンストラクタ数や構成が引数に依存して変化するようなInductiveな型を定義します。
動機としては「Inductiveで定義される型」を一般化したいというものです。

最初は最も簡単な例から始めて、最終的に「任意のある種の再帰するInductive型」が記述できるような定義をして行きます。

ソースコードは[こちら](https://github.com/nekonistyle/SSReflect/blob/master/genind.v)


# コンストラクタ数が引数に依存する型

Coqでは`Inductive`は`Fixpoint`で定義できず、実際にコンストラクタは固定数のものしか定義できません。しかしながら、事実上、引数に依存するようなコンストラクタを持つ型を定義することができます。

具体的にいくつか例を見ていきます。


# 自然数`n`を引数にとり、`n`個の無引数コンストラクタを持つ型

まずは最も簡単な例である、自然数`n`を引数にとり, 実質`n`個の無引数のコンストラクタを持つ型`nconstructor`を考えます。
これは以下のように定義します。

```coq
  Notation empty := Empty_set.

  Inductive nconstructor (n:nat) : Type :=
  | NConstructor of iter n (sum unit) empty.
```

実際の定義はコンストラクタは1つで、`unit`型の`n`個の直和を引数にとっています。

## `m`番目のコンストラクタを返す関数

この`nconstructor n.+1`型の上に、コンストラクタとして動く関数を定義していきます。(`n = 0`の時はコンストラクタが存在しない)
この型の`m`番目の事実上のコンストラクタ`nthcon n m`は以下の関数で表せます。

```coq
  Fixpoint nthcon_rec (n m:nat) : iter n.+1 (sum unit) empty :=
    match n return iter n.+1 (sum unit) empty with
    | 0 => inl tt
    | n'.+1 => match m with
               | 0 => inl tt
               | m'.+1 => inr (nthcon_rec n' m')
               end
    end.
```

```coq
  Definition nthcon (n m:nat) : nconstructor n.+1 :=
    NConstructor (nthcon_rec n m).
```


### コンストラクタの一意性

```coq
  Lemma nthcon_rec_uniq (n m m':nat) :
    m <= n -> m' <= n -> nthcon_rec n m = nthcon_rec n m' -> m = m'.
```

```coq
  Lemma nthcon_uniq (n m m':nat) :
    m <= n -> m' <= n -> nthcon n m = nthcon n m' -> m = m'.
```

### コンストラクタによる場合分け

全ての`nconstructor n.+1`がいずれかのコンストラクタで表せることは以下の定理よりわかります。


```coq
  Lemma nthcon_case (n:nat) (x:nconstructor n.+1) :
    exists m, m <= n /\ x = nthcon n m.
```

ただし、実際に場合分けをするなら以下の定理`nthconP`を使います。
こちらの方が`exists`を`case`したり`rewrite`する必要がなく、単に`case : (nthconP x)`で`x`を`nthcon n m`に書き換えてくれるため、使い勝手がよくなります。

```coq
  Variant nthcon_or n : nconstructor n.+1 -> Set :=
  | NthconOr m of m <= n : nthcon_or (nthcon n m).
```

```coq
  Lemma nthconP (n:nat) (x:nconstructor n.+1) : nthcon_or x.
```

### 帰納原理

帰納原理は以下のように示せます。

```coq
  Lemma my_nconstructor_ind (n:nat) (P:nconstructor n.+1 -> Prop):
    (forall m, m <= n -> P (nthcon _ m)) -> forall x, P x.
```

## `day`型

これを使って、実際にSoftware Foundationの最初に学んだような、曜日を表す`day`型を作ってみます。

```coq
  Definition day := nconstructor 7.
```

```coq
  Definition monday : day := nthcon _ 0.
  Definition tuesday : day := nthcon _ 1.
  Definition wednesday : day := nthcon _ 2.
  Definition thursday : day := nthcon _ 3.
  Definition friday : day := nthcon _ 4.
  Definition saturday : day := nthcon _ 5.
  Definition sunday : day := nthcon _ 6.
```

## 補足

`n`個の無引数コンストラクタを持つ型を定義しましたが、実際に`n`個からなる有限型を表すなら単にmathcompのfinType.vにある順序数型`'I_n`を使う方がいいと思います。


# 引数を取るInductiveな型

上では自然数を引数にとり、それに依存する個数の無引数コンストラクタを作りましたが、今回は引数を取るものを考えていきます。
具体的には適当な型`T`と`T`上のリスト`s:seq T`を引数にとり、`s`上の各要素`x:T`を`f:T -> Type`で型に変換した`f x`型の値を引数にとるコンストラクタを定義していきます。
つまり、コンストラクタ数はリスト`s`の長さに等しくなります。

例えば`T := Type`、`f x := x`、`s := [:: unit, nat]`ならば、`unit`型を引数に取るコンストラクタと`nat`型の引数を取るコンストラクタの2つからなる`Inductive`な型を表します。`unit`型は1点集合なので、これは`option nat`型と同型になります。

ちなみに引数は直接`seq Type`ではなく、`seq T`を`f`を変換するようにワンクッション置いて定義したのは、後述する再帰呼び出しを行う場合でも使えるようにするためです。


### 定義

具体的に作った型`mkInductive`は以下の通りです。

```coq
  Inductive mkInd (T:Type) (f:T -> Type) : seq T -> Type :=
  | MkIndNil : empty -> mkInd f [::]
  | MkIndCons x s : f x + mkInd f s -> mkInd f (x :: s).
```

```coq
  Inductive mkInductive (T:Type) (f:T -> Type) (s:seq T) : Type :=
  | MkInductive of mkInd f s.
```

`nconstructor`のときは自然数`n`をとり、`iter n (sum unit) empty`を引数にInductive型を定義していましたが、今回は`foldr (sum \o f) empty s`ではなく、わざわざ`mkInd`型を定義して、これを用いて定義してます。
これも後に定義する再帰する型のために必要な記述です。

まず, `mkInd`に関する性質を見ていきます。

### `mkInd`の帰納原理

`mkInd`の帰納原理がうまく自動生成されないので、自分で定義します。

```coq
Definition mymkInd_ind (T:Type) (f:T -> Type) (P:forall s,mkInd f s -> Prop)
    (IHf:forall x s (t:f x), P (x :: s) (MkIndCons (inl t)))
    (IHcons:forall x s (t:mkInd f s), P _ t -> P (x :: s) (MkIndCons (inr t))):
    forall s (x:mkInd f s), P _ x :=
    fix loop s x : P s x :=
      match x with
      | MkIndNil e => match e with end
      | MkIndCons x s' t => match t with
                            | inl fx => IHf _ _ fx
                            | inr t' => IHcons _ _ _ (loop s' t')
                            end
      end.
```

まず、`mkInd`はリスト`s`に依存して型が変化するので、命題`P`も任意のリスト`s`に対する形で定義します。

帰納法の仮定ですが、`mkIndNil`は空集合`empty`を引数にとっており、この値が仮定に現れることはないので`mkIndCons`の場合のみを考えます。
`f x`のときと再帰する場合の直和になっているのでこの2つを仮定に取ります。

証明は`fix`を使って証明項を直接書いて定義します。


## コンストラクタ

`mkInductive`のコンストラクタは引数`s:seq T`の各要素に対して1つ定義されます。
ここでは`n < size s`に対し、`n`番目のコンストラクタについて考えます。

### `n`番目のコンストラクタの型

まず、自然数`n`をとり、`n`番目のコンストラクタの型を返す関数`eachcon`を定義します。

```coq
  Fixpoint eachcon (T:Type) (f:T -> Type) (s:seq T) (n:nat) : Type :=
    match s with
    | [::] => empty
    | x :: s' => match n with
                  | 0 => f x
                  | n'.+1 => eachcon f s' n'
                  end
    end.
```

ちなみに`eachcon f s n = nth (empty:Type) (map f s) n`が成り立ちますが、記述が長いので関数として定義しました。

### `n`番目のコンストラクタ

次にこの値からコンストラクタ、すなわち自然数`n`に対し、`n`番目のコンストラクタの型`eachcon f s n`をもらって`mkInductive f s`型を返す関数を作ります。
まずは返り値を`mkInd f s`型にしたものを定義するのですが、ここで`s = [::]`のときはコンストラクタが存在しないので、`eachcon`の`s = [::]`のときは`empty`型を返す定義になっています。

```coq
  Fixpoint mkcon_rec (T:Type) (f:T -> Type) (s:seq T) (n:nat):
    eachcon f s n -> mkInd f s :=
    match s, n return eachcon f s n -> mkInd f s with
    | [::],_ => MkIndNil f
    | x :: s',0 => @MkIndCons _ f _ _ \o inl
    | x :: s',n'.+1 => @MkIndCons _ _ _ _ \o inr \o @mkcon_rec _ f s' n'
    end.
```

これを用いて`n`番目のコンストラクタが`mkcon f s n`が定義できます。

```coq
  Definition mkcon (T:Type) (f:T -> Type) (s:seq T) (n:nat):
    eachcon f s n -> mkInductive f s :=
    @MkInductive _ _ _ \o @mkcon_rec _ f s n.
```

### コンストラクタの一意性

`n`番目のコンストラクタの引数`eachcon f s n`に対するコンストラクタは`mkcon f s n`であり、引数の型が`n`に依存するので型レベルで一意性が言えます。

また、同じコンストラクタの異なる引数に対して異なる値を返すという意味での一意性は、coqでは`T`が決定可能な型、例えば`eqType`の場合は以下のように証明できます。

```coq
  Lemma mkcon_inj (T:eqType) (f:T -> Type) (s:seq T) (n:nat):
    injective (@mkcon _ f s n).
```

ここで、決定可能性が必要になる理由は、`mkInd`が依存型で書かれているため、そのコンストラクタで`case`したとき、例えば`mkIndCon (inl a) = mkIndCon (inl b)`で`case`すると、`a = b`ではなく`existT [eta f] x a = exists [eta f] x b`のような命題が出てくるためです。

ここから`existT`を取り除くにはcoqの標準ライブラリ[Eqdep_dec.v](https://coq.inria.fr/doc/V8.19.0/stdlib/Coq.Logic.Eqdep_dec.html)にある以下の定理が必要になります。

```coq:Eqdep_dec.v
Lemma 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`が決定可能な型でないといけないということです。


### コンストラクタによる場合分け

次の定理で場合分けできることがわかります。

```coq
  Lemma mkcon_case (T:Type) (f:T -> Type) (s:seq T) (x:mkInductive f s):
    exists n, n < size s /\ exists a:eachcon f s n, x = mkcon a.
```

ただし、これもこのままでは使いづらいので、以下の`mkconP`を証明します。`mkconP x`を`case`してやると`x`を各`mkcon a`に書き換えてくれます。

```coq
  Variant mkcon_or (T:Type) (f:T -> Type) (s:seq T) : mkInductive f s -> Prop :=
  | MkconOr n (a:eachcon f s n) of n < size s : mkcon_or (mkcon a).
```

```coq
  Lemma mkconP (T:Type) (f:T -> Type) (s:seq T) (x:mkInductive f s) :
    mkcon_or x.
```


## 帰納原理

これを用いて帰納原理が証明できます。

```coq
  Lemma my_mkInductive_ind (T:Type) (f:T -> Type) (s:seq T)
        (P:mkInductive f s -> Prop):
    (forall n, n < size s ->
               forall a:eachcon f s n, P (mkcon a)) ->
    forall x, P x.
```


# 再帰する「Inductiveに定義される型」

上で定義した`mkInductive`を使って、再帰するInductiveに定義される型を定義します。

本記事では特にリスト`seq (Type * nat)`を使い、リストの各要素`(T,n)`に対し、`T`型の引数と`n`個の再帰呼び出しを行うコンストラクタを持つ型を返す型を定義します。

例えば、`(unit,0) : Type * nat`に対するコンストラクタの引数は`unit`型で1つあり、型`T`に対して`(T,1) : Type * nat`に対するコンストラクタは`T`型と再帰する引数が1つあるコンストラクタになります。つまり、`unit`型が1点集合であることを考えると`[:: (unit:Type,0); (T,1)]`で実質的に型`T`上のリストを定義できるようになります。(実装は後述します)


## 定義

n個の引数の再帰呼び出しを行うInductiveな型を一般化するためには、再帰する型を[Coq/SSReflectで自然数nを引数に取ってn分木の型を返す型をInductiveに定義する](https://qiita.com/nekonibox/items/710eb444189417069d22)で`n`分木を定義したときのようにInductiveで定義された型の引数に渡す必要があります。

そこで長さの証明付きリストを定義します。


### 長さの証明付きリスト`vector`型

上の記事では自作の`sizseq`型を作っていますが、今回はCoqの標準ライブラリである[VectorDef.v](https://coq.inria.fr/doc/v8.9/stdlib/Coq.Vectors.VectorDef.html)の`t`型(Vector型)を使います。

akrさん、ご助言いただきありがとうございます。

```coq:VectorDef.v
  Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).
```

ここでは、名前を`vector`型に変更しておきます。

```coq
  Definition vector := Vector.t.
  Definition vnil (T:Type) : vector T 0 := Vector.nil _.
  Definition vcons (T:Type) (n:nat) (x:T) (s:vector T n) := Vector.cons _ x _ s.
```

`vector`上の`foldr`関数も`seq`の`foldr`と引数の順番が合うように再定義しておきます。

```coq
  Definition vfoldr (A B:Type) (f:A -> B -> B) (x0:B) (n:nat) (s:vector A n) :=
    Vector.fold_right f s x0.
```

#### `vnil`と`vcons`の一意性

通常のリストと異なり、`vector`型の`vnil`や`vcons`の一意性の証明が非常に厄介で、後に使うことになるため先に示しておきます。

```coq
  Lemma vector0nil (T:Type) : all_equal_to (vnil T).

  Lemma vectorScons (T:Type) n (s:vector T n.+1) :
    exists x (s':vector T n), s = vcons x s'.
```

akrさんの[サイト](http://www.a-k-r.org/d/2024-05.html)を参考にいたしました。ご指摘ありがとうございます。

### 定義

これと先ほど定義した`mkInductive`を用いて、再帰呼び出しを行うInductiveの型`basicInductive`を定義します。

```coq
  Inductive basicInductive (s:seq (Type * nat)) : Type :=
  | BasicInductive
      of mkInd (fun tn => tn.1 * vector (basicInductive s) tn.2:Type) s.
```

ここでポイントなのは、先ほど述べたように`f:Type * nat -> Type`の中に`(basicInductive s)`が入れることで再帰呼び出しを表現できる点です。

実際に引数のリスト`s:seq (Type * nat)`の各要素`(t,n):Type * nat`に対し、`t * vector (basicInductive s) n -> basicInductive s`という型のコンストラクタ、すなわち`t`型の引数と再帰する`n`個の引数からなるコンストラクタを定義するのと同等な定義になっています。

## コンストラクタ

`basicInductive s`上の各`n`番目のコンストラクタ`basicInductiveCon s n`は以下のように定義されます。

```coq
  Definition basicInductiveCon (s:seq (Type * nat)) (n:nat) :
    eachcon (fun tn => tn.1 * vector (basicInductive s) tn.2:Type) s n ->
    basicInductive s := @BasicInductive _ \o @mkcon_rec _ _ _ _.
```


## 帰納原理

`basicInductive`は`mkInductive`を用いて定義しましたが、ここでは再帰呼び出しを行うので、`my_mkInductive_ind`ではなく、再帰呼び出しに対応した帰納原理を再定義します。

まずはその帰納原理を記述するための準備をします。

### 準備

「帰納法の仮定が各`n`番目のコンストラクタの型`eachcon f s n`型で成り立つ」ということを記述するための関数を定義します。

```coq
  Fixpoint eachconProp (T:Type) (f:T -> Type) (P:forall x,f x -> Prop)
           (s:seq T) (n:nat) : eachcon f s n -> Prop :=
    match s,n return eachcon f s n -> Prop with
    | [::],_ => fun => True
    | t :: s',0 => @P _
    | t :: s',n'.+1 => @eachconProp _ _ P s' n'
    end.
```

これを用いて帰納原理を証明します。

### 帰納原理

```coq
  Lemma my_basicInductive_ind
        (s:seq (Type * nat)) (P:basicInductive s -> Prop):
    let f : Type * nat -> Type :=
        fun tn => tn.1 * vector (basicInductive s) tn.2:Type in
    (forall n,
      n < size s ->
      forall x:eachcon f s n,
        eachconProp (fun _ x => vfoldr (and \o P) True x.2) x ->
        P (basicInductiveCon x)) ->
    forall x, P x.
```

この命題の証明も`fix`を使いますが、詳細は[ソース](https://github.com/nekonistyle/SSReflect/blob/master/genind.v)をご覧ください。

意味としては、任意の`n`番目のコンストラクタの任意の要素`x:eachcon f s n`に対する命題を示します。
このとき、コンストラクタ`x:eachcon f s n`上の`x.2`個の再帰する各要素に対して`P`が成り立つことが帰納法の仮定になります。


## `basicInductive`を用いてリストを定義してみる

上で述べたように、`basicInductive`の引数に以下の`seqdef : seq (Type * nat)`を渡すことにより、リスト型`myseq`を定義することができます。

```coq
  Definition seqdef (T:Type) : seq (Type * nat) := [:: (unit:Type,0); (T,1)].
```

```coq
  Definition myseq (T:Type) := basicInductive (seqdef T).
```

`myseq`上の`nil`と`cons`も以下のように定義できます。
```coq
  Definition mynil (T:Type) : myseq T :=
    @basicInductiveCon (seqdef T) 0 (tt,vnil _).
  Definition mycons (T:Type) (x:T) (s:myseq T) : myseq T :=
    @basicInductiveCon (seqdef T) 1 (x,vcons s (vnil _)).
```

まずは`myseq`が`mynil`か`mycons`のどちらかで表せることを示します。

```coq
  Lemma myseq_case (T:Type) (s:myseq T) :
    s = mynil T \/ exists x s', s = mycons x s'.
```

これも使いやすいように以下の定理`myseqP`を証明します。

```coq
  Variant myseq_or (T:Type) : myseq T -> Prop :=
  | MyseqOrNil : myseq_or (mynil T)
  | MyseqOrCons x s: myseq_or (mycons x s).

  Lemma myseqP (T:Type) (s:myseq T) : myseq_or s.
```

この証明や次の帰納原理の証明で先ほどの`vnil`や`vcons`の一意性が必要になります。

### 一位性

コンストラクタの一位性ですが、`mynil`の場合引数を取らないので問題はないです。
しかし`mycons`の場合が問題になります。

示すべき命題は以下の2つです。

```coq
(*
  Lemma mycons_injl (T:Type) (x x':T) (s s':myseq T):
    mycons x s = mycons x' s' -> x = x'.
*)
  Lemma mycons_injr (T:Type) (x x':T) (s s':myseq T):
    mycons x s = mycons x' s' -> s = s'.
  Proof. by case. Qed.
```

ここで`mycons x s = mycons x' s'`を`case`すると、`s = s'`しか出てこず、おそらく後者の`mycons_injr`しか示せないです。
前者`mycons_injl`を示すのはおそらく`Type`上の、すなわち"型"同士における決定可能性が必要になります。
このようになる理由としては前述の通り、依存型で定義された型を`case`すると`existT`が出てきてしまう問題に引っかかるためです。しかしながら、`myseq`では`f`と`s`を具体的な値で指定しているので、後者はうまく`case`できて証明できるようです。


### 帰納原理

`myseq`の帰納原理は以下のようになります。

```coq
    Lemma myseq_ind (T:Type) (P:myseq T -> Prop):
      P (mynil _) -> (forall x s, P s -> P (mycons x s)) -> forall s, P s.
```

#### ~~問題点~~

**以下は解決済み、追加公理なしで示せます**

~~実は、定義で使用している`sizseq`ですが、(恐らく)Coqでは以下のような`SizNil`の一意性が証明できません。~~


```coq
    Lemma sizseq0nil (T:Type) : all_equal_to (SizNil T).
                             (* forall x, x = SizNil T *)
```

`sizseq`の定義を見ると

```coq
  Inductive sizseq (T:Type) : nat -> Type :=
  | SizNil : sizseq T 0
  | SizCons n : T -> sizseq T n -> sizseq T n.+1.
```

なので、`sizseq T 0`型の値が`SizNil`しかないのは明らかで、`case`で場合分けすれば簡単に示せるように思えます。しかしながら、`=`の定義は両辺とも同じ型でなければならず、場合分けで型が変化するような依存型の変数の場合は`case`による場合分けが使えないです。

ならばそもそも`sizseq`ではない他の長さの証明付きリスト、例えば`tuple`型や以下のように定義される型を使えばいいと思いますが、

```coq
Inductive sizseq' (T:Type) (n:nat) := Sizseq' (s:seq T) of size s == n.
```

`basicInductive s`のように再帰呼び出しを行うInductiveを定義する場合、`basicInductive s`をInductiveに定義された型のコンストラクタの直接の引数に渡さなければ定義が通らない(恐らく)なので、この問題を回避しつつ`sizseq`を使う以外の方法が分かりませんでした。


そこで、これを示すために異なる型の上でも定義できるequalityである`JMeq`の公理を使います。([JMeqライブラリ](https://coq.inria.fr/doc/V8.19.2/stdlib/Coq.Logic.JMeq.html))
@yoshihiro503 様、アドバイスありがとうございます。

```coq
Inductive JMeq (A:Type) (x:A): forall B:Type, B -> Prop :=
  JMeq_refl : JMeq x x.
Axiom : JMeq_eq A (x y:A): JMeq x y -> x = y.
```

この公理を用いると先ほどの`myseq_ind`が証明できます。

```coq
    Require Import JMeq.
    
    Lemma myseq_ind (T:Type) (P:myseq T -> Prop):
      P (mynil _) -> (forall x s, P s -> P (mycons x s)) -> forall s, P s.
```


# まとめ

特定の条件を満たした「Inductiveに定義させる型」を一般化しました。