Stream: Coq users

Topic: How to use debug flag?


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Apr 17 2023 at 11:03):

probably, you also want Set Debug Tactic Unification.

view this post on Zulip Paolo Giarrusso (Apr 17 2023 at 11:05):

because Coq has two unification algorithms, and they have separate debug flags

view this post on Zulip spaceloop (Apr 17 2023 at 11:58):

Thanks! That worked :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Jun 25 2024 at 15:02 UTC