如何使用 solve_direct 建议的规则？（按（规则……）并不总是有效）答案

【问题标题】：How can I use rules suggested by solve_direct? (by (rule …) doesn't always work)如何使用 solve_direct 建议的规则？（按（规则……）并不总是有效）
【发布时间】：2013-08-29 12:59:24
【问题描述】：

有时<statement> solve_direct（我通常通过<statement> try 调用）列出了一些库定理，并说“当前目标可以直接解决：……”。

让<theorem>成为solve_direct的一个搜索结果，那么在大多数情况下我可以证明<statement> by (rule theorem)。

但是，有时这样的证明不被接受，导致错误消息“无法应用初始证明方法”。

是否有一种通用的、不同的技术来重用solve_direct 发现的定理？

还是取决于个人情况？我可以尝试制定一个最小的示例并将其附加到这个问题上。

【问题讨论】：

问题可能是由链式事实、假设中的元逻辑连接词、目标中的元变量（或类型变量）或其他因素引起的。我也许可以帮助理解一个具体的例子。
确实，我以后可能会寻求帮助并发布一个具体的例子。但是，我从其他回复中了解到，在许多实际情况下，有很多方法可以完成这项工作，现在我觉得很好。

标签： solver proof isabelle theorem-proving

【解决方案1】：

就个人而言，我只是倾向于使用：

apply (metis thm)

这在大多数情况下都有效，不会强迫我非常努力地思考（但如果需要棘手的解决方案，偶尔也会失败）。

通常也可以使用的其他方法包括：

apply (rule thm)                 (* If "thm" has no premises. *)
apply (erule thm)                (* If "thm" has a single premise. *)
apply (erule thm, assumption+)   (* If "thm" has multiple premises. *)

为什么没有一个单一的答案？答案有点复杂：

在内部，solve_direct 调用 find_theorems solves，然后执行以下操作：

fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
(* ... *)
if Thm.no_prems thm then rtac thm 1 goal
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;

这是类似于 rule thm 的 ML 代码，如果规则没有前提，或者：

apply (erule thm, assumption+)

如果规则有多个前提。正如 Brian 对您的问题所评论的那样，如果假设中有复杂的元逻辑连接词（norm_hhf_tac 处理，但据我所知并未直接暴露为 Isabelle 方法），上述方法可能仍然失败。

如果你愿意，你可以写一个新方法直接暴露find_theorems使用的策略，如下：

ML {*
  fun solve_direct_tac thm ctxt goal =
  if Thm.no_prems thm then rtac thm 1 goal
  else (etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
*}

method_setup solve =
  {* Attrib.thm >> (fn thm => fn ctxt =>
        SIMPLE_METHOD' (K (solve_direct_tac thm ctxt ))) *}
  "directly solve a rule"

然后可以按如下方式使用：

lemma "⟦ a; b ⟧ ⟹ a ∧ b"
  by (solve conjI)

这有望解决solve_direct 向您抛出的任何问题。

【讨论】：

感谢您指出如何真正做到正确。正如我从最终用户的角度所问的那样，这种方法对我来说太过分了。确实是by (metis thm) 之一，或者有时by metis（事实证明metis 不需要这个定理），或者有时by (simp add: thm) 在我迄今为止遇到的情况下对我有用。
@ChristophLange：我不倾向于知道此类问题的答案，所以我查看了 Isabelle 的源代码来解决它们；我只是写下了我的思维模式，所以我的答案似乎不是通过占卜来的。 :) 不过，可能值得将我的妙语移到答案的顶部。
您也可以使用apply (erule (1) thm)，而不是apply (erule thm, assumption+)，其中1 是要使用的附加场所的数量。
@davidg，并不是说它的风格很好，但你能扩展你的方法来进行搜索吗？这样by (solve_direct) 总是可以工作:-)
@JoachimBreitner：如果solve_direct 输出一条与try [[by (erule (2) foo)]] 类似的消息，点击证明将其插入缓冲区（与 Sledgehammer 一样），这可能会有用。也许尝试在邮件列表中请求？

【解决方案2】：

我找到了另一种将solve_direct 的建议与by rule 结合使用的方法。当建议库中的某些非常基本的规则（例如Hilbert_Choice.someI2）时，似乎上下文中的一个事实实际上就是一个可能适用的规则本身。以下内容至少在两种具体情况下对我有用 (source)：

重新检查“类似规则”的事实、其他事实（如果有）和目标
如有必要，重新排序其他事实
做证明using <other_facts> ... by (rule <rule-like-fact>)

【讨论】：

+1 为上面提到的 github 上的变更集。各种打样工具各有千秋，往往信息量更大（也便于后期打样维护），避免重锤，打样更精准。这需要在实践中得到很好的平衡，自动推理能力既不会太多也不会太少。

【解决方案3】：

您可以尝试fact 或rule_tac。如果我没记错的话，rule 有时在存在其他事实的情况下无法应用给定规则，我不完全确定原因；这个问题必须由比我更熟悉这些方法的实现细节的人来回答。

【讨论】：

如果可能的话，我应该说我想避免apply 风格的语法（我认为这是rule_tac 所暗示的）。如果fact 表示by (fact thm)，这在我的某些情况下不起作用。我从 grepping 库中看到，有很多方法可以使用规则对内置的自动证明者进行参数化（可以看到，例如，当 grepping for someI2 时，solve_direct 曾经建议我作为规则），但是我不知道有什么好的教程来描述这些（例如，可与 Tobias Nipkow 的“结构化 Isar 证明的教程介绍”相媲美）——你呢？
rule 要求链式事实匹配规则的假设前缀。如果您希望规则忽略链接的事实，您需要先将它们插入到目标中。这可以通过- 方法完成，（如by - (rule foo)）。