[Merged by Bors] - feat(Tactic/Simproc): nested quantifiers in existsAndEq

[vasnesterov]

Generalize the existsAndEq simproc to nested existential quantifiers.

For example ∃ a, p a ∧ ∃ b, a = f b ∧ q b now simplifies to ∃ b, p (f b) ∧ q b.

---

This PR continues the work from #23365.

Original PR: #23365

[vasnesterov]

Comments from Original PR #23365

This section contains 8 comment(s) from the original PR, excluding bot comments.

---

@JovanGerb (2025-03-30 23:56 UTC):
I took the liberty to make some changes myself. Feel free to revert any changes you disagree with.

Qq

• instead of mkEqRefl x, we can assert that $x =Q $y and then usereturn q(rfl).
• We can use Simp.ResultQ directly instead of using a dependent product.

Style

• I think multi line doc-strings should have /-- and -/ on their own line.

Code simplifications

• I split out findEqPath to be called outside of findEq.
• In findEq, I changed the type so it doesn't return an Option, but throws failure immediately.
• in finEq.go, I replaced isDefEqQ with == where we are checking equality with the free variable. And I removed an unnecessary isDefEqQ.
• if p then if q then return x => if p && q then return x
• let x := y; return x => return y
• return ← x => x
• let .some _ := .. => let some _ := ..

---

@JovanGerb (2025-03-31 00:19 UTC):
Some considerations for improving the performance, which aren't very important

Faster failure:

• calling findEqPath before calling Simproc.ofQ and before doing ~q matching would give some speedup.

Faster proof generation:

• The elements of Path could have an additional type for .exists, which could save us from some attempting ~q matches that will be unsuccessful.
• In withExistsElimAlongPathImp, you could also return the proofs of the And nodes, not only the witnesses of the Exists nodes. This would save you the trouble of having to compute them again in mkBeforeToAfter.go.
• In withExistsElimAlongPathImp, you build the list by by snoc-ing it (_ ++ [_]). This would be more efficient using cons (_ :: _) and a List.reverse at the end. But for such small use cases it doesn't matter.

---

@vasnesterov (2025-04-02 11:47 UTC):
Thanks, @JovanGerb!

• I think multi-line docstrings should have /-- and -/ on their own lines.

I don’t mind, but I was taught the opposite in another review.

• In findEq, I changed the type so it no longer returns an Option but throws failure immediately.

I actually tried to distinguish between cases where everything works correctly but the simproc is not applicable (return none) and cases where an assumption in my code is broken (failure). In the latter case, I’d like to throw a user-visible error so we can detect and debug it. What is the common practice for this? Should I just use throwError instead of failure?

• Calling findEqPath before Simproc.ofQ and before performing ~q matching would improve performance.

I don’t think I understand. findEqPath takes the body of the leading quantifier (with a bound fvar variable). How can I call it before matching?

• In withExistsElimAlongPathImp, you build the list by appending elements (_ ++ [_]). Using cons (_ :: _) and reversing the list at the end (List.reverse) would be more efficient. However, for such a small use case, it doesn’t matter.

I think the performance benefits here are too minor to justify complicating the code.

---

@JovanGerb (2025-04-02 12:23 UTC):

• Yes, I seem to have misremembered there being a consensus on how to style multi-line comments
• Yes, I didn't think of it, but using failure is actually a bad idea because it doesn't produce a useful error message. They should instead be throwError "...". Do you agree that if findEqPath succeeds, we should expect the simproc to either succeed or throw an error?
• You can use non-Qq methods to match with the Exists and instantiate the body with a free variable. But I don't know if this saves significant time.
• Agreed

---

@JovanGerb (2025-04-02 22:10 UTC):
I marked it as a pre simproc, so the test with Prod.exists now works as we would want.

---

@JovanGerb (2025-04-07 22:03 UTC):
This looks good to me now, appart from the question of whether the existing existsAndEq should get removed.

---

@JovanGerb (2025-04-08 05:43 UTC):
I think you can avoid changing the noshake file now

---

@grunweg (2025-05-23 09:57 UTC):
Jovan approved this, so let's find a reviewer/maintainer to take a look. @eric-wieser Do you have time to give this a look?

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[JovanGerb]

What is the state of this PR now? From what I remember, I approved it, but it was then also suggested that it should be upstreamed to core (so it should be refactored without Qq).

[vasnesterov]

I thought it may be easier to review the code with Qq, and then refactor it in a separate PR. I'm ready to do it here though.

[grunweg]

I personally think that
(1) this PR can land in mathlib before being upstreamed
(2) a rewriting to avoid qq can happen after this PR has landed
(3) qq should be polished and adopted in core.

But my opinion may be irrelevant here, as I don't speak enough metaprogramming (at the moment) to review this PR anyway.

[vasnesterov]

@grunweg I totally agree

[Vierkantor]

Not for this PR, but: are you also planning to do the equivalent rules for foralls? Rewriting ∀ x, x = a -> P x to P a.

[Vierkantor]

Do I understand correctly that exs are used as the witnesses? Maybe in the example disambiguate between the bound variables in ∃ c b and the free variables in exs = [b, c].

[vasnesterov]

Yes, body depends on free variables f₁, ..., fₙ and in that function we substitute exactly these variables as the witnesses.

[vasnesterov]

Not for this PR, but: are you also planning to add the equivalent rules for foralls? Rewriting ∀ x, x = a -> P x to P a.

This is done by forall_eq. The dual version of this simproc could handle ∀ x, P x ∨ x ≠ a ∨ Q x, rewriting it as P a ∨ Q a.
But it seems less useful to me, and this simproc would also need to trigger on all .forallE expressions (i.e. all dependent arrows), which are very common, so it might slow things down.

[Vierkantor]

Thanks so much for all your work! Let's get this merged 🎉

bors d+

[mathlib-bors]

✌️ vasnesterov can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[vasnesterov]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Post-Build Step
• Lint style