|
| 1 | +import Mathlib.Tactic |
| 2 | +import Mathlib.Logic.Function.Basic |
| 3 | +import Mathlib.Data.Nat.Basic |
| 4 | +import Mathlib.Data.Nat.ModEq |
| 5 | +-- import Mathlib.CategoryTheory.Category.Basic |
| 6 | +-- import Mathlib.Combinatorics.Quiver.Basic |
| 7 | +import Mathlib.Dynamics.FixedPoints.Basic |
| 8 | +import Mathlib.Dynamics.PeriodicPts.Defs |
| 9 | +import Mathlib.Dynamics.Flow |
| 10 | +import Mathlib.Topology.Defs.Basic |
| 11 | + |
| 12 | +def step (n : Nat) : Nat := |
| 13 | + if Even n then |
| 14 | + n / 2 |
| 15 | + else |
| 16 | + 3 * n + 1 |
| 17 | + |
| 18 | +theorem step.odd_even {n} (h : Odd n) : Even (step n) := by |
| 19 | + simp only [step, Nat.not_even_iff_odd.mpr h] |
| 20 | + apply Odd.add_odd |
| 21 | + · exact Nat.odd_mul.mpr ⟨by decide, h⟩ |
| 22 | + · decide |
| 23 | + |
| 24 | +theorem step.not_injective : ¬ step.Injective := by |
| 25 | + rw [Function.Injective] |
| 26 | + push_neg |
| 27 | + use 1, 8; decide |
| 28 | + |
| 29 | +theorem step.surjective : step.Surjective := by |
| 30 | + intro n |
| 31 | + use 2 * n |
| 32 | + simp [step] |
| 33 | + |
| 34 | +def step.continuous : Continuous step where |
| 35 | + isOpen_preimage := by simp |
| 36 | + |
| 37 | +theorem step.minimalPeriod_one : step.minimalPeriod 1 = 3 := by |
| 38 | + apply Function.minimalPeriod_eq_prime <;> decide |
| 39 | + |
| 40 | +theorem step.one_had_period_3 : step.IsPeriodicPt 3 1 := by |
| 41 | + decide |
| 42 | + |
| 43 | +theorem step.isPeriodicPt_one : 1 ∈ step.periodicPts := by |
| 44 | + rw [Function.mem_periodicPts] |
| 45 | + use 3; decide |
| 46 | + |
| 47 | +def step.periodicOrbit_one : Cycle Nat := |
| 48 | + ↑(List.map (fun (n : ℕ) => step^[n] 1) (List.range 3)) |
| 49 | + |
| 50 | +theorem step.periodicOrbit_one_def : step.periodicOrbit 1 = step.periodicOrbit_one := by |
| 51 | + rw [Function.periodicOrbit, step.minimalPeriod_one] |
| 52 | + decide |
| 53 | + |
| 54 | +theorem step.fixedZero : step.fixedPoints = {0} := by |
| 55 | + rw [Function.fixedPoints] |
| 56 | + ext x |
| 57 | + constructor |
| 58 | + · intro x_fixed |
| 59 | + rw [Set.mem_setOf, Function.IsFixedPt, step] at x_fixed |
| 60 | + simp |
| 61 | + by_cases heven : Even x |
| 62 | + · let ⟨r, hx⟩ := heven |
| 63 | + rw [if_pos heven, hx, <- mul_two, Nat.mul_div_cancel r (by linarith)] at x_fixed |
| 64 | + omega |
| 65 | + · rw [if_neg heven] at x_fixed |
| 66 | + omega |
| 67 | + · simp [Function.IsFixedPt] |
| 68 | + rintro rfl |
| 69 | + decide |
| 70 | + |
| 71 | + |
| 72 | + |
| 73 | + |
| 74 | +variable {n m : Nat} |
| 75 | + |
| 76 | +def GoesTo (n m : Nat) : Prop := |
| 77 | + ∃i, step^[i] n = m |
| 78 | + |
| 79 | +infixr:50 " |=> " => GoesTo |
| 80 | + |
| 81 | +instance GoesTo.Trans : Trans GoesTo GoesTo GoesTo where |
| 82 | + trans {α β γ} := by |
| 83 | + rintro ⟨ia, rfl⟩ ⟨ib, rfl⟩ |
| 84 | + exact ⟨ib + ia, Function.iterate_add_apply step ib ia α⟩ |
| 85 | + |
| 86 | +def GoesTo.trans : Transitive GoesTo := by intro α β γ αβ βγ; exact GoesTo.Trans.trans αβ βγ |
| 87 | + |
| 88 | +@[refl] |
| 89 | +theorem GoesTo.rfl : n |=> n := ⟨0, by simp⟩ |
| 90 | +theorem GoesTo.reflexive : Reflexive GoesTo := by intro x; rfl |
| 91 | + |
| 92 | + |
| 93 | +def GoesTo.flow : Flow ℕ ℕ := |
| 94 | + Flow.fromIter step.continuous |
| 95 | + |
| 96 | +theorem GoesTo.even_path : (n * 2) |=> n := ⟨1, by simp [step]⟩ |
| 97 | + |
| 98 | + |
| 99 | +theorem GoesTo.odd_path: n ≡ 4 [MOD 6] -> (n - 1) / 3 |=> n := by |
| 100 | + intro hm |
| 101 | + have : ¬Even ((n-1)/3) := by |
| 102 | + apply Nat.not_even_iff_odd.mpr |
| 103 | + apply Nat.odd_iff.mpr |
| 104 | + rcases n |
| 105 | + case zero => norm_num; contradiction |
| 106 | + case succ k => |
| 107 | + · have hm' : k ≡ 3 [MOD 6] := by |
| 108 | + apply (Nat.ModEq.add_right_cancel' 1) |
| 109 | + rw [Nat.add_one] |
| 110 | + simpa |
| 111 | + calc (Nat.succ k - 1) / 3 % 2 |
| 112 | + _ = k / 3 % 2 := by simp |
| 113 | + _ = k % 6 / 3 := by |
| 114 | + -- rw [Nat.div_mod_eq_mod_mul_div] -- This theorem is gone now :/ |
| 115 | + sorry |
| 116 | + _ = 3 % 6 / 3 := by rw [hm'] |
| 117 | + _ = 1 := by norm_num |
| 118 | + have onelen : 1 ≤ n := by |
| 119 | + calc |
| 120 | + _ ≤ 4 := by simp |
| 121 | + _ = 4 % 6 := by decide |
| 122 | + _ = n % 6 := by rw [hm] |
| 123 | + _ ≤ n := Nat.mod_le n 6 |
| 124 | + have three_dvd_n_sub_one : 3 ∣ n - 1 := by |
| 125 | + apply (Nat.modEq_iff_dvd' onelen).mp |
| 126 | + rw [Nat.ModEq.comm] at hm |
| 127 | + apply Nat.ModEq.of_dvd ((by decide): 3 ∣ 6) hm |
| 128 | + use 1 |
| 129 | + rw [Function.iterate_one, step, if_neg this, Nat.mul_div_cancel' three_dvd_n_sub_one, Nat.sub_add_cancel onelen] |
| 130 | + |
| 131 | +theorem GoesTo.even_family : ∀k, (n * 2^k) |=> n := by sorry |
| 132 | + |
| 133 | +-- -- Complains that this does not terminate |
| 134 | +-- theorem GoesTo.even_family : ∀k, (n * 2^k) |=> n := by |
| 135 | +-- rintro (_ | i) |
| 136 | +-- · simp; rfl |
| 137 | +-- · calc n * 2 ^ Nat.succ i |
| 138 | +-- _ = n * 2 ^ i * 2 := by rw [Nat.pow_succ, <- mul_assoc] |
| 139 | +-- _ |=> n * 2 ^ i := even_path |
| 140 | +-- _ |=> _ := by |
| 141 | +-- apply even_family _ |
| 142 | + |
| 143 | +theorem GoesTo.odd_family : n ≡ 1 [MOD 6] -> ∀k, (n * 2^(2*k+2) - 1)/3 |=> n := by |
| 144 | + intro hn k |
| 145 | + have : n * 2 ^ (2 * k + 2) ≡ 4 [MOD 6] := by |
| 146 | + rw [<- one_mul 4] |
| 147 | + apply Nat.ModEq.mul hn |
| 148 | + induction k with |
| 149 | + | zero => simp; rfl |
| 150 | + | succ i hi => |
| 151 | + calc 2 ^ (2 * Nat.succ i + 2) % 6 |
| 152 | + _ = 2 ^ (2 * i + 2 + 2) % 6 := by rw [Nat.mul_succ] |
| 153 | + _ = (2 ^ (2 * i + 2) * 4) % 6 := by rw [Nat.pow_add] |
| 154 | + _ = 4 % 6 * (4 % 6) % 6 := by rw [Nat.mul_mod, hi] |
| 155 | + calc (n * 2^(2 * k + 2) - 1) / 3 |
| 156 | + _ |=> n * 2^(2 * k + 2) := odd_path this |
| 157 | + _ |=> n := even_family _ |
| 158 | + |
| 159 | +theorem GoesTo.odd_family2 : n ≡ 5 [MOD 6] -> ∀k, (n * 2^(2*k+1) - 1)/3 |=> n := by |
| 160 | + intro hn k |
| 161 | + calc (n * 2 ^ (2 * k + 1) - 1) / 3 |
| 162 | + _ |=> n * 2 ^ (2 * k + 1) := by |
| 163 | + apply odd_path |
| 164 | + rw [Nat.ModEq, ((by decide) : 4 ≡ 5 * 2 [MOD 6]), <- Nat.ModEq] |
| 165 | + apply Nat.ModEq.mul hn |
| 166 | + induction k with |
| 167 | + | zero => simp; rfl |
| 168 | + | succ i ih => |
| 169 | + calc 2 ^ (2 * i + 2 + 1) % 6 |
| 170 | + _ = 2 ^ (2 * i + 1) * 2 ^ 2 % 6 := by ring_nf |
| 171 | + _ = 2 ^ (2 * i + 1) % 6 * (2 ^ 2 % 6) % 6 := by rw [Nat.mul_mod] |
| 172 | + _ = 2 % 6 * (2 ^ 2 % 6) % 6 := by rw [ih] |
| 173 | + _ = 2 % 6 := by norm_num |
| 174 | + _ |=> n := even_family _ |
0 commit comments