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

perf: avoid mkEqMP and mkEqMPR in simp (#7690)

Browse source 
This PR avoids `mkEqMP` and `mkEqMPR` in `simp`. It creates the proof
term without relying on unification.
This commit is contained in:
Leonardo de Moura 2025-03-26 17:26:56 -07:00 • committed by GitHub
parent 9466c5db25
commit 69160750f2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 20 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -865,28 +865,34 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray
simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
/--
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`.
Applies the result `r` for `type` (which is inhabited by `val`). Returns `none` if the goal was closed. Returns `some (val', type')`
otherwise, where `val' : type'` and `type'` is the simplified `type`.
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Simp.Result) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do
This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
def applySimpResult (mvarId : MVarId) (val : Expr) (type : Expr) (r : Simp.Result) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do
if mayCloseGoal && r.expr.isFalse then
match r.proof? with
| some eqProof => mvarId.assign (← mkFalseElim (← mvarId.getType) (← mkEqMP eqProof proof))
| none => mvarId.assign (← mkFalseElim (← mvarId.getType) proof)
| some eqProof => mvarId.assign (← mkFalseElim (← mvarId.getType) (mkApp4 (mkConst ``Eq.mp [levelZero]) type r.expr eqProof val))
| none => mvarId.assign (← mkFalseElim (← mvarId.getType) val)
return none
else
match r.proof? with
| some eqProof => return some ((← mkEqMP eqProof proof), r.expr)
| some eqProof =>
let u ← getLevel type
return some (mkApp4 (mkConst ``Eq.mp [u]) type r.expr eqProof val, r.expr)
| none =>
if r.expr != prop then
return some ((← mkExpectedTypeHint proof r.expr), r.expr)
if r.expr != type then
return some ((← mkExpectedTypeHint val r.expr), r.expr)
else
return some (proof, r.expr)
return some (val, r.expr)
@[deprecated applySimpResult (since := "2025-03-26")]
def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Simp.Result) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) :=
applySimpResult mvarId proof prop r mayCloseGoal
def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (Expr × Expr)) := do
let localDecl ← fvarId.getDecl
applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r mayCloseGoal
applySimpResult mvarId (mkFVar fvarId) localDecl.type r mayCloseGoal
/--
Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@ -896,7 +902,7 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
(mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (Expr × Expr) × Stats) := do
let (r, stats) ← simp prop ctx simprocs discharge? stats
return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
return (← applySimpResult mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
match r with
@ -950,7 +956,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
let (r, stats') ← simp type ctx simprocs discharge? stats
stats := stats'
match r.proof? with
| some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
| some _ => match (← applySimpResult mvarIdNew (mkFVar fvarId) type r) with
| none => return (none, stats)
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
| none =>

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

@ -625,7 +625,7 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
if let some r ← dischargeEqnThmHypothesis? e then return some r
let r ← simp e
if let some p ← dischargeRfl r.expr then
return some (← mkEqMPR (← r.getProof) p)
return some (mkApp4 (mkConst ``Eq.mpr [levelZero]) e r.expr (← r.getProof) p)
else if r.expr.isTrue then
return some (← mkOfEqTrue (← r.getProof))
else