嵌套∃和平等的简化表述

Question

我碰到一个证明来了，我不能轻松地自动直到我把这个引理成伊莎贝尔的简化器设置：

lemma ex_ex_eq_hint: 
    "(∃x. (∃xs ys. x = f xs ys ∧ P xs ys) ∧ Q x) ⟷ 
    (∃xs ys. Q (f xs ys) ∧ P xs ys)" 
    by auto 

现在我想知道：是否有一个很好的理由简化器或古典推理器不能一般地自动执行这种简化？有没有更多的这个引理的一般形式，可以添加到默认的simpset来实现这一点？

Answer 1

在Isabelle2015中，简化器知道许多规则来消除由等式确定的存在性约束变量。对于你的情况下，相关的有simp_thms(36-40)：

• (∃x. ?P) ⟷ ?P
• ∃x. x = ?t
• ∃x. ?t = x
• (∃x. x = ?t ∧ ?P x) ⟷ ?P ?t
• (∃x. ?t = x ∧ ?P x) ⟷ ?P ?t

此外，ex_simps(1-2)推existentials成合取如果一方不不是离子结合的变量：

• (∃x. ?P x ∧ ?Q) ⟷ (∃x. ?P x) ∧ ?Q
• (∃x. ?P ∧ ?Q x) ⟷ ?P ∧ (∃x. ?Q x)

在许多情况下，这些规则是足够的，以消除存在量词。然而，在你的情况下，还存在xs和ys之间的其他存在量词。原则上，上述规则和ex_comm即(∃x y. ?P x y) ⟷ (∃y x. ?P x y)（以及op &的关联性，无论如何都是默认的简单规则）就足以通过重写来证明您的引理。然而，人们必须将存在的从中拉出来，然后对量词进行排列，使得x被绑定在最内层。在一般情况下，这些步骤都不是需要的。而且，交换性也受到伊莎贝尔的术语顺序的限制，所以简化器甚至可能不会采用这种方式。

因此，这个问题一般不能用一组有限的重写规则来解决，因为可能有任意多的量词嵌套。然而，它可以通过一个简化形式来解决，该简单形式在存在量词上触发并且搜索量化的谓语词以得到被绑定变量的平等。如果平等出现在可以消除存在的位置，那么它必须在现场制定适当的重写规则（转换可能对此有用）。

但是，simproc应该确保它不会过多地干扰目标的结构。在你的例子中已经可以看到一些这样的干扰。在左侧，谓词Q不在内部量词的范围内，但它在右侧。

这意味着在所有情况下这种转换是不可取的。例如，在左边，auto,fastforce等所使用的古典推理可以归入一个存在量词，然后使用经典推理通过分析Q来找到x的实例。这可能导致进一步简化等于x = f xs ys，这可能导致进一步的实例化。相反，在右侧，推理者首先必须为存在量词引入两个原理变量，然后才能开始查看Q。

总之，我建议你分析一下你的设置，看看为什么这种形式的量词嵌套在目标状态下完全发生。也许你可以对它进行调整，使得一切都可以与现有规则配合使用。