remove nat hack

leanprover-community · Nov 1, 2023 · 96be0b3 · 96be0b3
1 parent f2fc75c
commit 96be0b3
Show file tree

Hide file tree

Showing 6 changed files with 42 additions and 34 deletions.
diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean
@@ -23,8 +23,8 @@ If `a` and `d` are natural numbers, then `add_succ a d` is the proof that
 @[MyNat_decide]
 axiom add_succ (a d : MyNat) : a + (succ d) = succ (a + d)
 
--- don't tell the viewers, we cheat with decide because
--- we used axioms to define nat
-@[MyNat_decide]
-theorem toNat_add (m n : MyNat) : (m + n).toNat = m.toNat + n.toNat := by
-  induction n <;> simp [MyNat_decide, Nat.add_succ, *];
+-- -- don't tell the viewers, we cheat with decide because
+-- -- we used axioms to define nat
+-- @[MyNat_decide]
+-- theorem toNat_add (m n : MyNat) : (m + n).toNat = m.toNat + n.toNat := by
+--   induction n <;> simp [MyNat_decide, Nat.add_succ, *];
diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
@@ -6,6 +6,9 @@ import Game.Levels.Algorithm.L07succ_ne_succ
 import Mathlib.Tactic
 namespace MyNat
 
+@[MyNat_decide]
+lemma ofNat_succ : (OfNat.ofNat (Nat.succ n) : ℕ) = MyNat.succ (OfNat.ofNat n) := _root_.rfl
+
 macro "MyDecide" : tactic => `(tactic|(
   try simp only [MyNat_decide]
   try decide
@@ -40,6 +43,7 @@ example : 4 ≠ 5 := by
 example : (0 : ℕ) + 0 = 0 := by
   MyDecide
 
+set_option pp.all true in
 example : (2 : ℕ) + 2 = 4 := by
   MyDecide
 
@@ -58,9 +62,10 @@ example : (2 : ℕ) * 2 ≠ 5 := by
 example : (3 : ℕ) ^ 2 ≠ 37 := by
   MyDecide
 
-example : (2 : ℕ) ≤ 3 := by
-  MyDecide
+-- **TODO** uncomment test when decidableLE instance is created
+-- example : (2 : ℕ) ≤ 3 := by
+--   MyDecide
 
--- **TODO** uncomment test when Divisibility World hits
+-- **TODO** uncomment test when Divisibility World hits and decidableDvd instance is created
 -- example : (2 : ℕ) ∣ 4 := by MyDecide
 --
diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean
@@ -33,9 +33,12 @@ instance instofNat {n : Nat} : OfNat MyNat n where
 instance : ToString MyNat where
   toString p := toString (toNat p)
 
-@[MyNat_decide]
+@[simp]
 theorem zero_eq_0 : MyNat.zero = 0 := rfl
 
+@[MyNat_decide]
+theorem zero_eq_zero : (0 : ℕ) = MyNat.zero := rfl
+
 def one : MyNat := MyNat.succ 0
 
 -- TODO: Why does this not work here??
@@ -46,15 +49,15 @@ theorem eq_toNat_eq : ∀ (m n : MyNat), m.toNat = n.toNat → m = n
   | zero, zero, _ => rfl
   | succ m, succ n, h => congrArg succ $ eq_toNat_eq m n (Nat.succ.inj h)
 
-@[MyNat_decide]
-theorem eq_iff_eq_toNat (m n : MyNat) : m = n ↔ m.toNat = n.toNat := by
-  refine ⟨by simp_all, eq_toNat_eq _ _⟩
+--@[MyNat_decide]
+--theorem eq_iff_eq_toNat (m n : MyNat) : m = n ↔ m.toNat = n.toNat := by
+--  refine ⟨by simp_all, eq_toNat_eq _ _⟩
 
-@[MyNat_decide]
-theorem ne_iff_ne_toNat (m n : MyNat) : m ≠ n ↔ m.toNat ≠ n.toNat := by
-  simp [MyNat_decide]
+--@[MyNat_decide]
+--theorem ne_iff_ne_toNat (m n : MyNat) : m ≠ n ↔ m.toNat ≠ n.toNat := by
+--  simp [MyNat_decide]
 
-@[MyNat_decide]
-theorem toNat_ofNat : ∀ (n : Nat), (MyNat.ofNat n).toNat = n
-  | .zero => rfl
-  | .succ n => congrArg Nat.succ (toNat_ofNat n)
+--@[MyNat_decide]
+--theorem toNat_ofNat : ∀ (n : Nat), (MyNat.ofNat n).toNat = n
+--  | .zero => rfl
+--  | .succ n => congrArg Nat.succ (toNat_ofNat n)
diff --git a/Game/MyNat/LE.lean b/Game/MyNat/LE.lean
@@ -22,15 +22,15 @@ theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c :=
 
 example (a b : Nat) : a ≤ b ↔ ∃ c, b = a + c := by exact _root_.le_iff_exists_add
 
-@[MyNat_decide]
-theorem toNat_le (m n : MyNat) : m ≤ n ↔ m.toNat ≤ n.toNat :=
-⟨ fun ⟨a, ha⟩ ↦ _root_.le_iff_exists_add.2 ⟨toNat a, by simp [ha, MyNat_decide]⟩,
-  by
-    intro h
-    rw [_root_.le_iff_exists_add] at h
-    cases' h with c hc
-    use ofNat c
-    simp [MyNat_decide, hc]⟩
+-- @[MyNat_decide]
+-- theorem toNat_le (m n : MyNat) : m ≤ n ↔ m.toNat ≤ n.toNat :=
+-- ⟨ fun ⟨a, ha⟩ ↦ _root_.le_iff_exists_add.2 ⟨toNat a, by simp [ha, MyNat_decide]⟩,
+--   by
+--     intro h
+--     rw [_root_.le_iff_exists_add] at h
+--     cases' h with c hc
+--     use ofNat c
+--     simp [MyNat_decide, hc]⟩
 
 --  induction n <;> simp [MyNat_decide, *, Nat.pow_zero, Nat.pow_succ];
 

diff --git a/Game/MyNat/Multiplication.lean b/Game/MyNat/Multiplication.lean
@@ -13,6 +13,6 @@ axiom mul_zero (a : MyNat) : a * 0 = 0
 @[MyNat_decide]
 axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a
 
-@[MyNat_decide]
-theorem toNat_mul (m n : MyNat) : (m * n).toNat = m.toNat * n.toNat := by
-  induction n <;> simp [MyNat_decide, *, Nat.mul_succ];
+-- @[MyNat_decide]
+-- theorem toNat_mul (m n : MyNat) : (m * n).toNat = m.toNat * n.toNat := by
+--   induction n <;> simp [MyNat_decide, *, Nat.mul_succ];
diff --git a/Game/MyNat/Power.lean b/Game/MyNat/Power.lean
@@ -16,8 +16,8 @@ axiom pow_zero (m : ℕ) : m ^ 0 = 1
 @[MyNat_decide]
 axiom pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m
 
-@[MyNat_decide]
-theorem toNat_pow (m n : MyNat) : (m ^ n).toNat = m.toNat ^ n.toNat := by
-  induction n <;> simp [MyNat_decide, *, Nat.pow_zero, Nat.pow_succ];
+-- @[MyNat_decide]
+-- theorem toNat_pow (m n : MyNat) : (m ^ n).toNat = m.toNat ^ n.toNat := by
+--   induction n <;> simp [MyNat_decide, *, Nat.pow_zero, Nat.pow_succ];
 
 end MyNat