ComputableQuotientCodes.lean

1 import RealizationBoundaries.ComputablePresentations
2 import Mathlib.Data.Nat.Nth
3 
4 /-! # From redundant computable codes to an actual computable copy -/
5 set_option autoImplicit false
6 set_option backward.isDefEq.respectTransparency false
7 noncomputable section
8 namespace RealizationBoundaries
9 
10 /-- Redundant natural codes are permitted, but equality of their actual meanings
11 must be oracle computable. This is stronger than a merely enumerable relator
12 presentation. -/
13 structure OracleRawGroupCodes (X : ℕ → Bool) (H : Type*) [AddGroup H] where
14   names : ℕ → H
15   names_surjective : Function.Surjective names
16   zero : ℕ
17   add : ℕ → ℕ → ℕ
18   equal : ℕ → ℕ → ℕ
19   zero_spec : names zero = 0
20   add_spec : ∀ i j, names (add i j) = names i + names j
21   equal_spec : ∀ i j, equal i j = 0 ↔ names i = names j
22   add_computable : OracleComputable X (fun k => add k.unpair.1 k.unpair.2)
23   equal_computable : OracleComputable X (fun k => equal k.unpair.1 k.unpair.2)
24 
25 namespace OracleRawGroupCodes
26 variable {X : ℕ → Bool} {H : Type*} [AddGroup H]
27 
28 /-- The least natural code of its equality class. -/
29 def Canonical (c : OracleRawGroupCodes X H) (n : ℕ) : Prop :=
30   ∀ m < n, c.names m ≠ c.names n
31 
32 instance canonical_decidable (c : OracleRawGroupCodes X H) : DecidablePred c.Canonical := by
33   intro n
34   exact Classical.propDecidable _
35 
36 theorem canonical_code_exists (c : OracleRawGroupCodes X H) (x : H) :
37     ∃ n, c.Canonical n ∧ c.names n = x := by
38   classical
39   let h := c.names_surjective x
40   refine ⟨Nat.find h, ?_, Nat.find_spec h⟩
41   intro m hm he
42   exact Nat.find_min h hm (he.trans (Nat.find_spec h))
43 
44 theorem canonical_names_injective (c : OracleRawGroupCodes X H) :
45     Function.Injective (fun n : {n // c.Canonical n} => c.names n.val) := by
46   intro n m h
47   apply Subtype.ext
48   by_contra hn
49   rcases lt_or_gt_of_ne hn with hnm | hmn
50   · exact m.property n.val hnm h
51   · exact n.property m.val hmn h.symm
52 
53 theorem canonical_infinite (c : OracleRawGroupCodes X H) [Infinite H] :
54     {n | c.Canonical n}.Infinite := by
55   intro hf
56   have hi : Set.Finite (Set.range c.names) := by
57     apply (hf.image c.names).subset
58     rintro x ⟨n, rfl⟩
59     obtain ⟨m, hm, he⟩ := c.canonical_code_exists (c.names n)
60     exact ⟨m, hm, he⟩
61   have hu : Set.range c.names = Set.univ := Set.range_eq_univ.mpr c.names_surjective
62   exact Set.infinite_univ (hu ▸ hi)
63 
64 /-- Finite equality-product: nonzero exactly when no preceding code has the
65 same meaning as the supplied code. -/
66 def previousProduct (c : OracleRawGroupCodes X H) (q n : ℕ) : ℕ :=
67   Nat.rec 1 (fun m r => r * c.equal m q) n
68 
69 theorem previousProduct_ne_zero (c : OracleRawGroupCodes X H) (q n : ℕ) :
70     c.previousProduct q n ≠ 0 ↔ ∀ m < n, c.equal m q ≠ 0 := by
71   induction n with
72   | zero => simp [previousProduct]
73   | succ n ih =>
74     change c.previousProduct q n * c.equal n q ≠ 0 ↔ _
75     rw [mul_ne_zero_iff, ih]
76     constructor
77     · rintro ⟨h, hn⟩ m hm
78       rcases Nat.lt_succ_iff_lt_or_eq.mp hm with hm | rfl
79       · exact h m hm
80       · exact hn
81     · intro h
82       exact ⟨fun m hm => h m (Nat.lt_succ_of_lt hm), h n (Nat.lt_succ_self n)⟩
83 
84 /-- Zero is the successful canonical-code test. -/
85 def canonicalTest (c : OracleRawGroupCodes X H) (n : ℕ) : ℕ :=
86   if c.previousProduct n n = 0 then 1 else 0
87 
88 theorem canonicalTest_correct (c : OracleRawGroupCodes X H) (n : ℕ) :
89     c.canonicalTest n = 0 ↔ c.Canonical n := by
90   simp only [canonicalTest, ite_eq_right_iff, one_ne_zero, imp_false]
91   change c.previousProduct n n ≠ 0 ↔ c.Canonical n
92   rw [c.previousProduct_ne_zero]
93   exact forall_congr' fun m => imp_congr_right fun _ => (c.equal_spec m n).not
94 
95 theorem previousProduct_computable (c : OracleRawGroupCodes X H) :
96     OracleComputable X (fun k => c.previousProduct k.unpair.1 k.unpair.2) := by
97   have he : OracleComputable X
98       (fun k => c.equal k.unpair.2.unpair.1 k.unpair.1) :=
99     c.equal_computable.comp ((OracleComputable.left.comp OracleComputable.right).pair
100       OracleComputable.left) |>.of_eq (fun k => by simp)
101   exact OracleComputable.prec (step := fun q m r => r * c.equal m q) (OracleComputable.const 1)
102     ((OracleComputable.right.comp OracleComputable.right).mul he)
103 
104 theorem canonicalTest_computable (c : OracleRawGroupCodes X H) :
105     OracleComputable X c.canonicalTest :=
106   (c.previousProduct_computable.comp (OracleComputable.id.pair OracleComputable.id)).isZero
107     |>.of_eq (fun n => by simp [canonicalTest])
108 
109 end OracleRawGroupCodes
110 
111 namespace OracleComputable
112 variable {X : ℕ → Bool} {f g : ℕ → ℕ}
113 
114 theorem add (hf : OracleComputable X f) (hg : OracleComputable X g) :
115     OracleComputable X (fun n => f n + g n) :=
116   (Nat.Primrec.add.recursiveIn : OracleComputable X (Nat.unpaired (· + ·))).comp
117     (hf.pair hg) |>.of_eq (fun n => by simp [Nat.unpaired])
118 
119 /-- The count of successful zero tests below a finite bound. -/
120 def zeroCount (test : ℕ → ℕ) (n : ℕ) : ℕ :=
121   Nat.rec 0 (fun m r => r + if test m = 0 then 1 else 0) n
122 
123 theorem zeroCount_computable (ht : OracleComputable X f) :
124     OracleComputable X (zeroCount f) := by
125   have hi := (ht.comp (OracleComputable.left.comp OracleComputable.right)).isZero
126   have hrec := OracleComputable.prec (step := fun _ m r => r + if f m = 0 then 1 else 0) (OracleComputable.const 0)
127     ((OracleComputable.right.comp OracleComputable.right).add hi)
128   exact (hrec.comp ((OracleComputable.const 0).pair OracleComputable.id)).of_eq
129     (fun n => by simp [zeroCount])
130 
131 theorem zeroCount_eq_count (test : ℕ → ℕ) (n : ℕ) :
132     zeroCount test n = Nat.count (fun m => test m = 0) n := by
133   induction n with
134   | zero => simp [zeroCount]
135   | succ n ih =>
136     change zeroCount test n + (if test n = 0 then 1 else 0) = _
137     rw [Nat.count_succ, ih]
138 
139 /-- A zero test for the relation: candidate `m` is successful and has exactly
140 `n` successful predecessors. -/
141 def nthTest (test : ℕ → ℕ) (k : ℕ) : ℕ :=
142   if test k.unpair.2 = 0 ∧ zeroCount test k.unpair.2 = k.unpair.1 then 0 else 1
143 
144 theorem nthTest_computable (ht : OracleComputable X f) :
145     OracleComputable X (nthTest f) := by
146   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
147   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
148   have hp : Computable (fun k : ℕ =>
149       if k.unpair.1 = 0 ∧ k.unpair.2.unpair.1 = k.unpair.2.unpair.2 then 0 else 1) :=
150     (Primrec.ite ((Primrec.eq.comp hl (Primrec.const 0)).and
151       (Primrec.eq.comp (hl.comp hr) (hr.comp hr)))
152       (Primrec.const 0) (Primrec.const 1)).to_comp
153   exact (of_computable hp).comp ((ht.comp right).pair
154     (((zeroCount_computable ht).comp right).pair left))
155       |>.of_eq (fun k => by simp [nthTest])
156 
157 theorem nthTest_correct (test : ℕ → ℕ) (n m : ℕ) :
158     nthTest test (Nat.pair n m) = 0 ↔
159       test m = 0 ∧ Nat.count (fun t => test t = 0) m = n := by
160   simp [nthTest, zeroCount_eq_count]
161 
162 /-- Increasing enumeration of an infinite oracle-decidable set is an actual
163 terminating oracle computation. -/
164 theorem nth_zero_computable (test : ℕ → ℕ) (ht : OracleComputable X test)
165     (hi : {n | test n = 0}.Infinite) :
166     OracleComputable X (Nat.nth (fun n => test n = 0)) := by
167   have total : ∀ n, ∃ m, nthTest test (Nat.pair n m) = 0 := by
168     intro n
169     refine ⟨Nat.nth (fun m => test m = 0) n, (nthTest_correct test _ _).mpr ?_⟩
170     exact ⟨Nat.nth_mem_of_infinite hi n, Nat.count_nth_of_infinite hi n⟩
171   apply (find (nthTest_computable ht) total).of_eq
172   intro n
173   have hm := (nthTest_correct test n _).mp (Nat.find_spec (total n))
174   have he := Nat.nth_count (p := fun m => test m = 0) hm.1
175   rw [hm.2] at he
176   exact he.symm
177 
178 end OracleComputable
179 
180 namespace OracleRawGroupCodes
181 variable {X : ℕ → Bool} {H : Type*} [AddGroup H] [Infinite H]
182 
183 theorem canonicalTest_infinite (c : OracleRawGroupCodes X H) :
184     {n | c.canonicalTest n = 0}.Infinite := by
185   have he : {n | c.canonicalTest n = 0} = {n | c.Canonical n} :=
186     Set.ext (c.canonicalTest_correct)
187   rw [he]
188   exact c.canonical_infinite
189 
190 /-- Increasing enumeration of the least equality-class representatives. -/
191 def enumCode (c : OracleRawGroupCodes X H) : ℕ → ℕ :=
192   Nat.nth (fun n => c.canonicalTest n = 0)
193 
194 theorem enumCode_computable (c : OracleRawGroupCodes X H) :
195     OracleComputable X c.enumCode :=
196   OracleComputable.nth_zero_computable c.canonicalTest c.canonicalTest_computable
197     c.canonicalTest_infinite
198 
199 theorem enumCode_canonical (c : OracleRawGroupCodes X H) (n : ℕ) :
200     c.Canonical (c.enumCode n) :=
201   (c.canonicalTest_correct _).mp (Nat.nth_mem_of_infinite c.canonicalTest_infinite n)
202 
203 theorem enumNames_injective (c : OracleRawGroupCodes X H) :
204     Function.Injective (fun n => c.names (c.enumCode n)) := by
205   intro n m h
206   have hc := c.canonical_names_injective
207     (show (fun k : {n // c.Canonical n} => c.names k.val)
208       ⟨c.enumCode n, c.enumCode_canonical n⟩ =
209       (fun k : {n // c.Canonical n} => c.names k.val)
210       ⟨c.enumCode m, c.enumCode_canonical m⟩ from h)
211   exact Nat.nth_injective c.canonicalTest_infinite (congrArg Subtype.val hc)
212 
213 omit [Infinite H] in
214 theorem enumNames_surjective (c : OracleRawGroupCodes X H) :
215     Function.Surjective (fun n => c.names (c.enumCode n)) := by
216   intro x
217   obtain ⟨m, hm, he⟩ := c.canonical_code_exists x
218   refine ⟨Nat.count (fun n => c.canonicalTest n = 0) m, ?_⟩
219   unfold enumCode
220   dsimp only
221   rw [Nat.nth_count (p := fun n => c.canonicalTest n = 0) ((c.canonicalTest_correct m).mpr hm)]
222   exact he
223 
224 /-- An actual bijective naming, obtained from the computed canonical enumeration. -/
225 def namesEquiv (c : OracleRawGroupCodes X H) : ℕ ≃ H :=
226   Equiv.ofBijective (fun n => c.names (c.enumCode n))
227     ⟨c.enumNames_injective, c.enumNames_surjective⟩
228 
229 /-- Search for the unique canonical name of a raw code. -/
230 def indexTest (c : OracleRawGroupCodes X H) (k : ℕ) : ℕ :=
231   c.equal (c.enumCode k.unpair.2) k.unpair.1
232 
233 theorem indexTest_computable (c : OracleRawGroupCodes X H) :
234     OracleComputable X c.indexTest :=
235   c.equal_computable.comp ((c.enumCode_computable.comp OracleComputable.right).pair
236     OracleComputable.left) |>.of_eq (fun k => by simp [indexTest])
237 
238 omit [Infinite H] in
239 theorem indexTest_total (c : OracleRawGroupCodes X H) (n : ℕ) :
240     ∃ t, c.indexTest (Nat.pair n t) = 0 := by
241   obtain ⟨t, ht⟩ := c.enumNames_surjective (c.names n)
242   refine ⟨t, ?_⟩
243   simpa only [indexTest, Nat.unpair_pair] using (c.equal_spec _ _).mpr ht
244 
245 /-- Canonical index extraction terminates by surjectivity of the enumeration. -/
246 def index (c : OracleRawGroupCodes X H) (n : ℕ) : ℕ :=
247   Nat.find (c.indexTest_total n)
248 
249 theorem index_computable (c : OracleRawGroupCodes X H) :
250     OracleComputable X c.index :=
251   OracleComputable.find c.indexTest_computable c.indexTest_total
252 
253 theorem index_spec (c : OracleRawGroupCodes X H) (n : ℕ) :
254     c.namesEquiv (c.index n) = c.names n := by
255   apply (c.equal_spec _ _).mp
256   simpa only [indexTest, index, Nat.unpair_pair] using Nat.find_spec (c.indexTest_total n)
257 
258 /-- Redundant codes with decidable oracle equality yield a genuine computable
259 Nat-domain copy of every infinite group they enumerate. No quotient equality is
260 silently treated as decidable. -/
261 def toOracleGroupCopy (c : OracleRawGroupCodes X H) : OracleGroupCopy X H where
262   names := c.namesEquiv
263   zero := c.index c.zero
264   add := fun i j => c.index (c.add (c.enumCode i) (c.enumCode j))
265   zero_spec := (c.index_spec c.zero).trans c.zero_spec
266   add_spec := by
267     intro i j
268     exact (c.index_spec _).trans (c.add_spec _ _)
269   add_computable := by
270     have ha := c.add_computable.comp
271       ((c.enumCode_computable.comp OracleComputable.left).pair
272         (c.enumCode_computable.comp OracleComputable.right))
273     exact c.index_computable.comp ha |>.of_eq (fun k => by simp)
274 
275 /-- The existence form needed by concrete raw normal-form constructions. -/
276 theorem oracleGroupCopy_of_rawCodes (c : OracleRawGroupCodes X H) :
277     Nonempty (OracleGroupCopy X H) :=
278   ⟨c.toOracleGroupCopy⟩
279 
280 end OracleRawGroupCodes
281 
282 end RealizationBoundaries

Back to source controls