From b42415de68be1f9aeaf4d483848a54602e138ecc Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 12 Nov 2023 12:10:25 +0000
Subject: [PATCH] remove incomplete code

---
 Game/MyNat/DecidableDvd.lean | 31 -----------------------------
 Game/MyNat/DecidableLe.lean  | 38 ------------------------------------
 2 files changed, 69 deletions(-)
 delete mode 100644 Game/MyNat/DecidableDvd.lean
 delete mode 100644 Game/MyNat/DecidableLe.lean

diff --git a/Game/MyNat/DecidableDvd.lean b/Game/MyNat/DecidableDvd.lean
deleted file mode 100644
index cd29645..0000000
--- a/Game/MyNat/DecidableDvd.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import Game.MyNat.DecidableLe
-import Game.Levels.LessOrEqual
-import Game.Levels.Multiplication
-
--- NOTE: this probably needs a whole new "advanced algorithm world"
--- where we develop a theory of a % b computably, and show that for b > 0,
--- b ∣ a ↔ a % b = 0 (and hence it's decidable)
-
-namespace MyNat
-
-instance : Dvd MyNat where
-  dvd a b := ∃ c, a * c = b
-
-instance instDecidableDvd : DecidableRel (α := ℕ) (· ∣ ·)
-| 0, 0 => isTrue <| by
-  show _ ∣ 0
-  use 0
-  rw [mul_zero]
-  rfl
-| 0, succ m => isFalse <| by
-  rintro ⟨a, ha⟩
-  rw [zero_mul] at ha
-  apply zero_ne_succ at ha
-  exact ha
-| succ m, n =>
-  show Decidable (succ m ∣ n) by
-  -- idea : just show m ∣ n iff n % m = 0 and show that n % m is computable
-  sorry
-
--- *TODO* uncomment when working
--- example : (2 : ℕ) ∣ 4 := by MyDecide
diff --git a/Game/MyNat/DecidableLe.lean b/Game/MyNat/DecidableLe.lean
deleted file mode 100644
index a78d7d2..0000000
--- a/Game/MyNat/DecidableLe.lean
+++ /dev/null
@@ -1,38 +0,0 @@
-import Game.MyNat.DecidableEq
-import Game.Levels.LessOrEqual
-
-namespace MyNat
-
-instance instDecidableLe : DecidableRel (α := ℕ) (· ≤ ·)
-| 0, _ => isTrue <| by
-  show 0 ≤ _
-  apply MyNat.zero_le
-| succ m, 0 => isFalse <| by
-  show ¬ succ m ≤ 0
-  rintro ⟨a, ha⟩
-  symm at ha
-  apply eq_zero_of_add_right_eq_zero at ha
-  apply succ_ne_zero at ha
-  exact ha
-| succ m, succ n =>
-  match instDecidableLe m n with
-  | isTrue (h : m ≤ n) => isTrue <| by
-    show succ m ≤ succ n
-    rcases h with ⟨a, rfl⟩
-    use a
-    rw [succ_add]
-    rfl
-  | isFalse (h : ¬ m ≤ n) => isFalse <| by
-    show ¬ succ m ≤ succ n
-    contrapose! h
-    rcases h with ⟨a, ha⟩
-    use a
-    rw [succ_add] at ha
-    apply succ_inj at ha
-    exact ha
-
-example : (20 : ℕ) ≤ 30 := by
-  decide
-
-example : ¬ ((30 : ℕ) ≤ 20) := by
-  decide