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

refactor: add helper methods for simp

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-07 13:27:49 -08:00
parent b1b4705c14
commit c303bf6916
1 changed files with 35 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -510,12 +510,11 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.
simpTargetCore mvarId ctx discharge?
/--
Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
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) : MetaM (Option (Expr × Expr)) := do
let r ← simp prop ctx discharge?
def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Simp.Result) : MetaM (Option (Expr × Expr)) := do
if r.expr.isConstOf ``False then
match r.proof? with
| some eqProof => assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (← mkEqMP eqProof proof))
@ -530,21 +529,44 @@ def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context)
else
return some (proof, r.expr)
def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) : MetaM (Option (Expr × Expr)) := do
let localDecl ← getLocalDecl fvarId
applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r
/--
Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
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) : MetaM (Option (Expr × Expr)) := do
let r ← simp prop ctx discharge?
applySimpResultToProp mvarId proof prop r
def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
match r with
| none => return none
| some (value, type') =>
let localDecl ← getLocalDecl fvarId
if localDecl.type != type' then
let mvarId ← assert mvarId localDecl.userName type' value
let mvarId ← tryClear mvarId localDecl.fvarId
let (fvarId, mvarId) ← intro1P mvarId
return some (fvarId, mvarId)
else
return some (fvarId, mvarId)
/--
Simplify `simp` result to the given local declaration. Return `none` if the goal was closed.
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) : MetaM (Option (FVarId × MVarId)) := do
applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r)
def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM (Option (FVarId × MVarId)) := do
withMVarContext mvarId do
checkNotAssigned mvarId `simp
let localDecl ← getLocalDecl fvarId
let type ← instantiateMVars localDecl.type
match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
| none => return none
| some (value, type') =>
if type != type' then
let mvarId ← assert mvarId localDecl.userName type' value
let mvarId ← tryClear mvarId localDecl.fvarId
let (fvarId, mvarId) ← intro1P mvarId
return some (fvarId, mvarId)
else
return some (fvarId, mvarId)
applySimpResultToLocalDeclCore mvarId fvarId (← simpStep mvarId (mkFVar fvarId) type ctx discharge?)
abbrev FVarIdToLemmaId := FVarIdMap Name