fix tests

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

@@ -210,7 +210,7 @@ theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} → (l : { l : List α // l
     | nil => simp at w'
     | cons x l' =>
       cases l' with
-      | nil => simp at w'; omega
+      | nil => simp at w'
       | cons y l' =>
         rw [mergeSort]
         congr 2

src/Init/Data/Nat/Lemmas.lean

@@ -50,6 +50,11 @@ protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
 @[simp] protected theorem add_right_cancel_iff {n : Nat} : m + n = k + n ↔ m = k :=
   ⟨Nat.add_right_cancel, fun | rfl => rfl⟩
 
+@[simp] protected theorem add_left_eq_self  {a b : Nat} : a + b = b ↔ a = 0 := by omega
+@[simp] protected theorem add_right_eq_self {a b : Nat} : a + b = a ↔ b = 0 := by omega
+@[simp] protected theorem self_eq_add_right {a b : Nat} : a = a + b ↔ b = 0 := by omega
+@[simp] protected theorem self_eq_add_left  {a b : Nat} : a = b + a ↔ b = 0 := by omega
+
 @[simp] protected theorem add_le_add_iff_left {n : Nat} : n + m ≤ n + k ↔ m ≤ k :=
   ⟨Nat.le_of_add_le_add_left, fun h => Nat.add_le_add_left h _⟩
 

tests/lean/run/2669.lean

@@ -6,7 +6,7 @@ def f : Nat → Nat := fun x => x - x
 example (n : Nat) : False := by
   let g := f n
   have : g + n = n := by
-    fail_if_success simp (config := { zeta := false }) [Nat.zero_add] -- Should not succeed
+    fail_if_success simp (config := { zeta := false }) [Nat.zero_add, -Nat.add_left_eq_self] -- Should not succeed
     simp [g]
   sorry
 

tests/lean/run/4290.lean

@@ -1,3 +1,5 @@
+attribute [-simp] Nat.self_eq_add_right -- This was later added to the simp set and interfere with the test.
+
 def foo : Nat := 0
 def bar : Nat := 0
 

tests/lean/run/letDeclSimp.lean

@@ -1,3 +1,5 @@
+attribute [-simp] Nat.add_left_eq_self -- This was later added to the simp set and interfere with the test.
+
 example (a : Nat) : let n := 0; n + a = a := by
   intro n
   fail_if_success simp (config := { zeta := false })

tests/lean/simp_trace.lean

@@ -83,6 +83,9 @@ example : (a ∧ (b ∧ b)) = (a ∧ b) := by simp only [my_thm]
 example : x - 1 + 1 = x := by simp (discharger := sorry) [Nat.sub_add_cancel]
 
 -- The following examples test simplification at hypotheses.
+section
+-- These lemmas were subsequently added to the simp set and confuse the test.
+attribute [-simp] Nat.add_left_eq_self Nat.add_right_eq_self
 
 -- Two simp lemmas applied to one hypothesis.
 example (h' : bla x = x) : x + x = x := by
@@ -114,6 +117,8 @@ example (h' : bla x = x) : bla x = x := by
   simp [bla, h] at *
   exact h'
 
+end
+
 -- This example tests tracing of class projections.
 
 class HasProp (A) where

tests/lean/simp_trace.lean.expected.out

@@ -75,7 +75,7 @@ Try this: simp only [bla, h] at h'
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 Try this: simp only [bla, h, List.length_append] at *
-simp_trace.lean:99:101-100:40: error: unsolved goals
+simp_trace.lean:102:101-103:40: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α
@@ -88,7 +88,7 @@ h₂ : xs.length + ys.length = y
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 [Meta.Tactic.simp.rewrite] List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
 Try this: simp only [bla, h, List.length_append] at *
-simp_trace.lean:103:101-104:53: error: unsolved goals
+simp_trace.lean:106:101-107:53: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α