I am investigating a particular bad case of slow unification failure (in both new and old unification). The situation is this: I ask Coq to unify `f a b ~= f a x`

. This fails in first approximation because `b ~!= x`

. Coq reduces `f`

on the LHS to `f' p`

, yielding `f' p a b ~= f a x`

. Coq then asks `f' p ~= f`

, `a ~= a`

, and `b ~= x`

. The first query seems silly but is useful in general when we don't start out with `f .. ~= f ..`

, I assume. However, I am wondering if Coq couldn't be smarter for the other two queries. We have already established that unifying the last two arguments does not lead to success. I see that it is possible that the first new query could, in general, instantiate evars. But in this case it does not and the second and third new query are 100% identical to those we asked before. With any luck they might even be physically equal in OCaml. Is there any way to leverage these particular circumstances?

Unifying has effect at a distance, so you must also check that the third unification problem is stable under state expansion. It might be the case that `f' p ~= f`

extends the state.

The specific situation arises in a development that uses canonical structures (but TC would yield the same result) for syntax overloading. I end up with expressions of the form `a + b + c + d + f + g + h ... + x`

with varying `x`

s (but otherwise identical). Every occurrence of `+`

is a projection and can be reduced at least once. This leads to what I believe to be an exponential blowup of unification queries. Every attempt ultimately fails because of the difference in the last operand. But there are still on the order of 2^n (n being the number of `+`

in the term) combinations for unification to go through. I think it's not quite 2^n because unification always reduces on one side first. Still, it's huge.

I wonder if the second query is actually the problem here. I see that I can only observe this slowdown if `a`

is an evar.

That could of course change the outcome of the third query

Maybe the optimization I am thinking of already exists

Can `?a ~= ?a`

extend the state?

Here's a minimal example. The real example has more reductions in every node and fewer operands but it seems to be the same problem:

```
Structure Op := { op_type : Type; op_op : op_type -> op_type -> op_type }.
Arguments op_op {_}.
Infix "#" := op_op (right associativity, at level 0).
Canonical Op_nat : Op := {|op_type := nat; op_op := Nat.add|}.
Parameter a b c d e f g h i j k : nat.
Goal True.
eassert (forall x y,
a # b # c # d # e # f # g # h # i # j # k # x
=
a # b # c # d # e # f # g # h # i # j # k # y
).
intros.
Timeout 5 apply eq_refl || idtac. (* fails quickly *)
Abort.
Goal True.
eassert (forall x y,
a # b # c # d # e # f # g # h # i # j # k # ?[evar] # x =
a # b # c # d # e # f # g # h # i # j # k # ?evar # y
).
intros.
Timeout 5 apply eq_refl || idtac. (* times out *)
```

I think the "problem" here is that if the terms are ground (evar free) then evarconv calls conversion, which has a similar but not equal heuristic. So you are comparing apples and oranges, unfortunately

Yes, I understand. The comparison is only meant to add some.. dramatic flourish to the last line timing out. :)

I forgot to mention here that I opened https://github.com/coq/coq/issues/14747 to track this.

Coq is not alone in this, BTW. I spent a few minutes to learn just enough lean to see if their unification algorithm suffers from the same problem and it does indeed. (Although it seems to unify things in a different order so I have to use left-associative notation for the operator to trigger this.)

That is probably lean 3, though. Their javascript-based live thingy doesn't actually mention the version.

Pierre-Marie Pédrot said:

Unifying has effect at a distance, so you must also check that the third unification problem is stable under state expansion. It might be the case that

`f' p ~= f`

extends the state.

I keep coming back to this in my mind and it confuses me. Can `f' p ~= f`

really extend the state if `f' p`

is the result of reducing `f`

? I cannot come up with an example where this is true.

on the last line, can record `eta`

expand `?e`

into `Constructor ?e1 ... ?en`

? I agree on `beta`

/`delta`

and haven't checked the other rules.

I don't think it expands evars like that on its own.

Last updated: Oct 16 2021 at 07:02 UTC