chore: cleanup #5167 workarounds after update stage0 (#5175)

PR #5167 implemented RFC #5046, but it required several workarounds due
to staging issues. This PR cleans up these workarounds.

src/Init/ByCases.lean

@@ -57,8 +57,7 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 -- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
 theorem ite_some_none_eq_none [Decidable P] :
     (if P then some x else none) = none ↔ ¬ P := by
-  have : some x ≠ none := Option.noConfusion
-  simp only [ite_eq_right_iff, this]
+  simp only [ite_eq_right_iff, reduceCtorEq]
   rfl
 
 @[simp] theorem ite_some_none_eq_some [Decidable P] :

src/Init/Data/BitVec/Lemmas.lean

@@ -993,9 +993,8 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
     x.signExtend v = x.zeroExtend v := by
   ext i
   by_cases hv : i < v
-  · have : (false = true) = False := by simp
-    simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
-      BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, this]
+  · simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
+      BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
     rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
     simp [BitVec.testBit_toNat]
   · simp only [getLsb_zeroExtend, hv, decide_False, Bool.false_and]

src/Init/Data/List/Count.lean

@@ -47,11 +47,11 @@ theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a
     if h : p x then
       rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
       · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
-      · simp [h, not_true_eq_false, decide_False, not_false_eq_true]
+      · simp [h]
     else
       rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
       · rfl
-      · simp [h, not_false_eq_true, decide_True]
+      · simp [h]
 
 theorem countP_eq_length_filter (l) : countP p l = length (filter p l) := by
   induction l with
@@ -234,7 +234,7 @@ theorem count_erase (a b : α) :
       rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
     else
       have hc_beq := beq_false_of_ne hc
