Putting information in a goal

Stream: metaprogramming / tactics

[Jason Rute]

Aesop has a feature where you can supply custom rules via docs#Aesop.TacGen (example) added by @Kaiyu Yang. It lets you add rules which are given in text form, making it useful for using AI models to suggest next steps. But there isn't an easy way to pass information forward so that at the next goal, my tactic prediction function can see information from a previous TacGen call. Is there a way to put information in a goal?

One coarse way is to add information to the goal is by using let ___myvar___ := my_data. I'm wondering if there is any cleaner approaches. Maybe hiding information into a hidden local context element or some other useful location linked by the goal metavariable.

[Jason Rute]

It is also very possible that if I just look back one step from TacGen, that it might be that Aesop itself has a nice way to do something like this where I don't even have to hide information in the goal. I'd be more than happy with that.

[Kyle Miller]

Rather than a let, another way is to wrap the target in some metadata.

Or, you could add an implementation detail fvar that somehow encodes the data you want to store.

[Mario Carneiro]

the two standard approaches are either using .mdata (like src#Lean.mkLHSGoalRaw) or an identity function (like src#optParam). You need an identity function if the data you want to store is or contains Exprs

[Jannis Limperg]

Unfortunately all of these approaches suck in different ways when you interact with arbitrary tactics (i.e., you don't control precisely which tactics are applied to your goals):

• There's no guarantee that mdata is preserved by anything. In fact, expressions that differ only in mdata are considered equal by, e.g., caches.
• Custom identity functions may be destroyed by whnf if reducible, or block computation if not.
• implDetail hyps (which are hidden local hypotheses) can be turned into regular hyps by revert-based tactics such as subst, so are not guaranteed to remain hidden except if you put them at the top of the local context (but then they can't depend on anything).
• If you store the data externally somehow and it references local hypotheses (fvars), you have to update the FVarIds because tactics may change the FVarId of an fvar even if the fvar has remained "the same". Some tactics provide FVarSubsts to do this, but others don't.

I've been struggling with this issue since Lean 3 and have yet to see a solution that works well for data with fvars. However, if you don't need to reference fvars, then the mentioned solutions should be fine.

[Eric Rodriguez]

Should there be testing to guarantee that mdata is preserved as expected with tactics? Maybe that's wise to do from now on.

[Jannis Limperg]

There's no such expectation I think; as far as I know, not even core reliably preserves mdata. So it can only be used for heuristic stuff, e.g. pretty-printing (where it's not so important whether the heuristic fires), or when you can precisely control what happens with your expressions.