Difference between DiscrTree.getMatch and DiscrTree.getUnify

Stream: lean4

[Michael Sammler]

Hi, I am trying to understand how to use DiscrTree and it seems that simp uses getMatch while typeclass inference uses getUnify. I had a hard time understand what the difference between the two since I did not see documentation for them and the code a bit too tricky for me to understand. Does someone have an intuition what the difference between the two is and when to use which?

[Notification Bot]

This topic was moved here from #new members > Difference between DiscrTree.getMatch and DiscrTree.getUnify by Kyle Miller.

[Jannis Limperg]

I think getUnify may assign metavariables in the expression being matched against while getMatch may not. But I'm not sure.

[Jovan Gerbscheid]

Indeed, there are two ways to match with a DiscrTree: unifying, or just matching. Type class search needs to unify, because its target may have metavariables that it wants to unify (due to outParams). On the other hand simp doesn't want to instantiate metavariables in the expression that is being simplified.

[Michael Sammler]

That helps for knowing when to use which, thanks! Thought I have to admit I still don't really understand how it works. From what I see, the DiscrTree does not instantiate metavariables itself (which would be weird anyway if there are multiple matches), but getUnify treats .star differently from getMatch.

[Jovan Gerbscheid]

Yes, DiscrTree doesn't actually do the unification. Rather, it gives a list of results that probably unify with the target. Then these results should be attempted one by one with unification, i.e. isDefEq.

Thus, DiscrTree works as a first filter that limits the amount of expressions that we have to try to unify.

[Jovan Gerbscheid]

When using getMatch (which is most use cases), you need the function to be wrapped in a withNewMCtxDepth, to avoid instantiating the metavariables in the matched expression.