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

feat: track simp lemmas through the core tactics

Browse source
This commit is contained in:
Mario Carneiro 2022-09-19 20:00:05 -04:00 • committed by Leonardo de Moura
parent 687f1c2271
commit 0961561d4e
16 changed files with 105 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -42,7 +42,7 @@ where
go mvarId
else if let some mvarId ← whnfReducibleLHS? mvarId then
go mvarId
else match (← simpTargetStar mvarId {}) with
else match (← simpTargetStar mvarId {}).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId => go mvarId
| TacticResultCNM.noChange =>

4
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View file

@ -105,7 +105,7 @@ where
def simpMatchWF? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (mvarId : MVarId) : MetaM (Option MVarId) :=
mvarId.withContext do
let target ← instantiateMVars (← mvarId.getType)
let targetNew ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
if mvarId != mvarIdNew then return some mvarIdNew else return none
where
@ -169,7 +169,7 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
go mvarId
else if let some mvarId ← whnfReducibleLHS? mvarId then
go mvarId
else match (← simpTargetStar mvarId { config.dsimp := false }) with
else match (← simpTargetStar mvarId { config.dsimp := false }).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId => go mvarId
| TacticResultCNM.noChange =>

2
src/Lean/Elab/Tactic/Conv/Pattern.lean
View file

@ -48,7 +48,7 @@ private def pre (pattern : AbstractMVarsResult) (found? : IO.Ref (Option Expr))
private def findPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (MVarId × Simp.Result)) := do
let found? ← IO.mkRef none
let result ← Simp.main e (← getContext) (methods := { pre := pre pattern found? })
let (result, _) ← Simp.main e (← getContext) (methods := { pre := pre pattern found? })
if let some newGoal ← found?.get then
return some (newGoal.mvarId!, result)
else

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

@ -19,7 +19,7 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
@[builtinTactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => withMainContext do
let { ctx, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
let lhs ← getLhs
let result ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
applySimpResult result
@[builtinTactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do

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

@ -265,7 +265,7 @@ For many tactics other than the simplifier,
one should use the `withLocation` tactic combinator
when working with a `location`.
-/
def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (fvarIdToLemmaId : FVarIdToLemmaId := {}) (loc : Location) : TacticM Unit := do
def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (fvarIdToLemmaId : FVarIdToLemmaId := {}) (loc : Location) : TacticM NameSet := do
match loc with
| Location.targets hyps simplifyTarget =>
withMainContext do
@ -275,24 +275,25 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
withMainContext do
go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) fvarIdToLemmaId
where
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId) : TacticM NameSet := do
let mvarId ← getMainGoal
let result? ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp) (fvarIdToLemmaId := fvarIdToLemmaId)
match result? with
| none => replaceMainGoal []
| some (_, mvarId) => replaceMainGoal [mvarId]
return usedSimps
/-
"simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
-/
@[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
let { ctx, fvarIdToLemmaId, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
dischargeWrapper.with fun discharge? =>
discard <| dischargeWrapper.with fun discharge? =>
simpLocation ctx discharge? fvarIdToLemmaId (expandOptLocation stx[5])
@[builtinTactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
match (← simpAll (← getMainGoal) ctx) with
match (← simpAll (← getMainGoal) ctx).1 with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
@ -308,7 +309,7 @@ def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do
where
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
let mvarId ← getMainGoal
let result? ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
let (result?, _) ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]

2
src/Lean/Meta/Tactic/AC/Main.lean
View file

@ -145,7 +145,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
config := Simp.neutralConfig
}
let tgt ← instantiateMVars (← mvarId.getType)
let res ← Simp.main tgt simpCtx (methods := { post })
let (res, _) ← Simp.main tgt simpCtx (methods := { post })
let newGoal ← applySimpResultToTarget mvarId tgt res
newGoal.refl
where

2
src/Lean/Meta/Tactic/Acyclic.lean
View file

@ -37,7 +37,7 @@ where
let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
-- TODO: we only need the `sizeOf` simp theorems
match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }) with
match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }).1 with
| some _ => return false
| none =>
let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)

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

