用嵌套的∃和等式简化表达式 [英] Simplify expressions with nested ∃ and an equality

问题描述

我遇到了一个证明，直到将这个引理投入到Isabelle的简化器集中之后，我才能轻易实现自动化:

I came across a proof that I could not easily automate until I threw this lemma into Isabelle’s simplifier set:

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中以实现此目的?

Now I am wondering: Is there a good reason why the simplifier or the classical reasoner is not able perform this simplification in general and automatically? Is there a more general form of this lemma that could be added to the default simpset to achieve this?

推荐答案

在Isabelle2015中，简化程序知道许多规则，这些规则可以消除由相等性确定的存在性绑定的变量.对于您的情况，相关的是simp_thms(36-40):

In Isabelle2015, the simplifier knows a number of rules to eliminate existentially bound variables which are determined by equality. For your case, the relevant ones are 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

• (∃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)会将存在性推送到合取物中.

Additionally, ex_simps(1-2) push existentials into conjuncts if one side does not mention the bound variable:

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

• (∃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绑定在最内层.在一般情况下，这些步骤都不是可取的.此外，可交换性受Isabelle的术语顺序约束，因此简化程序甚至可能不会按预期方式应用它.

In many cases, these rules suffice to eliminate the existential quantifier. In your case, however, there are further existential quantifiers for xs and ys in between. In principle, the above rules and ex_comm, i.e., (∃x y. ?P x y) ⟷ (∃y x. ?P x y) (and associativity of op &, but that's a default simp rule anyway), suffice to prove your lemma by rewriting. However, one would have to pull the existentials out of the conjuncts and then permute the quantifiers such that x is bound innermost. None of these steps is desireable in the general case. Moreover,commutativity is subject to Isabelle's term order, so the simplifier might not even apply it in the indended way.

因此，此问题通常无法通过一组有限的重写规则来解决，因为可能有许多嵌套的量词.但是，这可以通过一个simproc解决，该simproc触发存在量词，并在量化的谓词项中搜索绑定变量的相等性.如果相等出现在可以消除存在的位置上，则必须当场产生适当的重写规则(转换可能对此有用).

Thus, this problem cannot be solved in general by a finite set of rewrite rules, because there may be arbitrarily many nestings of quantifiers. It could, however, be solved by a simproc which triggers on existential quantifiers and searches the quantified predicate term for an equality of the bound variable. If the equality appears in a position such that the existential can be eliminated, then it has to produce the appropriate rewrite rule on the spot (conversions might be useful for that).

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

However, the simproc should make sure that it does not disturb the structure of the goal too much. Some of such disturbance can already be seen in your example. On the left hand side, the predicate Q is not in the scope of the inner quantifiers, but it is on the right-hand side.

这意味着尚不清楚在所有情况下是否都需要此转换.例如，在左侧，auto，fastforce等使用的经典推理器可以进入一个存在量词下，然后使用经典推理通过分析Q来找到x的实例化.这可能导致等式x = f xs ys的进一步简化，这可能导致进一步的实例化.相反，在右侧，推理者必须首先为存在量词引入两个示意图变量，然后才能开始查看Q.

This means that it is not clear that this transformation is desirable in all cases. For example, on the left-hand side, the classical reasoner used by auto, fastforce, etc. can go under one existential quantifier and then use classical reasoning to find an instantiation for x by analysing Q. This may lead to further simplifications of the equality x = f xs ys, which can lead to further instantiations. In contrast, on the right-hand side, the reasoner first has to introduce two schematic variables for existential quantifiers before it can even start to look at Q.

因此，总而言之，我建议您分析您的设置，以了解为什么这种形式的量词嵌套是在目标状态下发生的.也许您可以对其进行调整，以使所有内容都与现有规则集兼容.

So in summary, I recommend that you analyse your setup to see why this form of quantifier nesting has occured at all in a goal state. Maybe you can adjust it such that everything works with the existing set of rules.

这篇关于用嵌套的∃和等式简化表达式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！