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 congruence
.
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.
maybe try 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"
https://github.com/coq/coq/pull/13597
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: Oct 13 2024 at 01:02 UTC