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
40 lines
1.2 KiB
Text
40 lines
1.2 KiB
Text
/-
|
|
Tests for `Sym.simp` theorem set attributes.
|
|
-/
|
|
module
|
|
|
|
import SymSimpAttr.Decl
|
|
public meta import Lean.Elab.Tactic.Basic
|
|
public meta import Lean.Meta.Sym
|
|
|
|
open Lean Elab Tactic Meta
|
|
|
|
-- Add a proposition as a rewrite theorem
|
|
@[my_sym_simp] theorem add_zero_nat (a : Nat) : a + 0 = a := Nat.add_zero a
|
|
|
|
-- Add a definition (equation theorems)
|
|
@[my_sym_simp] def myAdd : Nat → Nat → Nat
|
|
| 0, b => b
|
|
| a + 1, b => (myAdd a b) + 1
|
|
|
|
-- Tactic that uses the theorem set
|
|
elab "sym_simp_set" "[" id:ident "]" : tactic => do
|
|
let some ext ← Sym.Simp.getSymSimpExtension? id.getId
|
|
| throwError "Unknown Sym.simp set: {id.getId}"
|
|
let thms ← ext.getTheorems
|
|
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_set [my_sym_simp]
|
|
|
|
-- Test: rewrite theorem from the set
|
|
example (n : Nat) : n + 0 = n := by sym_simp_set [my_sym_simp]
|
|
|
|
-- Test: equation theorems from definition
|
|
example : myAdd 3 2 = 5 := by sym_simp_set [my_sym_simp]
|