feat: allow users to disable simpCtorEq simproc (#5167)

`simp only` will not apply this simproc anymore. Users must now write
`simp only [reduceCtorEq]`. See RFC #5046 for motivation.
This PR also renames simproc to `reduceCtorEq`. 

close #5046 


@semorrison A few `simp only ...` tactics will probably break in
Mathlib. Fix: include `reduceCtorEq`.

src/Init/ByCases.lean

@@ -57,7 +57,8 @@ 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
-  simp only [ite_eq_right_iff]
+  have : some x ≠ none := Option.noConfusion
+  simp only [ite_eq_right_iff, this]
   rfl
 
 @[simp] theorem ite_some_none_eq_some [Decidable P] :

src/Init/Data/AC.lean

@@ -260,7 +260,7 @@ theorem Context.evalList_sort (ctx : Context α) (h : ContextInformation.isComm
     simp [ContextInformation.isComm, Option.isSome] at h
     match h₂ : ctx.comm with
     | none =>
-      simp only [h₂] at h
+      simp [h₂] at h
     | some val =>
       simp [h₂] at h
       exact val.down

src/Init/Data/BitVec/Lemmas.lean

@@ -993,8 +993,9 @@ 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
-  · simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
-      BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte]
+  · 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]
     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 only [h, not_true_eq_false, decide_False, not_false_eq_true]
+      · simp [h, not_true_eq_false, decide_False, not_false_eq_true]
     else
       rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]
       · rfl
