From 7f51628986f95067ca88988aa5974be002df6b2b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 30 Mar 2023 16:44:44 -0700 Subject: [PATCH] fix: simp: strip mdata when testing for True/False Fixes #2173 --- src/Lean/Meta/Tactic/Simp/Main.lean | 16 ++++++++-------- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpAll.lean | 2 +- tests/lean/run/2173.lean | 21 +++++++++++++++++++++ 4 files changed, 31 insertions(+), 10 deletions(-) create mode 100644 tests/lean/run/2173.lean diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index d51a741618..fc6abfd771 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -769,7 +769,7 @@ where go (e : Expr) : Bool := match e with | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b - | _ => e.isConstOf ``False + | _ => e.consumeMData.isConstOf ``False abbrev Discharge := Expr → SimpM (Option Expr) @@ -826,7 +826,7 @@ mutual else withReader (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do let r ← simp e { pre := pre, post := post, discharge? := discharge? } - if r.expr.isConstOf ``True then + if r.expr.consumeMData.isConstOf ``True then try return some (← mkOfEqTrue (← r.getProof)) catch _ => @@ -877,7 +877,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do let target ← instantiateMVars (← mvarId.getType) let (r, usedSimps) ← simp target ctx discharge? usedSimps - if mayCloseGoal && r.expr.isConstOf ``True then + if mayCloseGoal && r.expr.consumeMData.isConstOf ``True then match r.proof? with | some proof => mvarId.assign (← mkOfEqTrue proof) | none => mvarId.assign (mkConst ``True.intro) @@ -900,7 +900,7 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp. 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 - if mayCloseGoal && r.expr.isConstOf ``False then + if mayCloseGoal && r.expr.consumeMData.isConstOf ``False then match r.proof? with | some eqProof => mvarId.assign (← mkFalseElim (← mvarId.getType) (← mkEqMP eqProof proof)) | none => mvarId.assign (← mkFalseElim (← mvarId.getType) proof) @@ -948,7 +948,7 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res if r.proof?.isNone then -- New result is definitionally equal to input. Thus, we can avoid creating a new variable if there are dependencies let mvarId ← mvarId.replaceLocalDeclDefEq fvarId r.expr - if mayCloseGoal && r.expr.isConstOf ``False then + if mayCloseGoal && r.expr.consumeMData.isConstOf ``False then mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) return none else @@ -984,7 +984,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di | none => return (none, usedSimps) | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value } | none => - if r.expr.isConstOf ``False then + if r.expr.consumeMData.isConstOf ``False then mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) 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 ...` @@ -1026,7 +1026,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t let type ← instantiateMVars (← fvarId.getType) let (typeNew, usedSimps') ← dsimp type ctx usedSimps := usedSimps' - if typeNew.isConstOf ``False then + if typeNew.consumeMData.isConstOf ``False then mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) return (none, usedSimps) if typeNew != type then @@ -1035,7 +1035,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t let target ← mvarId.getType let (targetNew, usedSimps') ← dsimp target ctx usedSimps usedSimps := usedSimps' - if targetNew.isConstOf ``True then + if targetNew.consumeMData.isConstOf ``True then mvarId.assign (mkConst ``True.intro) return (none, usedSimps) if let some (_, lhs, rhs) := targetNew.eq? then diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 33b25082aa..aa3103faff 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -186,7 +186,7 @@ def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstanc | none => return none def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do - if e.hasFVar || e.hasMVar || e.isConstOf ``True || e.isConstOf ``False then + if e.hasFVar || e.hasMVar || e.consumeMData.isConstOf ``True || e.consumeMData.isConstOf ``False then return none else try diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index 2b91db680c..b342565df8 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean @@ -121,7 +121,7 @@ def main : M (Option MVarId) := do let entries := (← get).entries let (_, mvarId) ← mvarId.assertHypotheses <| entries.filterMap fun e => -- Do not assert `True` hypotheses - if e.type.isConstOf ``True then none else some { userName := e.userName, type := e.type, value := e.proof } + if e.type.consumeMData.isConstOf ``True then none else some { userName := e.userName, type := e.type, value := e.proof } mvarId.tryClearMany (entries.map fun e => e.fvarId) end SimpAll diff --git a/tests/lean/run/2173.lean b/tests/lean/run/2173.lean new file mode 100644 index 0000000000..d67431611a --- /dev/null +++ b/tests/lean/run/2173.lean @@ -0,0 +1,21 @@ +set_option pp.raw true + +example (n : Nat) : 0 = 0 := by + match n with + | _ => simp (config := {decide := false}) -- this is the default, so masks the problem? + +example : True := by + have : True := ⟨⟩ + simp (config := {decide := false}) -- unsolved goals + +example : True := by + let _x : True := ⟨⟩ + simp (config := {decide := false}) -- unsolved goals + +example : True := by + suffices True by simp (config := {decide := false}) -- unsolved goals + constructor + +example : True := by + show True + simp (config := {decide := false}) -- unsolved goals