Stream: Coq devs & plugin devs

Topic: Unification and futile queries after a step of reduction

Janno (Aug 05 2021 at 13:41):

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?

Pierre-Marie Pédrot (Aug 05 2021 at 13:49):

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.

Janno (Aug 05 2021 at 13:49):

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 xs (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.

Janno (Aug 05 2021 at 13:52):

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.

Janno (Aug 05 2021 at 13:52):

That could of course change the outcome of the third query

Janno (Aug 05 2021 at 13:53):

Maybe the optimization I am thinking of already exists

Janno (Aug 05 2021 at 13:55):

Can ?a ~= ?a extend the state?

Janno (Aug 05 2021 at 14:35):

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 *)

Enrico Tassi (Aug 06 2021 at 13:15):

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

Janno (Aug 06 2021 at 13:24):

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

Janno (Aug 06 2021 at 13:27):

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

Janno (Aug 06 2021 at 13:32):

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.)

Janno (Aug 06 2021 at 13:35):

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

Janno (Aug 06 2021 at 14:29):

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.

Paolo Giarrusso (Aug 06 2021 at 15:17):

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.

Janno (Aug 09 2021 at 07:53):

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

Last updated: Apr 19 2024 at 14:02 UTC