From 4f86d517288c3261cca54644021af698c883a10e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 29 Apr 2024 09:20:55 +0200
Subject: [PATCH 01/16] basic (untested) version of tags

---
 Lean/Egg.lean             |  1 +
 Lean/Egg/Tactic/Tags.lean | 25 +++++++++++++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 Lean/Egg/Tactic/Tags.lean

diff --git a/Lean/Egg.lean b/Lean/Egg.lean
index 6999a8a..ea33525 100644
--- a/Lean/Egg.lean
+++ b/Lean/Egg.lean
@@ -27,3 +27,4 @@ import Egg.Tactic.Explanation
 import Egg.Tactic.Guides
 import Egg.Tactic.Premises
 import Egg.Tactic.Trace
+import Egg.Tactic.Tags
diff --git a/Lean/Egg/Tactic/Tags.lean b/Lean/Egg/Tactic/Tags.lean
new file mode 100644
index 0000000..db18abe
--- /dev/null
+++ b/Lean/Egg/Tactic/Tags.lean
@@ -0,0 +1,25 @@
+import Lean
+
+open Lean
+
+initialize eggXtension : SimplePersistentEnvExtension Name NameSet ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn    := NameSet.insert
+    addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
+  }
+
+syntax (name := insertEgg) "insert_egg " ident : command
+syntax (name := showEgg) "show_gg_set" : command
+
+open Lean.Elab
+open Lean.Elab.Command
+
+@[command_elab insertEgg] def elabInsertEgg : CommandElab := fun stx => do
+  IO.println s!"inserting {stx[1].getId}"
+  modifyEnv fun env => eggXtension.addEntry env stx[1].getId
+
+@[command_elab showEgg] def elabShowBla : CommandElab := fun _ => do
+  IO.println s!"egg set: {eggXtension.getState (← getEnv) |>.toList}"
+
+initialize eggTag : TagAttribute ←
+  registerTagAttribute `egg "Tag for marking lemmas used for equality saturation"

From 6899538b7aeb6fec33e676974336362643f0717b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 29 Apr 2024 10:02:57 +0200
Subject: [PATCH 02/16] fix some typos in tags

---
 Lean/Egg/Tactic/Tags.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lean/Egg/Tactic/Tags.lean b/Lean/Egg/Tactic/Tags.lean
index db18abe..eebd8e4 100644
--- a/Lean/Egg/Tactic/Tags.lean
+++ b/Lean/Egg/Tactic/Tags.lean
@@ -8,8 +8,8 @@ initialize eggXtension : SimplePersistentEnvExtension Name NameSet ←
     addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
   }
 
-syntax (name := insertEgg) "insert_egg " ident : command
-syntax (name := showEgg) "show_gg_set" : command
+syntax (name := insertEgg) "#insert_egg " ident : command
+syntax (name := showEgg) "#show_egg_set" : command
 
 open Lean.Elab
 open Lean.Elab.Command

From d979ffd8ce0623c9da2e05c9573584865392325d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 29 Apr 2024 10:03:08 +0200
Subject: [PATCH 03/16] Add a few test cases for tags (not working yet, ofc)

---
 Lean/Egg/Tests/Tags.lean | 72 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)
 create mode 100644 Lean/Egg/Tests/Tags.lean

diff --git a/Lean/Egg/Tests/Tags.lean b/Lean/Egg/Tests/Tags.lean
new file mode 100644
index 0000000..fb65d4a
--- /dev/null
+++ b/Lean/Egg/Tests/Tags.lean
@@ -0,0 +1,72 @@
+import Egg
+
+class One (α) where one : α
+instance [One α] : OfNat α 1 where ofNat := One.one
+
+class Inv (α) where inv : α → α
+postfix:max "⁻¹" => Inv.inv
+
+class Group (α) extends Mul α, One α, Inv α where
+  mul_assoc     (a b c : α) : (a * b) * c = a * (b * c)
+  one_mul       (a : α)     : 1 * a = a
+  mul_one       (a : α)     : a * 1 = a
+  inv_mul_self  (a : α)     : a⁻¹ * a = 1
+  mul_inv_self  (a : α)     : a * a⁻¹ = 1
+
+variable [Group α] (a b x y : α)
+
+#insert_egg mul_assoc
+#insert_egg one_mul
+#insert_egg mul_one
+#insert_egg inv_mul_self
+#insert_egg mul_inv_self
+
+#show_egg_set
+
+
+@[egg]
+theorem inv_mul_cancel_left : a⁻¹ * (a * b) = b := by
+  egg
+
+#show_egg_set
+
+@[egg]
+theorem mul_inv_cancel_left : a * (a⁻¹ * b) = b :=  by
+  egg
+
+@[egg]
+theorem group_cancel : (∀ a : α, a * b = a) → a = 1 := by
+  intros h
+  egg [h]
+
+@[egg]
+lemma mul_eq_de_eq_inv_mul : x = a⁻¹ * y → a * x = y := by
+ egg
+
+def hPow : α → Nat → α
+    | _, 0 => 1
+    | a, (n+1) => a * hPow a n
+
+instance [Group α] : HPow α Nat α := ⟨hPow⟩
+
+def OrderN (n : Nat) (a : α) : Prop := a^n = 1
+
+-- not defining the cardinality here for space reasons
+def card (α) [Group α] : Nat := sorry
+
+-- This one should not go through! not an equality
+@[egg]
+theorem ex_min_order : ∃ n : Nat, OrderN n a ∧ (∀ n', n' < n → ¬ OrderN n a) := sorry
+
+-- This should also be recognized as an equality
+@[egg]
+theorem card_order : OrderN (card α) a := by
+  sorry
+
+def Abelian (α) [Group α] : Prop := ∀ a b : α, a * b = b * a
+
+def commutator := a*b*a⁻¹*b⁻¹
+
+-- Ideally, egg can see through this prop that there's an equality?
+@[egg]
+theorem all_commutators_trivial_abelian : (∀ a b : α, commutator a b = 1) → Abelian α := by sorry

From dec0d8097563f75e3894d6f3f0367f8fd339eaf1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 29 Apr 2024 16:41:00 +0200
Subject: [PATCH 04/16] add a scoped env extension that stores the tagged egg
 theorems

---
 Lean/Egg/Tactic/Tags.lean | 107 +++++++++++++++++++++++++++++++++-----
 Lean/Egg/Tests/Tags.lean  |  12 ++---
 2 files changed, 99 insertions(+), 20 deletions(-)

diff --git a/Lean/Egg/Tactic/Tags.lean b/Lean/Egg/Tactic/Tags.lean
index eebd8e4..69d64ae 100644
--- a/Lean/Egg/Tactic/Tags.lean
+++ b/Lean/Egg/Tactic/Tags.lean
@@ -2,24 +2,105 @@ import Lean
 
 open Lean
 
-initialize eggXtension : SimplePersistentEnvExtension Name NameSet ←
-  registerSimplePersistentEnvExtension {
-    addEntryFn    := NameSet.insert
-    addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
-  }
+namespace Egg
 
-syntax (name := insertEgg) "#insert_egg " ident : command
-syntax (name := showEgg) "#show_egg_set" : command
+/--
+This validates that a theorem can be used by the `egg` tactic (it ultimately boils down to an equality.)
+
+Unimplemented: Currently, this is a noop.
+-/
+def validateEggTheorem : Name → AttrM Unit := fun _ => pure ()
+
+-- Ideally this should be at some point a discrimination tree
+abbrev EggTheorems := Array Name
+
+abbrev EggEntry := Name -- later: Lean.Meta.SimpEntry
+
+def addEggTheoremEntry (d : EggTheorems) (e : EggEntry) : EggTheorems :=
+  d.push e
+
+abbrev EggXtension := SimpleScopedEnvExtension EggEntry EggTheorems
 
 open Lean.Elab
 open Lean.Elab.Command
 
-@[command_elab insertEgg] def elabInsertEgg : CommandElab := fun stx => do
-  IO.println s!"inserting {stx[1].getId}"
-  modifyEnv fun env => eggXtension.addEntry env stx[1].getId
+def EggXtension.getTheorems (ext : EggXtension) : CoreM EggTheorems :=
+  return ext.getState (← getEnv)
+
+/--
+This function does the appropriate preprocessing from a `Name` to record a theorem as
+an `egg` theorem.
+
+For now, this preprocessing is nothing (just store the name in a singleton `Array`).
+However, in the future this can be used like simp to do more efficient preprocessing
+and deal with other kinds of `egg` lemmas (or even import `simp` lemmas).
+-/
+private def mkEggTheoremsFromConst (declName : Name) : MetaM EggTheorems :=
+  pure #[declName]
+
+def addEggTheorem (ext : EggXtension) (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
+  let eggThms ← mkEggTheoremsFromConst declName
+  for eggThm in eggThms do
+    ext.add eggThm attrKind
+
+def mkEggXt (name : Name := by exact decl_name%) : IO EggXtension :=
+  registerSimpleScopedEnvExtension {
+    name     := name
+    initial  := {}
+    addEntry := fun d e => addEggTheoremEntry d e
+  }
+
+def mkEggAttr (attrName : Name) (attrDescr : String) (ext : EggXtension)
+    (ref : Name := by exact decl_name%) : IO Unit :=
+  registerBuiltinAttribute {
+    ref   := ref
+    name  := attrName
+    descr := attrDescr
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName _stx attrKind => do
+      let go : MetaM Unit := do
+        let info ← getConstInfo declName
+        if (← Meta.isProp info.type) then
+          addEggTheorem ext declName attrKind
+        else
+          throwError "invalid 'egg', it is not a proposition"
+      discard <| go.run {} {}
+    erase := fun declName => do
+      let s := ext.getState (← getEnv)
+      let s := s.erase (declName)
+      modifyEnv fun env => ext.modifyState env fun _ => s
+  }
+
+
+abbrev EggXtensionMap := HashMap Name EggXtension
+
+builtin_initialize eggXtensionMapRef : IO.Ref EggXtensionMap ← IO.mkRef {}
+
+def registerEggAttr (attrName : Name) (attrDescr : String)
+    (ref : Name := by exact decl_name%) : IO EggXtension := do
+  let ext ← mkEggXt ref
+  mkEggAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
+  eggXtensionMapRef.modify fun map => map.insert attrName ext
+  return ext
+
+builtin_initialize eggXtension : EggXtension ← registerEggAttr `egg "equality saturation theorem theorem"
+
+
+syntax (name := showEgg) "#show_egg_set" : command
 
