should aesop unfold semireducible definitions?

Stream: mathlib4

[Floris van Doorn]

I would like to start a discussion whether aesop should unfold semireducible definitions. I think it shouldn't (by default), and wrote this in an RFC aesop#146. I am reposting here for more visibility.

I don't use aesop myself all that much, so others with more experience might have a different view than I do, but below is my viewpoint.

I think aesop (and all other automation) should apply lemmas up to instances transparency by default. Otherwise, I don't think it is possible to make performant automation.
It is unreasonable to expect automation to be quick if it can unfold almost any definitions, and experimentally, sometimes apply ... takes seconds to fail (even if the lemma "obviously" doesn't apply). Sure, in those cases we could do better in Mathlib, marking more things irreducible, but we cannot only fix in on Mathlib's side.

My experience is that aesop is often very slow, and there have been multiple PRs to Mathlib moving away from aesop because of performance reasons: 1 2 3 4. I am assuming this is because of the transparency of apply rules, but maybe I'm wrong there.

This will lead to a regression in capabilities of aesop and we will need to mark more things as unfoldable by aesop. Maybe specialized tactics like aesop_cat can work up to semireducible transparency.

I already talked to @Jannis Limperg about this in person, but I never wrote up the suggestion on Zulip/Github.

[Matthew Ballard]

In principle, I agree. Is it as simple as sprinkling a few withReducibleAndInstances? (Before the fallout)

[Matthew Ballard]

Re aesop_cat: this replacement is also happening there as @Kevin Buzzard has experienced

[Matthew Ballard]

Proofs change to ext; simp or just rfl and speed up geometrically which comports with transparency being the difference

[Jannis Limperg]

I'm not opposed to this at all. I think design-wise it would make a lot of sense for all 'automation' tactics (which is a bit of an ill-defined category, but probably clear enough in practice) to standardise on one transparency.

I'm not clear on whether this transparency should be instances or reducible. At the moment, Aesop's indexing is up to reducible transparency, but when indexing succeeds, the rules are run at default transparency. I'm not sure whether the DiscrTree supports instances transparency, but I guess it should.

Aesop already allows the transparencies of all rules to be adjusted, so it would be fairly easy to check how much of Mathlib breaks at different transparency settings.

With all that said, the slowness in the linked PRs does not seem to be caused by the transparency of apply. One of the PRs effectively replaces simp_all (run by Aesop) with simp_all only [...]. The other three replace aesop-based continuity with fun_prop. The latter has three advantages:

• It uses a discrimination tree that efficiently supports some fragment of higher-order unification. This is useful because all continuity goals are higher-order since the goal contains a function. Core's discrimination tree, which Aesop uses, makes no attempt at higher-order unification, so for a goal Continuous f it returns every lemma with conclusion Continuous _ as a possible match, regardless of the shape of f. As a result, continuity rules are effectively unindexed. However, it's not clear to me whether the fun_prop discrimination tree preserves the completeness of indexing; that's why I never switched to it. (cc @Jovan Gerbscheid)
• aesop runs a lot of built-in rules which are unlikely to be useful for continuity. In particular, it frequently simps intermediate goals, which is very costly. It would be easy to disable these built-in rules in continuity, at the cost of some inevitable breakage.
• fun_prop is restricted to lemmas of particular shapes, which gives it more optimisation opportunities. I've never looked into this in detail, though.

When Aesop is slow, my first guess would be that its repeated simp calls are the cause. A student of mine is currently working towards better caching of simp in Aesop, but it's hard.

[Jovan Gerbscheid]

Discrimination trees index up to reducible transparency. I think it makes little difference with the instances transparency, because instance arguments are always indexed with a star (so they are ignored).

[Jovan Gerbscheid]

I presume that with completeness you mean that whenever two terms unify in reducible transparency, then they will unify in the discrimination tree. I think if core's DiscrTree has this, then my RefinedDiscrTree should as well.

[Matthew Ballard]

I thought the instance projections were intentionally not unfolded for indexing the keys

[Matthew Ballard]

When Aesop is slow, my first guess would be that its repeated simp calls are the cause.

This is also something that is problematic in the library due to statements with very weak keys

[Jovan Gerbscheid]

Matthew Ballard said:

I thought the instance projections were intentionally not unfolded for indexing the keys

For example + is an instance projection function. You don't want this to unfold to the specific definition of addition, because you want it to match with the general lemma add_comm.

[Matthew Ballard]

Right, perhaps I misunderstood what you said

[Jovan Gerbscheid]

No, I didn't say it right at first

[Jireh Loreaux]

Jannis Limperg said:

When Aesop is slow, my first guess would be that its repeated simp calls are the cause

I recently came across this, where a single simp_all call by aesop caused several seconds worth of slowness, but simp solved the goal immediately. (the context was only moderately sized, not enormous)

[Floris van Doorn]

Ok, maybe my assumption that aesop is mostly slow because of slow apply statements is wrong, and it's mostly simp that is slow (I've had some cases where simp was instantaneous but aesop timed out, but I didn't try simp_all).

[Floris van Doorn]

I'm not clear on whether this transparency should be instances or reducible. At the moment, Aesop's indexing is up to reducible transparency, but when indexing succeeds, the rules are run at default transparency. I'm not sure whether the DiscrTree supports instances transparency, but I guess it should.

This surprises me a little. Indexing is up to reducible, and instance arguments are part of the key in a discrimination tree? I would imagine that would stifle simp, since I would imagine that in the presence if diamonds you need to unfold instances to see whether a lemma applies (even at the matching stage).

[Jannis Limperg]

Jovan Gerbscheid said:

I presume that with completeness you mean that whenever two terms unify in reducible transparency, then they will unify in the discrimination tree. I think if core's DiscrTree has this, then my RefinedDiscrTree should as well.

Yes. More formally, if t and u unify at reducible transparency, and the mapping t -> v was added to the RefinedDiscrTree T, then T.getUnify u should return v. You think this holds?

[Jannis Limperg]

I'm interested in this simp vs aesop business. If you come across any examples where simp is fast but aesop is slow, I'd like to hear about them. Bonus points if simp_all is also fast because then it's definitely Aesop's 'fault'.

[Jannis Limperg]

Btw, set_option trace.aesop.stats in aesop reports how much time was spent executing each rule (cumulatively) in an Aesop call. You can also set_option aesop.collectStats true at the start of a file and then #aesop_stats at the end to get aggregate stats for all Aesop calls in that file. (Also works for multiple files.)

[Jovan Gerbscheid]

Floris van Doorn said:

Indexing is up to reducible, and instance arguments are part of the key in a discrimination tree?

Instance arguments are ignored (they are indexed as a star) in the key in a discrimination tree. So the discrimination tree doesn't check whether the instance is correct.

[Jovan Gerbscheid]

Jannis Limperg said:

Yes. More formally, if t and u unify at reducible transparency, and the mapping t -> v was added to the RefinedDiscrTree T, then T.getUnify u should return v. You think this holds?

I think in RefinedDiscrTree it does hold for getMatch, and not for getUnify. There are some edge cases with metavariables where getUnify fails to find a unifying key, due to how RefinedDiscrTree gives metavariables an index. I think this could be fixed, but the majority of use cases (such as simp) use getMatch anyways.

Another case where completeness doesn't hold is that you can manually pass a WhnfCoreConfig, which allows you to disable certain reductions, but that is the sane in core's DiscrTree.

[Floris van Doorn]

Jovan Gerbscheid said:

Instance arguments are ignored (they are indexed as a star) in the key in a discrimination tree. So the discrimination tree doesn't check whether the instance is correct.

Ok, thanks! Then it should have very little difference to match up to reducible eq or instance eq, and the only question is the reducibility of unification after finding a match.

[Jovan Gerbscheid]

For the rw?? tactic, I need to use the reducible setting, because that is what rw uses. I would guess simp also uses that, but I don't know. I think isDefEq at reducible transparency can change the transparency setting for instance arguments, so that the instance arguments can still be unified.