I was interested in getting e-graphs for Coq terms. Does this exist? I know this exists:

The congruence closure tactic’s source code appears to mention that it does “e-matching”: coq/ccalgo.ml at 63837173f8901ba0f4f078c577aa499c5a257d01 · coq/coq · GitHub

but I remember reading that congruence closure tactic in coq was limited (only FOL? Can’t remember what it was).

Is this true? What is missing for an e-graph to work in Coq? In particular, I am also curious how UIP/Univalence would be incorporated if at all.

Hum, you’re asking a rather technical question. Maybe could you write to Pierre Corbineau, author of `congruence`

who would know how to answer. For details on `congruence`

, there is also of course the reference manual https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html#coq:tacn.congruence.

Regarding UIP, I don’t believe it is taken into account, but if you `pose proof UIP`

, it might use it. I would say that univalence is a priori unrelated (but you can state an equality of types and `congruence`

will consider it).

Best,

1 Like