Patrick Nicodemus (Apr 29 2023 at 18:02): Patrick Nicodemus (Apr 29 2023 at 18:02):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?
Paolo Giarrusso (Apr 29 2023 at 20:51):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)
Paolo Giarrusso (Apr 29 2023 at 20:54):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
Paolo Giarrusso (Apr 29 2023 at 20:57):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.
Paolo Giarrusso (Apr 29 2023 at 21:08):and itauto appears to reuse congruence as a blackbox (at a skim of the associated code and paper)
Gaëtan Gilbert (Apr 29 2023 at 21:28):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 13 2024 at 01:02 UTC