誘導命題のCoq - disj_conj_intro_patterns

Question

Coqの任意の誘導命題定義が与えられた場合、誘導命題に対して誘導戦略を呼び出すときに使用する合理的なdisj_conj_intro_patternを導出する一般的な式はありますか？

一般に、帰納的定義のコンストラクタのいずれかの完全なintro_patternは、複数の仮説と複数の帰納仮説を（名前を）必要とすることがあります。この場合、パターンに含まれる名前の順序付けには、パラメータ、続いて1つの仮説および対応する帰納的仮説、続いて仮説および帰納仮説からなる1つまたは複数の追加の対が続く。例えば、ソフトウェアの基礎は、以下を含む： - これら2つのコンストラクタ各フォーム

の表現が含まれているため、おそらく

Inductive exp_match {T} : list T -> reg_exp T -> Prop := 
| MEmpty : exp_match [] EmptyStr 
| MChar : forall x, exp_match [x] (Char x) 
| MApp : forall s1 re1 s2 re2, 
      exp_match s1 re1 -> 
      exp_match s2 re2 -> 
      exp_match (s1 ++ s2) (App re1 re2) 
| MUnionL : forall s1 re1 re2, 
       exp_match s1 re1 -> 
       exp_match s1 (Union re1 re2) 
| MUnionR : forall re1 s2 re2, 
       exp_match s2 re2 -> 
       exp_match s2 (Union re1 re2) 
| MStar0 : forall re, exp_match [] (Star re) 
| MStarApp : forall s1 s2 re, 
       exp_match s1 re -> 
       exp_match s2 (Star re) -> 
       exp_match (s1 ++ s2) (Star re). 

Notation "s =~ re" := (exp_match s re) (at level 80). 

Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T), 
    s =~ re -> 
    In x s -> 
    In x (re_chars re). 
Proof. 
    intros T s re x Hmatch Hin. 
    induction Hmatch 
    as [ 
     |x' 
     |s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 
     |s1 re1 re2 Hmatch IH|re1 s2 re2 Hmatch IH 
     |re|s1 s2 re Hmatch1 IH1 Hmatch2 IH2]. 

この例では、MAPPとMStarAppためintro_patterns各仮説と誘導仮説の二対を有します

X - > Y - > zがこのについて

、現在のリファレンスマニュアルのみ

を言っているようですdisj_conj_intro_pattern

として0

誘導用語これは、誘導用語として動作しますが、 文脈で導入された変数に名前を付けるために disj_conj_intro_patternで名前を使用しています。 disj_conj_intro_patternは、通常、[ p11 ... p1n1 | ... | pm1 ... pmnm] mはコンストラクタの数で、 という種類のものです。 i番目の目標の 文脈で誘導によって導入された各変数は、の順序でリストpi1 ... piniからその名前を取得します。十分な名前がない場合、帰納変数は の残りの変数の名前を作り出します。より一般的には、pijは任意の離散的/結合的な導入パターン（8.3.2節を参照）とすることができます。 インスタンスの場合、1つのコンストラクタを持つ誘導型の場合、[p1 ... pn]の代わりに という表記（p1、...、pn）を使用できます。

これは、指定された誘導定義の完全なdisj_conj_intro_patternの正しい形式を決定する方法を指定していないようです。

上記の私の経験的観察は、1）各コンストラクタの仮パラメータが最初に来て、コンストラクタの仮説が対応する帰納的仮説と対になっていること。 2）仮説と帰納仮説の組の数は、コンストラクタ内の仮説の数、問題の総和から求められる。それともそれ以上はありますか？

リファレンスマニュアルのTacticsの章と、第1章のGallina文法のパターンに関する非常に一般的な議論の他に、関連する他の文書はありますか？

Answer 1

私があなたの質問を正しく理解していれば、答えは「はい」です。誘導のためのイントロパターンを導出できます。

Coqは帰納的定義の誘導原理を自動的に生成し、接尾辞として_indを追加するので、exp_matchの誘導原理はexp_match_indになります。コマンドを使用してタイプexp_match_indを探索すると、必要なイントロパターンを生成できます。

Check exp_match_ind. 

(* output: 
exp_match_ind 
    : forall (T : Type) (P : list T -> reg_exp T -> Prop), 
     P [] EmptyStr -> 
     (forall x : T, P [x] (Char x)) -> 
     (forall (s1 : list T) (re1 : reg_exp T) 
      (s2 : list T) (re2 : reg_exp T), 
     s1 =~ re1 -> 
     P s1 re1 -> 
     s2 =~ re2 -> P s2 re2 -> P (s1 ++ s2) (App re1 re2)) -> 
     (forall (s1 : list T) (re1 re2 : reg_exp T), 
     s1 =~ re1 -> P s1 re1 -> P s1 (Union re1 re2)) -> 
     (forall (re1 : reg_exp T) (s2 : list T) (re2 : reg_exp T), 
     s2 =~ re2 -> P s2 re2 -> P s2 (Union re1 re2)) -> 
     (forall re : reg_exp T, P [] (Star re)) -> 
     (forall (s1 s2 : list T) (re : reg_exp T), 
     s1 =~ re -> 
     P s1 re -> 
     s2 =~ Star re -> P s2 (Star re) -> P (s1 ++ s2) (Star re)) -> 
     forall (l : list T) (r : reg_exp T), l =~ r -> 
     P l r 
*) 

このタイプは、あなたが目標P l rを証明するためにサブゴールの束を証明する必要があること（あなたが最初のforall「ヘッダーを」スキップ場合）と述べています。トップレベルのすべての->はサブゴールを分離：

1）MEmpty場合：

P [] EmptyStr 

何の仮説はありません、我々は induction Hmatch as [ |で始まる理由、それはだ - |の左側には何もありません注意してください。

2）MChar場合：

(forall x : T, P [x] (Char x)) 

この場合、イントロパターンは単純です：いくつかのx'のために、私たちはP [x'] (Char x')を証明する必要があります。この時点で私たちのパターンとなる：[ | x' ...

3）MApp場合：

(forall (s1 : list T) (re1 : reg_exp T) 
     (s2 : list T) (re2 : reg_exp T), (* s1 re1 s2 re2 *) 
     s1 =~ re1 ->      (* Hmatch1 *) 
     P s1 re1 ->      (* IH1 *) 
     s2 =~ re2 ->      (* Hmatch2 *) 
     P s2 re2 ->      (* IH2 *) 
     P (s1 ++ s2) (App re1 re2))  (* the current subgoal *) 

私は定理in_re_matchに使用されるものに応じて上記のコメントの変数と仮説をマークしました。この時点でのパターンは次のようになります。[ | x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 ...

残りの部分ゴールは同様に行われ、定理で使用されるパターンになります。