chore: update stage0

stage0/src/Init/Data/Nat/Div.lean

@@ -119,7 +119,7 @@ theorem mod_one (x : Nat) : x % 1 = 0 := by
   have : (y : Nat) → y < 1 → y = 0 := by
     intro y
     cases y with
-    | zero   => intro h; exact rfl -- TODO remove exact
+    | zero   => intro h; rfl
     | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)
   exact this _ h
 

stage0/src/Init/Data/String/Extra.lean

@@ -38,7 +38,7 @@ theorem one_le_csize (c : Char) : 1 ≤ csize c := by
 
 theorem eq_empty_of_bsize_eq_zero (h : s.endPos = {}) : s = "" := by
   match s with
-  | ⟨[]⟩   => exact rfl -- TODO: remove exact
+  | ⟨[]⟩   => rfl
   | ⟨c::cs⟩ =>
     injection h with h
     simp [endPos, utf8ByteSize, utf8ByteSize.go] at h

stage0/src/Lean/Meta/Tactic/Refl.lean

@@ -8,7 +8,7 @@ import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta
 
-def refl (mvarId : MVarId) (reduceIfGround := true) : MetaM Unit := do
+def refl (mvarId : MVarId) : MetaM Unit := do
   withMVarContext mvarId do
     checkNotAssigned mvarId `apply
     let targetType ← getMVarType' mvarId
@@ -17,14 +17,8 @@ def refl (mvarId : MVarId) (reduceIfGround := true) : MetaM Unit := do
     let lhs ← instantiateMVars targetType.appFn!.appArg!
     let rhs ← instantiateMVars targetType.appArg!
     let success ←
-      if (← useReduceAll lhs rhs) then
-        let lhs' ← reduceAll lhs
-        let rhs' ← reduceAll rhs
-        if lhs' == rhs' then
-          pure true
-        else
-          -- Catch corner cases such as `Nat.zero` and the `0` literal
-          isDefEq lhs' rhs'
+      if (← useKernel lhs rhs) then
+        pure (Kernel.isDefEq (← getEnv) {} lhs rhs)
       else
         isDefEq lhs rhs
     unless success do
@@ -33,9 +27,10 @@ def refl (mvarId : MVarId) (reduceIfGround := true) : MetaM Unit := do
     let α := targetType.appFn!.appFn!.appArg!
     assignExprMVar mvarId (mkApp2 (mkConst ``Eq.refl  us) α lhs)
 where
-  useReduceAll (lhs rhs : Expr) : MetaM Bool := do
-    if !reduceIfGround then return false
-    else if lhs.hasFVar || lhs.hasMVar || lhs.hasFVar || lhs.hasMVar then return false
-    else return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
+  useKernel (lhs rhs : Expr) : MetaM Bool := do
+    if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then
+      return false
+    else
+      return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
 
 end Lean.Meta

stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c

@@ -281,7 +281,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tacti
 LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed_declRange(lean_object*);
 static lean_object* l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Tactic_evalOpen___spec__3___closed__7;
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRenameInaccessibles_declRange___closed__6;
-lean_object* l_Lean_Meta_refl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_refl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_maxRecDepth;
 LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalClear(lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalOpen_declRange___closed__5;
@@ -12643,78 +12643,77 @@ lean_inc(x_1);
 x_10 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
 if (lean_obj_tag(x_10) == 0)
 {
-lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; 
+lean_object* x_11; lean_object* x_12; lean_object* x_13; 
 x_11 = lean_ctor_get(x_10, 0);
 lean_inc(x_11);
 x_12 = lean_ctor_get(x_10, 1);
 lean_inc(x_12);
 lean_dec(x_10);
-x_13 = 1;
 lean_inc(x_8);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
-x_14 = l_Lean_Meta_refl(x_11, x_13, x_5, x_6, x_7, x_8, x_12);
-if (lean_obj_tag(x_14) == 0)
+x_13 = l_Lean_Meta_refl(x_11, x_5, x_6, x_7, x_8, x_12);
+if (lean_obj_tag(x_13) == 0)
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_15 = lean_ctor_get(x_14, 1);
-lean_inc(x_15);
-lean_dec(x_14);
-x_16 = lean_box(0);
-x_17 = l_Lean_Elab_Tactic_replaceMainGoal(x_16, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_15);
-if (lean_obj_tag(x_17) == 0)
+lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_14 = lean_ctor_get(x_13, 1);
+lean_inc(x_14);
+lean_dec(x_13);
+x_15 = lean_box(0);
+x_16 = l_Lean_Elab_Tactic_replaceMainGoal(x_15, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_14);
+if (lean_obj_tag(x_16) == 0)
 {
-uint8_t x_18; 
-x_18 = !lean_is_exclusive(x_17);
-if (x_18 == 0)
+uint8_t x_17; 
+x_17 = !lean_is_exclusive(x_16);
+if (x_17 == 0)
 {
-lean_object* x_19; lean_object* x_20; 
-x_19 = lean_ctor_get(x_17, 0);
-lean_dec(x_19);
-x_20 = lean_box(0);
-lean_ctor_set(x_17, 0, x_20);
-return x_17;
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_ctor_get(x_16, 0);
+lean_dec(x_18);
+x_19 = lean_box(0);
+lean_ctor_set(x_16, 0, x_19);
+return x_16;
 }
 else
 {
-lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-x_21 = lean_ctor_get(x_17, 1);
-lean_inc(x_21);
-lean_dec(x_17);
-x_22 = lean_box(0);
-x_23 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_23, 0, x_22);
-lean_ctor_set(x_23, 1, x_21);
-return x_23;
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_20 = lean_ctor_get(x_16, 1);
+lean_inc(x_20);
+lean_dec(x_16);
+x_21 = lean_box(0);
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_21);
+lean_ctor_set(x_22, 1, x_20);
+return x_22;
 }
 }
 else
 {
-uint8_t x_24; 
-x_24 = !lean_is_exclusive(x_17);
-if (x_24 == 0)
+uint8_t x_23; 
+x_23 = !lean_is_exclusive(x_16);
+if (x_23 == 0)
 {
-return x_17;
+return x_16;
 }
 else
 {
-lean_object* x_25; lean_object* x_26; lean_object* x_27; 
-x_25 = lean_ctor_get(x_17, 0);
-x_26 = lean_ctor_get(x_17, 1);
-lean_inc(x_26);
+lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_24 = lean_ctor_get(x_16, 0);
+x_25 = lean_ctor_get(x_16, 1);
 lean_inc(x_25);
-lean_dec(x_17);
-x_27 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_27, 0, x_25);
-lean_ctor_set(x_27, 1, x_26);
-return x_27;
+lean_inc(x_24);
+lean_dec(x_16);
+x_26 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_26, 0, x_24);
+lean_ctor_set(x_26, 1, x_25);
+return x_26;
 }
 }
 }
 else
 {
-uint8_t x_28; 
+uint8_t x_27; 
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
@@ -12723,29 +12722,29 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_28 = !lean_is_exclusive(x_14);
-if (x_28 == 0)
+x_27 = !lean_is_exclusive(x_13);
+if (x_27 == 0)
 {
-return x_14;
+return x_13;
 }
 else
 {
-lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-x_29 = lean_ctor_get(x_14, 0);
-x_30 = lean_ctor_get(x_14, 1);
-lean_inc(x_30);
+lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+x_28 = lean_ctor_get(x_13, 0);
+x_29 = lean_ctor_get(x_13, 1);
 lean_inc(x_29);
-lean_dec(x_14);
-x_31 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_31, 0, x_29);
-lean_ctor_set(x_31, 1, x_30);
-return x_31;
+lean_inc(x_28);
+lean_dec(x_13);
+x_30 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_30, 0, x_28);
+lean_ctor_set(x_30, 1, x_29);
+return x_30;
 }
 }
 }
 else
 {
-uint8_t x_32; 
+uint8_t x_31; 
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
@@ -12754,23 +12753,23 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_32 = !lean_is_exclusive(x_10);
-if (x_32 == 0)
+x_31 = !lean_is_exclusive(x_10);
+if (x_31 == 0)
 {
 return x_10;
 }
 else
 {
-lean_object* x_33; lean_object* x_34; lean_object* x_35; 
-x_33 = lean_ctor_get(x_10, 0);
-x_34 = lean_ctor_get(x_10, 1);
-lean_inc(x_34);
+lean_object* x_32; lean_object* x_33; lean_object* x_34; 
+x_32 = lean_ctor_get(x_10, 0);
+x_33 = lean_ctor_get(x_10, 1);
 lean_inc(x_33);
+lean_inc(x_32);
 lean_dec(x_10);
-x_35 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_35, 0, x_33);
-lean_ctor_set(x_35, 1, x_34);
-return x_35;
+x_34 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_34, 0, x_32);
+lean_ctor_set(x_34, 1, x_33);
+return x_34;
 }
 }
 }