## Stream: Coq users

### Topic: congruence and specialization

#### Andrej Dudenhefner (Jul 07 2021 at 10:05):

`congruence` sometimes unfolds definitions and sometimes specializes hypotheses. I want to understand when (and/or whether this could be improved upon). Consider the following example, where (1) is not coherent with (3) and (2) is not coherent with (4). Bug or intention?

``````Definition twice (f: nat -> nat) x := f (f x).

Lemma twice_def f x : twice f x = f (f x).
Proof. reflexivity. Qed.

Definition twice_spec f := forall x, twice f x = f (f x).

Goal forall f x, twice f x = f (f x).
Proof.
intros f x.
Fail congruence. (* (1) somewhat expected; still curious since https://github.com/coq/coq/issues/13778 *)
pose proof (H := twice_def).
Fail congruence. (* (2) unexpected, H could be specialized with f, x *)
assert (H' : twice_spec f) by exact (H f).
Fail Fail congruence. (* (3) unexpected, H' needs unfolding; why different from (1)? *)
clear H'.
specialize (H f).
congruence. (* (4) somewhat expected, H is instantiated with x; why different from (2)? *)
Qed.
``````

#### Andrej Dudenhefner (Jul 13 2021 at 15:09):

I did some digging in the code and found the answer: `congruence` is not able to specialize variables that occur as `App` heads.
In the above, in `f (f x)` the variable `f` cannot be instantiated. Compare with the following example

``````Axiom p : (nat -> nat) -> nat.
Goal (forall f, p f = f 0) -> forall f, p f = f 0.

Definition ap {X Y : Type} (f : X -> Y) (x : X) := f x.

Goal (forall f, p f = ap f 0) -> forall f, p f = ap f 0.
Proof. congruence. Qed.
``````

The first goal fails because it contains `f 0` where `f` needs to be instantiated.
The second goal succeeds because in `ap f 0` the variable `f` is not applied to an argument.
I'm not sure whether `congruence` can be improved to handle the general case.

#### Stéphane Desarzens (Jul 13 2021 at 15:37):

Implements the standard Nelson and Oppen congruence closure algorithm ...

From having a quick look at the paper of Nelson and Oppen, I think the abstract algorithm should be able to deal with this. But probably it's the implementation that doesn't recognize that `(forall f, p f = f 0)` describes an equality that it can use.

#### Guillaume Melquiond (Jul 13 2021 at 15:53):

That seems a bit doubtful. Nelson-Oppen is a first-order algorithm. It should not even notice `p f`.

#### Andrej Dudenhefner (Jul 14 2021 at 06:34):

From what I understand looking at the code, it implements a rudimentary matching procedure for which it is faster/simpler knowing the exact head of a (nested) application. It would require a larger overhaul (and I suspect that it is indeed possible) of the internal `congruence` code to accommodate for the described failing examples. Also for performance reasons, using Coqs unification for this could be too powerful/slow.

#### Andrej Dudenhefner (Jul 14 2021 at 10:54):

I am now experimenting with an extension PR#14650 of `congruence` that covers the failing example.

Last updated: Jan 28 2023 at 06:30 UTC