Stream: Mtac2

Topic: Unification types

view this post on Zulip Michael Soegtrop (Sep 07 2020 at 07:54):

Is there some documentation for the different unification types defined in pattern.v, namely

=> UniMatch
=n> UniMatchNoRed
=u> UniCoq
=c> UniEvarConv

I can imagine what UniMatchNoRed does - I guess it behaves similar to a match in Ltac1 - but the difference between the others is not obvious from the name.

There is a lot of other syntax in pattern.v which I am convinced serves some very useful purpose, but it is really hard to tell which.

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:12):

Maybe they use unification (apply:)/tactic unification (apply) / unicoq unification?

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:12):

EvarConv is one of the unification algorithms, after all.

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:13):

(IIRC it’s the one in ssreflect, but this zulip has authoritative answers)

view this post on Zulip Paolo Giarrusso (Sep 07 2020 at 10:13):

https://mattermost.mpi-sws.org/iris/pl/hd1pguiz1bbdxgnkq99qswrixo and discussion around seems to confirm your guess for UniMatchNoRed.

view this post on Zulip Janno (Sep 07 2020 at 11:32):

Sorry, forgot to reply to this thread. @Beta Ziliani is the expert but my current understanding is this: *Match* implies that the pattern will not try to instantiate evars in the value it is compared against. The two different Match differ in how much reduction they perform in the value (but they never reduce in the pattern, IIRC.). UniCoq is full unification with the unicoq algorithm, including reduction and evar instantiation on both sides (pattern and value). UniEvarconv is the same but with Coq's own unification algorithm.

view this post on Zulip Beta Ziliani (Sep 07 2020 at 13:33):

this is correct

Last updated: Feb 06 2023 at 05:03 UTC