Aesop and cases

Stream: mathlib4

[Scott Morrison]

@Jannis Limperg, a feature request for aesop.

I've like an analogue of introsTransparency? but for aesop_destruct_products. Do you think this would be viable? This would be helpful for recovering some missing functionality from obviously.

In particular, I would like both of the following to succeed:

example (h :{ x : Unit // False}) : False := by aesop -- succeeds
def T := { x : Unit // False}
example (h : T) : False := by aesop -- fails

[Scott Morrison]

(This is what is causing the first failure of aesop_cat in !4#2815, and possibly also many of the aesop vs obviously regressions in the category theory library that I am way behind on. :-)

[Scott Morrison]

And on a separate PR, https://github.com/leanprover-community/mathlib4/pull/2296, trying to replace obviously by aesop is failing for the same reason: obviously could do cases on an empty hypothesis, that aesop isn't willing to see.

[Jannis Limperg]

This can certainly be done. I'll look at it as soon as I've repaired my Emacs installation.

[Jannis Limperg]

Actually, it would kill the indexing for destructProducts (and perhaps cases etc.) since that only works with reducible transparency. But I guess that's a tradeoff you'll be willing to make. The alternative would be to register explicit cases or unfold rules for types like T.

[Scott Morrison]

I'd prefer not to have to add explicit rules. The users of the category theory library shouldn't have to reconfigure aesop when they define new type synyonyms when setting up new category instances.

[Scott Morrison]

So yes, I understand there would be a performance trade-off here. :-(

[Jannis Limperg]

On it. It's a bit more work than I thought, but not terribly much.

[Jannis Limperg]

I may have overengineered this a tiny bit. In addition to destructProductsTransparency, there are now also transparency options for the other builtin rules and for the rule builders (where it makes sense to change the transparency). So you can specify that, e.g., a specific apply rule should be applied at reducible transparency. !4#3501 is the bump PR.