0

わかりやすいように編集

特殊な種類の木の特性を証明しようとしています。このツリーは次のようなものです。問題は、Coq によって生成された誘導原理が、ツリーのプロパティを証明するには不十分であることです。より簡単な例として、次のタイプがすべての「ツリー」を表すとします。

Inductive prv_tree(E:BES) : statement -> Prop :=
| REFL (G:propVar_relation)(a:Prop) : 
  prv_tree E (G |- a ---> a)
| TRA (G:propVar_relation) (a b c:Prop) :
  prv_tree E (G |- a ---> b) -> prv_tree E (G |- b ---> c) ->
    prv_tree E (G |- a ---> c).

次に、すべてのツリーの健全性を証明するには (含意など)、次の補題を証明する必要があります。

Lemma soundness: forall E:BES, forall f g:Prop, forall R G:propVar_relation, 
  (prv_tree E (G |- f ---> g)) -> (E,G,R |= f --> g).

そのためには、ツリーの構造に帰納法を適用する必要があります。ただし、intros;induction H.そうすると、最初のサブゴールは(E,G,R |= f --> g)、必要な f と g の構造に関する情報が失われることです (必要です(E,G,R |= a --> a))。(また、帰納の場合、帰納仮説は と述べています(E,G,R |= f --> g)が、これは私には奇妙に思えます)。

私が試みた別のアプローチは(G |- f ---> g)、 f と g の構造を利用可能にしておくために を覚えておくことです。その後、証明は次のように進みます。intros;remember (G |- f --> g) as stmt in H.induction H.次に、基本ケースに期待するような目標と環境を取得します。ただし、ケース TRA を証明するために、次の証明コンテキストを取得します。

H : prv_tree E (G0 |- a --> b)
H0 : prv_tree E (G0 |- b --> c)
IHprv_tree1 : G0 |- a --> b = G |- f --> g -> (E,G,R |= f --> g)
IHprv_tree2 : G0 |- b --> c = G |- f --> g -> (E,G,R |= f --> g)

私は誘導仮説が

IHprv_tree1 : prv_tree E (G0 |- a --> b) -> (E,G,R |= a --> b)
IHprv_tree2 : prv_tree E (G0 |- b --> c) -> (E,G,R |= b --> c)

古いテキスト

特殊な種類の木の特性を証明しようとしています。このツリーは、21 の異なるルールを使用して構築できます (ここではすべてを繰り返しません)。問題は、Coq によって生成された誘導原理が、ツリーのプロパティを証明するには不十分であることです。

ツリーは次のように構築されます

Inductive prv_tree (E:BES): (*BES ->*) statement -> Prop := 
.... (*constructors go here*).

これらのコンストラクタの 1 つが

CTX: forall a b c:propForm, forall x:propVar, forall G:propVar_relation,
  (prv_tree E (makeStatement G a b) -> 
    (prv_tree E (makeStatement G (replace c x a) (replace c x b))))

私の目標は証明することです

Lemma soundness: forall E:BES, forall f g:propForm, forall G:propVar_relation, 
  forall tree:prv_tree E (makeStatement G f g), rel_cc_on_propForm E (cc_max E) G f g.

makeStatement G f gそうしないと、f と g の構造に関する情報が失われるので、これを行うために覚えています。次に、ツリーに誘導を適用します。すべてのケースを個別の補題として証明しました。これは、基本ケースにうまく使用できます。ただし、帰納的なケースでは、Coq によって提示された帰納仮説は使用できません。

たとえば、前述の CTX コンストラクターの場合、次の帰納仮説が得られます。

IHP {| context := G; stm_l := a; stm_r := b |} =
  {| context := empty_relation; stm_l := replace c x a;
  stm_r := replace c x b |} ->
    E, cc_max E |- replace c x a <,_ empty_relation replace c x b

私は使用できません。代わりに、次のようなものが欲しい

IHP prv_tree E {| context := G; stm_l := a; stm_r := b |} ->
  E, cc_max E |- replace c x a <,_ empty_relation replace c x b

誰かがこれを修正する方法を私に説明できますか? これまでのところ、私は prv_tree で独自の誘導原理を定義しようとしましたが、これは同じ問題を引き起こすので、これは間違っていたのでしょうか?

私自身の誘導原理におけるCTXのステートメントは次のとおりです。

  (forall a b c:propForm, forall x:propVar, forall G:propVar_relation, 
    (prv_tree E {| context := G; stm_l := a; stm_r := b |} ) ->
      P {| context := G; stm_l := replace c x a; stm_r := replace c x b |})
4

2 に答える 2

0

私はあなたの問題を理解したと思いますが、あなたの質問の全体を記入しなければなりませんでした. @ejgallego が提案したように、自己完結型の例を思いついた方が簡単だったでしょう。

これが私があなたの問題をどのようにモデル化したかです：

Axiom BES : Type.
Axiom propVar_relation : Type.

Inductive statement :=
| Stmt : propVar_relation -> Prop -> Prop -> statement.

Notation "G |- a ---> b" := (Stmt G a b) (at level 50).

Inductive prv_tree(E:BES) : statement -> Prop :=
| REFL (G:propVar_relation)(a:Prop) : 
  prv_tree E (G |- a ---> a)
| TRA (G:propVar_relation) (a b c:Prop) :
  prv_tree E (G |- a ---> b) -> prv_tree E (G |- b ---> c) ->
    prv_tree E (G |- a ---> c).

Lemma soundness: forall (E: BES) (f g:Prop) (R G:propVar_relation),
  (prv_tree E (G |- f ---> g)) -> R = R.

実際、あなたの質問で説明したのと同じ問題に遭遇します。解決策はrevert、記憶の後、誘導を行う前です。

intros.
remember (G |- f ---> g) as stmt. revert f g R G Heqstmt.
induction H; intros.

誘導仮説はまだ奇妙ですが、うまくいくはずです。

于 2016-02-11T13:52:55.820 に答える
0

ご協力ありがとうございました。結局、私は自分で解決策を見つけました。秘訣はh:statement -> Prop、誘導原理によって予想されるようにヘルパー関数 を定義し、 の代わりにこの関数を使用することでし(E,G,R |= f --> g)た。

于 2016-02-11T14:18:38.803 に答える