From 96be0b30ac69e050bd90f2a9913edfd55a3a54b9 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 1 Nov 2023 00:12:20 +0000 Subject: [PATCH] remove nat hack --- Game/MyNat/Addition.lean | 10 +++++----- Game/MyNat/DecidableEq.lean | 11 ++++++++--- Game/MyNat/Definition.lean | 25 ++++++++++++++----------- Game/MyNat/LE.lean | 18 +++++++++--------- Game/MyNat/Multiplication.lean | 6 +++--- Game/MyNat/Power.lean | 6 +++--- 6 files changed, 42 insertions(+), 34 deletions(-) diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean index ebeac00..ae314ef 100644 --- 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 index 5703900..96d5ca5 100644 --- 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 index abbdef7..3225f28 100644 --- 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 index 3a84707..831b6d2 100644 --- 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 index e26c14c..3a5992f 100644 --- 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 index 2af501f..4eed2f0 100644 --- 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