feat: use simp (config := { arith := true }) at decreasing_tactic

closes #262

src/Init/WFTactics.lean

@@ -18,6 +18,7 @@ macro "decreasing_tactic" : tactic =>
     | apply Nat.pred_lt'; assumption           -- i-1 < i if j < i
     | apply Nat.sub_succ_lt_self; assumption   -- a - (i+1) < a - i if i < a
     | assumption
+    | simp (config := { arith := true })
     -- TODO: linearith
     -- TODO: improve
 ))

tests/lean/letRecMissingAnnotation.lean.expected.out

@@ -1,4 +1,4 @@
-letRecMissingAnnotation.lean:4:6-4:34: error: tactic 'assumption' failed
+letRecMissingAnnotation.lean:4:6-4:34: error: unsolved goals
 as : Array Nat
 i s : Nat
 h : i < Array.size as

tests/lean/mutwf1.lean.expected.out

@@ -3,7 +3,7 @@ case h.a
 n : Nat
 h : n ≠ 0
 ⊢ Nat.sub n 0 ≠ 0
-mutwf1.lean:37:22-37:28: error: tactic 'assumption' failed
+mutwf1.lean:37:22-37:28: error: unsolved goals
 case h
 n : Nat
-⊢ n + 1 < n
+⊢ False

tests/lean/run/262.lean

@@ -0,0 +1,16 @@
+mutual
+
+inductive ConE : Type where
+| nilE : ConE
+| extE : ConE → TyE → ConE
+
+inductive TyE : Type where
+| UE : ConE → TyE
+
+end
+
+def length (ΓE : ConE) : Nat :=
+  match ΓE with
+  | ConE.nilE => 0
+  | ConE.extE ΓE AE => (length ΓE) + 1
+termination_by _ e => e

tests/lean/wf2.lean.expected.out

@@ -1,3 +1,3 @@
-wf2.lean:3:8-3:17: error: tactic 'assumption' failed
+wf2.lean:3:8-3:17: error: unsolved goals
 x y : Nat
 ⊢ x - 1 < x