Upcoming changes to Aesop forward rules

Stream: lean4

[Jannis Limperg]

@Xavier Généreux and I have been working for some time on a new, much faster implementation of forward reasoning (forward and destruct rules) in Aesop. This is now close to ready for prime-time. The new implementation should be backward-compatible (modulo new bugs), except for three changes. I'd like to hear from users of Aesop's forward reasoning (e.g. @Son Ho) whether you expect these changes to adversely affect your use cases.

1) forward and destruct rules will always use reducible transparency.

This means that the premises of a forward rule will be matched against hypotheses with reducible transparency.

Currently, the transparency is customisable, but by default, hypotheses are matched with default (semireducible) transparency. However, the last premise of each forward rule is indexed in a discrimination tree, so hypotheses are effectively matched against that premise with a weird mixture of reducible and default transparency.

It would be possible to reimplement the old behaviour, but only with substantial effort. Transparency choices other than reducible would also come with a performance hit. (They already do now, but the new implementation relies more on indexing and would therefore suffer comparatively more.)

2) destruct rules will no longer clear non-propositional hypotheses.

Currently, when a destruct rule (n : Nat) -> P n -> Q n is applied to hypotheses m : Nat and h : P m, it clears m and h unless there are other hypotheses in the goal that depend on them.

With the proposed change, the rule only clears matched hypotheses if their types are propositions. So m will remain in the goal, but if P is a proposition, then h will still be cleared.

This change is not really necessary, but I think this behaviour makes more sense, so I'm sneaking it in anyway. :smiling_devil:

3) forward and destruct rules will no longer support custom indexing modes

Currently, custom indexing modes can be specified for forward and destruct rules, using the (imode := ...) builder option. The new implementation uses a different indexing scheme, so this builder option will no longer be available.

[Son Ho]

This makes sense to me. The use of reducible transparency shouldn't be an issue for me, though I will need to test them on my use cases - I'm looking forward to the new version of the forward reasoning.

[Jannis Limperg]

Great, thanks! I'll give you a branch with these changes soon.

[Joachim Breitner]

Jannis Limperg said:

This change is not really necessary, but I think this behaviour makes more sense, so I'm sneaking it in anyway. :smiling_devil:

Just curious why it makes more sense to leave a type like m : Nat in the context when it’s not mentioned anywhere anymore?

[Jannis Limperg]

Throwing away propositions is more easily reversible. For example, if Q n generalises P n and we have the destruct rule forall n, P n -> Q n, then applying this rule loses no information with the new approach. With the old approach, the rule is also reversible if n : Nat (or, generally, if the type of n is inhabited), but it's more cumbersome. Admittedly, I expect this to have about zero impact in practice.

[Jannis Limperg]

There's actually one more change I forgot:

4) Forward rules can now add the same proposition multiple times.

Currently, Aesop tracks which propositions have already been added by forward rules. If a forward rule then attempts to add a prop that was already added by another forward rule, the rule fails and the prop is not added again.

The new system ensures a weaker property: each forward rule is run once for each distinct list of valid inputs. So if we have, for example, the rule r : forall a : α, P a -> Q aand hypotheses x : α, hx : P x, y : α, hy : P y then the rule will be applied once to x and hx and once to y and hy. However, if we additionally have hy' : P y and P is not a Prop, then r will be applied again, resulting in an additional hypothesis of type Q y. And if there is another rule that derives Q x or Q y, this will also result in duplicates.

If this turns out to be troublesome, it wouldn't be too much work to restore the old behaviour, but it would cost a bit of performance.

[Jannis Limperg]

I've backtracked on the last change, so new forward reasoning should now act exactly like old forward reasoning with respect to duplicate hypotheses. We'll see whether this creates performance issues in practice.

[Jannis Limperg]

@Son Ho Aesop's forward-code branch is now ready for testing the new forward reasoning. You should be able to use this instead of master in your lakefile.{lean,toml}. The Aesop version on this branch is intended to be functionally equivalent to Aesop master, except for the changes mentioned above.