Simplify expressions with nested ∃ and an equality

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

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?

Solution

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

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)

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.

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).

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.

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.