From 0242eb7eded1fbb2f2dc08cff1bde975dceba396 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Feb 2022 09:09:01 -0800
Subject: [PATCH] feat: use `simp (config := { arith := true })` at
 `decreasing_tactic`

closes #262
---
 src/Init/WFTactics.lean                          |  1 +
 .../letRecMissingAnnotation.lean.expected.out    |  2 +-
 tests/lean/mutwf1.lean.expected.out              |  4 ++--
 tests/lean/run/262.lean                          | 16 ++++++++++++++++
 tests/lean/wf2.lean.expected.out                 |  2 +-
 5 files changed, 21 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/262.lean

diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean
index 189e2a3a91..040d7d50fb 100644
--- a/src/Init/WFTactics.lean
+++ b/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
 ))
diff --git a/tests/lean/letRecMissingAnnotation.lean.expected.out b/tests/lean/letRecMissingAnnotation.lean.expected.out
index a7bfe99a96..06403ceb7b 100644
--- a/tests/lean/letRecMissingAnnotation.lean.expected.out
+++ b/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
diff --git a/tests/lean/mutwf1.lean.expected.out b/tests/lean/mutwf1.lean.expected.out
index a320431528..2a11e5c1bd 100644
--- a/tests/lean/mutwf1.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/262.lean b/tests/lean/run/262.lean
new file mode 100644
index 0000000000..1bdf7f375a
--- /dev/null
+++ b/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
diff --git a/tests/lean/wf2.lean.expected.out b/tests/lean/wf2.lean.expected.out
index 0f7891ef0c..54860035bb 100644
--- a/tests/lean/wf2.lean.expected.out
+++ b/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