Came across papers in Lean and Agda discussing the use of e-graphs.

https://cs.au.dk/~spitters/Emil.pdf

https://arxiv.org/abs/1701.04391

Has anyone tried implementing e-graphs in Coq? Are there any projects which do this?

congruence closure is supported by tactics like congruence and itauto (https://coq.inria.fr/distrib/current/refman/proofs/automatic-tactics/logic.html#coq:tacn.congruence)

but `congruence`

appears to far predate Selsam and de Moura's work you're citing (2017), so it's unlikely to deal with indexed data well

Ah indeed > Note that the Coq system even has a tactic congruence that performs congruence closure, but it does not handle dependent types at all and only works on the simply-typed subset of the language.

and itauto appears to reuse congruence as a blackbox (at a skim of the associated code and paper)

Has anyone tried implementing e-graphs in Coq? Are there any projects which do this?

needs uip or cubical apparently (from the pdf you linked) so not vanilla coq

Last updated: Oct 04 2023 at 23:01 UTC