chore: update tests

tests/lean/allFieldForConstants.lean

@@ -105,7 +105,7 @@ mutual
 
   theorem listStringLen_flatList (cs : List Foo) : listStringLen (flatList cs) = textLengthList cs := by
     match cs with
-    | [] => simp
+    | [] => simp [listStringLen]
     | f :: fs => simp [listStringLen_append, listStringLen_flatList fs, listStringLen_flat f]
 end
 

tests/lean/letFun.lean

@@ -7,4 +7,4 @@
 example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
   simp (config := { beta := false }) [h1]
   trace_state
-  simp [h2]
+  simp (config := { decide := true }) [h2]

tests/lean/matchOfNatIssue.lean

@@ -1,7 +1,7 @@
 example (x : Int) (h : x = 2) : Int.div 2 1 = x := by
   simp [Int.div]
   trace_state
-  simp [h]
+  simp (config := { decide := true }) [h]
 
 example (n : Nat) : Int.div (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n / 0) := by
   simp [Int.div]

tests/lean/run/1293.lean

@@ -15,7 +15,7 @@ instance {arr : Array String} {f : String → String} {n : Nat} : Coe (Array (Id
 
 def store1 : Store := {
   arr := #["a", "b", "c", "d", "e"]
-  ids := #[⟨2, by simp⟩]
+  ids := #[⟨2, by decide⟩]
 }
 
 def tryCoeStore := {

tests/lean/run/1302.lean

@@ -1,6 +1,6 @@
 @[simp] theorem get_cons_zero {as : List α} : (a :: as).get ⟨0, Nat.zero_lt_succ _⟩ = a := rfl
 
-example (a b c : α) : [a, b, c].get ⟨0, by simp⟩ = a := by
+example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
   simp
 
 example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
@@ -9,5 +9,5 @@ example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
 example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
   simp
 
-example (a b c : α) : [a, b, c].get ⟨0, by simp⟩ = a := by
+example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
   rw [get_cons_zero]

tests/lean/run/1380.lean

@@ -4,6 +4,6 @@ theorem Nat.lt_succ_iff {m n : Nat} : m < succ n ↔ m ≤ n := sorry
 variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
 theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial
 set_option trace.Meta.Tactic.simp true in
-example (hv: v₁ < v₂) : True := foo n v₁ v₂ ‹_› ‹_› (by simp only[hv, Fin.mk.injEq, Nat.ne_of_gt, Nat.lt_succ_iff])
+example (hv: v₁ < v₂) : True := foo n v₁ v₂ ‹_› ‹_› (by simp (config := { decide := true }) only [hv, Fin.mk.injEq, Nat.ne_of_gt, Nat.lt_succ_iff])
 
 #check Fin.mk.injEq

tests/lean/run/1921.lean

@@ -1,9 +1,9 @@
 @[simp] theorem Array.size_singleton : #[a].size = 1 := rfl
-@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases usize_size_eq <;> simp [*]
+@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases usize_size_eq <;> simp (config := { decide := true }) [*]
 
 def f := #[true].any id 0 USize.size
 
 -- `native_decide` used to prove `false` here, due to a bug in `Array.anyMUnsafe`.
 example : f = true := by native_decide
 
-example : f = true := by simp [f, Array.any, Array.anyM]
+example : f = true := by simp (config := { decide := true }) [f, Array.any, Array.anyM]

tests/lean/run/891.lean

@@ -44,7 +44,7 @@ example : f 'b' n = 2 := by
   simp[f]
 
 example : f 'c' n = 3 := by
-  simp[f]
+  simp (config := { decide := true }) [f]
 
 def g : String → Nat → Nat
  | "hello", _ => 1
@@ -58,7 +58,7 @@ example : g "world" n = 2 := by
   simp[g]
 
 example : g "abc" n = 3 := by
-  simp[g]
+  simp (config := { decide := true }) [g]
 
 def fn : Fin 8 → Nat → Nat
  | 2, _ => 1

tests/lean/run/def10.lean

@@ -27,4 +27,4 @@ theorem ex6 : g x y z > 0 := by
   split
   next => decide
   next => decide
-  next a b c h₁ h₂ => simp [f_eq h₁]
+  next a b c h₁ h₂ => simp (config := { decide := true }) [f_eq h₁]

tests/lean/run/defaultEliminator.lean

@@ -28,4 +28,4 @@ example (x y : Nat) : f x y > 0 := by
   | succ_succ x y ih => simp [f, ih]
 
 example (x y : Nat) : f x y > 0 := by
-  induction x, y <;> simp [f, *]
+  induction x, y <;> simp (config := { decide := true }) [f, *]

tests/lean/run/eqnsAtSimp.lean

@@ -15,5 +15,5 @@ decreasing_by
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
-  | zero => simp
+  | zero => simp [isEven]
   | succ x ih => simp [Nat.mul_succ, Nat.add_succ, isEven, isOdd, ih]

tests/lean/run/maze.lean

@@ -292,5 +292,5 @@ def maze1 := ┌───┐
 def foo : can_escape maze1 := by
   apply step_west
   set_option trace.Meta.debug true in
-  simp
+  simp (config := { decide := true })
   out

tests/lean/run/mergeSortCPDT.lean

@@ -26,8 +26,8 @@ theorem List.length_split_of_atLeast2 {as : List α} (h : as.atLeast2) : as.spli
   match as with
   | []  => simp at h
   | [_] => simp at h
-  | [_, _] => simp [split]
-  | [_, _, _] => simp [split]
+  | [_, _] => simp (config := { decide := true }) [split]
+  | [_, _, _] => simp (config := { decide := true }) [split]
   | a::b::c::d::as =>
     -- TODO: simplify using linear arith and more automation
     have : (c::d::as).atLeast2 := by simp_arith

tests/lean/run/mutualDefThms.lean

@@ -54,7 +54,7 @@ mutual
 
   theorem listStringLen_flatList (cs : List Foo) : listStringLen (flatList cs) = textLengthList cs := by
     match cs with
-    | [] => simp
+    | [] => simp [listStringLen]
     | f :: fs => simp [listStringLen_append, listStringLen_flatList fs, listStringLen_flat f]
 end
 

tests/lean/run/set.lean

@@ -8,7 +8,7 @@ def Set.pred (p : α → Prop) : Set α := p
 notation "{" a "|" p "}" => Set.pred (fun a => p)
 
 theorem ex1 : (1, 3) ∈ { (n, m) | n < 2 ∧ m < 5 } := by
-  simp [Set.in, Set.pred]
+  simp (config := { decide := true }) [Set.in, Set.pred]
 
 def Set.union (s₁ s₂ : Set α) : Set α :=
   { a | a ∈ s₁ ∨ a ∈ s₂ }

tests/lean/run/simp6.lean

@@ -16,13 +16,13 @@ theorem ex5 : (10 = 20) = False :=
 #print ex5
 
 theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
-  by simp
+  by simp (config := { decide := true })
 
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
   fail_if_success simp (config := { decide := false })
-  simp
+  simp (config := { decide := true })
 
 theorem ex8 : (10 + 2000 = 20) = False :=
   by simp
@@ -32,4 +32,4 @@ def fact : Nat → Nat
   | x+1 => (x+1) * fact x
 
 theorem ex9 : (if fact 100 > 10 then true else false) = true :=
-  by simp
+  by simp (config := { decide := true })

tests/lean/run/simp_all.lean

@@ -13,7 +13,7 @@ theorem ex3 (h₁ : a = 0) (h₂ : a + b = 0) : f (b + c) = c := by
   simp [h₂]
 
 theorem ex4 (h₁ : a = f a) (h₂ : b + 0 = 0) : f b = 0 := by
-  simp_all [-h₁]
+  simp_all (config := { decide := true }) [-h₁]
 
 theorem ex5 (h₁ : a = f a) (h₂ : b + 0 = 0) : f (b + a) = a := by
   simp_all [-h₁, f]

tests/lean/unfold1.lean

@@ -11,7 +11,7 @@ decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
-  | zero => simp
+  | zero => simp [isEven]
   | succ x ih =>
     unfold isEven
     trace_state