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