'适用（规则）'或'证明'使用什么规则？

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的区域谓词。

我不知道有什么方法可以查看实际发生的情况。