-@[command_elab showEgg] def elabShowBla : CommandElab := fun _ => do
+--
+--
+--#check Lean.Meta.mkSimpAttr
+--
+--@[command_elab insertEgg] def elabInsertEgg : CommandElab := fun stx => do
+--  IO.println s!"inserting {stx[1].getId}"
+--  modifyEnv fun env => eggXtension.addEntry env stx[1].getId
+--
+@[command_elab showEgg] def elabShowEgg : CommandElab := fun _ => do
   IO.println s!"egg set: {eggXtension.getState (← getEnv) |>.toList}"
+--
+--
+--initialize eggTag : TagAttribute ←
+--  registerTagAttribute `egg "Tag for marking lemmas used for equality saturation" (validate := validateEggTheorem)
 
-initialize eggTag : TagAttribute ←
-  registerTagAttribute `egg "Tag for marking lemmas used for equality saturation"
+end Egg
diff --git a/Lean/Egg/Tests/Tags.lean b/Lean/Egg/Tests/Tags.lean
index fb65d4a..1bb0e2f 100644
--- a/Lean/Egg/Tests/Tags.lean
+++ b/Lean/Egg/Tests/Tags.lean
@@ -15,13 +15,11 @@ class Group (α) extends Mul α, One α, Inv α where
 
 variable [Group α] (a b x y : α)
 
-#insert_egg mul_assoc
-#insert_egg one_mul
-#insert_egg mul_one
-#insert_egg inv_mul_self
-#insert_egg mul_inv_self
-
-#show_egg_set
+attribute [egg] Group.mul_assoc
+attribute [egg] Group.one_mul
+attribute [egg] Group.mul_one
+attribute [egg] Group.inv_mul_self
+attribute [egg] Group.mul_inv_self
 
 
 @[egg]

From 37fa0189dbee462a606463808c8b3eacb6bf7653 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 29 Apr 2024 16:48:58 +0200
Subject: [PATCH 05/16] initalize, not builtin

---
 Lean/Egg/Tactic/Tags.lean | 4 ++--
 Lean/Egg/Tests/mathlib4   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Lean/Egg/Tactic/Tags.lean b/Lean/Egg/Tactic/Tags.lean
index 69d64ae..c55ee60 100644
--- a/Lean/Egg/Tactic/Tags.lean
+++ b/Lean/Egg/Tactic/Tags.lean
@@ -74,7 +74,7 @@ def mkEggAttr (attrName : Name) (attrDescr : String) (ext : EggXtension)
 
 abbrev EggXtensionMap := HashMap Name EggXtension
 
-builtin_initialize eggXtensionMapRef : IO.Ref EggXtensionMap ← IO.mkRef {}
+initialize eggXtensionMapRef : IO.Ref EggXtensionMap ← IO.mkRef {}
 
 def registerEggAttr (attrName : Name) (attrDescr : String)
     (ref : Name := by exact decl_name%) : IO EggXtension := do
@@ -83,7 +83,7 @@ def registerEggAttr (attrName : Name) (attrDescr : String)
   eggXtensionMapRef.modify fun map => map.insert attrName ext
   return ext
 
-builtin_initialize eggXtension : EggXtension ← registerEggAttr `egg "equality saturation theorem theorem"
+initialize eggXtension : EggXtension ← registerEggAttr `egg "equality saturation theorem theorem"
 
 
 syntax (name := showEgg) "#show_egg_set" : command
diff --git a/Lean/Egg/Tests/mathlib4 b/Lean/Egg/Tests/mathlib4
index 10d8231..7b780c1 160000
--- a/Lean/Egg/Tests/mathlib4
+++ b/Lean/Egg/Tests/mathlib4
@@ -1 +1 @@
-Subproject commit 10d8231f2c0c98fda9db81682683b3a3f3228791
+Subproject commit 7b780c19c9ad67558e3cc34c3cb565faa21164b0

From 6736b71228c5326a9d3ec6c0cb6531685da74ffc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 29 Apr 2024 17:16:08 +0200
Subject: [PATCH 06/16] add info for show command and add guards in tests to
 show that tagging and extension work

---
 Lean/Egg/Tactic/Tags.lean | 2 +-
 Lean/Egg/Tests/Tags.lean  | 5 +++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/Lean/Egg/Tactic/Tags.lean b/Lean/Egg/Tactic/Tags.lean
index c55ee60..7fc4640 100644
--- a/Lean/Egg/Tactic/Tags.lean
+++ b/Lean/Egg/Tactic/Tags.lean
@@ -97,7 +97,7 @@ syntax (name := showEgg) "#show_egg_set" : command
 --  modifyEnv fun env => eggXtension.addEntry env stx[1].getId
 --
 @[command_elab showEgg] def elabShowEgg : CommandElab := fun _ => do
-  IO.println s!"egg set: {eggXtension.getState (← getEnv) |>.toList}"
+   logInfo m!"egg set: {eggXtension.getState (← getEnv) |>.toList}"
 --
 --
 --initialize eggTag : TagAttribute ←
diff --git a/Lean/Egg/Tests/Tags.lean b/Lean/Egg/Tests/Tags.lean
index 1bb0e2f..0432550 100644
--- a/Lean/Egg/Tests/Tags.lean
+++ b/Lean/Egg/Tests/Tags.lean
@@ -21,11 +21,16 @@ attribute [egg] Group.mul_one
 attribute [egg] Group.inv_mul_self
 attribute [egg] Group.mul_inv_self
 
+/-- info: egg set: [Group.mul_assoc, Group.one_mul, Group.mul_one, Group.inv_mul_self, Group.mul_inv_self] -/
+ #guard_msgs(info) in
+#show_egg_set
 
 @[egg]
 theorem inv_mul_cancel_left : a⁻¹ * (a * b) = b := by
   egg
 
+/-- info: egg set: [Group.mul_assoc, Group.one_mul, Group.mul_one, Group.inv_mul_self, Group.mul_inv_self, inv_mul_cancel_left] -/
+ #guard_msgs(info) in
 #show_egg_set
 
 @[egg]

From feec93bcd8b6c24f6f13901e2bd2e56e8ba92225 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Fri, 17 May 2024 17:00:36 +0200
Subject: [PATCH 07/16] adapt mathlib4 submodule commit to main commit hash

---
 Lean/Egg/Tests/mathlib4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lean/Egg/Tests/mathlib4 b/Lean/Egg/Tests/mathlib4
index 7b780c1..711af92 160000
--- a/Lean/Egg/Tests/mathlib4
+++ b/Lean/Egg/Tests/mathlib4
@@ -1 +1 @@
-Subproject commit 7b780c19c9ad67558e3cc34c3cb565faa21164b0
+Subproject commit 711af927c3966b12c6a486a7df0f0d2fbdb0d78d

From 2095fa10ed17851bfe37625818aa0c37811b2aa7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Fri, 24 May 2024 17:42:30 +0200
Subject: [PATCH 08/16] build  tagged

---
 Lean/Egg/Core/Premise/Rewrites.lean |  1 +
 Lean/Egg/Tactic/Premises/Parse.lean | 14 ++++++++++++++
 2 files changed, 15 insertions(+)

diff --git a/Lean/Egg/Core/Premise/Rewrites.lean b/Lean/Egg/Core/Premise/Rewrites.lean
index 0ba992c..e45a105 100644
--- a/Lean/Egg/Core/Premise/Rewrites.lean
+++ b/Lean/Egg/Core/Premise/Rewrites.lean
@@ -39,6 +39,7 @@ namespace Rewrite
 
 structure Config where
   norm? : Option Config.Normalization := none
