Stream: Coq users

Topic: e-graphs in Coq?


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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: Jun 16 2024 at 03:41 UTC