'適用（規則）'或'證明'使用什麼規則？

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所有規則。其中之一是由proof應用的默認規則（您將通過您獲得的子目標識別它）。

對於消除規則，你可以使用，例如，

lemma assumes "A | B" shows "P" 
using assms 
find_theorems elim 
proof 

Answer 3

其他答案已經告訴你如何確定rule應用哪些引理。請注意，proof不會調用rule，但方法default。在大多數情況下，default與rule的功能相同，但例如，以證明它稱爲unfold_locales的區域謂詞。

我不知道有什麼方法可以查看實際發生的情況。