+  tagged? : Option Name := `egg
   amb   : MVars.Ambient
 
 def from? (proof : Expr) (type : Expr) (src : Source) (cfg : Config) : MetaM (Option Rewrite) := do
diff --git a/Lean/Egg/Tactic/Premises/Parse.lean b/Lean/Egg/Tactic/Premises/Parse.lean
index ab25f43..f518ef7 100644
--- a/Lean/Egg/Tactic/Premises/Parse.lean
+++ b/Lean/Egg/Tactic/Premises/Parse.lean
@@ -1,5 +1,6 @@
 import Egg.Core.Premise.Rewrites
 import Egg.Core.Premise.Facts
+import Egg.Tactic.Tags
 import Lean
 
 open Lean Meta Elab Tactic
@@ -113,6 +114,19 @@ private def Premises.taggedRw (prem : Name) (idx : Nat) (cfg : Rewrite.Config) :
   let rws ← Premises.explicit ident idx mk .tagged
   return rws.elems
 
+private def Premises.elabTagged (prems : Array Name) (cfg : Rewrite.Config) : TacticM Rewrites := do
+  let mut rws : Rewrites := #[]
+  for prem in prems, idx in [:prems.size] do
+    rws := rws ++ (← taggedRw prem idx cfg)
+  return rws
+
+def Premises.buildTagged (cfg : Rewrite.Config) : TacticM Rewrites :=
+  match cfg.tagged? with
+    | none => return {}
+    | some _ => do -- This should later use this `Name` to find the proper extension
+      let prems := eggXtension.getState (← getEnv)
+      elabTagged prems cfg
+
 -- Note: This function is expected to be called with the lctx which contains the desired premises.
 --
 -- Note: We need to filter out auxiliary declaration and implementation details, as they are not

From 12a0c738d7846a8d7eb20f09d87adc6558f5224b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Fri, 24 May 2024 18:10:31 +0200
Subject: [PATCH 09/16] move tagged config to Config.Gen, build tagged in Gen

---
 Lean/Egg/Core/Config.lean           | 1 +
 Lean/Egg/Core/Premise/Rewrites.lean | 1 -
 Lean/Egg/Tactic/Premises/Gen.lean   | 9 +++++----
 Lean/Egg/Tactic/Premises/Parse.lean | 4 ++--
 4 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/Lean/Egg/Core/Config.lean b/Lean/Egg/Core/Config.lean
index 1623166..4b90c0d 100644
--- a/Lean/Egg/Core/Config.lean
+++ b/Lean/Egg/Core/Config.lean
@@ -21,6 +21,7 @@ structure Encoding extends Normalization where
 
 structure Gen where
   builtins      := true
+  tagged?       := some `egg
   genTcProjRws  := true
   genTcSpecRws  := true
   genGoalTcSpec := false
diff --git a/Lean/Egg/Core/Premise/Rewrites.lean b/Lean/Egg/Core/Premise/Rewrites.lean
index e45a105..0ba992c 100644
--- a/Lean/Egg/Core/Premise/Rewrites.lean
+++ b/Lean/Egg/Core/Premise/Rewrites.lean
@@ -39,7 +39,6 @@ namespace Rewrite
 
 structure Config where
   norm? : Option Config.Normalization := none
-  tagged? : Option Name := `egg
   amb   : MVars.Ambient
 
 def from? (proof : Expr) (type : Expr) (src : Source) (cfg : Config) : MetaM (Option Rewrite) := do
diff --git a/Lean/Egg/Tactic/Premises/Gen.lean b/Lean/Egg/Tactic/Premises/Gen.lean
index 95c5fae..faff79b 100644
--- a/Lean/Egg/Tactic/Premises/Gen.lean
+++ b/Lean/Egg/Tactic/Premises/Gen.lean
@@ -30,14 +30,15 @@ private def tracePremises
 partial def gen
     (goal : Congr) (ps : TSyntax `egg_premises) (guides : Guides) (cfg : Config)
     (amb : MVars.Ambient) : TacticM (Rewrites × Facts) := do
+  let tagged ← Premises.buildTagged cfg amb
   let ⟨⟨basic, basicStxs⟩, facts⟩ ← Premises.elab { norm? := cfg, amb } ps
