## Reading

This class, we will read
**Congruence Closure in Intensional Type Theory** [PDF] [DOI] by Daniel Selsam and Leonardo de Moura. As a short bonus reading, we'll also read the two-pager **Congruence Closure in Cubical Type Theory** [PDF] by Emil Holm Gjørup and Bas Spitters.

If you were paying way too much attention to the proof repair reading, you may have seen me allude to these things called **e-graphs**, and cite these papers. Neither of these papers *say the word* e-graph, but that's what they're about.

E-graphs are these super wonderful **data structures** for managing **equality and equivalence information.** They are traditionally used inside of constraint solvers and automated theorem provers to implement **congruence closure**, an efficient algorithm for equational reasoning---but they can also be used to implement **rewrite systems**.

Probably the best explanation of e-graphs I've seen comes from the documentation for an e-graph library called egg. What the first paper we'll read this week does that is so cool is implement congruence closure with these data structures in a dependent type theory, since traditional solvers and automated theorem provers don't handle dependent types. So basically this paper **takes the central insights at the core of many solvers and automated theorem provers, and lifts it into a dependently typed proof assistant**. It's quite incredible.

The result is a **really powerful tactic** for solving proof goals that follow from series of equations. But as I hinted at in the proof repair paper from before spring break, these have the potential to help with other kinds of automation too---like a much better workflow for **proof repair** across type equivalences when managing a large project with many different datatypes that change! So one thing I'd love to do is **build e-graphs into PUMPKIN Pi**---let me know if you're interested!

Oh, but there's just one problem. Remember when I said early on that equality is one of the hardest problems in type theory? Well, equality in dependent type theory is *hard* and *controversial*, and the first paper we'll read makes **a particular assumption about equality**. This assumption is not one that, say, Coq makes by default, and it's actually *inconsistent* with Cubical Agda (and homotopy type theory more generally).

Enter the second paper---a short two-pager on e-graphs in Cubical Agda. This uses a **different notion of equality** that comes from cubical type theory (an implementation of homotopy type theory). But it's a short paper and, from what I gather, not yet implemented efficiently. Still, these two papers together offer a balanced view of the design space so far in implementing e-graphs for proof assistants based on dependent type theory.

You can find a reading guide and the discussion questions below. A public version of the slides can be found here.

Please note that **this is due the morning before class**, so that we can discuss it in person. And **please install the artifact before Thursday's class**.