当且仅当它解决当前目标时应用方法答案

【问题标题】：Apply a method if and only if it solves the current goal当且仅当它解决当前目标时应用方法
【发布时间】：2013-03-08 09:07:20
【问题描述】：

有时，当我在写应用风格的证明时，我想要一种将证明方法foo 修改为

在第一个目标上尝试foo。如果它解决了目标，很好；如果确实如此不解决，恢复原状，失败。

这出现在以下代码中：

qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+

在进一步进行一些更改后，对simp 的调用将不再完全解决目标，然后这将循环。如果我可以指定类似的东西

qed (solve_goal(subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail))+

或（替代建议的语法）

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)!)+

或者（也许更好的语法）

qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+

它会停在这个脚本无法解决的第一个目标上。

【问题讨论】：

我猜你的fibs.simps 或fib.simps 触发了循环行为（可能是由于一般的左侧和右侧的if）？通常可以用条件规则替换它们。
我提交了patch implementing this，让我们看看会发生什么。
@Joachim Breitner：仅作记录，我个人认为在结构化证明（如您的示例）中，这样的怪物不属于qed ;)。我总是更喜欢在相应的proof/qed 中明确设置另一个子证明。但是，您说的是apply 脚本，我完全同意。（也许您可以将示例中的qed 变成apply？）
我在proof 中提出的方法创造了几个目标，其中只有一个是不平凡的；在适当的 isar 中证明了这一点。如果fibs.simps 没有循环，其他问题将由qed simp 解决（您认为可以吗？）。上面的怪物最接近我更喜欢的概念simp。我本可以使用apply_end，但我认为那更糟糕。

标签： proof isabelle

【解决方案1】：

Isabelle 没有这样的组合器，这也是我想念的。通常，如果我将 auto 或 simp 调用替换为 fastforce 或 force（具有解决或失败行为），我可以避免对此类组合器的需要。

因此，如果您的示例中的 simp 应该解决目标（不循环），

qed (subst fibs.simps, (subst fib.simps)?, fastforce simp: nth_zipWith nth_tail)+

可能是一个更强大的变体。

【讨论】：

啊，终于有了使用fastforce 或force 的理由——我从不觉得需要它们，只使用auto 和simp。尽管如此，是否可以使用ML {* .. *} 实现这样的组合器，或者该部分不可扩展？
Isabelle/Isar 方法子语言可以通过method_setup 进行扩展，但少数方法组合符是固定的。所以你可以根据任意复杂的战术和战术定义自己的证明方法，但不会改变证明方法表达式的程式化方式。

【解决方案2】：

自从Eisbach proof script language 出现以来，现在已支持此功能。导入"~~/src/HOL/Eisbach/Eisbach"后可以替换

apply foo

与

apply (solves ‹foo›)

如果solves 产生任何新目标，则该行将失败。这可以与[1] 结合使用，如

apply (solves ‹(auto)[1]›)

如果需要。

solves的定义其实很简单：

method solves methods m = (m; fail)

【讨论】：

【解决方案3】：

虽然没有可用的内置策略或组合器，但您可以自己实现一个，如下所示：

ML {*
fun solved_tac thm =
  if nprems_of thm = 0 then Seq.single thm else Seq.empty
*}

method_setup solved = {*
  Scan.succeed (K (SIMPLE_METHOD solved_tac))
*}

这将创建一个新方法solved，如果当前目标已完全解决，该方法将成功，如果仍有一个或多个子目标剩余，则该方法失败。

可以这样使用，例如：

lemma "a ∨ ¬ a "
  apply ((rule disjI1, solved) | (simp, solved))
  done

如果没有solved 子句，Isabelle 将选择apply 步骤的rule disjI1 一侧，从而使您无法实现目标。在每一边都有solved 子句，Isabelle 尝试使用rule disjI1，当它无法解决目标时，切换到simp，然后就成功了。

这可用于通过使用 Isabelle 的 (...)[1] 语法来解决个人目标。例如，以下语句将尝试使用simp 解决尽可能多的子目标，但如果simp 无法完全解决子目标，则将保持子目标不变：

apply ((simp, solved)[1])+

【讨论】：

太好了，这让我可以拥有想要的method[1!]（如果method 解决了第一个目标，即使还有其他目标，它也会成功）(method, solved)[1]。
我想我也开始了类似的代码，如果开放目标的数量是 n...
@JoachimBreitner：谢谢。本来想提这个的，但没想到。我在最后添加了一个示例，希望对未来的搜索者有所帮助。

【解决方案4】：

Isabelle 的 Isar 语言不提供该功能；这是故意的，而不是错误，正如on the isabelle developer list 解释的那样：

Isar 证明方法语言被设计成某种方式，以达到证明文本中某些操作方面的“风格化”规范。它排除了任何类型的编程或复杂的控制故意的结构。

【讨论】：