auto for Lean4

Stream: lean4

[Simon Hudon]

@Jannis Limperg I thought I'd respond to you here.

Simon Hudon: I don't know if that's relevant but I have a prototype of Coq-style auto I've been working on, using discrimination tree to index lemmas and combining forward and backward reasoning. I'd be happy to polish it off if that helps

Jannis Limperg: Do publish please! I'm interested in your integration of forward reasoning in particular.

The repo is already published but the version in question is not in master yet. I'll get it merged quickly. What I'm doing for forward reasoning is that some rules that are marked as @[auto] get marked as forward rules for e.g. (p /\ q -> p) when the antecedent is in some sense more complex than the consequent. Then, every iteration starts with a forward reasoning phase to create new assumptions by applying forward rules and next, we check if we can use intro or apply a backward rule (which can include assumptions)

[Jannis Limperg]

Nice, thanks! My tactic supports this style of forward reasoning as well, but it requires more explicit annotations (so you have to say "this should be an elim rule"). What exactly is your heuristic for deciding to make something an elim rule? If it's robust, I could integrate it as well.

[Simon Hudon]

Right now, I'm only calculating the tree size of the antecedent vs consequent and if the consequent is smaller than the antecedent, I label it as a forward rule. I don't have a big number of proofs using it yet so I'm waiting to see how it does over time and how well it plays along with the heuristics for backward reasoning (i.e. starting with the rules with fewer assumptions and with rules that are less general)