|
| 1 | +import Mathlib.Computability.Halting |
| 2 | +import Mathlib.Computability.Partrec |
| 3 | +import Mathlib.Computability.PartrecCode |
| 4 | +import Mathlib.Data.Set.Finite.Lemmas |
| 5 | + |
| 6 | +/-! |
| 7 | +# Kleene tree: an infinite tree with no computable path |
| 8 | +
|
| 9 | +This file defines the Kleene tree, a (binary) tree which is computable, |
| 10 | +infinite and does not have a computable path, following (not strictly) a |
| 11 | +paper of Andrej Bauer (see references). |
| 12 | +
|
| 13 | +## Main Definitions |
| 14 | +
|
| 15 | +* `Node`: A node in the complete binary tree. It is encoded as a `List Bool`, |
| 16 | + to be read from right to left (this choice makes it easier for inductive constructions). |
| 17 | +* `BinaryTree`: The structure representing a (binary) tree, using the suffix relationship |
| 18 | + to represent the asendency relationship. |
| 19 | +* `Path`: An (infinite) path through the complete binary tree, encoded as a function `ℕ → Bool`. |
| 20 | + To retrieve the `n`-th `Node` of a path `p`, we just call `p.get_node n`. |
| 21 | +* `kleeneTree`: A particular instance of `BinaryTree`, which is the main construction here. |
| 22 | +
|
| 23 | +## Main Results |
| 24 | +
|
| 25 | +* `separation_problem`: An impossibility result (similar to the Halting problem), |
| 26 | + used to construct Kleene tree. |
| 27 | +* `kleene_tree_computable`: Kleene tree is computable, meaning that we can algorithmically decide |
| 28 | + membership of a `Node`. |
| 29 | +* `kleene_tree_infinite`: Kleene tree is infinite, which we prove by constructing a particular |
| 30 | + injection from `ℕ → Node`. |
| 31 | +* `kleene_tree_no_computable_path`: Kleene tree does not have a computable `Path`: any path |
| 32 | + (e.g., as given by weak Kőnig's lemma) must be non-computable. |
| 33 | +
|
| 34 | +## References |
| 35 | +
|
| 36 | +* [Andrej Bauer, *Kőnig's Lemma and Kleene Tree*](https://math.andrej.com/wp-content/uploads/2006/05/kleene-tree.pdf) |
| 37 | +-/ |
| 38 | + |
| 39 | +open List |
| 40 | + |
| 41 | +abbrev Node := List Bool |
| 42 | + |
| 43 | +structure BinaryTree where |
| 44 | + nodes : Set Node |
| 45 | + root_mem : nil ∈ nodes |
| 46 | + suffix_closed : |
| 47 | + ∀ {p q : Node}, q ∈ nodes → IsSuffix p q → p ∈ nodes |
| 48 | + root : nodes := ⟨nil, root_mem⟩ |
| 49 | + |
| 50 | +abbrev Path := ℕ → Bool |
| 51 | + |
| 52 | +namespace Path |
| 53 | + |
| 54 | +def get_node (p : Path) : ℕ → Node |
| 55 | +| 0 => nil |
| 56 | +| n + 1 => p n :: p.get_node n |
| 57 | + |
| 58 | +lemma get_node_length {p : Path} : (p.get_node n).length = n := by |
| 59 | + induction n with |
| 60 | + | zero => simp only [get_node, length_nil] |
| 61 | + | succ n ih => simp only [get_node, length_cons, ih] |
| 62 | + |
| 63 | +lemma get_node_suffix {p : Path} (n m : ℕ) : ∃ t, p.get_node (n + m) = t ++ p.get_node n := by |
| 64 | + induction m with |
| 65 | + | zero => simp |
| 66 | + | succ m ih => |
| 67 | + let ⟨t, ht⟩ := ih |
| 68 | + rw [← Nat.add_assoc] |
| 69 | + nth_rewrite 1 [get_node] |
| 70 | + rw [ht] |
| 71 | + use p (n + m) :: t |
| 72 | + rw [cons_append] |
| 73 | + |
| 74 | +end Path |
| 75 | + |
| 76 | +open Nat.Partrec |
| 77 | + |
| 78 | +def bounded_separator : ℕ → Node → Bool := fun k node => |
| 79 | + List.recOn |
| 80 | + node |
| 81 | + true |
| 82 | + fun head tail itail => |
| 83 | + (Option.casesOn |
| 84 | + (Code.evaln k (Code.ofNatCode tail.length) 0) |
| 85 | + true |
| 86 | + fun v => head = decide (v = 0)) |
| 87 | + && itail |
| 88 | + |
| 89 | +lemma bounded_separator_primrec₂ : Primrec₂ bounded_separator := |
| 90 | + Primrec.list_rec |
| 91 | + Primrec.snd |
| 92 | + (Primrec.const true) |
| 93 | + (Primrec.and.comp₂ |
| 94 | + (Primrec.option_casesOn |
| 95 | + (Code.primrec_evaln.comp <| |
| 96 | + Primrec.pair |
| 97 | + (Primrec.pair |
| 98 | + (Primrec.fst.comp Primrec.fst) |
| 99 | + ((Primrec.ofNat Code).comp <| Primrec.list_length.comp <| |
| 100 | + Primrec.fst.comp <| Primrec.snd.comp Primrec.snd) |
| 101 | + ) |
| 102 | + (Primrec.const 0) |
| 103 | + ) |
| 104 | + (Primrec.const true) |
| 105 | + (Primrec.beq.comp |
| 106 | + (Primrec.fst.comp <| Primrec.snd.comp Primrec.fst) |
| 107 | + (Primrec.eq.decide.comp Primrec.snd (Primrec.const 0))).to₂ |
| 108 | + ).to₂ |
| 109 | + (Primrec.snd.comp₂ <| Primrec.snd.comp₂ Primrec.snd.to₂) |
| 110 | + ) |
| 111 | + |
| 112 | +lemma bounded_separator_mono {k₁ k₂ : ℕ} (node : Node) : |
| 113 | + k₁ ≤ k₂ → bounded_separator k₂ node → bounded_separator k₁ node |
| 114 | +:= by induction node with |
| 115 | + | nil => simp [bounded_separator] |
| 116 | + | cons head tail itail => |
| 117 | + intro hk₁₂ hk₂ |
| 118 | + simp only [bounded_separator, Bool.and_eq_true] at itail hk₂ ⊢ |
| 119 | + constructor |
| 120 | + · rcases Option.eq_none_or_eq_some (Code.evaln k₁ (Code.ofNatCode tail.length) 0) |
| 121 | + with hnone | ⟨x, hx⟩ |
| 122 | + · simp only [hnone] |
| 123 | + · simp only [Eq.trans hx (Option.mem_def.1 (Code.evaln_mono hk₁₂ hx)).symm, hk₂.left] |
| 124 | + · exact itail hk₁₂ hk₂.right |
| 125 | + |
| 126 | +lemma bounded_separator_suffix {node : Node} (t : List Bool) : |
| 127 | + bounded_separator k (t ++ node) → bounded_separator k node |
| 128 | +:= by induction t with |
| 129 | + | nil => simp |
| 130 | + | cons head tail itail => |
| 131 | + intro h |
| 132 | + simp only [bounded_separator, cons_append, length_append, Bool.and_eq_true] at h ⊢ itail |
| 133 | + exact itail h.right |
| 134 | + |
| 135 | +lemma bounded_separator_stable (p : Path) (h : m ≤ n) : |
| 136 | + bounded_separator k (p.get_node n) → bounded_separator k (p.get_node m) := by |
| 137 | + intro hn |
| 138 | + let ⟨t, ht⟩ := Path.get_node_suffix (p := p) m (n - m) |
| 139 | + rw [Nat.add_sub_of_le h] at ht |
| 140 | + rw [congrArg (bounded_separator k) ht] at hn |
| 141 | + exact bounded_separator_suffix t hn |
| 142 | + |
| 143 | +def kleeneTree : BinaryTree where |
| 144 | + nodes := { node | bounded_separator node.length node } |
| 145 | + root_mem := by simp [bounded_separator] |
| 146 | + suffix_closed := by |
| 147 | + intro p q hq hpq |
| 148 | + unfold IsSuffix at hpq |
| 149 | + let ⟨t, ht⟩ := hpq |
| 150 | + simp only [Set.mem_setOf_eq, ← ht] at hq |
| 151 | + exact bounded_separator_mono (k₁ := p.length) (k₂ := (t ++ p).length) p (by simp) |
| 152 | + <| bounded_separator_suffix t hq |
| 153 | + |
| 154 | +lemma ofNatCode_encode {c : Code} : Code.ofNatCode c.encodeCode = c := |
| 155 | + by simp [← Code.ofNatCode_eq, ← Code.encodeCode_eq, Denumerable.ofNat_encode] |
| 156 | + |
| 157 | +lemma primrec_encodeCode : Primrec Code.encodeCode := by |
| 158 | + rw [← Code.encodeCode_eq] |
| 159 | + exact Primrec.encode_iff.2 Primrec.id |
| 160 | + |
| 161 | +open Classical in |
| 162 | +theorem separation_problem : |
| 163 | + ¬∃ sep : Code → Bool, Computable sep ∧ |
| 164 | + ∀ c : Code, ((c.eval 0).map (fun v => sep c = (v = 0))).getOrElse true := by |
| 165 | + rintro ⟨sep, ⟨hcomp, hsep⟩⟩ |
| 166 | + let ⟨c, e⟩ := |
| 167 | + Code.fixed_point |
| 168 | + (Computable.cond |
| 169 | + hcomp |
| 170 | + (Computable.const (Code.const 1)) |
| 171 | + (Computable.const (Code.const 0)) |
| 172 | + ) |
| 173 | + by_cases H : sep c |
| 174 | + all_goals |
| 175 | + simp only [H, cond] at e |
| 176 | + have hceval := (congrArg (fun f => f 0) e).symm |
| 177 | + simp [Code.eval_const] at hceval |
| 178 | + let hsepc := hsep c |
| 179 | + rw [hceval] at hsepc |
| 180 | + simp only [Part.map_some, one_ne_zero, decide_false, Part.getOrElse_some] at hsepc |
| 181 | + grind only |
| 182 | + |
| 183 | +theorem kleene_tree_computable : ComputablePred kleeneTree.nodes := by |
| 184 | + simp [kleeneTree] |
| 185 | + have hp : Primrec (fun node => decide (bounded_separator node.length node)) := by |
| 186 | + simp only [Bool.decide_eq_true] |
| 187 | + exact bounded_separator_primrec₂.comp Primrec.list_length Primrec.id |
| 188 | + exact (Primrec.primrecPred hp).computablePred |
| 189 | + |
| 190 | +def bounded_node_builder (k : ℕ) : ℕ → Node |
| 191 | +| 0 => nil |
| 192 | +| n + 1 => |
| 193 | + (Option.casesOn |
| 194 | + (Code.evaln k (Code.ofNatCode n) 0) |
| 195 | + true |
| 196 | + fun v => decide (v = 0)) :: bounded_node_builder k n |
| 197 | + |
| 198 | +lemma node_builder_length (n : ℕ) : (bounded_node_builder k n).length = n := by |
| 199 | + induction n with |
| 200 | + | zero => trivial |
| 201 | + | succ n ih => simp [bounded_node_builder, ih] |
| 202 | + |
| 203 | +lemma node_builder_separator (n : ℕ) : bounded_separator k (bounded_node_builder k n) := by |
| 204 | + induction n with |
| 205 | + | zero => simp [bounded_separator, bounded_node_builder] |
| 206 | + | succ n ih => |
| 207 | + unfold bounded_node_builder bounded_separator |
| 208 | + dsimp [List.recOn] |
| 209 | + unfold bounded_separator at ih |
| 210 | + simp only [Bool.and_eq_true] |
| 211 | + constructor |
| 212 | + · simp only [node_builder_length] |
| 213 | + rcases Option.eq_none_or_eq_some (Code.evaln k (Code.ofNatCode n) 0) with hnone | ⟨x, hx⟩ |
| 214 | + · simp only [hnone, true_eq_decide_iff] |
| 215 | + · simp only [hx, decide_eq_decide, Bool.decide_iff_dist, BEq.rfl] |
| 216 | + · exact ih |
| 217 | + |
| 218 | +theorem kleene_tree_infinite : kleeneTree.nodes.Infinite := by |
| 219 | + have hmem : ∀ n, bounded_node_builder n n ∈ kleeneTree.nodes := by |
| 220 | + intro n |
| 221 | + unfold kleeneTree |
| 222 | + simp only [Set.mem_setOf_eq, node_builder_length, node_builder_separator] |
| 223 | + have hinj : Function.Injective fun n => bounded_node_builder n n := by |
| 224 | + unfold Function.Injective |
| 225 | + intro a₁ a₂ heq |
| 226 | + dsimp at heq |
| 227 | + grind only [!node_builder_length] |
| 228 | + exact Set.infinite_of_injective_forall_mem hinj hmem |
| 229 | + |
| 230 | +open Classical in |
| 231 | +theorem kleene_tree_no_computable_path {p : Path} : |
| 232 | + (∀ n : ℕ, p.get_node n ∈ kleeneTree.nodes) → ¬ Computable p := by |
| 233 | + intro hpath hpcomp |
| 234 | + unfold kleeneTree at hpath |
| 235 | + simp only [Set.mem_setOf_eq] at hpath |
| 236 | + let sep := fun c : Code => p c.encodeCode |
| 237 | + have hsep : ∀ c : Code, ((c.eval 0).map (fun v => sep c = (v = 0))).getOrElse true := by |
| 238 | + intro c |
| 239 | + rcases Part.eq_none_or_eq_some (c.eval 0) with hnone | ⟨x, hx⟩ |
| 240 | + · simp only [hnone, Part.map_none, Part.getOrElse_none] |
| 241 | + · have hxmem : x ∈ c.eval 0 := by simp only [hx, Part.mem_some_iff] |
| 242 | + let ⟨k, hk⟩ := Code.evaln_complete.1 hxmem |
| 243 | + simp only [decide] |
| 244 | + unfold sep |
| 245 | + let hmaxkcsucc := hpath <| max k c.encodeCode.succ |
| 246 | + rw [Path.get_node_length] at hmaxkcsucc |
| 247 | + let hcsucc := bounded_separator_stable p le_sup_right hmaxkcsucc |
| 248 | + simp only [bounded_separator, Nat.succ_eq_add_one, Path.get_node, Path.get_node_length, |
| 249 | + ofNatCode_encode, Bool.and_eq_true] at hcsucc |
| 250 | + let hcsuccl := hcsucc.left |
| 251 | + rw [Code.evaln_mono (k₁ := k) (k₂ := max k c.encodeCode.succ) le_sup_left hk] at hcsuccl |
| 252 | + simpa [hx] using hcsuccl |
| 253 | + exact separation_problem ⟨sep, And.intro (hpcomp.comp primrec_encodeCode.to_comp) hsep⟩ |
0 commit comments