はじめに

本記事はTPP2024で発表した内容になります。

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

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

ソースコードはこちら

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

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

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

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

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

  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は以下の関数で表せます。

  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.

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

コンストラクタの一意性

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

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

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

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

  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に書き換えてくれるため、使い勝手がよくなります。

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

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

帰納原理

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

  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型を作ってみます。

  Definition day := nconstructor 7.

  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は以下の通りです。

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

  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の帰納原理がうまく自動生成されないので、自分で定義します。

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

  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型を返す定義になっています。

  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が定義できます。

  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の場合は以下のように証明できます。

  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にある以下の定理が必要になります。

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が決定可能な型でないといけないということです。

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

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

  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に書き換えてくれます。

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

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

帰納原理

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

  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に定義するでn分木を定義したときのようにInductiveで定義された型の引数に渡す必要があります。

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

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

上の記事では自作のsizseq型を作っていますが、今回はCoqの標準ライブラリであるVectorDef.vのt型(Vector型)を使います。

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

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型に変更しておきます。

  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と引数の順番が合うように再定義しておきます。

  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の一意性の証明が非常に厄介で、後に使うことになるため先に示しておきます。

  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さんのサイトを参考にいたしました。ご指摘ありがとうございます。

定義

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

  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は以下のように定義されます。

  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型で成り立つ」ということを記述するための関数を定義します。

  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.

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

帰納原理

  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を使いますが、詳細はソースをご覧ください。

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

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

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

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

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

myseq上のnilとconsも以下のように定義できます。

  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のどちらかで表せることを示します。

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

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

  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つです。

(*
  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の帰納原理は以下のようになります。

    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の一意性が証明できません。~~

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

sizseqの定義を見ると

  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型や以下のように定義される型を使えばいいと思いますが、

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

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

そこで、これを示すために異なる型の上でも定義できるequalityであるJMeqの公理を使います。(JMeqライブラリ)
@yoshihiro503 様、アドバイスありがとうございます。

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が証明できます。

    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に定義させる型」を一般化しました。