7

apply-scriptで使用する場合apply (rule)、通常、適切なルールが選択されます。同じことがproof構造化された証明にも当てはまります。使用されたルールの名前はどこで学習/検索できますか？

4

3 に答える 3

5

rule_trace次のように使用してみてください。

lemma "a ∧ b"
  using [[rule_trace]]
  apply rule

これは出力に表示されます：

rules:
  ?P ⟹ ?Q ⟹ ?P ∧ ?Q
  ?P ⟹ ?Q ⟹ ?P ∧ ?Q 
proof (prove): step 2

goal (2 subgoals):
 1. a
 2. b

ルールの名前が必要な場合は、find_theorems;を使用してみてください。それらを直接決定できるかどうかはわかりません。

于 2013-03-21T11:56:23.673 に答える
3

Pure.intro// （introまたはiffその?またはバリアントの1つ）として宣言されたものはすべて、!デフォルトの導入ルールと見なされます（つまり、現在のファクトがチェーンされていない場合）。同様に、Pure.elim/ elim/として宣言されているものはすべて、iffデフォルトの削除ルールと見なされます（つまり、現在のファクトが連鎖している場合）。通常、後の宣言が前の宣言よりも優先されます（少なくとも、同じ種類の宣言が使用されている場合...たとえば、Pure.intro?とintroの混合などは、異なる結果になる可能性があります）。

ただし、これは原則としてどのようなルールが考慮されているかを示しているにすぎません。どのルールが適用されたかを直接知る方法がわかりません。find_theorems introしかし、あなたが疑問に思っていた線の真上から正しいルールを見つけるのは比較的簡単です。例えば、

lemma "A & B"
find_theorems intro
proof

目標への導入ルールとして適用できるすべてのルールが表示されますA & B。それらの1つは、によって適用されるデフォルトのルールですproof（取得したサブゴールによって認識されます）。

消去ルールには、たとえば、

lemma assumes "A | B" shows "P"
using assms
find_theorems elim
proof
于 2013-03-21T11:54:35.180 に答える
3

他の回答は、どの見出語がによって適用されるかを決定する方法をすでに示していますrule。proofを呼び出すのruleではなく、メソッドを呼び出すことに注意してくださいdefault。ほとんどの場合default、と同じようruleに動作しますが、たとえば、ロケール述語を証明するために。を呼び出しますunfold_locales。

そこで実際に何が起こっているのかを知る方法はわかりません。

于 2013-03-25T20:55:20.763 に答える