4

「あなたが尋ねている質問は主観的であるように思われ、閉じられる可能性があります。」

まあ、私はそれを知っていますが、それでもここで尋ねる価値があると感じています。

ヒントデータベースと自動を使用する必要があると何度も言われてきました。これは、これまでで最高のものであるためです。しかし、それを数回使用しようとすると、些細なことでまったくイライラしました。これが起こり続けることの1つです。

Section Annoying.

Variable T : Type.
Variable P : T -> Prop.

Axiom notP : forall x, ~ P x.
Hint Resolve notP.

Goal forall (x : T), P x -> False.
intros x.
auto. (* nothing... *)
replace (P x -> False) with (~ P x) by reflexivity.
(* fold not. does not work, don't know why either but that is not the point here... *)
auto.
Qed.

End Annoying.

したがって、私の質問は、人々がヒントデータベースをどのように使用し、そのような問題に遭遇しないようにするかということです。効果的なヒントデータベースの経験則はありますか？

4

1 に答える 1

3

自動は、変更されていない定理を目標に適用することによって機能します。それは、それらの形状の構文的観察によって適用する定理を探します。したがって、notPの定理はフォームの目標にのみ適用されます

〜P..。

P x-> Falseの形式の目標は、構文的にこの形式ではありません。実際、自動戦術は次のように機能します。最初に可能な限りイントロを使用し、次に定理を適用してみます。だからあなたの目標はに変換されます

H：P x
=========
 誤り

次に、Falseを証明できる定理を適用しようとします。残念ながら、インスタンス化の推測が必要ない定理のみを適用しようとします（戦術で使用できる定理が適用され、「with」拡張は必要ありません）。したがって、「forall a、P a-> False」という形式のステートメントを持つ定理は、autoによって使用されることはありません。これは、applyがaをインスタンス化する方法を知っていると文句を言うためです。

したがって、自動の適切な候補証明は、イントロを使用して適用するだけで実行できる証明であり、展開や適用のインスタンスはありません...引数への定理の手動適用はなく、各ステップで右端の式（定理の矢印の終わりにある）は、目標の結論に現れる述語として述語を使用します。

ある時点での目標は「〜P x」であるため、厄介な例が機能します。したがって、メインシンボルはそうではなく、autoはこのメインシンボルのテーブルにレンマnotPを持っています。

うまく機能する例を次に示します。

変数my_le：nat->nat->Prop。

仮説my_le_n：forall x、my_lexx。

仮説my_le_S：forall xy、my_le xy-> my_le x（S y）。

ヒントmy_le_nmy_le_Sを解決します。

補題トト：my_le1014。
証拠。
自動。
Qed。

ヒントコマンドの後、autoのテーブルには2つの見出語「my_le_n」と「my_le_S」があり、ゴールのメインシンボルがmy_leの場合に使用されます。「my_le1014」を見ると、これら2つの見出語を順番に試します。最初の失敗は失敗しますが、2番目の目標が適用され、新しい目標「my_le 10 13」が生成されます。これは、autoが「my_le_n」を適用できるようになるまで数回繰り返すことができます。したがって、autoは、特定の目標に適用できるいくつかの定理が存在する可能性があるという事実から分岐が生じる可能性のツリーを探索します。また、ブランチの長さは5に制限されているため、my_le1015はautoによって解決されません。autoに数値引数を指定することにより、分岐の長さを変更できます。したがって、「auto 20」は、「my_le1015」およびその他の同様のインスタンスを解決します。

于 2013-01-11T09:00:51.420 に答える