0

Coqで任意の帰納命題定義が与えられた場合、帰納命題で帰納戦術を呼び出すときに使用する合理的なdisj_conj_intro_patternを導出するための一般式はありますか?

一般に、帰納的定義のコンストラクターのいずれかの完全な intro_pattern には、複数の仮説および複数の帰納的仮説 (の名前) が必要な場合があります。この場合、パターンで提供される名前の順序には、すべてのパラメーターが含まれる場合があります。 1 つの仮説と対応する帰納的仮説、その後に仮説と帰納的仮説からなる 1 つまたは複数の追加のペアが続きます。たとえば、Software Foundations には次のものが含まれます。

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 にはそれぞれ、仮説と帰納的仮説の 2 つのペアがあります。おそらく、これら 2 つのコンストラクターにはそれぞれ次の形式の式が含まれているためです。

x -> y -> z

これについては、現在のリファレンス マニュアルには次のようにしか書かれていません。

disj_conj_intro_pattern としての帰納項

これは誘導項として動作しますが、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) 仮説と帰納的仮説のペアの数は、コンストラクター内の仮説の数、問題の合計から得られますか? それともそれ以上のものがありますか？

リファレンスマニュアルの戦術の章と、第1章のガリーナ文法のパターンに関する非常に一般的な議論以外に、これに関する他の関連文書はありますか?

4

1 に答える 1

0

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

Coqは、任意の帰納的定義の帰納原理を自動的に生成し_ind、接尾辞として追加する名前を付けます。そのため、の帰納原理は にexp_matchなりexp_match_indます。exp_match_indコマンドを使用してタイプを調べるとCheck、必要なイントロ パターンを作成できます。

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

このタイプは、（最初​​のforall「ヘッダー」をスキップした場合）ゴールを証明するために一連のサブゴールを証明する必要があることを示していますP l r。->最上位のEveryは、サブゴールを分離します。

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

残りのサブゴールは同様に行うことができ、定理で使用されるパターンになります。

于 2016-08-31T07:19:37.750 に答える