fix: simp gets stuck on autoParam

src/Lean/Expr.lean

@@ -1559,6 +1559,12 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
   let e' := e.consumeMData.consumeTypeAnnotations
   if e' == e then e else cleanupAnnotations e'
 
+def isFalse (e : Expr) : Bool :=
+  e.cleanupAnnotations.isConstOf ``False
+
+def isTrue (e : Expr) : Bool :=
+  e.cleanupAnnotations.isConstOf ``True
+
 /-- Return true iff `e` contains a free variable which satisfies `p`. -/
 @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool :=
   let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else

src/Lean/Meta/MatchUtil.lean

@@ -40,7 +40,7 @@ def matchEqHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
     return none
 
 def matchFalse (e : Expr) : MetaM Bool := do
-  testHelper e fun e => return e.isConstOf ``False
+  testHelper e fun e => return e.isFalse
 
 def matchNot? (e : Expr) : MetaM (Option Expr) :=
   matchHelper? e fun e => do

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

@@ -11,11 +11,11 @@ builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
   unless e.isAppOfArity ``ite 5 do return .continue
   let c := e.getArg! 1
   let r ← simp c
-  if r.expr.isConstOf ``True then
+  if r.expr.isTrue then
     let eNew  := e.getArg! 3
     let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
     return .visit { expr := eNew, proof? := pr }
-  if r.expr.isConstOf ``False then
+  if r.expr.isFalse then
     let eNew  := e.getArg! 4
     let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
     return .visit { expr := eNew, proof? := pr }
@@ -25,13 +25,13 @@ builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
   unless e.isAppOfArity ``dite 5 do return .continue
   let c := e.getArg! 1
   let r ← simp c
-  if r.expr.isConstOf ``True then
+  if r.expr.isTrue then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_true) c pr
     let eNew  := mkApp (e.getArg! 3) h |>.headBeta
     let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
     return .visit { expr := eNew, proof? := prNew }
-  if r.expr.isConstOf ``False then
+  if r.expr.isFalse then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_false) c pr
     let eNew  := mkApp (e.getArg! 4) h |>.headBeta

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -650,7 +650,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   let target ← instantiateMVars (← mvarId.getType)
   let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
-  if mayCloseGoal && r.expr.consumeMData.isConstOf ``True then
+  if mayCloseGoal && r.expr.isTrue then
     match r.proof? with
     | some proof => mvarId.assign (← mkOfEqTrue proof)
     | none => mvarId.assign (mkConst ``True.intro)
@@ -673,7 +673,7 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray
 
   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.consumeMData.isConstOf ``False then
+  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)
@@ -721,7 +721,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.consumeMData.isConstOf ``False then
+    if mayCloseGoal && r.expr.isFalse then
       mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
       return none
     else
@@ -757,7 +757,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
         | none => return (none, usedSimps)
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
-        if r.expr.consumeMData.isConstOf ``False then
+        if r.expr.isFalse then
           mvarIdNew.assign (← mkFalseElim (← mvarIdNew.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 ...`
@@ -802,7 +802,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.consumeMData.isConstOf ``False then
+      if typeNew.isFalse then
         mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
         return (none, usedSimps)
       if typeNew != type then
@@ -811,7 +811,7 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
       let target ← mvarIdNew.getType
       let (targetNew, usedSimps') ← dsimp target ctx usedSimps
       usedSimps := usedSimps'
-      if targetNew.consumeMData.isConstOf ``True then
+      if targetNew.isTrue then
         mvarIdNew.assign (mkConst ``True.intro)
         return (none, usedSimps)
       if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -182,7 +182,7 @@ def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
 @[inline] def simpUsingDecide : Simproc := fun e => do
   unless (← getConfig).decide do
     return .continue
-  if e.hasFVar || e.hasMVar || e.consumeMData.isConstOf ``True || e.consumeMData.isConstOf ``False then
+  if e.hasFVar || e.hasMVar || e.isTrue || e.isFalse then
     return .continue
   try
     let d ← mkDecide e
@@ -288,7 +288,7 @@ Discharge procedure for the ground/symbolic evaluator.
 def dischargeGround (e : Expr) : SimpM (Option Expr) := do
   trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
   let r ← simp e
-  if r.expr.consumeMData.isConstOf ``True then
+  if r.expr.isTrue then
     try
       return some (← mkOfEqTrue (← r.getProof))
     catch _ =>
@@ -431,7 +431,7 @@ where
   go (e : Expr) : Bool :=
     match e with
     | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
-    | _ => e.consumeMData.isConstOf ``False
+    | _ => e.isFalse
 
 def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
   (← getLCtx).findDeclRevM? fun localDecl => do
@@ -484,7 +484,7 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
   else
     withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
       let r ← simp e
-      if r.expr.consumeMData.isConstOf ``True then
+      if r.expr.isTrue then
         try
           return some (← mkOfEqTrue (← r.getProof))
         catch _ =>

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -130,7 +130,7 @@ def main : M (Option MVarId) := do
     let mut toClear := #[]
     let mut modified := false
     for e in (← get).entries do
-      if e.type.consumeMData.isConstOf ``True then
+      if e.type.isTrue then
         -- Do not assert `True` hypotheses
         toClear := toClear.push e.fvarId
       else if modified || e.type != e.origType then

tests/lean/run/2862.lean

@@ -0,0 +1,2 @@
+example (h : False := by trivial) : False := by
+  simp at h