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.
"the congruence paper"? I've never seen anything but "congruence failed" — so I think error's not on your part
I see how to solve this goal, but this seems pretty artificial, so I see why somebody would drop support for it from
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.
Set Congruence Verbose?
the docs has no examples using
congruence with, so ultimately clueless.
Paging @Pierre Corbineau .
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.
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"
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
Thanks Gaëtan for looking into the issue.
Last updated: Sep 23 2023 at 07:01 UTC