-  let (basic, basicStxs, pruned₁) ← prune basic basicStxs (remove := #[])
+  let (basic, basicStxs, pruned₁) ← prune basic basicStxs (remove := tagged)
   let builtins ← if cfg.builtins then Rewrites.builtins { norm? := cfg, amb } else pure #[]
-  let (builtins, _, pruned₂) ← prune builtins (remove := basic)
+  let (builtins, _, pruned₂) ← prune builtins (remove := tagged ++ basic)
   let tc ← genTcRws (basic ++ builtins) facts.elems
-  let (tc, _, pruned₃) ← prune tc (remove := basic ++ builtins)
+  let (tc, _, pruned₃) ← prune tc (remove := tagged ++ basic ++ builtins)
   tracePremises ⟨basic, basicStxs⟩ builtins tc (pruned₁ ++ pruned₂ ++ pruned₃) facts cfg
-  let rws := basic ++ builtins ++ tc
+  let rws := tagged ++ basic ++ builtins ++ tc
   catchInvalidConditionals rws
   return (rws, facts.elems)
 where
diff --git a/Lean/Egg/Tactic/Premises/Parse.lean b/Lean/Egg/Tactic/Premises/Parse.lean
index f518ef7..3992ee5 100644
--- a/Lean/Egg/Tactic/Premises/Parse.lean
+++ b/Lean/Egg/Tactic/Premises/Parse.lean
@@ -120,12 +120,12 @@ private def Premises.elabTagged (prems : Array Name) (cfg : Rewrite.Config) : Ta
     rws := rws ++ (← taggedRw prem idx cfg)
   return rws
 
-def Premises.buildTagged (cfg : Rewrite.Config) : TacticM Rewrites :=
+def Premises.buildTagged (cfg : Config) (amb : MVars.Ambient ): TacticM Rewrites :=
   match cfg.tagged? with
     | none => return {}
     | some _ => do -- This should later use this `Name` to find the proper extension
       let prems := eggXtension.getState (← getEnv)
-      elabTagged prems cfg
+      elabTagged prems { norm? := cfg, amb}
 
 -- Note: This function is expected to be called with the lctx which contains the desired premises.
 --

From cf3b9a9c7ae9162471c5dff7a2905b51685e6171 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Sat, 25 May 2024 08:32:24 +0200
Subject: [PATCH 10/16] fix reconstruction for egg-tagged theorems

---
 Lean/Egg/Core/Explanation/Parse.lean |  2 ++
 Lean/Egg/Tactic/Premises/Gen.lean    |  5 +++--
 Lean/Egg/Tests/Tags.lean             | 15 +++++++++------
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/Lean/Egg/Core/Explanation/Parse.lean b/Lean/Egg/Core/Explanation/Parse.lean
index e6a4a5a..e9146a8 100644
--- a/Lean/Egg/Core/Explanation/Parse.lean
+++ b/Lean/Egg/Core/Explanation/Parse.lean
@@ -36,6 +36,7 @@ syntax "*" noWs num                      : egg_basic_fwd_rw_src
 syntax "⊢"                               : egg_basic_fwd_rw_src
 syntax "↣" noWs num                      : egg_basic_fwd_rw_src
 syntax "◯" noWs num                      : egg_basic_fwd_rw_src
+syntax "□" noWs num (noWs "/" noWs num)? : egg_basic_fwd_rw_src
 
 syntax "[" egg_tc_proj_loc num "," num "]" : egg_tc_proj
 
@@ -119,6 +120,7 @@ private def parseTcProjLocation : (TSyntax `egg_tc_proj_loc) → Source.TcProjLo
 
 private def parseBasicFwdRwSrc : (TSyntax `egg_basic_fwd_rw_src) → Source
   | `(egg_basic_fwd_rw_src|#$idx$[/$eqn?]?) => .explicit idx.getNat (eqn?.map TSyntax.getNat)
+  | `(egg_basic_fwd_rw_src|□$idx$[/$eqn?]?) => .tagged idx.getNat (eqn?.map TSyntax.getNat)
   | `(egg_basic_fwd_rw_src|*$idx)           => .star (.fromUniqueIdx idx.getNat)
   | `(egg_basic_fwd_rw_src|⊢)               => .goal
   | `(egg_basic_fwd_rw_src|↣$idx)           => .guide idx.getNat
diff --git a/Lean/Egg/Tactic/Premises/Gen.lean b/Lean/Egg/Tactic/Premises/Gen.lean
index faff79b..0da7f63 100644
--- a/Lean/Egg/Tactic/Premises/Gen.lean
+++ b/Lean/Egg/Tactic/Premises/Gen.lean
@@ -12,11 +12,12 @@ namespace Egg.Premises
 -- TODO: Perform pruning during generation, not after.
 
 private def tracePremises
-    (basic : WithSyntax Rewrites) (builtins tc pruned : Rewrites) (facts : WithSyntax Facts)
+    (basic : WithSyntax Rewrites) (tagged builtins tc pruned : Rewrites) (facts : WithSyntax Facts)
     (cfg : Config.Gen) : TacticM Unit := do
   let cls := `egg.rewrites
   withTraceNode cls (fun _ => return "Rewrites") do
     withTraceNode cls (fun _ => return m!"Basic ({basic.elems.size})") do basic.elems.trace basic.stxs cls
+    withTraceNode cls (fun _ => return m!"Tagged ({tagged.size})") do tagged.trace #[] cls
     withTraceNode cls (fun _ => return m!"Generated ({tc.size})") do tc.trace #[] cls
     withTraceNode cls (fun _ => return m!"Builtin ({builtins.size})") do builtins.trace #[] cls
     withTraceNode cls (fun _ => return m!"Hypotheses ({facts.elems.size})") do
@@ -37,7 +38,7 @@ partial def gen
   let (builtins, _, pruned₂) ← prune builtins (remove := tagged ++ basic)
   let tc ← genTcRws (basic ++ builtins) facts.elems
   let (tc, _, pruned₃) ← prune tc (remove := tagged ++ basic ++ builtins)
-  tracePremises ⟨basic, basicStxs⟩ builtins tc (pruned₁ ++ pruned₂ ++ pruned₃) facts cfg
+  tracePremises ⟨basic, basicStxs⟩ tagged builtins tc (pruned₁ ++ pruned₂ ++ pruned₃) facts cfg
   let rws := tagged ++ basic ++ builtins ++ tc
   catchInvalidConditionals rws
   return (rws, facts.elems)
diff --git a/Lean/Egg/Tests/Tags.lean b/Lean/Egg/Tests/Tags.lean
index 0432550..0289563 100644
--- a/Lean/Egg/Tests/Tags.lean
+++ b/Lean/Egg/Tests/Tags.lean
@@ -37,14 +37,13 @@ theorem inv_mul_cancel_left : a⁻¹ * (a * b) = b := by
 theorem mul_inv_cancel_left : a * (a⁻¹ * b) = b :=  by
   egg
 
+-- TODO: should egg (or a version of egg) do the intros automatically to get an eq goal?
 @[egg]
-theorem group_cancel : (∀ a : α, a * b = a) → a = 1 := by
-  intros h
-  egg [h]
+theorem mul_eq_de_eq_inv_mul : x = a⁻¹ * y → a * x = y := by
+ intros h
+ egg [h]
 
-@[egg]
-lemma mul_eq_de_eq_inv_mul : x = a⁻¹ * y → a * x = y := by
- egg
+-- Here come some tests for egg accepting/rejecting tagged lemmas
 
 def hPow : α → Nat → α
     | _, 0 => 1
@@ -73,3 +72,7 @@ def commutator := a*b*a⁻¹*b⁻¹
 -- Ideally, egg can see through this prop that there's an equality?
 @[egg]
 theorem all_commutators_trivial_abelian : (∀ a b : α, commutator a b = 1) → Abelian α := by sorry
+
+/-- We should not break egg after adding these lemmas -/
+example : a * b = b * a := by
+  egg

From a62fb1adf0fd28f217f4abf46bd2e83c81ebffa2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Sat, 25 May 2024 09:19:42 +0200
Subject: [PATCH 11/16] factor out validate, still doesn't quite work to
 validate when tagging

---
 Lean/Egg/Tactic/Premises/Parse.lean    | 39 +------------------
 Lean/Egg/Tactic/Premises/Validate.lean | 53 ++++++++++++++++++++++++++
 Lean/Egg/Tactic/Tags.lean              |  8 +++-
 3 files changed, 60 insertions(+), 40 deletions(-)
 create mode 100644 Lean/Egg/Tactic/Premises/Validate.lean

diff --git a/Lean/Egg/Tactic/Premises/Parse.lean b/Lean/Egg/Tactic/Premises/Parse.lean
index 3992ee5..6f4791b 100644
--- a/Lean/Egg/Tactic/Premises/Parse.lean
+++ b/Lean/Egg/Tactic/Premises/Parse.lean
@@ -1,5 +1,6 @@
 import Egg.Core.Premise.Rewrites
 import Egg.Core.Premise.Facts
+import Egg.Tactic.Premises.Validate
 import Egg.Tactic.Tags
 import Lean
 
@@ -17,44 +18,6 @@ syntax "[" egg_premise,+ ("; " egg_premise,+)? "]" : egg_premise_list
 declare_syntax_cat egg_premises
 syntax (egg_premise_list)? : egg_premises
 
-inductive Premise.Raw where
-  | single (expr : Expr) (type? : Option Expr := none)
-  | eqns (exprs : Array Expr)
-
--- We don't just elaborate premises directly as:
--- (1) this can cause problems for global constants with typeclass arguments, as Lean sometimes
---     tries to synthesize the arguments and fails if it can't (instead of inserting mvars).
--- (2) global constants which are definitions with equations (cf. `getEqnsFor?`) are supposed to
---     be replaced by their defining equations.
-partial def Premise.Raw.elab (prem : Term) : TacticM Premise.Raw := do
-  if let some hyp ← optional (getFVarId prem) then
-    -- `prem` is a local declaration.
-    let decl ← hyp.getDecl
-    if decl.isImplementationDetail || decl.isAuxDecl then
-      throwErrorAt prem "egg does not support using auxiliary declarations"
-    else
-      return .single (.fvar hyp) (← hyp.getType)
-  else if let some const ← optional (resolveGlobalConstNoOverload prem) then
-    if let some eqs ← getEqnsFor? const (nonRec := true) then
-      -- `prem` is a global definition.
-      return .eqns <| ← eqs.mapM fun eqn => Tactic.elabTerm (mkIdent eqn) none
-    else
-      -- `prem` is an global constant which is not a definition with equations.
-      let env ← getEnv
-      let some info := env.find? const | throwErrorAt prem m!"unknown constant '{mkConst const}'"
-      match info with
-      | .defnInfo _ | .axiomInfo _ | .thmInfo _ | .opaqueInfo _ =>
-        let lvlMVars ← List.replicateM info.numLevelParams mkFreshLevelMVar
-        let val := if info.hasValue then info.instantiateValueLevelParams! lvlMVars else .const info.name lvlMVars
-        let type := info.instantiateTypeLevelParams lvlMVars
-        return .single val type
-      | _ => throwErrorAt prem "egg requires arguments to be theorems, definitions or axioms"
-  else
-    -- `prem` is an invalid identifier or a term which is not an identifier.
-    -- We must use `Tactic.elabTerm`, not `Term.elabTerm`. Otherwise elaborating `‹...›` doesn't
-    -- work correctly. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Elaborate.20.E2.80.B9.2E.2E.2E.E2.80.BA
-    return .single (← Tactic.elabTerm prem none)
-
 structure WithSyntax (α) where
   elems : α
   stxs  : Array Syntax := #[]
diff --git a/Lean/Egg/Tactic/Premises/Validate.lean b/Lean/Egg/Tactic/Premises/Validate.lean
new file mode 100644
index 0000000..9deca2a
--- /dev/null
+++ b/Lean/Egg/Tactic/Premises/Validate.lean
@@ -0,0 +1,53 @@
+import Egg.Core.Premise.Rewrites
+
+open Lean Meta Elab Tactic
+
+inductive Premise.Raw where
+  | single (expr : Expr) (type? : Option Expr := none)
+  | eqns (exprs : Array Expr)
+
+inductive Premise.RawRaw where
+  | eqns (exprs : Array Name)
+  | single (expr : Expr) (type? : Option Expr := none)
+  | prem (prem : Term)
+
+
+def Premise.Raw.validate (prem : Term) : MetaM Premise.RawRaw := do
+  if let some const ← optional (resolveGlobalConstNoOverload prem) then
+    if let some eqs ← getEqnsFor? const (nonRec := true) then
+      -- `prem` is a global definition.
+      return .eqns eqs
+    else
+      -- `prem` is an global constant which is not a definition with equations.
+      let env ← getEnv
+      let some info := env.find? const | throwErrorAt prem m!"unknown constant '{mkConst const}'"
+      match info with
+      | .defnInfo _ | .axiomInfo _ | .thmInfo _ | .opaqueInfo _ =>
+        let lvlMVars ← List.replicateM info.numLevelParams mkFreshLevelMVar
+        let val := if info.hasValue then info.instantiateValueLevelParams! lvlMVars else .const info.name lvlMVars
+        let type := info.instantiateTypeLevelParams lvlMVars
+        return .single val type
+      | _ => throwErrorAt prem "egg requires arguments to be theorems, definitions or axioms"
+  else
+    -- `prem` is an invalid identifier or a term which is not an identifier.
+    -- We must use `Tactic.elabTerm`, not `Term.elabTerm`. Otherwise elaborating `‹...›` doesn't
+    -- work correctly. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Elaborate.20.E2.80.B9.2E.2E.2E.E2.80.BA
+    return .prem prem
+
+-- We don't just elaborate premises directly as:
+-- (1) this can cause problems for global constants with typeclass arguments, as Lean sometimes
+--     tries to synthesize the arguments and fails if it can't (instead of inserting mvars).
+-- (2) global constants which are definitions with equations (cf. `getEqnsFor?`) are supposed to
+--     be replaced by their defining equations.
+partial def Premise.Raw.elab (prem : Term) : TacticM Premise.Raw := do
+  if let some hyp ← optional (getFVarId prem) then
+    -- `prem` is a local declaration.
+    let decl ← hyp.getDecl
+    if decl.isImplementationDetail || decl.isAuxDecl then
+      throwErrorAt prem "egg does not support using auxiliary declarations"
+    else
+      return .single (.fvar hyp) (← hyp.getType)
+  match (← validate prem) with
+    | .eqns eqs => return .eqns <| ← eqs.mapM fun eqn => Tactic.elabTerm (mkIdent eqn) none
+    | .single val type? => return .single val type?
+    | .prem prem => return .single (← Tactic.elabTerm prem none)
diff --git a/Lean/Egg/Tactic/Tags.lean b/Lean/Egg/Tactic/Tags.lean
index 7fc4640..b85e6b9 100644
--- a/Lean/Egg/Tactic/Tags.lean
+++ b/Lean/Egg/Tactic/Tags.lean
@@ -1,6 +1,7 @@
+import Egg.Tactic.Premises.Validate
 import Lean
 
-open Lean
+open Lean Elab Tactic Term
 
 namespace Egg
 
@@ -9,7 +10,9 @@ This validates that a theorem can be used by the `egg` tactic (it ultimately boi
 
 Unimplemented: Currently, this is a noop.
 -/
-def validateEggTheorem : Name → AttrM Unit := fun _ => pure ()
+private def validateEggTheorem (thm : Term) : MetaM Unit := do
+  let _ ← Premise.Raw.validate thm
+  return ()
 
 -- Ideally this should be at some point a discrimination tree
 abbrev EggTheorems := Array Name
@@ -39,6 +42,7 @@ private def mkEggTheoremsFromConst (declName : Name) : MetaM EggTheorems :=
   pure #[declName]
 
 def addEggTheorem (ext : EggXtension) (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
+  let _ ← validateEggTheorem { raw := Syntax.ident default default declName []} -- ugly!
   let eggThms ← mkEggTheoremsFromConst declName
   for eggThm in eggThms do
     ext.add eggThm attrKind

From 562c14bda49aba5e6441f0a6b216d33a974a77ae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Sat, 25 May 2024 09:23:53 +0200
Subject: [PATCH 12/16] fix guard messages to consider new trace (with tagged
 rewrites)

---
 Lean/Egg/Tests/Conditional.lean     | 1 +
 Lean/Egg/Tests/Prune.lean           | 2 ++
 Lean/Egg/Tests/TC Proj Binders.lean | 1 +
 3 files changed, 4 insertions(+)

diff --git a/Lean/Egg/Tests/Conditional.lean b/Lean/Egg/Tests/Conditional.lean
index 42e849e..d96aa1a 100644
--- a/Lean/Egg/Tests/Conditional.lean
+++ b/Lean/Egg/Tests/Conditional.lean
@@ -95,6 +95,7 @@ info: [egg.rewrites] Rewrites
           expr:  [?l₂]
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Hypotheses (0)
diff --git a/Lean/Egg/Tests/Prune.lean b/Lean/Egg/Tests/Prune.lean
index b991ce5..2dfbde9 100644
--- a/Lean/Egg/Tests/Prune.lean
+++ b/Lean/Egg/Tests/Prune.lean
@@ -21,6 +21,7 @@ info: [egg.rewrites] Rewrites
           expr:  []
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Hypotheses (0)
@@ -55,6 +56,7 @@ info: [egg.rewrites] Rewrites
           expr:  [?n, ?m]
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Hypotheses (0)
diff --git a/Lean/Egg/Tests/TC Proj Binders.lean b/Lean/Egg/Tests/TC Proj Binders.lean
index ade179f..0e6badc 100644
--- a/Lean/Egg/Tests/TC Proj Binders.lean	
+++ b/Lean/Egg/Tests/TC Proj Binders.lean	
@@ -25,6 +25,7 @@ info: [egg.rewrites] Rewrites
           expr:  []
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (2)
     [egg.rewrites] #0[0?69632,0](⇔)
       [egg.rewrites] HMul.hMul = Mul.mul

From e573e539cc66fdcda8cef51f2c5495fa6f4e1cae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Sat, 25 May 2024 09:29:05 +0200
Subject: [PATCH 13/16] split basic tagged functionality from validation tests

---
 Lean/Egg/Tests/Tags.lean               | 34 ----------------
 Lean/Egg/Tests/WIP_ValidateTagged.lean | 54 ++++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 34 deletions(-)
 create mode 100644 Lean/Egg/Tests/WIP_ValidateTagged.lean

diff --git a/Lean/Egg/Tests/Tags.lean b/Lean/Egg/Tests/Tags.lean
index 0289563..dc154d1 100644
--- a/Lean/Egg/Tests/Tags.lean
+++ b/Lean/Egg/Tests/Tags.lean
@@ -42,37 +42,3 @@ theorem mul_inv_cancel_left : a * (a⁻¹ * b) = b :=  by
 theorem mul_eq_de_eq_inv_mul : x = a⁻¹ * y → a * x = y := by
  intros h
  egg [h]
-
--- Here come some tests for egg accepting/rejecting tagged lemmas
-
-def hPow : α → Nat → α
-    | _, 0 => 1
-    | a, (n+1) => a * hPow a n
-
-instance [Group α] : HPow α Nat α := ⟨hPow⟩
-
-def OrderN (n : Nat) (a : α) : Prop := a^n = 1
-
--- not defining the cardinality here for space reasons
-def card (α) [Group α] : Nat := sorry
-
--- This one should not go through! not an equality
-@[egg]
-theorem ex_min_order : ∃ n : Nat, OrderN n a ∧ (∀ n', n' < n → ¬ OrderN n a) := sorry
-
--- This should also be recognized as an equality
-@[egg]
-theorem card_order : OrderN (card α) a := by
-  sorry
-
-def Abelian (α) [Group α] : Prop := ∀ a b : α, a * b = b * a
-
-def commutator := a*b*a⁻¹*b⁻¹
-
--- Ideally, egg can see through this prop that there's an equality?
-@[egg]
-theorem all_commutators_trivial_abelian : (∀ a b : α, commutator a b = 1) → Abelian α := by sorry
-
-/-- We should not break egg after adding these lemmas -/
-example : a * b = b * a := by
-  egg
diff --git a/Lean/Egg/Tests/WIP_ValidateTagged.lean b/Lean/Egg/Tests/WIP_ValidateTagged.lean
new file mode 100644
index 0000000..3b4ecfc
--- /dev/null
+++ b/Lean/Egg/Tests/WIP_ValidateTagged.lean
@@ -0,0 +1,54 @@
+import Egg
+
+class One (α) where one : α
+instance [One α] : OfNat α 1 where ofNat := One.one
+
+class Inv (α) where inv : α → α
+postfix:max "⁻¹" => Inv.inv
+
+class Group (α) extends Mul α, One α, Inv α where
+  mul_assoc     (a b c : α) : (a * b) * c = a * (b * c)
+  one_mul       (a : α)     : 1 * a = a
+  mul_one       (a : α)     : a * 1 = a
+  inv_mul_self  (a : α)     : a⁻¹ * a = 1
+  mul_inv_self  (a : α)     : a * a⁻¹ = 1
+
+variable [Group α] (a b x y : α)
+
+attribute [egg] Group.mul_assoc
+attribute [egg] Group.one_mul
+attribute [egg] Group.mul_one
+attribute [egg] Group.inv_mul_self
+attribute [egg] Group.mul_inv_self
+
+def hPow : α → Nat → α
+    | _, 0 => 1
+    | a, (n+1) => a * hPow a n
+
+instance [Group α] : HPow α Nat α := ⟨hPow⟩
+
+def OrderN (n : Nat) (a : α) : Prop := a^n = 1
+
+-- not defining the cardinality here for space reasons
+def card (α) [Group α] : Nat := sorry
+
+-- This one should not go through! not an equality
+@[egg]
+theorem ex_min_order : ∃ n : Nat, OrderN n a ∧ (∀ n', n' < n → ¬ OrderN n a) := sorry
+
+-- This should also be recognized as an equality
+@[egg]
+theorem card_order : OrderN (card α) a := by
+  sorry
+
+def Abelian (α) [Group α] : Prop := ∀ a b : α, a * b = b * a
+
+def commutator := a*b*a⁻¹*b⁻¹
+
+-- Ideally, egg can see through this prop that there's an equality?
+@[egg]
+theorem all_commutators_trivial_abelian : (∀ a b : α, commutator a b = 1) → Abelian α := by sorry
+
+/-- We should not break egg after adding these lemmas -/
+example : a * b = b * a := by
+  egg

From 27f11e84b454b474fabf9af6315c8ee0ddc4ab34 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 3 Jun 2024 16:52:28 +0200
Subject: [PATCH 14/16] make freshman's dream work with tags

---
 Lean/Egg/Tests/Freshman.lean |  47 +++++++++-------
 README.md                    |   4 ++
 Rust/src/valid_match.rs      | 101 +++++++++++++++++++++--------------
 3 files changed, 94 insertions(+), 58 deletions(-)

diff --git a/Lean/Egg/Tests/Freshman.lean b/Lean/Egg/Tests/Freshman.lean
index ffa7fcc..27544bf 100644
--- a/Lean/Egg/Tests/Freshman.lean
+++ b/Lean/Egg/Tests/Freshman.lean
@@ -29,33 +29,44 @@ class CommRing (α) extends Zero α, One α, Add α, Sub α, Mul α, Div α, Pow
 class CharTwoRing (α) extends CommRing α where
   char_two (a : α) : a + a = 0
 
-open CommRing CharTwoRing Egg.Guides Egg.Config.Modifier in
-macro "char_two_ring" mod:egg_cfg_mod base:(egg_base)? guides:(egg_guides)? : tactic => `(tactic|
-  egg $mod [comm_add, comm_mul, add_assoc, mul_assoc, sub_canon, neg_add, div_canon, zero_add,
-  zero_mul, one_mul, distrib, pow_zero, pow_one, pow_two, pow_three, char_two] $[$base]? $[$guides]?
-)
+attribute [egg] CommRing.comm_add
+attribute [egg] CommRing.comm_mul
+attribute [egg] CommRing.add_assoc
+attribute [egg] CommRing.mul_assoc
+attribute [egg] CommRing.sub_canon
+attribute [egg] CommRing.neg_add
+attribute [egg] CommRing.div_canon
+attribute [egg] CommRing.zero_add
+attribute [egg] CommRing.zero_mul
+attribute [egg] CommRing.one_mul
+attribute [egg] CommRing.distrib
+attribute [egg] CommRing.pow_zero
+attribute [egg] CommRing.pow_one
+attribute [egg] CommRing.pow_two
+attribute [egg] CommRing.pow_three
+attribute [egg] CharTwoRing.char_two
 
 variable [CharTwoRing α] (x y : α)
 
 theorem freshmans_dream₂ : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
   calc (x + y) ^ 2
-   _ = (x + y) * (x + y)             := by char_two_ring
-   _ = x * (x + y) + y * (x + y)     := by char_two_ring
-   _ = x ^ 2 + x * y + y * x + y ^ 2 := by char_two_ring
-   _ = x ^ 2 + y ^ 2                 := by char_two_ring
+   _ = (x + y) * (x + y)             := by egg
+   _ = x * (x + y) + y * (x + y)     := by egg
+   _ = x ^ 2 + x * y + y * x + y ^ 2 := by egg
+   _ = x ^ 2 + y ^ 2                 := by egg
 
 theorem freshmans_dream₂' : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
-  char_two_ring
+  egg
 
 theorem freshmans_dream₃ : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
   calc (x + y) ^ 3
-   _ = (x + y) * (x + y) * (x + y)                     := by char_two_ring
-   _ = (x + y) * (x * (x + y) + y * (x + y))           := by char_two_ring
-   _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)       := by char_two_ring
-   _ = (x + y) * (x ^ 2 + y ^ 2)                       := by char_two_ring
-   _ = x * (x ^ 2 + y ^ 2) + y * (x ^ 2 + y ^ 2)       := by char_two_ring
-   _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2 := by char_two_ring
-   _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by char_two_ring
+   _ = (x + y) * (x + y) * (x + y)                     := by egg
+   _ = (x + y) * (x * (x + y) + y * (x + y))           := by egg
+   _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)       := by egg
+   _ = (x + y) * (x ^ 2 + y ^ 2)                       := by egg
+   _ = x * (x ^ 2 + y ^ 2) + y * (x ^ 2 + y ^ 2)       := by egg
+   _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2 := by egg
+   _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by egg
 
 theorem freshmans_dream₃' : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
-  char_two_ring
+  egg
diff --git a/README.md b/README.md
index d39bd2c..53c1adc 100644
--- a/README.md
+++ b/README.md
@@ -20,6 +20,8 @@ Then, add `import Egg` to the files that require `egg`.
 The syntax of `egg` is very similar to that of `simp` or `rw`:
 
 ```lean
+import Egg
+
 example : 0 = 0 := by
   egg
 
@@ -36,6 +38,8 @@ example (as bs : List α) : reverse (as ++ bs) = (reverse bs) ++ (reverse as) :=
 But you can use it to solve some equations which `simp` cannot:
 
 ```lean
+import Egg
+
 variable (a b c d : Int)
 
 example : ((a * b) - (2 * c)) * d - (a * b) = (d - 1) * (a * b) - (2 * c * d) := by
diff --git a/Rust/src/valid_match.rs b/Rust/src/valid_match.rs
index 7200dcd..0cf7827 100644
--- a/Rust/src/valid_match.rs
+++ b/Rust/src/valid_match.rs
@@ -1,47 +1,46 @@
-
-use std::collections::HashMap;
-use egg::*;
-use crate::lean_expr::*;
 use crate::analysis::*;
+use crate::lean_expr::*;
+use egg::*;
+use std::collections::HashMap;
 
 // An expression position is a sequence of coordinates which describe how to traverse nodes
-// starting at a given root node. Each coordinate dictates which child of a node to visit. 
+// starting at a given root node. Each coordinate dictates which child of a node to visit.
 // In an expression tree, each node has a unique position.
-type ExprPos = Vec<usize>; 
+type ExprPos = Vec<usize>;
 // A binder position of `None` indicates that the associated value does not appear under a binder.
 type BinderPos = Option<ExprPos>;
 
 // The given values are always used together in `match_is_valid_core`, so we given them a type.
 struct Location {
-    pos:           ExprPos,
-    parent_binder: BinderPos, 
-    binder_depth:  u64
+    pos: ExprPos,
+    parent_binder: BinderPos,
+    binder_depth: u64,
 }
 
 // Various data required for checking match validity.
 struct Context<'a> {
-    pat:            &'a PatternAst<LeanExpr>,
-    subst:          &'a Subst,
-    graph:          &'a LeanEGraph,
+    pat: &'a PatternAst<LeanExpr>,
+    subst: &'a Subst,
+    graph: &'a LeanEGraph,
     parent_binders: HashMap<Var, BinderPos>,
-    binder_depths:  HashMap<Var, u64>
+    binder_depths: HashMap<Var, u64>,
 }
 
-// This is the return type of `match_is_valid`. If the given match is invalid, 
-// the `Invalid` case is returned. If the given match is valid, a map is returned 
-// where each variable mapping to loose bound variables is assigned its binder depth. 
+// This is the return type of `match_is_valid`. If the given match is invalid,
+// the `Invalid` case is returned. If the given match is valid, a map is returned
+// where each variable mapping to loose bound variables is assigned its binder depth.
 // This information is need in `correct_bvar_indices`.
 pub enum MatchValidity {
     Invalid,
-    Valid(HashMap<Var, u64>)
+    Valid(HashMap<Var, u64>),
 }
 
 // A match (a substitution and pattern) is valid if both:
 // (1) No (non-loose) bound variables are matched.
-// (2) For each variable v in the substitution which maps to an e-class with loose bvars, 
+// (2) For each variable v in the substitution which maps to an e-class with loose bvars,
 //     v only appears under the same binder.
 //
-// Example of invalid matches: 
+// Example of invalid matches:
 // (1) Pattern term `(lam _, ?x)` matching against `(lam _, (bvar 0))`.
 // (2) Pattern term `(lam _ (lam _, ?x) ?x)` matching against `(lam _ (lam _, (bvar 2)) (bvar 2))`.
 //
@@ -49,11 +48,25 @@ pub enum MatchValidity {
 // the fact that our rewrites come from theorems of the form `forall x, y = z`. Thus, if a pattern
 // variable appears, it can never refer to a (non-loose) bound variable, as `x` cannot refer to any
 // bound variables in `y` or `z`.
-pub fn match_is_valid(subst: &Subst, pat: &PatternAst<LeanExpr>, graph: &LeanEGraph) -> MatchValidity {
-    let mut ctx = Context { pat, subst, graph, parent_binders: HashMap::new(), binder_depths: HashMap::new() };
+pub fn match_is_valid(
+    subst: &Subst,
+    pat: &PatternAst<LeanExpr>,
+    graph: &LeanEGraph,
+) -> MatchValidity {
+    let mut ctx = Context {
+        pat,
+        subst,
+        graph,
+        parent_binders: HashMap::new(),
+        binder_depths: HashMap::new(),
+    };
     let root_idx = pat.as_ref().len() - 1;
-    let loc = Location { pos: vec![], parent_binder: None, binder_depth: 0 };
-    
+    let loc = Location {
+        pos: vec![],
+        parent_binder: None,
+        binder_depth: 0,
+    };
+
     if match_is_valid_core(root_idx, loc, &mut ctx) {
         MatchValidity::Valid(ctx.binder_depths)
     } else {
@@ -65,43 +78,51 @@ fn match_is_valid_core(idx: usize, loc: Location, ctx: &mut Context) -> bool {
     match &ctx.pat.as_ref()[idx] {
         ENodeOrVar::Var(var) => {
             let loose_bvars = &ctx.graph[ctx.subst[*var]].data.loose_bvars;
-            if loose_bvars.is_empty() { 
+            if loose_bvars.is_empty() {
                 // If the given variable does not map to an e-class containing loose bvars, if cannot cause any problems.
-                return true 
+                return true;
             } else {
                 // If the given variable maps to an e-class containing loose bvars, we need to check Conditions (1) and (2).
 
-                // For Condition (1): If the variable maps to an e-class containing bound variables whose indices are 
+                // For Condition (1): If the variable maps to an e-class containing bound variables whose indices are
                 // exceeded by the current binder depth, then those bound variables must be non-loose in the context
                 // of `ctx.pat`, and are not allowed to be matched.
-                if loose_bvars.iter().any(|b| *b < loc.binder_depth) { return false }
+                if loose_bvars.iter().any(|b| *b < loc.binder_depth) {
+                    return false;
+                }
 
                 if let Some(required_parent) = ctx.parent_binders.get(var) {
-                    // For Condition (2): If the variable has already occured elsewhere in the pattern, 
+                    // For Condition (2): If the variable has already occured elsewhere in the pattern,
                     // then the parent binder of that occurrence must be the same as the current parent binder.
-                    return loc.parent_binder == *required_parent
+                    return loc.parent_binder == *required_parent;
                 } else {
                     // If the given variable has not been visited yet, record its parent binder and binder depth.
                     ctx.parent_binders.insert(*var, loc.parent_binder);
                     ctx.binder_depths.insert(*var, loc.binder_depth);
-                    return true
+                    return true;
                 }
             }
-        },
+        }
         ENodeOrVar::ENode(e) => {
             for (i, child) in e.children().iter().enumerate() {
                 // If `e` is a binder, set the parent binder and increase the binder depth for its body.
-                let (parent_binder, binder_depth) = 
-                    if e.is_binder() && i == 1 { 
-                        (Some(loc.pos.clone()), loc.binder_depth + 1) 
-                    } else { 
-                        (loc.parent_binder.clone(), loc.binder_depth) 
-                    };
-                let mut pos = loc.pos.clone(); pos.push(i);
-                let child_loc = Location { pos, parent_binder, binder_depth };
+                let (parent_binder, binder_depth) = if e.is_binder() && i == 1 {
+                    (Some(loc.pos.clone()), loc.binder_depth + 1)
+                } else {
+                    (loc.parent_binder.clone(), loc.binder_depth)
+                };
+                let mut pos = loc.pos.clone();
+                pos.push(i);
+                let child_loc = Location {
+                    pos,
+                    parent_binder,
+                    binder_depth,
+                };
 
                 let child_idx = usize::from(*child);
-                if !match_is_valid_core(child_idx, child_loc, ctx) { return false }
+                if !match_is_valid_core(child_idx, child_loc, ctx) {
+                    return false;
+                }
             }
             true
         }

From 48b20c5b58fcbfc01af401386122210c775abadd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 3 Jun 2024 16:53:16 +0200
Subject: [PATCH 15/16] Revert "make freshman's dream work with tags"

This reverts commit 27f11e84b454b474fabf9af6315c8ee0ddc4ab34.
---
 Lean/Egg/Tests/Freshman.lean |  47 +++++++---------
 README.md                    |   4 --
 Rust/src/valid_match.rs      | 101 ++++++++++++++---------------------
 3 files changed, 58 insertions(+), 94 deletions(-)

diff --git a/Lean/Egg/Tests/Freshman.lean b/Lean/Egg/Tests/Freshman.lean
index 27544bf..ffa7fcc 100644
--- a/Lean/Egg/Tests/Freshman.lean
+++ b/Lean/Egg/Tests/Freshman.lean
@@ -29,44 +29,33 @@ class CommRing (α) extends Zero α, One α, Add α, Sub α, Mul α, Div α, Pow
 class CharTwoRing (α) extends CommRing α where
   char_two (a : α) : a + a = 0
 
-attribute [egg] CommRing.comm_add
-attribute [egg] CommRing.comm_mul
-attribute [egg] CommRing.add_assoc
-attribute [egg] CommRing.mul_assoc
-attribute [egg] CommRing.sub_canon
-attribute [egg] CommRing.neg_add
-attribute [egg] CommRing.div_canon
-attribute [egg] CommRing.zero_add
-attribute [egg] CommRing.zero_mul
-attribute [egg] CommRing.one_mul
-attribute [egg] CommRing.distrib
-attribute [egg] CommRing.pow_zero
-attribute [egg] CommRing.pow_one
-attribute [egg] CommRing.pow_two
-attribute [egg] CommRing.pow_three
-attribute [egg] CharTwoRing.char_two
+open CommRing CharTwoRing Egg.Guides Egg.Config.Modifier in
+macro "char_two_ring" mod:egg_cfg_mod base:(egg_base)? guides:(egg_guides)? : tactic => `(tactic|
+  egg $mod [comm_add, comm_mul, add_assoc, mul_assoc, sub_canon, neg_add, div_canon, zero_add,
+  zero_mul, one_mul, distrib, pow_zero, pow_one, pow_two, pow_three, char_two] $[$base]? $[$guides]?
+)
 
 variable [CharTwoRing α] (x y : α)
 
 theorem freshmans_dream₂ : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
   calc (x + y) ^ 2
-   _ = (x + y) * (x + y)             := by egg
-   _ = x * (x + y) + y * (x + y)     := by egg
-   _ = x ^ 2 + x * y + y * x + y ^ 2 := by egg
-   _ = x ^ 2 + y ^ 2                 := by egg
+   _ = (x + y) * (x + y)             := by char_two_ring
+   _ = x * (x + y) + y * (x + y)     := by char_two_ring
+   _ = x ^ 2 + x * y + y * x + y ^ 2 := by char_two_ring
+   _ = x ^ 2 + y ^ 2                 := by char_two_ring
 
 theorem freshmans_dream₂' : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
-  egg
+  char_two_ring
 
 theorem freshmans_dream₃ : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
   calc (x + y) ^ 3
-   _ = (x + y) * (x + y) * (x + y)                     := by egg
-   _ = (x + y) * (x * (x + y) + y * (x + y))           := by egg
-   _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)       := by egg
-   _ = (x + y) * (x ^ 2 + y ^ 2)                       := by egg
-   _ = x * (x ^ 2 + y ^ 2) + y * (x ^ 2 + y ^ 2)       := by egg
-   _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2 := by egg
-   _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by egg
+   _ = (x + y) * (x + y) * (x + y)                     := by char_two_ring
+   _ = (x + y) * (x * (x + y) + y * (x + y))           := by char_two_ring
+   _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)       := by char_two_ring
+   _ = (x + y) * (x ^ 2 + y ^ 2)                       := by char_two_ring
+   _ = x * (x ^ 2 + y ^ 2) + y * (x ^ 2 + y ^ 2)       := by char_two_ring
+   _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2 := by char_two_ring
+   _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by char_two_ring
 
 theorem freshmans_dream₃' : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
-  egg
+  char_two_ring
diff --git a/README.md b/README.md
index 53c1adc..d39bd2c 100644
--- a/README.md
+++ b/README.md
@@ -20,8 +20,6 @@ Then, add `import Egg` to the files that require `egg`.
 The syntax of `egg` is very similar to that of `simp` or `rw`:
 
 ```lean
-import Egg
-
 example : 0 = 0 := by
   egg
 
@@ -38,8 +36,6 @@ example (as bs : List α) : reverse (as ++ bs) = (reverse bs) ++ (reverse as) :=
 But you can use it to solve some equations which `simp` cannot:
 
 ```lean
-import Egg
-
 variable (a b c d : Int)
 
 example : ((a * b) - (2 * c)) * d - (a * b) = (d - 1) * (a * b) - (2 * c * d) := by
diff --git a/Rust/src/valid_match.rs b/Rust/src/valid_match.rs
index 0cf7827..7200dcd 100644
--- a/Rust/src/valid_match.rs
+++ b/Rust/src/valid_match.rs
@@ -1,46 +1,47 @@
-use crate::analysis::*;
-use crate::lean_expr::*;
-use egg::*;
+
 use std::collections::HashMap;
+use egg::*;
+use crate::lean_expr::*;
+use crate::analysis::*;
 
 // An expression position is a sequence of coordinates which describe how to traverse nodes
-// starting at a given root node. Each coordinate dictates which child of a node to visit.
+// starting at a given root node. Each coordinate dictates which child of a node to visit. 
 // In an expression tree, each node has a unique position.
-type ExprPos = Vec<usize>;
+type ExprPos = Vec<usize>; 
 // A binder position of `None` indicates that the associated value does not appear under a binder.
 type BinderPos = Option<ExprPos>;
 
 // The given values are always used together in `match_is_valid_core`, so we given them a type.
 struct Location {
-    pos: ExprPos,
-    parent_binder: BinderPos,
-    binder_depth: u64,
+    pos:           ExprPos,
+    parent_binder: BinderPos, 
+    binder_depth:  u64
 }
 
 // Various data required for checking match validity.
 struct Context<'a> {
-    pat: &'a PatternAst<LeanExpr>,
-    subst: &'a Subst,
-    graph: &'a LeanEGraph,
+    pat:            &'a PatternAst<LeanExpr>,
+    subst:          &'a Subst,
+    graph:          &'a LeanEGraph,
     parent_binders: HashMap<Var, BinderPos>,
-    binder_depths: HashMap<Var, u64>,
+    binder_depths:  HashMap<Var, u64>
 }
 
