max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: make sure register_simp_attr declares an simp-like attribute parser for user simp attributes

Browse source 
closes #1164
This commit is contained in:
Leonardo de Moura 2022-05-26 19:49:33 -07:00
parent 7d8f8c0fbe
commit 3be437cad3
2 changed files with 32 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
View file

@ -411,7 +411,11 @@ def SimpTheoremsArray.isErased (thmsArray : SimpTheoremsArray) (thmId : Name) :
def SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName : Name) : Bool :=
thmsArray.any fun thms => thms.isDeclToUnfold declName
macro "register_simp_attr" id:ident descr:str : command => `(initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr)
macro "register_simp_attr" id:ident descr:str : command => do
let str := id.getId.toString
let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
`(initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr
syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr)
end Meta

27
tests/pkg/user_attr/UserAttr/Tst.lean
View file

@ -1,3 +1,4 @@
import Lean
import UserAttr.BlaAttr
@[bla] def f (x : Nat) := x + 2
@ -21,3 +22,29 @@ macro "my_simp" : tactic => `(simp [my_simp])
example : f x = id (x + 2) := by
my_simp
@[simp low, my_simp low]
theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry
@[simp high, my_simp high]
theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry
@[simp, my_simp]
theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry
set_option trace.Meta.Tactic.simp.rewrite true
-- Rewrites: expand_mul_add -> expand_mul_add -> lassoc_add
theorem ex1 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by simp only [my_simp]
-- Rewrites: expand_add_mul -> expand_mul_add -> lassoc_add
theorem ex2 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by simp
open Lean
open Lean.Meta
def checkProofs : MetaM Unit := do
let ConstantInfo.thmInfo info1 ← getConstInfo `ex1 | throwError "unexpected"
let ConstantInfo.thmInfo info2 ← getConstInfo `ex2 | throwError "unexpected"
unless info1.value == info2.value do
throwError "unexpected values"
#eval checkProofs