This project formalizes a small e-graph library in Lean 4, with the goal of being able to state and prove invariants about e-graphs and rule application.

The motivating example is attempting to prove that a rule saturates when the subterms of the right-hand side occur in the left-hand side, since the rule does not add any new e-classes.

The repository currently contains:

• a generic definition of first-order terms
• a generic finite e-graph model built from explicit equality edges
• congruence and representation relations over those graphs
• an executable congruence-closure approximation for matching
• a small arithmetic language with constants, variables, arithmetic operators, and let
• pattern matching and rewrite application for arithmetic terms
• example rewrites and example e-graphs

LeanEGraph/term.lean defines generic first-order terms Term σ together with:

• decidable equality
• a WellFormedTerm typeclass
• structural measures such as size and depth
• finite collections of subterms

LeanEGraph/arith.lean instantiates Term with a simple arithmetic signature:

• constants and variables
• add, mul, sub
• a binder-like lett

It also defines:

• a well-formedness predicate for arithmetic terms
• an evaluator eval : Arith → Option ℕ
• small example expressions with #eval sanity checks

LeanEGraph/egraph.lean contains the main e-graph development:

• EGraph, represented as a finite set of explicit equality edges
• explicitTerms, the subterms currently present in the graph
• CongRel and Represented, the semantic relations induced by the graph
• a finite congruence-closure procedure used by sameEClass
• generic patterns and rewrite rules
• arithmetic-specific matching, substitution, instantiation, and rewrite application
• statements relating syntactic containment of RHS subpatterns to the semantic property NoNewEClasses

The bottom of the file includes a worked arithmetic example showing three rewrite steps:

1. reassociate (x + 1) - 1
2. simplify a - a to 0
3. simplify a + 0 to a

The key rewrite-side notions are:

• NoNewEClasses r: every instantiated RHS term produced by r is already congruent to some explicit term in the original e-graph
• RHSContained r: every proper subpattern of r.rhs appears somewhere in r.lhs

The intended proof pipeline in LeanEGraph/egraph.lean is:

1. show that matched LHS subpatterns already have witnesses among old explicit terms
2. lift that fact to instantiated RHS subpatterns
3. conclude RHSContained r → NoNewEClasses r