@ -165,7 +165,9 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
| some e => return (← reduce e)
| none => pure ()
match (← unfold? e) with
| some e => reduce e
| some e' =>
recordSimpTheorem e.getAppFn.constName!
reduce e'
| none => return e
private partial def dsimp (e : Expr) : M Expr := do
@ -687,18 +689,20 @@ where
modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
return r
def main (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Result := do
def main (e : Expr) (ctx : Context) (usedSimps : NameSet := {}) (methods : Methods := {}) : MetaM (Result × NameSet) := do
let ctx := { ctx with config := (← ctx.config.updateArith) }
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
try
simp e methods ctx |>.run' {}
let (r, s) ← simp e methods ctx |>.run { usedTheorems := usedSimps }
pure (r, s.usedTheorems)
catch ex =>
if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
def dsimpMain (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Expr := do
def dsimpMain (e : Expr) (ctx : Context) (usedSimps : NameSet := {}) (methods : Methods := {}) : MetaM (Expr × NameSet) := do
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
try
dsimp e methods ctx |>.run' {}
let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
pure (r, s.usedTheorems)
catch ex =>
if ex.isMaxHeartbeat then throwNestedTacticEx `dsimp ex else throw ex
@ -806,13 +810,15 @@ end DefaultMethods
end Simp
def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM Simp.Result := do profileitM Exception "simp" (← getOptions) do
def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(usedSimps : NameSet := {}) : MetaM (Simp.Result × NameSet) := do profileitM Exception "simp" (← getOptions) do
match discharge? with
| none => Simp.main e ctx (methods := Simp.DefaultMethods.methods)
| some d => Simp.main e ctx (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
| none => Simp.main e ctx usedSimps (methods := Simp.DefaultMethods.methods)
| some d => Simp.main e ctx usedSimps (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
def dsimp (e : Expr) (ctx : Simp.Context) : MetaM Expr := do profileitM Exception "dsimp" (← getOptions) do
Simp.dsimpMain e ctx (methods := Simp.DefaultMethods.methods)
def dsimp (e : Expr) (ctx : Simp.Context)
(usedSimps : NameSet := {}) : MetaM (Expr × NameSet) := do profileitM Exception "dsimp" (← getOptions) do
Simp.dsimpMain e ctx usedSimps (methods := Simp.DefaultMethods.methods)
/--
Auxiliary method.
@ -828,24 +834,26 @@ def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result)
return mvarId
/-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option MVarId) := do
def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) := do
let target ← instantiateMVars (← mvarId.getType)
let r ← simp target ctx discharge?
let (r, usedSimps) ← simp target ctx discharge? usedSimps
if mayCloseGoal && r.expr.isConstOf ``True then
match r.proof? with
| some proof => mvarId.assign (← mkOfEqTrue proof)
| none => mvarId.assign (mkConst ``True.intro)
return none
return (none, usedSimps)
else
applySimpResultToTarget mvarId target r
return (← applySimpResultToTarget mvarId target r, usedSimps)
/--
Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
where `mvarId'` is the simplified new goal. -/
def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option MVarId) :=
def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) :=
mvarId.withContext do
mvarId.checkNotAssigned `simp
simpTargetCore mvarId ctx discharge? mayCloseGoal
simpTargetCore mvarId ctx discharge? mayCloseGoal usedSimps
/--
Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@ -876,9 +884,10 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`.
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do
let r ← simp prop ctx discharge?
applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal)
def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option (Expr × Expr) × NameSet) := do
let (r, usedSimps) ← simp prop ctx discharge? usedSimps
return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
match r with
@ -908,87 +917,99 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
else
applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option (FVarId × MVarId)) := do
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (usedSimps : NameSet := {}) : MetaM (Option (FVarId × MVarId) × NameSet) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let type ← instantiateMVars (← fvarId.getType)
applySimpResultToLocalDeclCore mvarId fvarId (← simpStep mvarId (mkFVar fvarId) type ctx discharge? mayCloseGoal)
let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx discharge? mayCloseGoal usedSimps
return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
abbrev FVarIdToLemmaId := FVarIdMap 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
def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {})
(usedSimps : NameSet := {}) : MetaM (Option (Array FVarId × MVarId) × NameSet) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let mut mvarId := mvarId
let mut toAssert := #[]
let mut replaced := #[]
let mut usedSimps := usedSimps
for fvarId in fvarIdsToSimp do
let localDecl ← fvarId.getDecl
let type ← instantiateMVars localDecl.type
let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
| none => pure ctx
| some thmId => pure { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem thmId }
let r ← simp type ctx discharge?
let (r, usedSimps') ← simp type ctx discharge? usedSimps
usedSimps := usedSimps'
match r.proof? with
| some _ => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
| none => return none
| none => return (none, usedSimps)
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
| none =>
if r.expr.isConstOf ``False then
mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
return none
return (none, usedSimps)
-- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
-- Reason: it introduces a `mkExpectedTypeHint`
mvarId ← mvarId.replaceLocalDeclDefEq fvarId r.expr
replaced := replaced.push fvarId
if simplifyTarget then
match (← simpTarget mvarId ctx discharge?) with
| none => return none
| some mvarIdNew => mvarId := mvarIdNew
| (none, usedSimps') => return (none, usedSimps')
| (some mvarIdNew, usedSimps') => mvarId := mvarIdNew; usedSimps := usedSimps'
let (fvarIdsNew, mvarIdNew) ← mvarId.assertHypotheses toAssert
let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
let mvarIdNew ← mvarIdNew.tryClearMany toClear
return (fvarIdsNew, mvarIdNew)
return (some (fvarIdsNew, mvarIdNew), usedSimps)
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := mvarId.withContext do
def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
(usedSimps : NameSet := {}) : MetaM (TacticResultCNM × NameSet) := mvarId.withContext do
let mut ctx := ctx
for h in (← getPropHyps) do
let localDecl ← h.getDecl
let proof := localDecl.toExpr
let simpTheorems ← ctx.simpTheorems.addTheorem localDecl.fvarId.name proof
ctx := { ctx with simpTheorems }
match (← simpTarget mvarId ctx discharge?) with
| none => return TacticResultCNM.closed
| some mvarId' =>
match (← simpTarget mvarId ctx discharge? (usedSimps := usedSimps)) with
| (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
| (some mvarId', usedSimps') =>
if (← mvarId.getType) == (← mvarId'.getType) then
return TacticResultCNM.noChange
return (TacticResultCNM.noChange, usedSimps)
else
return TacticResultCNM.modified mvarId'
return (TacticResultCNM.modified mvarId', usedSimps')
def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do
def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
(usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) := do
mvarId.withContext do
mvarId.checkNotAssigned `simp
let mut mvarId := mvarId
let mut usedSimps : NameSet := usedSimps
for fvarId in fvarIdsToSimp do
let type ← instantiateMVars (← fvarId.getType)
let typeNew ← dsimp type ctx
let (typeNew, usedSimps') ← dsimp type ctx
usedSimps := usedSimps'
if typeNew.isConstOf ``False then
mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
return none
return (none, usedSimps)
if typeNew != type then
mvarId ← mvarId.replaceLocalDeclDefEq fvarId typeNew
if simplifyTarget then
let target ← mvarId.getType
let targetNew ← dsimp target ctx
let (targetNew, usedSimps') ← dsimp target ctx usedSimps
usedSimps := usedSimps'
if targetNew.isConstOf ``True then
mvarId.assign (mkConst ``True.intro)
return none
return (none, usedSimps)
if let some (_, lhs, rhs) := targetNew.eq? then
if (← withReducible <| isDefEq lhs rhs) then
mvarId.assign (← mkEqRefl lhs)
return none
return (none, usedSimps)
if target != targetNew then
mvarId ← mvarId.replaceTargetDefEq targetNew
return some mvarId
pure () -- FIXME: bug in do notation if this is removed?
return (some mvarId, usedSimps)
end Lean.Meta

1
src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file

@ -73,6 +73,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
trace[Meta.Tactic.simp.rewrite] "{thm}, perm rejected {e} ==> {rhs}"
return none
trace[Meta.Tactic.simp.rewrite] "{thm}, {e} ==> {rhs}"
recordSimpTheorem thm.name
return some { expr := rhs, proof? }
else
unless lhs.isMVar do

22
src/Lean/Meta/Tactic/Simp/SimpAll.lean
View file

@ -20,10 +20,11 @@ structure Entry where
deriving Inhabited
structure State where
modified : Bool := false
mvarId : MVarId
entries : Array Entry := #[]
ctx : Simp.Context
modified : Bool := false
mvarId : MVarId
entries : Array Entry := #[]
ctx : Simp.Context
usedSimps : NameSet := {}
abbrev M := StateRefT State MetaM
@ -56,7 +57,9 @@ private partial def loop : M Bool := do
-- We disable the current entry to prevent it to be simplified to `True`
let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
match (← simpStep (← get).mvarId entry.proof entry.type ctx) with
let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx (usedSimps := (← get).usedSimps)
modify fun s => { s with usedSimps }
match r with
| none => return true -- closed the goal
| some (proofNew, typeNew) =>
unless typeNew == entry.type do
@ -94,7 +97,9 @@ private partial def loop : M Bool := do
}
-- simplify target
let mvarId := (← get).mvarId
match (← simpTarget mvarId (← get).ctx) with
let (r, usedSimps) ← simpTarget mvarId (← get).ctx (usedSimps := (← get).usedSimps)
modify fun s => { s with usedSimps }
match r with
| none => return true
| some mvarIdNew =>
unless mvarId == mvarIdNew do
@ -121,8 +126,9 @@ def main : M (Option MVarId) := do
end SimpAll
def simpAll (mvarId : MVarId) (ctx : Simp.Context) : MetaM (Option MVarId) := do
def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : NameSet := {}) : MetaM (Option MVarId × NameSet) := do
mvarId.withContext do
SimpAll.main.run' { mvarId := mvarId, ctx := ctx }
let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
return (r, s.usedSimps)
end Lean.Meta

10
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -37,9 +37,10 @@ def Context.mkDefault : MetaM Context :=
return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
structure State where
cache : Cache := {}
congrCache : CongrCache := {}
numSteps : Nat := 0
cache : Cache := {}
congrCache : CongrCache := {}
usedTheorems : NameSet := {}
numSteps : Nat := 0
abbrev SimpM := ReaderT Context $ StateRefT State MetaM
@ -98,6 +99,9 @@ def getSimpCongrTheorems : M SimpCongrTheorems :=
finally
modify fun s => { s with cache := cacheSaved }
def recordSimpTheorem (n : Name) : SimpM Unit :=
modify fun s => { s with usedTheorems := s.usedTheorems.insert n }
end Simp
export Simp (SimpM)

4
src/Lean/Meta/Tactic/Split.lean
View file

@ -17,7 +17,7 @@ def getSimpMatchContext : MetaM Simp.Context :=
}
def simpMatch (e : Expr) : MetaM Simp.Result := do
Simp.main e (← getSimpMatchContext) (methods := { pre })
(·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
where
pre (e : Expr) : SimpM Simp.Step := do
let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
@ -35,7 +35,7 @@ def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
applySimpResultToTarget mvarId target r
private def simpMatchCore (matchDeclName : Name) (matchEqDeclName : Name) (e : Expr) : MetaM Simp.Result := do
Simp.main e (← getSimpMatchContext) (methods := { pre })
(·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
where
pre (e : Expr) : SimpM Simp.Step := do
if e.isAppOf matchDeclName then

4
src/Lean/Meta/Tactic/SplitIf.lean
View file

@ -82,14 +82,14 @@ open SplitIf
def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
let mut ctx ← getSimpContext
if let some mvarId' ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
if let (some mvarId', _) ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
return mvarId'
else
unreachable!
def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
let mut ctx ← getSimpContext
if let some (_, mvarId') ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
return mvarId'
else
unreachable!

2
src/Lean/Meta/Tactic/Unfold.lean
View file

@ -17,7 +17,7 @@ private def getSimpUnfoldContext : MetaM Simp.Context :=
def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
if let some unfoldThm ← getUnfoldEqnFor? declName then
Simp.main e (← getSimpUnfoldContext) (methods := { pre := pre unfoldThm })
(·.1) <$> Simp.main e (← getSimpUnfoldContext) (methods := { pre := pre unfoldThm })
else
return { expr := (← deltaExpand e (· == declName)) }
where

2
tests/lean/1079.lean.expected.out
View file

@ -1,5 +1,5 @@
1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
[Meta.Tactic.simp.rewrite] h:1000, m ==> n
[Meta.Tactic.simp.rewrite] _uniq.82:1000, m ==> n
[Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
[Meta.Tactic.simp.unify] ite_self:1000, failed to unify
if ?c then ?a else ?a

2
tests/lean/run/simp1.lean
View file

@ -46,7 +46,7 @@ def tst2 : MetaM Unit := do
let s ← Meta.getSimpTheorems
let m ← s.post.getMatch lhs
trace[Meta.debug] "result: {m}"
assert! m.any fun s => s.name? == `ex2
assert! m.any fun s => s.name == `ex2
set_option trace.Meta.debug true in