UnificationProblems
This page is for collecting unification problems which Coq (or UniCoq) are not able to solve (yet).
This example is a simplification of a realistic example about proving properties of the composition of morphisms of monoids:
Axiom H : forall {a b : nat * unit}, fst a = fst b -> a = b.
Lemma lem1 (a : nat) (x y:unit) : (a, x) = (a, y).
Fail apply (H eq_refl).
Fail refine (H eq_refl).
(* fails, because "fst a ≡ fst b" entails too eagerly that "a ≡ b" w/o possibility of backtracking/postponing *)Bug #1214 shows a failure in unifying (if ?b then true else false) = ?b) ≡ (true = true). Contrastingly, ?b = if ?b then true else false)) ≡ (true = true) works.
Bug #8357 also shows a missing ability to backtrack/postpone in heuristically reducing cst args1 ≡ cst args2 into args1 ≡ args2 when cst is unfoldable (e.g. a projection). See this comment.
Backtracking is local to a given call to unification. If it locally works but happens to be later incompatible with a later call to unification on another problem, ability to backtrack is lost. See the example of a non-recoverable wrongly resolved f ?X ≡ f t problem with f unfoldable in PR #8357.
There is a pretty common pattern where an argument of an existential variable is a tuple of which components can be projected.
See e.g. Bug #5264 and Bug #3126 (or, more distantly, Bug #3823):
Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
intros T1 P1 H1.
eexists ?[x].
destruct H1 as [x1 H1].
Fail apply H1.
instantiate (x:=projT1 H1).
apply H1.Indeed, the first apply H1 has to solve ?x[H1:=existT P1 x1 H1] ≡ x1 which it could do by projecting x1 but it is not (yet) able to do it.
It is common to have unification problems of the form negb ?b = true or INR ?n = 2 (see Coq-club, 12 Nov 2016) which are canonically solvable, or even ifzero ?n = false or match ?n with 0 | 1 -> true | _ -> false end which are refinable (using candidates for the second one).
The price to pay is to reduce the problem to filtering on a disjunction of subproblems. So we shall need heuristics to control the risk of combinatorial explosion. Maybe by attaching subproblems to candidates?
In the following example submitted at #7078:
Inductive foo (n : nat) : nat -> Type := bar (_ : foo n n) : foo n n.
Fail Check fix a m (v : foo ?[n] m) := match v in foo _ m' return foo ?[p] m' with @bar _ v' => a ?[q] v' end.the resulting equation ?p@{m:=?q@{m:=m}; m':=?q@{m:=m}} == ?p@{m:=m; m':=?q@{m:=m}} can be resolved by following two disjoint paths: either restricting ?p to not use m, or instantiating ?q to be m. One would need a way to turn this equation into a disjunction so that the unification algorithm could continue to process without being blocked on the equation.
Let us consider the following successful problems:
Import EqNotations.
Check fun x y (a : x = y) (b : x = 0) => rew [fun z => z = 0] a in b : (y = 0). (* 1 *)
Check fun x (a : x = 0) (b : x = 0) => rew [fun z => z = 0] a in b : (0 = 0). (* 2 *)
Check fun y (a : 0 = y) (b : 0 = 0) => rew [fun z => z = 0] a in b : (y = 0). (* 3 *)
Check fun x y (a : S x = y) (b : S x = 0) => rew [fun z => z = 0] a in b : (y = 0). (* 4 *)
Check fun y (a : S 0 = y) (b : S 0 = 0) => rew [fun z => z = 0] a in b : (y = 0). (* 5 *)
Check fun x y (a : x = S y) (b : x = 0) => rew [fun z => z = 0] a in b : (S y = 0). (* 6 *)
Check fun x (a : x = S 0) (b : x = 0) => rew [fun z => z = 0] a in b : (S 0 = 0). (* 7 *)
Check fun x y (a : S x = S y) (b : S x = 0) => rew [fun z => z = 0] a in b : (S y = 0). (* 8 *)
Check fun y (a : S 0 = S y) (b : S 0 = 0) => rew [fun z => z = 0] a in b : (S y = 0). (* 9 *)
Check fun x (a : S x = S 0) (b : S x = 0) => rew [fun z => z = 0] a in b : (S 0 = 0). (* 10 *)Let us add the following successful problem, derived from a realistic situation.
Check fun x (a : fst x = 0) (b : fst x = 0) => rew [fun z => z = 0] a in b : (0 = 0). (* 11 *)In cases 1 to 7 and 11, there is a unique solution which is not found.
Import EqNotations.
Fail Check fun x y (a : x = y) (b : x = 0) => rew a in b : (y = 0).
Fail Check fun x (a : x = 0) (b : x = 0) => rew a in b : (0 = 0).
Fail Check fun y (a : 0 = y) (b : 0 = 0) => rew a in b : (y = 0).
Fail Check fun x y (a : S x = y) (b : S x = 0) => rew a in b : (y = 0).
Fail Check fun y (a : S 0 = y) (b : S 0 = 0) => rew a in b : (y = 0).
Fail Check fun x y (a : x = S y) (b : x = 0) => rew a in b : (S y = 0).
Fail Check fun x (a : x = S 0) (b : x = 0) => rew a in b : (S 0 = 0).
Fail Check fun x (a : fst x = 0) (b : fst x = 0) => rew a in b : (0 = 0).Indeed the problems are conjunctions of equations of the form ?P[x:=x,y:=y] t ≡ t = 0 and ?P[x:=x,y:=y] u ≡ u = 0 with t and u not unifiable and one of t or u neutral, i.e. an eliminated variable, an eliminated axiom, an inductive type, or a sort. The solution is unique, since t and u are in rigid position.
Assuming t, u and the right-hand sides in normal form, these are flexible/rigid problems canonically solvable by imitation (assuming none of t or u start with =, until obtaining ?P'[x:=x,y:=y] t ≡ t and ?P'[x:=x,y:=y] u ≡ u (and possibly extra equations if t or u is 0. Let us assume that it is t which is neutral. One can then use candidates to express that ?P' has two solutions for the first equation (namely ?P'[x:=x,y:=y] z := z or ?P'[x:=x,y:=y] z := t (t being assumed to have only x and y as free variables). The second equation now ensures that only the first solution is acceptable.
If t and u are not in normal form, should we head-normalize them, something that is done in the first-order unification heuristic and which does not seem inducing efficiency penalty in practice?
As for problems 8 to 10, which do not have a unique solution as they can also be solved e.g. using ?P := fun z => S (pred z) = 0, a heuristic could still be used as discussed in the next section.
In some sense, Coq's exitential variables have two levels of instance: the instance of the existential variable properly speaking and the arguments applied to the existential variables. For example, in context
x:nat
H:forall y (P:nat->Prop), P y -> True
p:x=0the term
H x ?[P] pgenerates the problem (?P[x:=x] x) ≡ (x=0) where ?P depends on x both because it is declared in the context containing x and because it is applied to x. The two solutions of the equation do not seem to have same value. The dependency on the applied x seems more expected than the other one and one might find the solution ?P[x] := fun x => x=0 more intuitive.
This is what happens with the first-order unification heuristic. If we had to solve (?P[x:=x] x) ≡ Q x), one would find ok that ?P is defined to be Q, i.e. fun x => Q x even though another solution is fun _ => Q x.
So, why not to solve (?P[x:=x] x) ≡ (x=0) the same way, giving priority to the purposely applied x over the x which is in the context by default.
Here is an example which is not solved with b : x = 0 while it would be if we had b : 0 = x, thanks to the first-order heuristic:
Import EqNotations.
Check fun x (a : x = 0) (b : x = 0) => rew a in b.
(* Problem is "(?P[x:=x] x) ≡ (x = 0)" *)Drawbacks: abstracting over all occurrences, especially in the presence of closed subterms is maybe too strong. In
Check fun x (a : 0 = x) (b : 0 = 0) => rew a in b.Do we really want to infer P[x] := fun y => y = y, or do we want to consider that P[x] := fun y => y = 0 or P[x] := fun y => 0 = y are equally good?
Extending the first-order unification heuristic into a Libal-Miller functions-as-constructors heuristic
This example is a simplification of a realistic example. It is similar to the one in the previous section but using functions-as-constructors extended pattern-unification rather than basic pattern-unification:
Check fun x (a : S x = 0) (b : S (S x) = 0) => rew a in b.
(* Problem is "(?P[x:=x] (S x)) ≡ (S (S x) = 0)" *)To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.