e-graphs

Stream: new members

[Bryan Gin-ge Chen]

Welcome! I guess you're talking about the paper "Efficient E-matching for SMT Solvers"? I'm probably not the right person to try to answer your question but maybe @Mario Carneiro or @Gabriel Ebner can help.

[Mario Carneiro]

What are e-graphs? Maybe I know them by another name, but that doesn't ring a bell

[Miguel Raz Guzmán Macedo]

Chiming here - would also be interested in knowing about egraph use in Lean. I take it the pattern matcher for tactics got an algorithmkc overhaul from Lean 3

[Miguel Raz Guzmán Macedo]

Bump. Does the synbolic rewriter in rfl use a particular algorithm for egraphs?

[Miguel Raz Guzmán Macedo]

If one wanted to add tactics similar to RUBI, would that be by overloading simp?

[Miguel Raz Guzmán Macedo]

https://rulebasedintegration.org/

[Eric Wieser]

What do you mean by the symbolic rewriter in rfl?

[Eric Wieser]

rfl is just a shorthand for docs#eq.refl, a constructor for docs#eq

[Miguel Raz Guzmán Macedo]

(deleted)

[Miguel Raz Guzmán Macedo]

@Eric Wieser here's waht I understand:

1. Lean4 has a "symbolic" rewriter for terms in the goals
   From the manual:

-- You can prove theorems about your functions.
-- The following theorem states that for any natural number `a`,
-- adding 2 twice produces a value equal to `a + 4`.
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
  -- The proof is by reflexivity. Lean "symbolically" reduces both sides of the equality
  -- until they are identical.
  rfl

2. the eq.refl you pointed to is in mathlib, aka Lean3.
3. In RUBI, the symbolic term rewriter is crucial for performance and solvability of integration problems.
4. Leo published a fundamental paper of egraphs for symbolic term rewriting, and @Alessandro and I are wondering if that was implemented as the symbolic term rewriter in Lean4.

[Mario Carneiro]

Lean 4's rfl is the same as lean 3's rfl. It's not a "symbolic rewriter", it compares values up to a relation called definitional equality

[Miguel Raz Guzmán Macedo]

Thanks Mario, nice to see you around here too :D

[Mario Carneiro]

which involves weakly normalizing both sides to a constructor

[Mario Carneiro]

I am everywhere

[Miguel Raz Guzmán Macedo]

Well I'm bringing this up because I'm "close" :tm: to porting RUBI to Julia, and from there porting RUBI to Lean wouldn't be "that much" additional effort. I would want to know which tactic I could dump a lhs = rhs ruleset, if at all feasible.

[Mario Carneiro]

As far as I know, nothing about egraphs or symbolic term rewriting is involved in the implementation of rfl and/or defeq in any version of lean. This is much more based on literature on dependent type theory, reduction and strong normalization stuff

[Miguel Raz Guzmán Macedo]

Oh neat.

[Mario Carneiro]

However, you will find more of leo's creativity in the simp tactic, which does symbolic term rewriting closer to what you are talking about

[Miguel Raz Guzmán Macedo]

Ah, that's the one. So I could in theory overload simp with a bunch of these integration rules, right?

[Mario Carneiro]

yes

[Mario Carneiro]

We've done that for derivatives in mathlib

[Mario Carneiro]

I think integration too but I guess the coverage is lower

[Mario Carneiro]

its ability to pattern match on lambdas is limited though, so most likely you would do a full integration routine as a dedicated tactic

[Miguel Raz Guzmán Macedo]

Ouch.

[Mario Carneiro]

I mean, it's pretty hard to recognize that in the function \lam x, sin x * (2 / cos x) you want to pull out the constant factor 2 (let's say this is a preprocessing step)

[Mario Carneiro]

you would have a huge number of possible patterns to look for to find the 2

[Miguel Raz Guzmán Macedo]

Yup, that's a transformation that egraphs can achieve linear in the number of patterns that match, without running into the phase ordering problem of some transformations will bork others.

Hence why we're asking :D

[Miguel Raz Guzmán Macedo]

This is a good overview (that I'm still becoming familiar with myself)
https://egraphs-good.github.io/

[Mario Carneiro]

I don't think I have seen anything like this implemented in lean

[Mario Carneiro]

It is possible to implement it yourself, of course

[Mario Carneiro]

(in lean 3 or lean 4, although it's probably better suited for lean 4)

[Miguel Raz Guzmán Macedo]

Yeah, condolences to the mathlib crowd, I'm learning Lean4 - the garbage collector's too good to pass up :muscle:

[Miguel Raz Guzmán Macedo]

(And in fact it will probably do amazingly in the benchmarks what with the functional but in place style not generating tons of allocations in all the symbolic computations.)

[Wojciech Nawrocki]

Bumping this thread to note a new work which (claims to?) achieve exponential (!) speedups on e-matching queries in the egg library.

[Martin Dvořák]

:eyes: 2022 :eyes:

[Utensil Song]

I was looking for the counter-part of e-graphs in Lean and came across this thread. Based on some search here, I assume it's not implemented in Lean yet.

I'm working on something based on it that should have been done in a proof assistant like Lean, but it's tempting to give it a try as it's a lighter, seemingly sufficient and possible faster solution.

I wonder:

1. the level of its efficiency in the eyes of Lean tactic developers
2. its soundness in the eyes of Lean type theorists
3. the closest mechanism in Lean, pros&cons etc.

Any comments will be greatly appreciated!

Also, here's their latest progress:

• paper Better Together: Unifying Datalog and Equality Saturation
• web demo (rust compiled to wasm): https://egraphs-good.github.io/egglog/ , there are quite some serious and sophisticated use cases like for Herbie’s EqSat
• code (rust): https://github.com/egraphs-good/egglog/
• code (high-level python binding): https://github.com/metadsl/egglog-python

[Marcus Rossel]

cc @Andrés Goens

[Andrés Goens]

@Utensil Song E-graphs (and congruence closure) were implemented in older versions of Lean: see this paper for the Lean 2 description and there's a mathlib tactic for Lean 3 called cc that ports that. If you use Lean 3, then that's great to use! As far as I understand it's not been ported to Lean 4 yet.

[Andrés Goens]

We have a prototype that uses egg, the predecessor of egglog in Lean 4, see: https://github.com/opencompl/egg-tactic-code this is not really mature yet, but we might get back to it at some point hopefully, perhaps integrate with egglog instead and/or with a native Lean 4 implementation, but that's work in progress. This is sound too, because it checks the proof witness generated by egg. If this is useful we're happy to help you use it too, but chances are it might not work for your use case (e.g. currently it doesn't support different types in the term, etc, so it's very bare-bones).

[Andrés Goens]

What's your use case?

[Utensil Song]

Thanks for the comprehensive explanation! It's great to know it naturally worked/works/will work with Lean 2/3/4 ! I'll check them out

[Utensil Song]

I need some experiments before I can determine the extent of my use cases. Now that knowing the results could integrate with Lean, it's definitely worth to dig deeper :big_smile:

[Utensil Song]

I was aware of cc but didn't connect the dots. It would seem that a full integration with egg/egglog could quite some more than cc.

[Utensil Song]

I was a bit concerned with its efficiency (particularly the space complexity) since it preserve more info than usual tree-ish heuristic based approach although it's quite efficient for a graph-based one. Will experiment with complicated use cases and report back.