chore: update RELEASES.md, add tests

RELEASES.md

@@ -11,6 +11,8 @@ of each version.
 v4.4.0 (development in progress)
 ---------
 
+* By default, `simp` will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by `simp`, and the `decide` tactic may be useful in such cases. The `decide` simp configuration option can be used to locally restore the old `simp` behavior, as in `simp (config := {decide := true})`; this includes using Decidable instances to verify side goals such as numeric inequalities.
+
 v4.3.0
 ---------
 

tests/lean/run/simpDecide.lean

@@ -0,0 +1,18 @@
+example : 0 < 4 := by decide
+
+example : 0 < 4 := by
+  fail_if_success { simp only }
+  simp (config := { decide := true }) only
+
+def fib : Nat → Nat
+| 0 => 0
+| 1 => 1
+| n+2 => fib (n+1) + fib n
+
+theorem fib_two : fib 2 = 1 := rfl
+
+example : 1 = fib (1 + 1) := by
+  fail_if_success { simp only [fib_two] }
+  simp (config := { decide := true }) only [fib_two]
+
+example : 1 = fib (1 + 1) := by simp only [fib_two, (by decide : 1 + 1 = 2)]