问题标签 [apply-script]

假设我有一个引理mylem: foo ?a = bar ?a，我需要将它应用到一个目标上，该目标有两次出现foo，例如baz (foo (f p q)) (foo (g r s))，但只出现在其中一个位置上。我知道有两种方法可以做到这一点，而不必写出所有的p, q...，这可能是复杂的表达式。

• 使用apply (subst mylem)后跟适当数量（此处为 0 或 1）的back命令。
• 使用apply (subst mylem[where a = 'foo x y', standard]), wherex和y是未绑定的名称。

这里的使用subst只是为了演示；我真的很想修改引理，例如，rule当有多个可能的匹配项我想以这种方式消除歧义时使用它。

这两种方法对我来说都是不好的风格。有没有更好的方法来实现这一目标？

如果我的目标状态是foo ==> bar --> qux，我知道我可以使用该语句

让出目标状态foo ==> bar ==> qux。另一个方向呢？哪个命令会让我回到目标状态foo ==> bar --> qux？

到目前为止我想出的最好的是

但这很笨拙，我想知道是否有更好的方法。

假设我有一个关于简单归纳定义集的引理：

（对我来说，保留“⋀x y”位很重要，因为引理实际上是在说明我的证明处于长应用链中间的状态。）

我在开始证明这个引理时遇到了麻烦。我想通过规则归纳来进行。

第一次尝试

我试着写

但这不起作用：该induct方法失败。我发现我可以通过修复x并y明确地解决这个问题，然后调用该induct方法，如下所示：

但是，由于我实际上处于应用链的中间，因此我宁愿不输入结构化证明块。

第二次尝试

我尝试使用该induct_tac方法，但不幸induct_tac的是没有foo.induct以我想要的方式应用该规则。如果我输入

那么第一个子目标是

这不是我想要的：我想要qux x []而不是qux x y. 该induct方法做到了这一点，但还有其他问题，如上所述。