test: grind homomorphism demo (#13497)

This PR adds an example for the Lean hackathon in Paris. It demonstrates
how users can implement https://hackmd.io/Qd0nkWdzQImVe7TDGSAGbA

tests/pkg/homo/Homo.lean

@@ -0,0 +1,25 @@
+import Homo.Init
+
+set_option warn.sorry false
+
+opaque TSpec : (α : Type) × α := ⟨Unit, ()⟩
+abbrev T : Type := TSpec.1
+instance : Inhabited T := ⟨TSpec.2⟩
+opaque add : T → T → T
+opaque le : T → T → Prop
+opaque pos : T → Prop
+opaque small : T → Prop
+opaque f : Nat → T
+opaque toInt : T → Int
+
+@[grind_homo] theorem T.eq (a b : T) : a = b ↔ toInt a = toInt b := sorry
+@[grind_homo] theorem T.le (a b : T) : le a b ↔ toInt a ≤ toInt b := sorry
+@[grind_homo] theorem T.pos (a : T) : pos a ↔ toInt a > 0 := sorry
+@[grind_homo] theorem T.small (a : T) : small a ↔ toInt a < 8 := sorry
+@[grind_homo] theorem T.add (a b : T) : toInt (add a b) = (toInt a + toInt b) % 128 := sorry
+@[grind_homo] theorem cleanLeft (a b n : Int) : (a % n + b) % n = (a + b) % n := by simp
+@[grind_homo] theorem cleanRight (a b n : Int) : (a + b % n) % n = (a + b) % n := by simp
+
+set_option trace.homo true
+example (b : T) : pos b → small b → le b (add b b) := by
+  grind

tests/pkg/homo/Homo/Init.lean

@@ -0,0 +1,96 @@
+module
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Sym.Simp.Attr
+import Lean.Meta.Sym.Simp.Simproc
+import Lean.Meta.Sym.Simp.Rewrite
+import Lean.Meta.AppBuilder
+
+namespace Homomorphism
+
+open Lean Meta Grind Sym Simp
+
+initialize registerTraceClass `homo
+initialize registerTraceClass `homo.visit
+
+/--
+Declares attribute `[grind_mono]` for marking theorems implementing the homomorphism.
+-/
+initialize homoSimpExtension : SymSimpExtension ←
+  registerSymSimpAttr `grind_homo "`grind` homomorphism attribute"
+
+/--
+Returns theorems marked with `[grind_mono]`
+-/
+def getTheorems : CoreM Theorems :=
+  homoSimpExtension.getTheorems
+
+/--
+Creates a simproc that applies the theorems marked with `[grind_mono]`.
+This simproc is meant to be applied as a `pre` method.
+
+Recall that `grind` internalizes terms bottom-up. By the time a
+simplification set runs on a term `e`, all subterms of `e` are already
+in the E-graph and have been processed by the pipeline.
+
+**Stop condition.** When simp encounters a term `t` during traversal:
+
+- If a rule matches `t`: apply it, continue (result is a new term).
+- If no rule matches `t` AND `t` is already in the E-graph:
+  stop, don't descend. Otherwise: descend normally.
+-/
+def mkRewriter : GoalM Sym.Simp.Simproc := do
+  let s ← get
+  -- Remark: We are not using any discharger. So, our rewriting rules are all context
+  -- independent.
+  let rw := (← getTheorems).rewrite
+  return fun e => do
+    trace[homo.visit] "{e}"
+    let r ← rw e
+    if !r.isRfl then return r
+    -- If `e` is already in the E-graph, we don't revisit its children
+    let done := s.enodeMap.contains { expr := e }
+    return .rfl (done := done)
+
+structure State where
+  cache : Sym.Simp.Cache := {}
+
+initialize homoExt : SolverExtension Sym.Simp.Cache ←
+  registerSolverExtension (return {})
+
+/-- Apply the homomorphism theorems. -/
+def applyHomo (e : Expr) : GoalM Sym.Simp.Result := do
+  let methods := { pre := (← mkRewriter) }
+  -- Reuse cache.
+  let persistentCache ← homoExt.getState
+  homoExt.modifyState fun _ => {} -- Improve uniqueness. This is a minor optimization
+  let (r, s) ← Sym.Simp.SimpM.run (Sym.Simp.simp e) (methods := methods) (s := { persistentCache })
+  homoExt.modifyState fun _ => s.persistentCache
+  return r
+
+/--
+Returns `true` if some theorem marked with `[grind_homo]` is applicable to `e`.
+
+Motivation: we don't want to start the simplifier and fail immediately.
+-/
+def isTarget (e : Expr) : CoreM Bool := do
+  let thms ← getTheorems
+  return !(thms.getMatch e).isEmpty
+
+/--
+Internalization procedure for this module. See `homoExt.setMethods`
+-/
+def internalize (e : Expr) (_ : Option Expr) : GoalM Unit := do
+  unless (← isTarget e) do return ()
+  let .step e₁ h₁ _ ← applyHomo e | return ()
+  let r ← preprocess e₁
+  let h ← mkEqTrans h₁ (← r.getProof)
+  let gen ← getGeneration e
+  Grind.internalize r.expr gen
+  trace[homo] "{e}\n====>\n{r.expr}"
+  pushEq e r.expr h
+
+initialize
+  homoExt.setMethods
+    (internalize := internalize)
+
+end Homomorphism

tests/pkg/homo/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package homo
+@[default_target] lean_lib Homo

tests/pkg/homo/lean-toolchain

@@ -0,0 +1 @@
+../../../build/release/stage1

tests/pkg/homo/run_test.sh

@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build