-      · simp only [h, not_false_eq_true, decide_True]
+      · simp [h, not_false_eq_true, decide_True]
 
 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 only [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
+      simp [hc_beq, if_false, count_cons, count_cons, count_erase a b l]
       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 only [false_or]
+    · simp
       constructor
       · rintro rfl
         simpa
       · rintro ⟨_, _, rfl, rfl⟩
         rfl
-    · simp only [cons.injEq, false_or, false_iff, not_exists, not_and]
+    · simp
       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 only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
+    simp [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
     split
     · simp_all
-    · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
+    · simp_all [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone]
       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/Lemmas.lean

@@ -639,7 +639,7 @@ theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α
       exact Nat.succ_le_succ_iff.mp h
 
 @[simp] theorem set_eq_nil (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by
-  cases l <;> cases n <;> simp only [set]
+  cases l <;> cases n <;> simp [set]
 
 theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
     (l.set n a).set m b = (l.set m b).set n a
@@ -1874,7 +1874,7 @@ theorem join_eq_append (xs : List (List α)) (ys zs : List α) :
   · induction xs generalizing ys with
     | nil =>
       simp only [join_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
-        exists_false, or_false, and_imp]
+        exists_false, or_false, and_imp, List.cons_ne_nil]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
     | cons x xs ih =>

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 only [range'_succ, false_and, cons.injEq, true_and, ih, exists_eq_left', false_or]
+        simp [range'_succ, ih, exists_eq_left']
         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 only [e, false_implies, implies_true, true_and, IH]
+    simp [e, false_implies, implies_true, true_and, IH]
   | 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 only [↓reduceIte, map_cons, cons.injEq, true_and]
+    · simp [↓reduceIte, map_cons, cons.injEq, true_and]
       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/List/Sublist.lean

@@ -767,7 +767,7 @@ theorem prefix_cons_iff : l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :
         refine ⟨s, by simp [h']⟩
 
 @[simp] theorem cons_prefix_cons : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂ := by
-  simp only [prefix_cons_iff, cons.injEq, false_or]
+  simp only [prefix_cons_iff, cons.injEq, false_or, List.cons_ne_nil]
   constructor
   · rintro ⟨t, ⟨rfl, rfl⟩, h⟩
     exact ⟨rfl, h⟩

src/Init/Data/Nat/Basic.lean

@@ -887,7 +887,7 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
 
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
-  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true]
+  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true, Nat.succ_ne_zero]
   | succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
   | succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)
 

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 only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
+      simp [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
       have ⟨d, dif⟩   := hyp x_pos xnz
       apply Exists.intro (d+1)
       simp_all
@@ -209,7 +209,7 @@ theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = fal
   have x_ge_n := Nat.ge_of_not_lt not_lt
   have ⟨i, ⟨i_ge_n, test_true⟩⟩ := ge_two_pow_implies_high_bit_true x_ge_n
   have test_false := p _ i_ge_n
-  simp only [test_true] at test_false
+  simp [test_true] at test_false
 
 private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
   induction x with

src/Init/Data/Nat/Div.lean

@@ -221,7 +221,7 @@ theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
   induction y, k using mod.inductionOn generalizing x with
     (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
   | base y k h =>
-    simp only [add_one, succ_mul, false_iff, Nat.not_le]
+    simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero]
     refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
     exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
   | ind y k h IH =>

src/Init/Data/Option/Lemmas.lean

@@ -162,7 +162,7 @@ theorem map_some : f <$> some a = some (f a) := rfl
 theorem map_eq_some : f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b := map_eq_some'
 
 @[simp] theorem map_eq_none' : x.map f = none ↔ x = none := by
-  cases x <;> simp only [map_none', map_some', eq_self_iff_true]
+  cases x <;> simp [map_none', map_some', eq_self_iff_true]
 
 theorem isSome_map {x : Option α} : (f <$> x).isSome = x.isSome := by
   cases x <;> simp

src/Lean/Meta/CtorRecognizer.lean

@@ -82,7 +82,13 @@ def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr))
       else return some (val, #[mkNatAdd e (toExpr (k-1))])
   else if let some r ← constructorApp? e then
     return some r
-  else
+  else try
+    /-
+    We added the `try` block here because `whnf` fails at terms `n ^ m`
+    when `m` is a big numeral, and `n` is a numeral. This is a little bit hackish.
+    -/
     constructorApp? (← whnf e)
+  catch _ =>
+    return none
 
 end Lean.Meta

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

@@ -75,3 +75,14 @@ builtin_dsimproc ↓ [simp, seval] dreduceDIte (dite _ _ _) := fun e => do
     | Decidable.isFalse _ h => return .visit (mkApp eb h).headBeta
     | _ => return .continue
   return .continue
+
+builtin_simproc [simp, seval] reduceCtorEq (_ = _) := fun e => withReducibleAndInstances do
+  let_expr Eq _ lhs rhs ← e | return .continue
+  match (← constructorApp'? lhs), (← constructorApp'? rhs) with
+  | some (c₁, _), some (c₂, _) =>
+    if c₁.name != c₂.name then
+      withLocalDeclD `h e fun h =>
+        return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
+    else
+      return .continue
+  | _, _ => return .continue

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

@@ -255,19 +255,6 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
-def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
-  match e.eq? with
-  | none => return .continue
-  | some (_, lhs, rhs) =>
-    match (← constructorApp'? lhs), (← constructorApp'? rhs) with
-    | some (c₁, _), some (c₂, _) =>
-      if c₁.name != c₂.name then
-        withLocalDeclD `h e fun h =>
-          return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
-      else
-        return .continue
-    | _, _ => return .continue
-
 @[inline] def simpUsingDecide : Simproc := fun e => do
   unless (← getConfig).decide do
     return .continue
@@ -446,8 +433,7 @@ partial def preSEval (s : SimprocsArray) : Simproc :=
 def postSEval (s : SimprocsArray) : Simproc :=
   rewritePost >>
   userPostSimprocs s >>
-  sevalGround >>
-  simpCtorEq
+  sevalGround
 
 def mkSEvalMethods : CoreM Methods := do
   let s ← getSEvalSimprocs
@@ -515,7 +501,6 @@ def postDefault (s : SimprocsArray) : Simproc :=
   userPostSimprocs s >>
   simpGround >>
   simpArith >>
-  simpCtorEq >>
   simpUsingDecide
 
 /--

src/Std/Sat/AIG/RelabelNat.lean

@@ -137,7 +137,7 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap
     next idx' _ _ =>
     replace hidx : idx ≤ idx' := by omega
     cases Nat.eq_or_lt_of_le hidx with
-    | inl hidxeq => simp only [hidxeq, ih3] at heq
+    | inl hidxeq => simp [hidxeq, ih3] at heq
     | inr hlt => apply ih4 <;> assumption
   | gate ih1 ih2 ih3 ih4 =>
     next idx' _ _ _ _ _ =>

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 only [false_iff]
+    simp [false_iff]
     apply hne
 
 def negate (c : DefaultClause n) : CNF.Clause (PosFin n) := c.clause.map Literal.negate
@@ -183,13 +183,13 @@ def insert (c : DefaultClause n) (l : Literal (PosFin n)) : Option (DefaultClaus
         · apply Or.inr
           constructor
           · intro heq
-            simp only [← heq] at hl
+            simp [← heq] at hl
           · simpa [hl, ← l'_eq_l] using heq1
         · simp only [Bool.not_eq_true] at hl
           apply Or.inl
           constructor
           · intro heq
-            simp only [← heq] at hl
+            simp [← heq] at hl
           · simpa [hl, ← l'_eq_l] using heq1
       · next l'_ne_l =>
         have := c.nodupkey l'
@@ -250,14 +250,14 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
     intro c' heq
     simp only [Fin.getElem_fin, fold_fn] at heq
     split at heq
-    · simp only at heq
+    · simp at heq
     · next acc =>
       specialize ih acc rfl
       rcases ih with ⟨hsize, ih⟩
       simp only at ih
       simp only [insert] at heq
       split at heq
-      · exact False.elim heq
+      · simp at heq
       · split at heq
         · next h_dup =>
           exfalso -- h_dup contradicts arrNodup

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 only [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
+              simp [hasAssignment, b_eq_false, ite_false, hasNeg_addPos] at h
               specialize ih l false
-              simp only [hasAssignment, ite_false] at ih
+              simp [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 only [hasAssignment, b_eq_false, l_eq_i, Array.getElem_modify_self i_in_bounds, ite_false, hasNeg_addPos] at hb
-          simp only [hasAssignment, b_eq_false, ite_false, hb]
+          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]
         · next l_ne_i =>
           simp only [Array.getElem_modify_of_ne i_in_bounds _ l_ne_i] at hb
           exact hb
@@ -508,9 +508,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq, not] at l_ne_b
-              split at l_ne_b
-              · simp only at l_ne_b
-              · simp only at l_ne_b
+              split at l_ne_b <;> simp at l_ne_b
             · next id_ne_idx => simp [id_ne_idx]
           · exact hf
         · exact Or.inr hf
@@ -551,7 +549,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
     · simp only [Prod.exists, Bool.exists_bool, not_exists, not_or, unit] at hl
       split
       · next some_eq_none =>
-        simp only at some_eq_none
+        simp at some_eq_none
       · next l _ _ heq =>
         simp only [Option.some.injEq] at heq
         rw [heq] at hl
@@ -565,7 +563,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
           simp only [deleteOne]
           split
           · next heq2 =>
-            simp only [heq] at heq2
+            simp [heq] at heq2
           · next l _ _ heq2 =>
             simp only [heq, Option.some.injEq] at heq2
             rw [heq2] at hl
@@ -608,9 +606,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
               specialize hl i
               simp only [unit, DefaultClause.mk.injEq, List.cons.injEq, Prod.mk.injEq, true_and, and_true,
                 Bool.not_eq_false, Bool.not_eq_true] at hl
-              by_cases b_val : b
-              · simp only [b_val, and_false] at hl
-              · simp only [b_val, false_and] at hl
+              by_cases b_val : b <;> simp [b_val] at hl
             · next id_ne_idx => simp [id_ne_idx]
           · exact hf
         · exact Or.inr hf
@@ -663,7 +659,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
         rcases List.getElem_of_mem h1 with ⟨i, h, h4⟩
         rw [List.getElem_set] at h4
         split at h4
-        · exact False.elim h4
+        · simp at h4
         · rw [← h4]
           apply List.getElem_mem
       · exact h1