Stream: Coq users

Topic: Can't get congruence error message


view this post on Zulip Kyle Ehrlich (Dec 07 2020 at 23:43):

I'm looking at the congruence paper and it gives this example for

Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube.

Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c.
Proof.
 congruence.
Qed.

according to the paper (and the coq documentation for congruence) I should get the error message Goal is solvable by congruence but some arguments are missing.Try "congruence with (Triple a?1?2) (Triple d c?3)",replacing meta variables by arbitrary terms. but I simply get "congruence failed" is there some verbosity option I am missing, or is something else causing these error messages not to happen as specified.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 01:36):

"the congruence paper"? I've never seen anything but "congruence failed" — so I think error's not on your part

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 01:39):

I see how to solve this goal, but this seems pretty artificial, so I see why somebody would drop support for it from congruence.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 01:42):

OTOH, https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:tacv.congruence-with and https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:exn.goal-is-solvable-by-congruence-but-some-arguments-are-missing-try-congruence-with-term-term-replacing-metavariables-by-arbitrary-terms are so hopelessly vague that I can't tell what they mean.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 01:43):

maybe try Set Congruence Verbose?

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 01:43):

the docs has no examples using congruence with, so ultimately clueless.

view this post on Zulip Paolo Giarrusso (Dec 08 2020 at 01:44):

Paging @Pierre Corbineau .

view this post on Zulip Pierre Corbineau (Dec 08 2020 at 07:00):

Hi, @Kyle Ehrlich and @Paolo Giarrusso .

Just looked into your comments. Thanks for "paging" me.
As suggested by the hint, "congruence with (Triple a a a) (Triple d c a)" works in the given example, BUT ...
It is also clear that there is a regression because the hint is not given anymore :oh_no:

Please submit a bug report for the absence of the "Goal is solvable by congruence but some arguments are missing." hint, so that the team can perform a proper bissection.

view this post on Zulip Gaëtan Gilbert (Dec 08 2020 at 09:20):

probably since https://github.com/coq/coq/commit/6bc9ef56c5833ee81d7298ab0c52146ad775e2a1
before it the info was output imperatively
after it gets put in the tactic failure, but the failure is later caught and replaced by "congruence failed"

view this post on Zulip Gaëtan Gilbert (Dec 08 2020 at 09:35):

https://github.com/coq/coq/pull/13597

view this post on Zulip Kyle Ehrlich (Dec 08 2020 at 15:01):

Thank you for your help.

@Paolo Giarrusso For reference this is what I am referring to as "the congruence paper" https://link.springer.com/chapter/10.1007/978-3-540-74464-1_6

view this post on Zulip Pierre Corbineau (Dec 08 2020 at 15:02):

Thanks Gaëtan for looking into the issue.


Last updated: Jan 29 2023 at 01:02 UTC