`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.
```

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.
Proof. Fail congruence. Admitted.
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.

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.

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

.

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.

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