feat(logic/basic): Push forall binders inside implications

[eric-wieser]

---

This causes a deterministic timeout at

mathlib/src/data/set/basic.lean

Lines 454 to 455 in 3419986

	@[simp] theorem union_subset_iff {s t u : set α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u :=
	by finish [iff_def, subset_def]

It's possible this fails because of the finish approach of

bring universal quantifiers to the outside (for ematching).

Which seems like the opposite of what this simp rule does.

[jcommelin]

@eric-wieser I can't put a finger on it, but for what it's worth, my intuition would also simp in the reverse direction of what you do in this PR.

[eric-wieser]

I think my motivation here was to allow the simplification

• (∀ a b c, f a = b → g b = c → p c) ↔ p (g (f a))
• (∀ a b, f a = b → ∀ c, g b = c → p c) ↔ p (g (f a)) (by forall_imp_indep in this PR)
• (∀ c, g (f a) = c → p c) ↔ p (g (f a)) (by forall_apply_eq_iff)
• p (g (f a)) ↔ p (g (f a)) (by forall_apply_eq_iff)
• true (by refl)

I don't have any particular motivation for needing this, but it seemed like it would be a neat thing for simp to do.

[jcommelin]

I agree that it's a nice showcase... maybe it can be made to work?

@digama0 @cipher1024 Does finish call simp under the hood?

[digama0]

I tried a similar thing for \ex x, a = x /\ p x <-> p a, but it's not reliable in general. We need a simp-proc or other tactic to search and destroy this particular pattern (generalized to the n-ary case). I don't think it is a good idea for this to be a simp lemma. (We already have the unary version as a simp lemma but the reorganizing can't be done properly by simp so it's not reliable in larger cases.)

[sgouezel]

Time to point to https://github.com/johoelzl/lean-simp-loop (which never made it into production, but should be kept in mind for Lean4)

[eric-wieser]

I tried a similar thing for \ex x, a = x /\ p x <-> p a, but it's not reliable in general.

What you're describing sounds more similar to the already-merged forall_apply_eq_iff, rather than to forall_imp_indep which contains no substitutions.

[digama0]

Right, you need a combination of both lemmas to simplify more complicated expressions like \forall x y z, y = f x -> p x y z to \forall x z, p x (f x) z. But forall_imp_indep is not a good simp lemma, in the sense that simp doesn't know how to reorder pis to to move the equality closer to the variable to eliminate, so for this use case a tactic with a bit more smarts is needed. For other uses of forall_imp_indep, as Johan says this isn't clearly the better direction, so I would prefer that we explicitly simp with it or its inverse as needed.

[robertylewis]

I'm in the process of doing a scattershot cleanup of old PRs, and it looks like this is (1) small and (2) unlikely to be merged, so I'll close. Feel free to reopen if there's more to discuss.