973062e4e1
This PR adds named theorem sets for `Sym.simp` with associated attributes, following the same pattern as `Meta.simp`'s `register_simp_attr`. - `register_sym_simp_attr my_set` creates a named set with its own `PersistentEnvExtension` and attribute - `@[my_set] theorem ...` adds a rewrite theorem - `@[my_set] def ...` adds equation theorems from the definition - `builtin_initialize symSimpExtension` registers a default `@[sym_simp]` set - `getSymSimpTheorems` / `getSymSimpExtension?` retrieve theorem sets at tactic time New files: - `Sym/Simp/Attr.lean`: attribute logic (`mkSymSimpAttr`, `registerSymSimpAttr`) - `Sym/Simp/RegisterCommand.lean`: `register_sym_simp_attr` macro Tests: - `tests/pkg/sym_simp_attr/`: package test with user-defined set (`my_sym_simp`) - `tests/elab/sym_simp_set.lean`: tests for the builtin `@[sym_simp]` set
38 lines
No EOL
1.1 KiB
Text
38 lines
No EOL
1.1 KiB
Text
/-
|
|
Tests for the builtin `@[sym_simp]` attribute.
|
|
-/
|
|
import Lean
|
|
|
|
open Lean Elab Tactic Meta
|
|
|
|
-- Add rewrite theorems to the default set
|
|
@[sym_simp] theorem add_zero_nat (a : Nat) : a + 0 = a := Nat.add_zero a
|
|
@[sym_simp] theorem zero_add_nat (a : Nat) : 0 + a = a := Nat.zero_add a
|
|
|
|
-- Add a definition (equation theorems)
|
|
@[sym_simp] def myMul : Nat → Nat → Nat
|
|
| 0, _ => 0
|
|
| a + 1, b => b + myMul a b
|
|
|
|
-- Tactic that uses the default sym_simp set
|
|
elab "sym_simp_default" : tactic => do
|
|
let thms ← Sym.Simp.getSymSimpTheorems
|
|
let rewrite := thms.rewrite
|
|
let methods : Sym.Simp.Methods := {
|
|
post := Sym.Simp.evalGround.andThen rewrite
|
|
}
|
|
liftMetaTactic1 fun mvarId => Sym.SymM.run do
|
|
let mvarId ← Sym.preprocessMVar mvarId
|
|
(← Sym.simpGoal mvarId methods).toOption
|
|
|
|
-- Test: ground evaluation
|
|
example : 2 + 3 = 5 := by sym_simp_default
|
|
|
|
-- Test: rewrite theorem
|
|
example (n : Nat) : n + 0 = n := by sym_simp_default
|
|
|
|
-- Test: both rewrite theorems
|
|
example (n : Nat) : 0 + n + 0 = n := by sym_simp_default
|
|
|
|
-- Test: equation theorems from definition
|
|
example : myMul 3 2 = 6 := by sym_simp_default |