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

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

The refman says:

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: Sep 23 2023 at 08:01 UTC