Kyle Ehrlich (Dec 07 2020 at 23:43): 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.
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
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.
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.
Paolo Giarrusso (Dec 08 2020 at 01:43):maybe try Set Congruence Verbose?
Paolo Giarrusso (Dec 08 2020 at 01:43):the docs has no examples using congruence with, so ultimately clueless.
Paolo Giarrusso (Dec 08 2020 at 01:44):Paging @Pierre Corbineau .
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.
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"
Gaëtan Gilbert (Dec 08 2020 at 09:35):https://github.com/coq/coq/pull/13597
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
Pierre Corbineau (Dec 08 2020 at 15:02):Thanks Gaëtan for looking into the issue.
Last updated: Apr 18 2024 at 01:01 UTC