9a3678935d
This PR adds validation to the `register_sym_simp` command: - Reject duplicate variant names - Validate `pre`/`post` syntax by elaborating them via `elabSymSimproc` in a minimal `GrindTacticM` context, catching unknown theorem names and unknown theorem set references at registration time Adds `withGrindTacticM` helper for running `GrindTacticM` from `CommandElabM`, and `validateOptionSimprocSyntax` for optional syntax validation. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
139 lines
3.5 KiB
Text
139 lines
3.5 KiB
Text
import Lean
|
|
|
|
/-! Tests for interactive `simp` tactic in `sym =>` mode -/
|
|
|
|
theorem test_zero_add : 0 + n = n := Nat.zero_add n
|
|
theorem test_add_zero : n + 0 = n := Nat.add_zero n
|
|
|
|
/-! ## Test 1: `simp` with named variant -/
|
|
|
|
register_sym_simp testNatSimp where
|
|
post := rewrite [test_zero_add, test_add_zero]
|
|
|
|
example (x : Nat) : 0 + x = x := by
|
|
sym =>
|
|
simp testNatSimp
|
|
tactic => rfl
|
|
|
|
/-! ## Test 2: named variant simplifies compound expression -/
|
|
|
|
example (x : Nat) : 0 + (x + 0) = x := by
|
|
sym =>
|
|
simp testNatSimp
|
|
tactic => rfl
|
|
|
|
/-! ## Test 3: named variant with extra theorems -/
|
|
|
|
theorem test_succ_add : Nat.succ n + m = Nat.succ (n + m) := Nat.succ_add n m
|
|
|
|
example (x : Nat) : 0 + (Nat.succ 0 + x) = Nat.succ (0 + x) := by
|
|
sym =>
|
|
simp testNatSimp [test_succ_add]
|
|
tactic => rfl
|
|
|
|
/-! ## Test 4: variant with ground evaluation (closes goal) -/
|
|
|
|
register_sym_simp groundSimp where
|
|
post := ground
|
|
|
|
example : (3 + 4 : Nat) = 7 := by
|
|
sym =>
|
|
simp groundSimp
|
|
|
|
/-! ## Test 5: variant with pre and post (ground in pre closes via evalGround in default) -/
|
|
|
|
register_sym_simp prePostSimp where
|
|
pre := ground
|
|
post := rewrite [test_zero_add]
|
|
|
|
example (x : Nat) : 0 + x = x := by
|
|
sym =>
|
|
simp prePostSimp
|
|
|
|
/-! ## Test 6: bare `simp` uses default methods (with `@[sym_simp]` set) -/
|
|
|
|
attribute [sym_simp] test_zero_add
|
|
|
|
example (x : Nat) : 0 + x = x := by
|
|
sym =>
|
|
simp
|
|
|
|
/-! ## Test 7: unknown variant produces error -/
|
|
|
|
/--
|
|
error: unknown Sym.simp variant `nonExistent`
|
|
-/
|
|
#guard_msgs in
|
|
example (x : Nat) : 0 + x = x := by
|
|
sym =>
|
|
simp nonExistent
|
|
|
|
/-! ## Test 8: `simp` with `>>` combinator in variant -/
|
|
|
|
register_sym_simp chainSimp where
|
|
post := ground >> rewrite [test_zero_add]
|
|
|
|
example (x : Nat) : 0 + x = x := by
|
|
sym =>
|
|
simp chainSimp
|
|
|
|
/-! ## Test 9: repeated simp shares cache -/
|
|
|
|
example (x y : Nat) : 0 + x = x ∧ 0 + y = y := by
|
|
sym =>
|
|
apply And.intro
|
|
· simp testNatSimp; tactic => rfl
|
|
· simp testNatSimp; tactic => rfl
|
|
|
|
/-! ## Test 10: verify persistent cache is shared across `simp` invocations.
|
|
The second `simp` should hit the persistent cache for shared subterms like `0`.
|
|
Enable trace to confirm (run manually to inspect). -/
|
|
|
|
register_sym_simp simple where
|
|
post := ground >> rewrite [Nat.zero_add, Nat.add_zero, true_and, and_true]
|
|
|
|
/--
|
|
trace: [sym.simp.debug.cache] persistent cache hit: x
|
|
[sym.simp.debug.cache] persistent cache hit: x
|
|
[sym.simp.debug.cache] persistent cache hit: 0
|
|
[sym.simp.debug.cache] persistent cache hit: x
|
|
[sym.simp.debug.cache] persistent cache hit: f (f (f (f x)))
|
|
[sym.simp.debug.cache] persistent cache hit: f (f (f (f x)))
|
|
[sym.simp.debug.cache] persistent cache hit: y
|
|
[sym.simp.debug.cache] persistent cache hit: f (f (f (f x))) = y
|
|
---
|
|
trace: [sym.simp.debug.cache] persistent cache hit: f (f (f (f x))) = y
|
|
-/
|
|
#guard_msgs in
|
|
set_option trace.sym.simp.debug.cache true in
|
|
example (f : Nat → Nat) (x y : Nat) (h : f (f (f (f x))) = y) : 0 + x = x ∧ 0 + f (f (f (f x))) = y := by
|
|
sym =>
|
|
simp simple
|
|
try simp simple
|
|
apply h
|
|
|
|
/-! ## Test 11: duplicate variant name is rejected -/
|
|
|
|
/--
|
|
error: Sym.simp variant `simple` is already registered
|
|
-/
|
|
#guard_msgs in
|
|
register_sym_simp simple where
|
|
|
|
/-! ## Test 12: unknown theorem in `rewrite [...]` is rejected -/
|
|
|
|
/--
|
|
error: Unknown constant `bla`
|
|
-/
|
|
#guard_msgs in
|
|
register_sym_simp simple₁ where
|
|
pre := rewrite [bla]
|
|
|
|
/-! ## Test 13: unknown theorem set in `rewrite setName` is rejected -/
|
|
|
|
/--
|
|
error: unknown Sym.simp theorem set `boo`
|
|
-/
|
|
#guard_msgs in
|
|
register_sym_simp simple₃ where
|
|
pre := rewrite boo
|