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

fix: do not generate equation theorems while processing dsimp arguments

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-25 18:11:32 -07:00
parent 6bc5433b17
commit 3cf642688b
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Elab/Tactic/Simp.lean
View file

@ -86,7 +86,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.
| .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
| .dsimp => return { (← elabDSimpConfigCore optConfig) with }
private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post : Bool) (inv : Bool) : MetaM Meta.SimpTheorems := do
private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM Meta.SimpTheorems := do
if e.isConst then
let declName := e.constName!
let info ← getConstInfo declName
@ -95,7 +95,10 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post
else
if inv then
throwError "invalid '←' modifier, '{declName}' is a declaration name to be unfolded"
thms.addDeclToUnfold declName
if kind == .dsimp then
return thms.addDeclToUnfoldCore declName
else
thms.addDeclToUnfold declName
else
thms.add #[] e (post := post) (inv := inv)
@ -126,7 +129,7 @@ inductive ResolveSimpIdResult where
If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
this option only makes sense for `simp_all`.
-/
private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) : TacticM ElabSimpArgsResult := do
private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
if stx.isNone then
return { ctx }
else
@ -162,7 +165,7 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool)
let term := arg[2]
match (← resolveSimpIdTheorem? term) with
| .expr e => thms ← addDeclToUnfoldOrTheorem thms e post inv
| .expr e => thms ← addDeclToUnfoldOrTheorem thms e post inv kind
| .ext ext => thmsArray := thmsArray.push (← ext.getTheorems)
| .none => thms ← addSimpTheorem thms term post inv
else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
@ -215,7 +218,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
else
getSimpTheorems
let congrTheorems ← getSimpCongrTheorems
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) {
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
config := (← elabSimpConfig stx[1] (kind := kind))
simpTheorems := #[simpTheorems], congrTheorems
}