Skip to main content

Questions tagged [unification]

Unification is a technique used in the implementation of proof assistants for purposes including solving of metavariables and resolution of type classes.

Filter by
Sorted by
Tagged with
1 vote
2 answers
287 views

How can I generate equalities from an application in Coq?

When I try to apply a lemma or constructor in Coq, I often run into the situation where lemma doesn't unify exactly with goal I'm working on, even though I know it could be rewritten to match. For ...
Matt's user avatar
  • 19
3 votes
1 answer
60 views

Coq: Unify with a pattern and get the result

I want to do change t with (f _), where t is a term and f is a function, but ...
Qinshi Wang's user avatar
1 vote
2 answers
138 views

Destruction of unification problem on application

Suppose I have a unification problem a b = f u Where f is neutral and u is WHNF and ...
ice1000's user avatar
  • 6,256
5 votes
0 answers
111 views

Can we bring unification results under cofibrations outside?

Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do ...
ice1000's user avatar
  • 6,256
6 votes
0 answers
80 views

What are Generic Arguments in Coq and how are they structured in their OCaml code?

I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
Charlie Parker's user avatar
3 votes
0 answers
66 views

SSReflect tuple constructor: why not use phantom?

I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
wdeweijer's user avatar
7 votes
1 answer
132 views

Tactic unification vs evarconv in Coq

I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a ...
James Wood's user avatar
  • 1,053