Does Coq have e-graphs (for Dependent Types)?

Miscellaneous
1

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”: https://github.com/coq/coq/blob/63837173f8901ba0f4f078c577aa499c5a257d01/plugins/cc/ccalgo.ml#L1008

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.

2

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