add decide tactic hack to Game/Tactic

leanprover-community · Nov 12, 2023 · 2500632 · 2500632
1 parent f5e9e29
commit 2500632
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 5 deletions.
diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
@@ -2,17 +2,14 @@ import Game.MyNat.Addition-- makes simps work?
 import Game.MyNat.PeanoAxioms
 import Game.Levels.Algorithm.L07succ_ne_succ
 import Mathlib.Tactic
+import Game.Tactic.decide
+
 namespace MyNat
 
 -- to get numerals of type MyNat to reduce to MyNat.succ (MyNat.succ ...)
 @[MyNat_decide]
 lemma ofNat_succ : (OfNat.ofNat (Nat.succ n) : ℕ) = MyNat.succ (OfNat.ofNat n) := _root_.rfl
 
-macro "decide" : tactic => `(tactic|(
-  try simp only [MyNat_decide]
-  try decide
-))
-
 instance instDecidableEq : DecidableEq MyNat
 | 0, 0 => isTrue <| by
   show 0 = 0

diff --git a/Game/Tactic/decide.lean b/Game/Tactic/decide.lean
@@ -0,0 +1,9 @@
+/- modified `decide` tactic which first runs a custom
+simp call to reduce numerals like `1 + 1` to
+`MyNat.succ (MyNat.succ MyNat.zero)
+-/
+
+macro "decide" : tactic => `(tactic|(
+  try simp only [MyNat_decide]
+  try decide
+))