-      simp [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
+      simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq]
       if ha : b = a then
         rw [ha, eq_comm] at hc
         rw [if_pos ((beq_iff_eq _ _).2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]

src/Init/Data/List/Erase.lean

@@ -39,13 +39,13 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er
   | cons x xs ih =>
     simp only [eraseP_cons, cond_eq_if]
     split <;> rename_i h
-    · simp
+    · simp only [reduceCtorEq, cons.injEq, false_or]
       constructor
       · rintro rfl
         simpa
       · rintro ⟨_, _, rfl, rfl⟩
         rfl
-    · simp
+    · simp only [reduceCtorEq, cons.injEq, false_or, false_iff, not_exists, not_and]
       rintro x h' rfl
       simp_all
 

src/Init/Data/List/Find.lean

@@ -737,10 +737,10 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
     split
     · simp_all
-    · simp_all [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
+    · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
       simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
 
 theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :

src/Init/Data/List/Nat/Range.lean

@@ -200,7 +200,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
       cases k with
       | zero => simp [range'_succ]
       | succ k =>
-        simp [range'_succ, ih, exists_eq_left']
+        simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]
         refine ⟨k, ?_⟩
         simp_all
         omega

src/Init/Data/List/Pairwise.lean

@@ -123,7 +123,7 @@ theorem pairwise_filterMap (f : β → Option α) {l : List β} :
   match e : f a with
   | none =>
     rw [filterMap_cons_none e, pairwise_cons]
-    simp [e, false_implies, implies_true, true_and, IH]
+    simp only [e, false_implies, implies_true, true_and, IH, reduceCtorEq]
   | some b =>
     rw [filterMap_cons_some e]
     simpa [IH, e] using fun _ =>

src/Init/Data/List/Sort/Lemmas.lean

@@ -136,7 +136,7 @@ theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1 
       simp only [map_cons, cons.injEq, true_and]
       rw [merge_stable, map_cons]
       exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
-    · simp [↓reduceIte, map_cons, cons.injEq, true_and]
+    · simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
       rw [merge_stable, map_cons]
       exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -123,7 +123,7 @@ theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i
     match mod_two_eq_zero_or_one x with
     | Or.inl mod2_eq =>
       rw [←div_add_mod x 2] at xnz
-      simp [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
+      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or, reduceCtorEq] at xnz
       have ⟨d, dif⟩   := hyp x_pos xnz
       apply Exists.intro (d+1)
       simp_all

src/Init/WFTactics.lean

@@ -26,7 +26,7 @@ macro "clean_wf" : tactic =>
   `(tactic| simp
      (config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false })
      only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel,
-           WellFoundedRelation.rel, sizeOf_nat])
+           WellFoundedRelation.rel, sizeOf_nat, reduceCtorEq])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
 reasoning after applying lexicographic order lemmas.

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -155,7 +155,7 @@ theorem isUnit_iff (c : DefaultClause n) (l : Literal (PosFin n)) :
   split
   · next l' heq => simp [heq]
   · next hne =>
-    simp [false_iff]
+    simp
     apply hne
 
 def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -154,9 +154,9 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
               exact cOpt_in_arr
             · next b_eq_false =>
               simp only [Bool.not_eq_true] at b_eq_false
-              simp [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
+              simp only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos, reduceCtorEq] at h
               specialize ih l false
-              simp [hasAssignment, ite_false] at ih
+              simp only [hasAssignment, ite_false] at ih
               rw [b_eq_false, Subtype.ext i_eq_l]
               exact ih h
           · next i_ne_l =>
@@ -302,8 +302,8 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus
             · next b_eq_false =>
               simp only [Bool.not_eq_true] at b_eq_false
               exact b_eq_false
-          simp [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb
-          simp [hasAssignment, b_eq_false, ite_false, hb]
+          simp only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos, reduceCtorEq] at hb
+          simp only [hasAssignment, b_eq_false, ite_false, hb, reduceCtorEq]
         · next l_ne_i =>
           simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
           exact hb

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -17,9 +17,6 @@ namespace Internal
 
 namespace DefaultFormula
 
--- TODO: remove aux lemma after update-stage0
-private theorem false_ne_true : (false = true) = False := by simp
-
 open Std.Sat
 open DefaultClause DefaultFormula Assignment ReduceResult
 
@@ -318,7 +315,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n)
     · apply Or.inr
       rw [i'_eq_i] at i_true_in_c
       apply And.intro i_true_in_c
-      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2
+      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2
       split at h2
       · next heq =>
         have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
@@ -408,8 +405,8 @@ theorem assignmentsInvariant_performRupCheck_of_assignmentsInvariant {n : Nat} (
     rw [hb] at h
     by_cases pi : p i
     · exact pi
-    · simp at pi
-      simp [pi, decide_True, h] at h1
+    · simp only at pi
+      simp [pi, h] at h1
   · simp only [Bool.not_eq_true] at hb
     rw [hb]
     rw [hb] at h

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -20,9 +20,6 @@ namespace DefaultFormula
 open Std.Sat
 open DefaultClause DefaultFormula Assignment
 
--- TODO: remove aux lemma after update-stage0
-private theorem false_ne_true : (false = true) = False := by simp
-
 theorem size_insertUnit {n : Nat} (units : Array (Literal (PosFin n)))
     (assignments : Array Assignment) (b : Bool) (l : Literal (PosFin n)) :
     (insertUnit (units, assignments, b) l).2.1.size = assignments.size := by
@@ -114,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           ⟨units.size, units_size_lt_updatedUnits_size⟩
         have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
         refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l]
+        simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l, reduceCtorEq]
         constructor
         · rfl
         · constructor
@@ -130,7 +127,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 apply Nat.lt_of_le_of_ne
                 · apply Nat.le_of_lt_succ
                   have k_property := k.2
-                  simp [insertUnit, h3, ite_false, Array.size_push] at k_property
+                  simp only [insertUnit, h3, ite_false, Array.size_push, reduceCtorEq] at k_property
                   exact k_property
                 · intro h
                   simp only [← h, not_true, mostRecentUnitIdx] at hk
@@ -140,7 +137,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
               exact h2 ⟨k.1, k_in_bounds⟩
       · next i_ne_l =>
         apply Or.inl
-        simp [insertUnit, h3, ite_false]
+        simp only [insertUnit, h3, ite_false, reduceCtorEq]
         rw [Array.getElem_modify_of_ne i_in_bounds _ (Ne.symm i_ne_l)]
         constructor
         · exact h1
@@ -192,7 +189,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           exact h5 (has_add _ true)
         | true, false =>
           refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
-          simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
+          simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq, reduceCtorEq]
           constructor
           · rw [Array.get_push_lt units l j.1 j.2, h1]
           · constructor
@@ -222,7 +219,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                     exact h4 ⟨k.1, h⟩ k_ne_j
                   · exfalso
                     have k_property := k.2
-                    simp [insertUnit, h5, ite_false, Array.size_push] at k_property
+                    simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] at k_property
                     rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                     · exact h k_lt_units_size
                     · simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
@@ -244,8 +241,8 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 · match h : assignments0[i.val]'_ with
                   | unassigned => rfl
                   | pos =>
-                    simp [addAssignment, h, ite_false, addNegAssignment] at h2
-                    simp [i_eq_l] at h2
+                    simp only [addAssignment, h, ite_false, addNegAssignment, reduceCtorEq] at h2
+                    simp only [i_eq_l] at h2
                     simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasPosAssignment, decidableGetElem?] at h5
                   | neg  => simp (config := {decide := true}) only [h] at h3
                   | both => simp (config := {decide := true}) only [h] at h3
@@ -259,7 +256,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                     exact h4 ⟨k.1, h⟩ k_ne_j
                   · exfalso
                     have k_property := k.2
-                    simp [insertUnit, h5, ite_false, Array.size_push] at k_property
+                    simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq] at k_property
                     rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                     · exact h k_lt_units_size
                     · simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
@@ -273,10 +270,10 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
       · next i_ne_l =>
         apply Or.inr ∘ Or.inl
         have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
-          simp [insertUnit, h5, ite_false, Array.size_push]
+          simp only [insertUnit, h5, ite_false, Array.size_push, reduceCtorEq]
           exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
         refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
-        simp [insertUnit, h5, ite_false]
+        simp only [insertUnit, h5, ite_false, reduceCtorEq]
         constructor
         · rw [Array.get_push_lt units l j.1 j.2, h1]
         · constructor
@@ -353,7 +350,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                 simp only
                 have k_eq_units_size : k.1 = units.size := by
                   have k_property := k.2
-                  simp [insertUnit, h, ite_false, Array.size_push] at k_property
+                  simp only [insertUnit, h, ite_false, Array.size_push, reduceCtorEq] at k_property
                   rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                   · exfalso; exact k_not_lt_units_size k_lt_units_size
                   · exact k_eq_units_size
@@ -876,7 +873,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
                 simp only [l'_eq_false, hasAssignment, ite_false] at h2
                 simp only [hasAssignment, l_eq_true, getElem!, l_eq_i, i_in_bounds,
                   Array.get_eq_getElem, ↓reduceIte, ↓reduceDIte, h1, addAssignment, l'_eq_false,
-                  hasPos_addNeg, decidableGetElem?, false_ne_true] at h
+                  hasPos_addNeg, decidableGetElem?, reduceCtorEq] at h
                 exact unassigned_of_has_neither _ h h2
               · intro k k_ne_zero k_ne_j_succ
                 have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
@@ -924,7 +921,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
               · simp only [l'] at l'_eq_true
                 simp only [hasAssignment, l'_eq_true, ite_true] at h2
                 simp only [hasAssignment, l_eq_false, ↓reduceIte, getElem!, l_eq_i, i_in_bounds,
-                  Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, false_ne_true] at h
+                  Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, reduceCtorEq] at h
                 exact unassigned_of_has_neither _ h2 h
               · intro k k_ne_j_succ k_ne_zero
                 have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -17,9 +17,6 @@ namespace Internal
 
 namespace DefaultFormula
 
--- TODO: remove aux lemma after update-stage0
-private theorem false_ne_true : (false = true) = False := by simp
-
 open Std.Sat
 open DefaultClause DefaultFormula Assignment ReduceResult
 
@@ -52,7 +49,7 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
         simp [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i]
         exact h
     · apply Exists.intro l.1
-      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, false_ne_true]
+      simp only [insertUnit, hl, ite_false, Array.getElem_modify_self l_in_bounds, reduceCtorEq]
       simp only [getElem!, l_in_bounds, dite_true, decidableGetElem?] at assignments_l_ne_unassigned
       by_cases l.2
       · next l_eq_true =>
@@ -184,7 +181,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re
     · apply Or.inr
       rw [i'_eq_i] at i_true_in_c
       apply And.intro i_true_in_c
-      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, false_ne_true] at h2
+      simp only [addAssignment, ← b_eq_false, addNegAssignment, ite_false, reduceCtorEq] at h2
       split at h2
       · next heq =>
         have hasPosAssignment_fi : hasAssignment true (f.assignments[i.1]'i_in_bounds) := by
@@ -669,7 +666,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
         simp only [ConfirmRupHintFoldEntailsMotive]
         split
         · simp [h1, hsize]
-        · simp [Array.size_modify, hsize]
+        · simp only [Array.size_modify, hsize, Bool.false_eq_true, false_implies, and_true, true_and]
           intro p pf
           have pacc := h1 p pf
           have pc : p ⊨ c := by
@@ -703,7 +700,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
               by_cases hb : b
               · simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
               · simp only [Bool.not_eq_true] at hb
-                simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, false_ne_true]
+                simp only [hasAssignment, addAssignment, hb, ite_false, ite_true, hasPos_addNeg, reduceCtorEq]
                 simp only [hasAssignment, ite_true] at pacc
                 exact pacc
           · next l_ne_i =>

tests/lean/mutwf1.lean

@@ -6,8 +6,8 @@ mutual
     | n, false => n + g n
   termination_by n b => (n, if b then 2 else 1)
   decreasing_by
-  · apply Prod.Lex.right; simp -- decide TODO: add `reduceCtorEq` at `clean_wf` after update-stage0
-  · apply Prod.Lex.right; simp -- decide
+  · apply Prod.Lex.right; decide
+  · apply Prod.Lex.right; decide
 
   def g (n : Nat) : Nat :=
     if h : n ≠ 0 then