Replace recursive definitions of algebraic operations with axioms

Game/MyNat/Addition.lean

@@ -2,11 +2,7 @@ import Game.MyNat.Definition
 
 namespace MyNat
 
-open MyNat
-
-def add : MyNat → MyNat → MyNat
-  | a, zero  => a
-  | a, MyNat.succ b => MyNat.succ (MyNat.add a b)
+opaque add : MyNat → MyNat → MyNat
 
 instance instAdd : Add MyNat where
   add := MyNat.add
@@ -17,11 +13,12 @@ instance instAdd : Add MyNat where
 `add_zero` is a `simp` lemma, because if you see `a + 0`
 you usually want to simplify it to `a`.
 -/
-@[simp]
-theorem add_zero (a : MyNat) : a + 0 = a := by rfl
+@[simp, MyNat_decide]
+axiom add_zero (a : MyNat) : a + 0 = a
 
 /--
 If `a` and `d` are natural numbers, then `add_succ a d` is the proof that
 `a + succ d = succ (a + d)`.
 -/
-theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
+@[MyNat_decide]
+axiom add_succ (a d : MyNat) : a + (succ d) = succ (a + d)

Game/MyNat/DecidableEq.lean

@@ -1,7 +1,7 @@
-import Game.MyNat.Addition-- makes simps work?
 import Game.MyNat.PeanoAxioms
-import Game.Levels.Algorithm.L07succ_ne_succ
-import Mathlib.Tactic
+import Game.Levels.Algorithm.L07succ_ne_succ -- succ_ne_succ
+import Game.Tactic.decide -- modified decide tactic
+
 namespace MyNat
 
 instance instDecidableEq : DecidableEq MyNat

Game/MyNat/DecidableTests.lean

@@ -0,0 +1,29 @@
+import Game.MyNat.DecidableEq
+import Game.MyNat.Power
+
+example : 4 = 4 := by
+  decide
+
+example : 4 ≠ 5 := by
+  decide
+
+example : (0 : ℕ) + 0 = 0 := by
+  decide
+
+example : (2 : ℕ) + 2 = 4 := by
+  decide
+
+example : (2 : ℕ) + 2 ≠ 5 := by
+  decide
+
+example : (20 : ℕ) + 20 = 40 := by
+  decide
+
+example : (2 : ℕ) * 2 = 4 := by
+  decide
+
+example : (2 : ℕ) * 2 ≠ 5 := by
+  decide
+
+example : (3 : ℕ) ^ 2 ≠ 37 := by
+  decide

Game/MyNat/Definition.lean

@@ -1,3 +1,5 @@
+import Game.Tactic.LabelAttr -- MyNat_decide attribute
+
 /-- Our copy of the natural numbers called `MyNat`, with notation `ℕ`. -/
 inductive MyNat where
 | zero : MyNat
@@ -13,22 +15,25 @@ namespace MyNat
 instance : Inhabited MyNat where
   default := MyNat.zero
 
-def myNatFromNat (x : Nat) : MyNat :=
+@[MyNat_decide]
+def ofNat (x : Nat) : MyNat :=
   match x with
   | Nat.zero   => MyNat.zero
-  | Nat.succ b => MyNat.succ (myNatFromNat b)
+  | Nat.succ b => MyNat.succ (ofNat b)
 
-def natFromMyNat (x : MyNat) : Nat :=
+@[MyNat_decide]
+def toNat (x : MyNat) : Nat :=
   match x with
   | MyNat.zero   => Nat.zero
-  | MyNat.succ b => Nat.succ (natFromMyNat b)
+  | MyNat.succ b => Nat.succ (toNat b)
 
-instance ofNat {n : Nat} : OfNat MyNat n where
-  ofNat := myNatFromNat n
+instance instofNat {n : Nat} : OfNat MyNat n where
+  ofNat := ofNat n
 
 instance : ToString MyNat where
-  toString p := toString (natFromMyNat p)
+  toString p := toString (toNat p)
 
+@[MyNat_decide]
 theorem zero_eq_0 : MyNat.zero = 0 := rfl
 
 def one : MyNat := MyNat.succ 0

Game/MyNat/LE.lean

@@ -15,8 +15,7 @@ def le (a b : ℕ) :=  ∃ (c : ℕ), b = a + c
 -- notation
 instance : LE MyNat := ⟨MyNat.le⟩
 
---@[leakage] theorem le_def' : MyNat.le = (≤) := rfl
-
-theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c := Iff.rfl
+-- We don't use this any more; I tell the users `≤` is *notation*
+-- theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c := Iff.rfl
 
 end MyNat

Game/MyNat/Multiplication.lean

@@ -2,13 +2,13 @@ import Game.MyNat.Addition
 
 namespace MyNat
 
-def mul : MyNat → MyNat → MyNat
-  | _, 0   => 0
-  | a, b + 1 => (MyNat.mul a b) + a
+opaque mul : MyNat → MyNat → MyNat
 
 instance : Mul MyNat where
   mul := MyNat.mul
 
-theorem mul_zero (a : MyNat) : a * 0 = 0 := by rfl
+@[MyNat_decide]
+axiom mul_zero (a : MyNat) : a * 0 = 0
 
-theorem mul_succ (a b : MyNat) : a * (succ b) = a * b + a := by rfl
+@[MyNat_decide]
+axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a

Game/MyNat/PeanoAxioms.lean

@@ -21,7 +21,7 @@ theorem succ_inj (a b : ℕ) (h : succ a = succ b) : a = b := by
 
 def is_zero : ℕ → Prop
 | 0 => True
-| succ n => False
+| succ _ => False
 
 lemma is_zero_zero : is_zero 0 = True := rfl
 lemma is_zero_succ (n : ℕ) : is_zero (succ n) = False := rfl

Game/MyNat/Power.lean

@@ -3,21 +3,16 @@ import Game.MyNat.Multiplication
 namespace MyNat
 open MyNat
 
-def pow : ℕ → ℕ → ℕ
-| _, zero => one
-| m, (succ n) => pow m n * m
+opaque pow : ℕ → ℕ → ℕ
 
+-- notation `a ^ b` for `pow a b`
 instance : Pow ℕ ℕ where
   pow := pow
 
--- notation a ^ b := pow a b
+@[MyNat_decide]
+axiom pow_zero (m : ℕ) : m ^ 0 = 1
 
--- Important note: This here is the real `rfl`, not the weaker game version
-
-example : (1 : ℕ) ^ 1 = 1 := by rfl
-
-theorem pow_zero (m : ℕ) : m ^ 0 = 1 := by rfl
-
-theorem pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := by rfl
+@[MyNat_decide]
+axiom pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m
 
 end MyNat

Game/Tactic/LabelAttr.lean

@@ -0,0 +1,5 @@
+import Std.Tactic.LabelAttr
+import Mathlib.Lean.Meta.Simp
+
+/-- Simp set for `functor_norm` -/
+register_simp_attr MyNat_decide

Game/Tactic/decide.lean

@@ -0,0 +1,16 @@
+import Game.Tactic.LabelAttr
+import Game.MyNat.Definition
+
+-- to get numerals of type MyNat to reduce to MyNat.succ (MyNat.succ ...)
+@[MyNat_decide]
+theorem ofNat_succ : (OfNat.ofNat (Nat.succ n) : ℕ) = MyNat.succ (OfNat.ofNat n) := _root_.rfl
+
+
+/- 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
+))