'適用（ルール）'または '証明'のルールは何ですか？

Question

適用スクリプトでapply (rule)を使用すると、通常は適切なルールが選択されます。同じことが構造化プルーフでproofにも当てはまります。使用されたルールの名前はどこで調べられますか？ Pure.intro/intro/iff（またはその?または!変種の一つ）として宣言されて

Answer 1

あなたは次のように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を使用して試すことができます。彼らが直接決定できるかどうかはわかりません。

Answer 2

すべてがデフォルトの導入ルールとして考えられている（つまり、何も現在の事実がで連鎖されていない場合）。同様に、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 

Answer 3

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

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