## Stream: Coq users

### Topic: Can't get congruence error message

#### 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: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):

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: May 19 2024 at 16:02 UTC