タイプのファミリーのための帰納的定義

Question

私はしばらくの間これを苦労してきました。正規表現r:Exp私はrに関連付けられた言語を表現しようとしていますが与えられ、ここで

Inductive Language : Exp -> Set :=                                   
    | LangLit  : forall c:char, Language (Lit c) 
    | LangAnd  : forall r1 r2: Exp, Language(r1) -> Language(r2) -> Language(And r1 r2) 
    | LangOrLeft : forall r1 r2: Exp, Language(r1) -> Language(Or r1 r2) 
    | LangOrRight : forall r1 r2: Exp, Language(r2) -> Language(Or r1 r2) 
    | LangEmpty : forall r: Exp, Language (Many r) 
    | LangMany : forall r: Exp, Language (Many r) -> Language r -> Language (Many r). 

合理的：そこから私は、誘導タイプのファミリーを定義する

Definition char := nat. 
Definition string := list char. 


Inductive Exp : Set := 
    | Lit : char -> Exp 
    | And : Exp -> Exp -> Exp 
    | Or : Exp -> Exp -> Exp 
    | Many: Exp -> Exp 

：私は、誘導型を持っていますタイプLanguage rとして、私は単一の帰納的定義でそうしています。

私が証明したいと思います：正規表現'c'の言語は単一の文字列"c"で作られている。すなわち

Lemma L1 : forall (c:char)(x:Language (Lit c)), 
    x = LangLit c. 

は（つまり、タイプLanguage (Lit c)は、一つだけの要素を持っているもちろん、私は必要があります。今すぐ）stringにLanguage rの要素を変換

をいくつかのセマンティクスを定義するには、この問題の詳細は重要ではなく、単に私の質問をやる気にさせる役割：私たちはnat代わりのExpとlを使用してみましょう私は種類List nのファミリーを定義するために、単一の誘導性の定義を使用しています。ここで再び

Parameter A:Set. 
Inductive List : nat -> Set := 
    | ListNil : List 0 
    | ListCons : forall (n:nat), A -> List n -> List (S n). 

：ら、私たちは、長さnのリストを表しタイプList nを定義します。

私が証明したいと思います：

Lemma L2: forall (x: List 0), 
    x = ListNil. 

（つまり、タイプList 0は一つだけの要素を持っています）。

私はこのアイデアを使い果たしました。

帰納的型（または述語）で（陰性）結果を証明しようとすると、関連するすべての仮説が目標（generalize）内にあることが確認され、型コンストラクタ）。しかし、この場合はelimは良いことではありません。

Answer 1

あなたがCoqの基本的なロジック以外のものを受け入れる場合は、Programライブラリで入手可能なdependent destruction戦術を使用することができます（私は最後の例を標準ライブラリベクトル）：

Require Coq.Vectors.Vector. 

Require Import Program. 

Lemma l0 A (v : Vector.t A 0) : v = @Vector.nil A. 
Proof. 
now dependent destruction v. 
Qed. 

あなたが用語を調べるならば、あなたはこの戦術が通過する証拠を得るためにJMeq_eq公理に頼っていることがわかります：

幸い

Print Assumptions l0. 

Axioms: 
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y 

を、それを証明することが可能です以前の補題の記述に小さな変更を加えることで、Coqの基本ロジックの外にある機能に頼ることなく、を実行できます。

Lemma l0_gen A n (v : Vector.t A n) : 
    match n return Vector.t A n -> Prop with 
    | 0 => fun v => v = @Vector.nil A 
    | _ => fun _ => True 
    end v. 
Proof. 
now destruct v. 
Qed. 

Lemma l0' A (v : Vector.t A 0) : v = @Vector.nil A. 
Proof. 
exact (l0_gen A 0 v). 
Qed. 

私たちは、この新証拠は、追加の公理を必要としないことがわかります。ここでは何が起こった

Print Assumptions l0'. 
Closed under the global context 

を？おおまかに言えば、Coqでは、インデックスが特定の形をしている依存型の条件についてケース分析を行うことはできません（例えば、0の場合）です。代わりに問題のある指標を変数に置き換えたより一般的なステートメントを証明しなければなりません。これはちょうどl0_gen補題がしていることです。どのようにして一致をnにしなければならなかったかに注目して、vに要約した関数を返します。これは、"convoy pattern"という別のインスタンスです。我々は

match n with 
| 0 => v = @Vector.nil A 
| _ => True 
end. 

を書いていたコックは、その枝が病気に型指定された作り、タイプVector.t A nを持つものとして0ブランチでvを見るでしょう。

このような一般化は、Coqで依存型プログラミングを行う大きな苦労の1つです。 Agdaのような他のシステムでは、この種のコードをもっと簡単に書くことができますが、Coqが基本的な理論に含めることを避けたい余分な公理に頼ることなくこれを行うことができるのは最近のことです（shown）。これが将来のバージョンで単純化されることを願っています。