Congruence

[spitters]

For future reference. This extension of the algorithm behind the congruence tactic that is compatible with HoTT.

[mattam82]

Yep, definitely would be great to have a HoTT/full-DTT compatible congruence, whereas Coq's current congruence closure algorithm does not handle dependency at all. We're thinking with N. Tabareau and E. Tanter that the "Equivalences for Free" parametricity + univalence translation + Soccola's idea could be mixed to give that a kind of generalized congruence with equality/equivalences working with dependency.

[spitters]

That sounds great.

[tlringer]

@spitters pointed me toward this thread. I've been thinking a lot about better congruence in HoTT. I think that the root of what you want is proof-producing e-graphs with equality up to transport as the notion of equality. I wrote a blog post about it here.

I link in that blog post to Leo de Moura's work in Lean, but in fact I think in HoTT it would be much simper and look not very different from what you'd do in a simply-typed logic, since HoTT gives you a much nicer notion of congruence over dependent types (seems to me that what the paper you linked to states as congruence is what Leo calls hcongr_ideal, except with the notion of equality we actually want).

I think it's even cooler than "just" implementing better congruence in HoTT though: The same exact data structure and algorithm could get you more efficient type-based search for automatic transport for large libraries than what you get using type classes, since you can think of this automatic transport as just being a rewrite system. I suspect it would be useful for congruence, but also for type-based automatic transport in DEVOID, in the univalent parametricity framework, and in CoqHoTT.

If there's enough critical interest, I'm happy to contribute to developing them. I'm talking to a number of people here at UW who work on e-graphs because I also need something similar for DEVOID. Regardless, I'd like to be looped in to whatever happens here.

[spitters]

This turns out to be easier in cubical type theory. PDF.

[tlringer]

I am thrilled that this is true!

This same insight means that you should be able to use egraphs to implement efficient type-directed search for automatic transport.

[tlringer]

@spitters, out of curiosity, what is broken about the commented out test cases in Examples.agda?

We are looking at the implementation as part of a reading group that includes me along with a lot of e-graph experts, with an eye on very efficient implementations of transport for cubical and later for HoTT. We were wondering why those cases aren't working yet.

[spitters]

I recall that they were just slow. @limemloh will confirm. In fact, I believe performance even improved with a later version of agda.

@tlringer Exciting. I'm looking forward to your findings.

[tlringer]

Thanks! Some thoughts from the reading group. For reference, Zach, Max, Chandra, and Remy are e-graph experts. My background is in proof automation and proof engineering more broadly (Zach also knows a lot about proof engineering).

1. Zach Tatlock: For non-Agda users, the use of reflection makes it confusing to read.
2. Mike He: Is this producing a term or just looking up information in the e-graph?
3. Remy Wang, Zach Tatlock, Max Willsey, Chandrakana Nandi, Talia Ringer, Ben Kushigian: Our conclusion from the code was that there are two kinds of edges in the e-graph (parent-child and equivalence), and there are cycles only between the two kinds of edges, but not for any single kind of edge. a. Is this right? b. Figure 1 was confusing to e-graph experts since it didn't show the parent-child edges.
4. Talia Ringer, Max Willsey: Do you anticipate being able to add hints (like equivalences the user has proven already) to the congruence procedure?
5. Talia Ringer, Max Willsey: Can hypotheses or (if applicable) hints be forall-quantified? If so, you will likely need e-matching. Have you thought about e-matching at all, and whether you'll need it?
6. Talia Ringer: I think you might also need e-matching to go from an implementation of congruence to automatic transport with a type-based search, but I'm not sure.
7. Zach Tatlock, Talia Ringer, Max Willsey: The primary efficiency gains would probably come from implementing this in an imperative metalanguage rather than reflectively, for very efficient hash-consing (findOrInsertCongr). Hash-consing is hard to do efficiently in a pure functional language, though alternatively you could add support for physical equality and implement fast hash-consing this way.
8. Talia Ringer: Does hcongr_ideal provably holding in the general case imply univalence? Does it imply the existence of something like an interval type? Just curious where it falls with relation to common axioms & assumptions, since the HoTT version can't prove the general case but the cubical version can.

My current absolutely crazy plan is to implement a simple version of cubical in Rust and try to back it by egg for efficient automatic transport with type-based search. This is a side project so I don't anticipate it being serious research for now, and I'm happy to have external contributions if anyone feels like trying, but I think understanding it well in cubical before moving on to HoTT is a good idea. (It might even be enough for me---I might be able to make my tool's metatheory cubical.)

[remysucre]

Hello Bas, glad to be chatting with you again :) To clarify, in our applications the graph contains two kinds of edges: 1. an equality edge from (the root of) a term to another term, and 2. an "AST" edge from an operator to its arguments (which are representatives of equivalent classes). E.g. from + to a and from + to b. We think the acyclic requirement applies only to equality edges. In fact it's not obvious you need AST edges here.