chore: update stage0

stage0/src/Init/Data/AC.lean

@@ -186,7 +186,7 @@ theorem Context.evalList_insert
     case inr =>
       split
       case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
-      case inr => simp_all [ih, evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
+      case inr => simp_all [evalList, EvalInformation.evalOp]; simp [ih]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] -- TODO: remove `simp [ih]` after `update stage0`
 
 theorem Context.evalList_sort_congr
   (ctx : Context α)

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

@@ -157,7 +157,18 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
-  transform e (post := fun e => return TransformStep.done (← reduce e))
+  let pre (e : Expr) : M TransformStep := do
+    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    return .visit e
+  let post (e : Expr) : M TransformStep := do
+    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    let eNew ← reduce e
+    if eNew != e then return .visit eNew else return .done e
+  transform e (pre := pre) (post := post)
 
 inductive SimpLetCase where
   | dep -- `let x := v; b` is not equivalent to `(fun x => b) v`
@@ -529,10 +540,21 @@ where
           | none    => mkImpCongr e rp rq
           | some hq =>
             let hq ← mkLambdaFVars #[h] hq
+            /-
+              We use the default reducibility setting at `mkImpDepCongrCtx` and `mkImpCongrCtx` because they use the theorems
+              ```lean
+              @implies_dep_congr_ctx : ∀ {p₁ p₂ q₁ : Prop}, p₁ = p₂ → ∀ {q₂ : p₂ → Prop}, (∀ (h : p₂), q₁ = q₂ h) → (p₁ → q₁) = ∀ (h : p₂), q₂ h
+              @implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
+              ```
+              And the proofs may be from `rfl` theorems which are now omitted. Moreover, we cannot establish that the two
+              terms are definitionally equal using `withReducible`.
+              TODO (better solution): provide the problematic implicit arguments explicitly. It is more efficient and avoids this
+              problem.
+             -/
             if rq.expr.containsFVar h.fvarId! then
-              return { expr := (← mkForallFVars #[h] rq.expr), proof? := (← mkImpDepCongrCtx (← rp.getProof) hq) }
+              return { expr := (← mkForallFVars #[h] rq.expr), proof? := (← withDefault <| mkImpDepCongrCtx (← rp.getProof) hq) }
             else
-              return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← mkImpCongrCtx (← rp.getProof) hq) }
+              return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← withDefault <| mkImpCongrCtx (← rp.getProof) hq) }
     else
       mkImpCongr e rp (← simp q)
 

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

@@ -130,7 +130,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
 /-
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
-def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name) (discharge? : Expr → SimpM (Option Expr)) (tag : String) : SimpM (Option Result) := do
+def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
   let candidates ← s.getMatchWithExtra e
   if candidates.isEmpty then
     trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
@@ -138,7 +138,7 @@ def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name)
   else
     let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
     for (thm, numExtraArgs) in candidates do
-      unless inErasedSet thm do
+      unless inErasedSet thm || (rflOnly && !thm.rfl) do
         if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs discharge? then
           trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
           return some result
@@ -224,15 +224,15 @@ def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (O
   else
     return none
 
-def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
   for thms in (← read).simpTheorems do
-    if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") then
+    if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
-def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
   for thms in (← read).simpTheorems do
-    if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") then
+    if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 

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

@@ -65,8 +65,11 @@ private partial def loop : M Bool := do
            ```
            In the first round, `h : x ≠ 0` is simplified to `h : ¬ x = 0`. If we don't use the same `id`, in the next round
            the first version would simplify it to `h : True`.
+
+           We must use `mkExpectedTypeHint` because `inferType proofNew` may not be equal to `typeNew` when
+           we have theorems marked with `rfl`.
         -/
-        let simpThmsNew ← (← getSimpTheorems).addTheorem proofNew (name? := entry.id)
+        let simpThmsNew ← (← getSimpTheorems).addTheorem (← mkExpectedTypeHint proofNew typeNew) (name? := entry.id)
         modify fun s => { s with
           modified         := true
           ctx.simpTheorems := simpThmsNew

stage0/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -47,27 +47,40 @@ def SimpTheorem.getName (s : SimpTheorem) : Name :=
   | some n => n
   | none   => "<unknown>"
 
-def isRflProofCore (type : Expr) (proof : Expr) : Bool :=
-  match type with
-  | .forallE _ _ type _ =>
-    if let .lam _ _ proof _ := proof then
-      isRflProofCore type proof
-    else
-      false
-  | _ =>
-    type.isAppOfArity ``Eq 3
-    &&
-    (proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2)
+mutual
+  partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
+    match type with
+    | .forallE _ _ type _ =>
+      if let .lam _ _ proof _ := proof then
+        isRflProofCore type proof
+      else
+        return false
+    | _ =>
+      if type.isAppOfArity ``Eq 3 then
+        if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then
+          return true
+        else if proof.isAppOfArity ``Eq.symm 4 then
+          -- `Eq.symm` of rfl theorem is a rfl theorem
+          isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
+        else if proof.isApp && proof.getAppFn.isConst then
+          -- The application of a `rfl` theorem is a `rfl` theorem
+          isRflTheorem proof.getAppFn.constName!
+        else
+          return false
+      else
+        return false
 
-def isRflTheorem (declName : Name) : CoreM Bool := do
-  let .thmInfo info ← getConstInfo declName | return false
-  return isRflProofCore info.type info.value
+  partial def isRflTheorem (declName : Name) : CoreM Bool := do
+    let .thmInfo info ← getConstInfo declName | return false
+    isRflProofCore info.type info.value
+end
 
-def isRflProof (proof : Expr) : CoreM Bool := do
+def isRflProof (proof : Expr) : MetaM Bool := do
+  trace[Meta.debug] "isRflProof: {proof}"
   if let .const declName .. := proof then
     isRflTheorem declName
   else
-    return false
+    isRflProofCore (← inferType proof) proof
 
 instance : ToFormat SimpTheorem where
   format s :=

stage0/stdlib/Lean/Meta/Tactic/Split.c

@@ -869,6 +869,8 @@ lean_object* x_18; lean_object* x_19;
 x_18 = lean_ctor_get(x_16, 1);
 lean_inc(x_18);
 lean_dec(x_16);
+lean_inc(x_9);
+lean_inc(x_8);
 lean_inc(x_2);
 x_19 = l_Lean_Meta_isRflTheorem(x_2, x_8, x_9, x_18);
 if (lean_obj_tag(x_19) == 0)

stage0/stdlib/Lean/Meta/Tactic/Unfold.c

@@ -184,6 +184,8 @@ LEAN_EXPORT lean_object* l_Lean_Meta_unfold_pre(lean_object* x_1, lean_object* x
 _start:
 {
 lean_object* x_10; 
+lean_inc(x_8);
+lean_inc(x_7);
 lean_inc(x_1);
 x_10 = l_Lean_Meta_isRflTheorem(x_1, x_7, x_8, x_9);
 if (lean_obj_tag(x_10) == 0)