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

feat: add simpLocalDecl

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-17 13:40:41 -07:00
parent 52b52b22ef
commit 4cfbe6030f
2 changed files with 30 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -181,7 +181,7 @@ private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ign
where
go (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : FVarIdToLemmaId) : TacticM Unit := do
liftMetaTactic1 fun mvarId =>
simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
return (← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)).map (·.2)
@[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (ctx := true) (ignoreStarArg := true)

46
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -414,26 +414,38 @@ def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context)
else
return some (proof, r.expr)
abbrev FVarIdToLemmaId := NameMap Name
def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option MVarId) := do
let mut mvarId := mvarId
let mut toAssert : Array Hypothesis := #[]
for fvarId in fvarIdsToSimp do
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM (Option (FVarId × MVarId)) := do
withMVarContext mvarId do
let localDecl ← getLocalDecl fvarId
let type ← instantiateMVars localDecl.type
let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
| none => pure ctx
| some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
| none => return none
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
if simplifyTarget then
match (← simpTarget mvarId ctx discharge?) with
| none => return none
| some mvarIdNew => mvarId := mvarIdNew
let (_, mvarIdNew) ← assertHypotheses mvarId toAssert
let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
return mvarIdNew
| some (value, type) =>
let mvarId ← assert mvarId localDecl.userName type value
let mvarId ← tryClear mvarId localDecl.fvarId
return some (fvarId, mvarId)
abbrev FVarIdToLemmaId := NameMap Name
def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option (Array FVarId × MVarId)) := do
withMVarContext mvarId do
let mut mvarId := mvarId
let mut toAssert : Array Hypothesis := #[]
for fvarId in fvarIdsToSimp do
let localDecl ← getLocalDecl fvarId
let type ← instantiateMVars localDecl.type
let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
| none => pure ctx
| some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
| none => return none
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
if simplifyTarget then
match (← simpTarget mvarId ctx discharge?) with
| none => return none
| some mvarIdNew => mvarId := mvarIdNew
let (fvarIdsNew, mvarIdNew) ← assertHypotheses mvarId toAssert
let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
return (fvarIdsNew, mvarIdNew)
end Lean.Meta