fix: simp: strip mdata when testing for True/False

Fixes #2173

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

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

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

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