この例でCoqのタイプシステムとは何ですか？

Question

私は以下の時間の定義に証明用語の一致部分にコックの型システムの動作について困惑している：

Set Implicit Arguments. 
Definition h := fun (a b : nat) (e : a = b) => 
(fun (x y : nat)(HC : b = y)(H : x = y) => 
(match H in (_ = y0) return (b = y0 -> b = x) with 
| @eq_refl _ _ => fun HC0 : b = x => HC0 
end HC)) a b (eq_refl b) e. 

チェックhは全体的なタイプがAB FORALL」で教えてくれる：NAT、A = b→b = a」となる。

Hの型はx = yなので、return節のためにb = y - > b = xの型を返すように見えます。以下の様々な項を適用した後、hの予想される型を得る。

ただし、fun HC0：b = x => HC0は、b = x - > b = xの識別関数です。私は、b = x - > b = xをタイプb = y - > b = xとして認識させるような強制はないと信じています。

私の最高の推測は、タイプx = xの@ eq_refl nat xであるHのコンストラクタが一意であることです。 Hもx = y型なので、xとyという名前は同じ項に結びついています。したがって、型システムは、b = x - > b = xがb = y - > b = xの型であると決定する。これは近いですか？この種の行動は説明されているのか、それともどこかに書かれていますか？私はイオタ削減を見たが、それは正しいとは思わない。

Answer 1

これはかなりです。この動作は文書化されています（this manual chapterの "マッチ... with ...エンドコンストラクション"を探してください）、何が起こっているのか分かりにくいかもしれません。

まず、コックにチェックする方法の典型的なmatchリコール：listタイプのすべてのコンストラクタはmatchに対応するブランチを有し、（2）各枝そのこと

Inductive list (T : Type) := 
| nil : list T 
| cons : T -> list T -> list T. 

Definition tail (T : Type) (l : list T) : list T := 
    match l with 
    | nil  => nil 
    | cons x l' => l' 
    end. 

コックチェック（1）各分岐に導入されたコンストラクタ引数が適切な型（ここではxがタイプTであり、l'が第2ブランチの型がlist Tであると仮定して、同じ型（この場合はlist T）を持ちます。

単純なケースでは、各ブランチをチェックするために使用されるタイプは、マッチ式全体のタイプとまったく同じです。ただし、ではなく、が常にtrueです。Coqは、チェックしているブランチから抽出した情報に基づいて、より特殊なタイプを使用することがあります。 上ケース分析を行うとき、これはeqのように、誘導タイプのインデックスを作成しばしば起こる：

Inductive eq (T : Type) (x : T) : T -> Prop := 
| eq_refl : eq T x x. 

（=表記はeqのためだけ中置構文糖である。）誘導型の

引数がに与えられましたコロンの右側はコークス特有のもので、のインデックスであるとして知られています。左に現れるもの（この場合、Tとx）は、のパラメータとして知られています。パラメータは、誘導型の宣言ではすべて異なる必要があり、すべてのコンストラクタの結果で使用されたものと正確に一致する必要があります。たとえば、以下の不正なスニペットを考えてみましょう。それはeq_refl'コンストラクタの結果にnat代わりのTを見つけたので

Inductive eq' (T : Type) (x : T) : T -> Type := 
| eq_refl' : eq nat 4 3. 

コックは、この例を拒否します。

インデックスには、この制限はありません。戻り値のコンストラクタに表示されるインデックスは、適切な型の任意の式にすることができます。さらに、その表現は、現在のコンストラクタによって異なる場合があります。このため、Coqでは、各ブランチの戻り値の型を、各ブランチのインデックスの選択によって変えることができます。オリジナルの例を少し簡略化したものを考えてみましょう。

Definition h (a b : nat) (e : a = b) : b = a := 
    match e in _ = x return x = a with 
    | eq_refl => eq_refl : a = a 
    end. 

eqに2番目の引数はインデックスであるので、原理的には使用されるコンストラクタに応じて変えることができます。 Coqは、使用されたコンストラクタを調べるときにそのインデックスが実際に何であるかだけを調べるので、一致の戻り値の型はそのインデックスに依存します。一致のin句は、誘導型のすべてのインデックスに名前を付けますこれらの名前は、return句で使用できるバインド変数になります。

ブランチを入力するとき、Coqはインデックスの値を調べ、in句で宣言された変数にそれらの値を代入します。この一致は1つの分岐のみを持ち、その分岐はインデックスをeのタイプ（この場合はa）の2番目の引数と同じにします。したがって、Coqはそのブランチのタイプがa = aであることを確認しようとします（つまり、xの代わりにx = aとa）。したがって、我々は単にeq_refl : a = aを提供することができ、我々は完了です。

これで、Coqはすべてのブランチが正しいことを確認したので、return句のタイプをeのインデックスがxに置き換えてマッチ式全体に割り当てます。この変数eはタイプa = bであり、インデックスはbであり、したがって結果のタイプはb = aです（つまり、x = a、bはxと置き換えられます）。

This answerは、パラメータとインデックスの相違点についてより多くの説明を提供します。