spaceloop (Apr 17 2023 at 10:36): spaceloop (Apr 17 2023 at 10:36):Hi, I'm trying to use the Debug Unification flag, but setting it does not give me any additional output beside the usual unification error. Fo rexample:
Set Debug Unification.
Goal forall x y z : nat, x + y = y + z -> x = z.
intros x y z H.
Fail rewrite H.
I just get
The command has indeed failed with message:
Found no subterm matching "x + y" in the current goal.
Using coq 8.13.2 and the Coqtail plugin for Vim.
Paolo Giarrusso (Apr 17 2023 at 11:03):probably, you also want Set Debug Tactic Unification.
Paolo Giarrusso (Apr 17 2023 at 11:05):because Coq has two unification algorithms, and they have separate debug flags
spaceloop (Apr 17 2023 at 11:58):Thanks! That worked :)
spaceloop (Apr 17 2023 at 12:15):Although it doesn't give me much helpful information. How can I use the other unificaiton/debug algorithm? Perhaps that has better output. Basically, I'm interested in finding which sub-term does not unify in two (large) terms that do not unify.
spaceloop (Apr 17 2023 at 12:18):Ah I'm sorry, it seems to give much more detailed debugging output when I use rewrite instead of apply, I was doing the latter. I will first investigate this debugging output :) If there are any other ways of easily finding which sub-terms cause unification failure, I'd be happy to know about those
Paolo Giarrusso (Apr 17 2023 at 15:42):with Require Import ssreflect you'll get a rewrite tactic that uses the other unification algorithm (and has a million other differences, typically for the better)
Last updated: Apr 20 2024 at 00:02 UTC