Implement naive conditional rewriting, without proof reconstruction

Lean/Egg/Core/Encode/Rewrites.lean

@@ -19,7 +19,8 @@ def Rewrite.encode (rw : Rewrite) (cfg : Config.Encoding) (amb : MVars.Ambient)
     lhs   := ← Egg.encode rw.lhs rw.src cfg amb
     rhs   := ← Egg.encode rw.rhs rw.src cfg amb
     dirs  := rw.validDirs
-    conds := ← rw.conds.mapM (Egg.encode · rw.src cfg amb)
+    -- We are encoding the *type* of each condition, not the condition mvar itself.
+    conds := ← rw.conds.mapM fun cond => do Egg.encode (← cond.mvarId!.getType) rw.src cfg amb
   }
 
 namespace Rewrites

Lean/Egg/Core/Premise/Rewrites.lean

@@ -19,15 +19,12 @@ structure Rewrite.MVars where
 structure Rewrite extends Congr where
   proof : Expr
   src   : Source
-  conds : Array Expr
+  conds : Array Expr -- This holds the *mvar* of each condition, not its type.
   mvars : Rewrite.MVars
   deriving Inhabited
 
 namespace Rewrite
 
-def isConditional (rw : Rewrite) : Bool :=
-  !rw.conds.isEmpty
-
 def validDirs (rw : Rewrite) : Directions :=
   let exprDirs := Directions.satisfyingSuperset rw.mvars.lhs.expr rw.mvars.rhs.expr
   let lvlDirs  := Directions.satisfyingSuperset rw.mvars.lhs.lvl rw.mvars.rhs.lvl

Lean/Egg/Tactic/Basic.lean

@@ -60,7 +60,6 @@ private partial def genPremises
   let ps ← Premises.parse cfg amb ps
   let tcRws ← genTcRws ps
   tracePremises ps tcRws cfg
-  throwOnConditionalRw ps.rws ps.rwsStx
   return (ps.rws ++ tcRws, ps.facts)
 where
   genTcRws (ps : Premises) : TacticM Rewrites := do
@@ -83,10 +82,6 @@ where
         tcRws    := tcRws ++ specRws
     return tcRws
 
-  throwOnConditionalRw (rws : Rewrites) (stxs : Array Syntax) : TacticM Unit := do
-    for rw in rws, stx in stxs do
-      if rw.isConditional then throwErrorAt stx "egg does not currently support conditional rewrites"
-
 private def processRawExpl
     (rawExpl : Explanation.Raw) (goal : Goal) (rws : Rewrites) (amb : MVars.Ambient) :
     TacticM Expr := do

Lean/Egg/Tactic/Trace.lean

@@ -66,6 +66,12 @@ def Rewrite.Encoded.trace (rw : Rewrite.Encoded) (cls : Name) : TacticM Unit :=
   withTraceNode cls (fun _ => return header) do
     Lean.trace cls fun _ => m!"LHS: {rw.lhs}"
     Lean.trace cls fun _ => m!"RHS: {rw.rhs}"
+    if rw.conds.isEmpty then
+      Lean.trace cls fun _ => "No Conditions"
+    else
+      withTraceNode cls (fun _ => return "Conditions") (collapsed := false) do
+        for cond in rw.conds do
+          Lean.trace cls fun _ => cond
 
 nonrec def Config.trace (cfg : Config) (cls : Name) : TacticM Unit := do
   let toEmoji (b : Bool) := if b then "✅" else "❌"

Lean/Egg/Tests/Conditional.lean

@@ -1,6 +1,4 @@
 import Egg
 
-/-- error: egg does not currently support conditional rewrites -/
-#guard_msgs in
-example (h : ∀ n : Nat, n > 2 → n = 5) : x = 5 := by
-  egg [h]
+example (x : Nat) (h₁ : ∀ n, n > 2 → n = x) (h₂ : 3 > 2) : 3 = x := by
+  egg (config := { exitPoint := some .beforeProof }) [h₁, h₂]

Lean/Egg/Tests/WIP.lean

@@ -1,10 +1,5 @@
 import Egg
 
-set_option trace.egg true in
-example (h : ∀ n, n > 2 → n = 5) : 3 = 5 := by
-  have h' : 3 > 2 := by simp
-  egg [h, h']
-
 -- The universe mvars (or universe params if you make this a theorem instead of an example) are
 -- different for the respective `α`s, so this doesn't hold by reflexivity. But `simp` can somehow
 -- prove this.

Rust/src/rewrite.rs

@@ -47,7 +47,15 @@ impl Applier<LeanExpr, LeanAnalysis> for LeanApplier {
             }
         }
 
-        // TODO: check conditions against facts
+        'cond_loop: for cond in self.conds.clone() {
+            // TODO: I think `add_instantiation` crashes when the pattern contains variables not covered by the subst.
+            //       Do we know that conditions' variables are always a subset of the rewrite's body's variables?
+            let id = graph.add_instantiation(&cond.ast, subst);
+            for fact in self.facts.clone() {
+                if id == graph.add_expr(&fact) { continue 'cond_loop }
+            } 
+            return vec![] // This is only reached if `cond` is not satisfied by any fact.
+        }
 
         // A substitution needs no shifting if it does not map any variables to e-classes containing loose bvars.
         // This is the case exactly when `var_depths` is empty.