-// This is the return type of `match_is_valid`. If the given match is invalid,
-// the `Invalid` case is returned. If the given match is valid, a map is returned
-// where each variable mapping to loose bound variables is assigned its binder depth.
+// This is the return type of `match_is_valid`. If the given match is invalid, 
+// the `Invalid` case is returned. If the given match is valid, a map is returned 
+// where each variable mapping to loose bound variables is assigned its binder depth. 
 // This information is need in `correct_bvar_indices`.
 pub enum MatchValidity {
     Invalid,
-    Valid(HashMap<Var, u64>),
+    Valid(HashMap<Var, u64>)
 }
 
 // A match (a substitution and pattern) is valid if both:
 // (1) No (non-loose) bound variables are matched.
-// (2) For each variable v in the substitution which maps to an e-class with loose bvars,
+// (2) For each variable v in the substitution which maps to an e-class with loose bvars, 
 //     v only appears under the same binder.
 //
-// Example of invalid matches:
+// Example of invalid matches: 
 // (1) Pattern term `(lam _, ?x)` matching against `(lam _, (bvar 0))`.
 // (2) Pattern term `(lam _ (lam _, ?x) ?x)` matching against `(lam _ (lam _, (bvar 2)) (bvar 2))`.
 //
@@ -48,25 +49,11 @@ pub enum MatchValidity {
 // the fact that our rewrites come from theorems of the form `forall x, y = z`. Thus, if a pattern
 // variable appears, it can never refer to a (non-loose) bound variable, as `x` cannot refer to any
 // bound variables in `y` or `z`.
-pub fn match_is_valid(
-    subst: &Subst,
-    pat: &PatternAst<LeanExpr>,
-    graph: &LeanEGraph,
-) -> MatchValidity {
-    let mut ctx = Context {
-        pat,
-        subst,
-        graph,
-        parent_binders: HashMap::new(),
-        binder_depths: HashMap::new(),
-    };
+pub fn match_is_valid(subst: &Subst, pat: &PatternAst<LeanExpr>, graph: &LeanEGraph) -> MatchValidity {
+    let mut ctx = Context { pat, subst, graph, parent_binders: HashMap::new(), binder_depths: HashMap::new() };
     let root_idx = pat.as_ref().len() - 1;
-    let loc = Location {
-        pos: vec![],
-        parent_binder: None,
-        binder_depth: 0,
-    };
-
+    let loc = Location { pos: vec![], parent_binder: None, binder_depth: 0 };
+    
     if match_is_valid_core(root_idx, loc, &mut ctx) {
         MatchValidity::Valid(ctx.binder_depths)
     } else {
@@ -78,51 +65,43 @@ fn match_is_valid_core(idx: usize, loc: Location, ctx: &mut Context) -> bool {
     match &ctx.pat.as_ref()[idx] {
         ENodeOrVar::Var(var) => {
             let loose_bvars = &ctx.graph[ctx.subst[*var]].data.loose_bvars;
-            if loose_bvars.is_empty() {
+            if loose_bvars.is_empty() { 
                 // If the given variable does not map to an e-class containing loose bvars, if cannot cause any problems.
-                return true;
+                return true 
             } else {
                 // If the given variable maps to an e-class containing loose bvars, we need to check Conditions (1) and (2).
 
-                // For Condition (1): If the variable maps to an e-class containing bound variables whose indices are
+                // For Condition (1): If the variable maps to an e-class containing bound variables whose indices are 
                 // exceeded by the current binder depth, then those bound variables must be non-loose in the context
                 // of `ctx.pat`, and are not allowed to be matched.
-                if loose_bvars.iter().any(|b| *b < loc.binder_depth) {
-                    return false;
-                }
+                if loose_bvars.iter().any(|b| *b < loc.binder_depth) { return false }
 
                 if let Some(required_parent) = ctx.parent_binders.get(var) {
-                    // For Condition (2): If the variable has already occured elsewhere in the pattern,
+                    // For Condition (2): If the variable has already occured elsewhere in the pattern, 
                     // then the parent binder of that occurrence must be the same as the current parent binder.
-                    return loc.parent_binder == *required_parent;
+                    return loc.parent_binder == *required_parent
                 } else {
                     // If the given variable has not been visited yet, record its parent binder and binder depth.
                     ctx.parent_binders.insert(*var, loc.parent_binder);
                     ctx.binder_depths.insert(*var, loc.binder_depth);
-                    return true;
+                    return true
                 }
             }
-        }
+        },
         ENodeOrVar::ENode(e) => {
             for (i, child) in e.children().iter().enumerate() {
                 // If `e` is a binder, set the parent binder and increase the binder depth for its body.
-                let (parent_binder, binder_depth) = if e.is_binder() && i == 1 {
-                    (Some(loc.pos.clone()), loc.binder_depth + 1)
-                } else {
-                    (loc.parent_binder.clone(), loc.binder_depth)
-                };
-                let mut pos = loc.pos.clone();
-                pos.push(i);
-                let child_loc = Location {
-                    pos,
-                    parent_binder,
-                    binder_depth,
-                };
+                let (parent_binder, binder_depth) = 
+                    if e.is_binder() && i == 1 { 
+                        (Some(loc.pos.clone()), loc.binder_depth + 1) 
+                    } else { 
+                        (loc.parent_binder.clone(), loc.binder_depth) 
+                    };
+                let mut pos = loc.pos.clone(); pos.push(i);
+                let child_loc = Location { pos, parent_binder, binder_depth };
 
                 let child_idx = usize::from(*child);
-                if !match_is_valid_core(child_idx, child_loc, ctx) {
-                    return false;
-                }
+                if !match_is_valid_core(child_idx, child_loc, ctx) { return false }
             }
             true
         }

From 2e0fdb3a2f777e88bdba8a0e608bc65c3dbe9c77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Mon, 3 Jun 2024 16:53:40 +0200
Subject: [PATCH 16/16] add a version of Freshman's dream with tags

---
 Lean/Egg/Tests/FreshmanTags.lean | 71 ++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)
 create mode 100644 Lean/Egg/Tests/FreshmanTags.lean

diff --git a/Lean/Egg/Tests/FreshmanTags.lean b/Lean/Egg/Tests/FreshmanTags.lean
new file mode 100644
index 0000000..45d3863
--- /dev/null
+++ b/Lean/Egg/Tests/FreshmanTags.lean
@@ -0,0 +1,71 @@
+import Egg
+
+class Inv (α) where inv : α → α
+postfix:max "⁻¹" => Inv.inv
+
+class Zero (α) where zero : α
+instance [Zero α] : OfNat α 0 where ofNat := Zero.zero
+
+class One (α) where one : α
+instance [One α] : OfNat α 1 where ofNat := One.one
+
+class CommRing (α) extends Zero α, One α, Add α, Sub α, Mul α, Div α, Pow α Nat, Inv α, Neg α where
+  comm_add  (a b : α)   : a + b = b + a
+  comm_mul  (a b : α)   : a * b = b * a
+  add_assoc (a b c : α) : a + (b + c) = (a + b) + c
+  mul_assoc (a b c : α) : a * (b * c) = (a * b) * c
+  sub_canon (a b : α)   : a - b = a + -b
+  neg_add   (a : α)     : a + -a = 0
+  div_canon (a b : α)   : a / b = a * b⁻¹
+  zero_add  (a : α)     : a + 0 = a
+  zero_mul  (a : α)     : a * 0 = 0
+  one_mul   (a : α)     : a * 1 = a
+  distrib   (a b c : α) : a * (b + c) = (a * b) + (a * c)
+  pow_zero  (a : α)     : a ^ 0 = 1
+  pow_one   (a : α)     : a ^ 1 = a
+  pow_two   (a : α)     : a ^ 2 = (a ^ 1) * a
+  pow_three (a : α)     : a ^ 3 = (a ^ 2) * a
+
+attribute [egg] CommRing.comm_add
+attribute [egg] CommRing.comm_mul
+attribute [egg] CommRing.add_assoc
+attribute [egg] CommRing.mul_assoc
+attribute [egg] CommRing.sub_canon
+attribute [egg] CommRing.neg_add
+attribute [egg] CommRing.div_canon
+attribute [egg] CommRing.zero_add
+attribute [egg] CommRing.zero_mul
+attribute [egg] CommRing.one_mul
+attribute [egg] CommRing.distrib
+attribute [egg] CommRing.pow_zero
+attribute [egg] CommRing.pow_one
+attribute [egg] CommRing.pow_two
+attribute [egg] CommRing.pow_three
+
+class CharTwoRing (α) extends CommRing α where
+  char_two (a : α) : a + a = 0
+
+variable [CharTwoRing α] (x y : α)
+
+theorem freshmans_dream₂ : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
+  egg calc (x + y) ^ 2
+   _ = (x + y) * (x + y)
+   _ = x * (x + y) + y * (x + y)
+   _ = x ^ 2 + x * y + y * x + y ^ 2
+   _ = x ^ 2 + y ^ 2  with [CharTwoRing.char_two]
+
+theorem freshmans_dream₂' : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
+  egg [CharTwoRing.char_two]
+
+theorem freshmans_dream₃ : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+  egg calc [CharTwoRing.char_two] (x + y) ^ 3
+   _ = (x + y) * (x + y) * (x + y)
+   _ = (x + y) * (x * (x + y) + y * (x + y))
+   _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)
+   _ = (x + y) * (x ^ 2 + y ^ 2)
+   _ = x * (x ^ 2 + y ^ 2) + y * (x ^ 2 + y ^ 2)
+   _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2
+   _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3
+
+theorem freshmans_dream₃' : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+  egg [CharTwoRing.char_two]