0 | ||| This module is based on Todd Waugh Ambridge's blog post series
  1 | ||| "Search over uniformly continuous decidable predicates on
  2 | ||| infinite collections of types"
  3 | ||| https://www.cs.bham.ac.uk/~txw467/tychonoff/
  4 |
  5 | module Search.Tychonoff.PartI
  6 |
  7 | import Data.DPair
  8 | import Data.Nat
  9 | import Data.Nat.Order
 10 | import Data.So
 11 | import Data.Vect
 12 | import Decidable.Equality
 13 | import Decidable.Decidable
 14 |
 15 | %default total
 16 |
 17 | ------------------------------------------------------------------------------
 18 | -- Searchable types
 19 | ------------------------------------------------------------------------------
 20 |
 21 | Pred : Type -> Type
 22 | Pred a = a -> Type
 23 |
 24 | 0 Decidable : Pred a -> Type
 25 | Decidable p = (x : a) -> Dec (p x)
 26 |
 27 | ||| Hilbert's epsilon is a function that for a given predicate
 28 | ||| returns a value that satisfies it if any value exists that
 29 | ||| that would satisfy it.
 30 | -- NB: this is not in the original posts, it's me making potentially
 31 | -- erroneous connections
 32 | 0 HilbertEpsilon : Pred x -> Type
 33 | HilbertEpsilon p = (v : x ** (v0 : x) -> p v0 -> p v)
 34 |
 35 | ||| A type is searchable if for any
 36 | ||| @ p a decidable predicate over that type
 37 | ||| @ x can be found such that if there exists a
 38 | ||| @ x0 satisfying p then x also satisfies p
 39 | 0 IsSearchable : Type -> Type
 40 | IsSearchable x = (0 p : Pred x) -> Decidable p -> HilbertEpsilon p
 41 |
 42 | private infix 0 <->
 43 | record (<->) (a, b : Type) where
 44 |   constructor MkIso
 45 |   forwards  : a -> b
 46 |   backwards : b -> a
 47 |   inverseL  : (x : a) -> backwards (forwards x) === x
 48 |   inverseR  : (y : b) -> forwards (backwards y) === y
 49 |
 50 | ||| Searchable is closed under isomorphisms
 51 | map : (a <-> b) -> IsSearchable a -> IsSearchable b
 52 | map (MkIso f g _ inv) search p pdec =
 53 |   let (xa ** prfa) = search (p . f) (\ x => pdec (f x)) in
 54 |   (f xa ** \ xb, pxb => prfa (g xb) $ replace {p} (sym $ inv xb) pxb)
 55 |
 56 | interface Searchable (0 a : Type) where
 57 |   constructor MkSearchable
 58 |   search : IsSearchable a
 59 |
 60 | Inhabited : Type -> Type
 61 | Inhabited a = a
 62 |
 63 | searchableIsInhabited : IsSearchable a -> Inhabited a
 64 | searchableIsInhabited search = fst (search (\ _ => ()) (\ _ => Yes ()))
 65 |
 66 | -- Finite types are trivially searchable
 67 |
 68 | ||| Unit is searchable
 69 | Searchable () where
 70 |   search p pdef = (() ** \ (), prf => prf)
 71 |
 72 | ||| Bool is searchable
 73 | Searchable Bool where
 74 |   search p pdec = case pdec True of
 75 |     -- if p True holds we're done
 76 |     Yes prf   => MkDPair True $ \ _, _ => prf
 77 |     -- otherwise p False is our best bet
 78 |     No contra => MkDPair False $ \case
 79 |       False => id
 80 |       True  => absurd . contra
 81 |
 82 | ||| Searchable is closed under finite sum
 83 | -- Note that this would enable us to go back and prove Bool searchable
 84 | -- via the iso Bool <-> Either () ()
 85 | (Searchable a, Searchable b) => Searchable (Either a b) where
 86 |   search p pdec =
 87 |     let (xa ** prfa) = search (p . Left) (\ xa => pdec (Left xa)) in
 88 |     let (xb ** prfb) = search (p . Right) (\ xb => pdec (Right xb)) in
 89 |     case pdec (Left xa) of
 90 |       Yes pxa => (Left xa ** \ _, _ => pxa)
 91 |       No npxa => case pdec (Right xb) of
 92 |         Yes pxb => (Right xb ** \ _, _ => pxb)
 93 |         No npxb => MkDPair (Left xa) $ \case
 94 |           Left xa' => \ pxa' => absurd (npxa (prfa xa' pxa'))
 95 |           Right xb' => \ pxb' => absurd (npxb (prfb xb' pxb'))
 96 |
 97 | ||| Searchable is closed under finite product
 98 | (Searchable a, Searchable b) => Searchable (a, b) where
 99 |   search p pdec =
100 |     -- How cool is that use of choice?
101 |     let (fb ** prfb) = Pair.choice $ \ a => search (p . (a,)) (\ b => pdec (a, b)) in
102 |     let (xa ** prfa) = search (\ a => p (a, fb a)) (\ xa => pdec (xa, fb xa)) in
103 |     MkDPair (xa, fb xa) $ \ (xa', xb'), pxab' => prfa xa' (prfb xa' xb' pxab')
104 |
105 | ||| Searchable for Vect
106 | %hint
107 | searchVect : Searchable a => (n : Nat) -> Searchable (Vect n a)
108 | searchVect 0 = MkSearchable $ \ p, pdec => ([] ** \case [] => id)
109 | searchVect (S n) = MkSearchable $ \ p, pdec =>
110 |   let %hint ih : Searchable (Vect n a)
111 |       ih = searchVect n
112 |       0 P : Pred (a, Vect n a)
113 |       P = p . Prelude.uncurry (::)
114 |       Pdec : Decidable P
115 |       Pdec = \ (x, xs) => pdec (x :: xs)
116 |   in bimap (uncurry (::)) (\ prf => \case (v0 :: vs0) => prf (v0, vs0))
117 |    $ search P Pdec
118 |
119 | ||| The usual LPO is for Nat only
120 | 0 LPO : Type -> Type
121 | LPO a = (f : a -> Bool) ->
122 |         Either (x : a ** f x === True) ((x : a) -> f x === False)
123 |
124 | 0 LPO' : Type -> Type
125 | LPO' a = (0 p : Pred a) -> Decidable p ->
126 |          Either (x : a ** p x) ((x : a) -> Not (p x))
127 |
128 | SearchableIsLPO : IsSearchable a -> LPO' a
129 | SearchableIsLPO search p pdec =
130 |   let (x ** prf) = search p pdec in
131 |   case pdec x of
132 |     Yes px => Left (x ** px)
133 |     No npx => Right (\ x', px' => absurd (npx (prf x' px')))
134 |
135 | LPOIsSearchable : LPO' a -> Inhabited a -> IsSearchable a
136 | LPOIsSearchable lpo inh p pdec = case lpo p pdec of
137 |   Left (x ** px) => (x ** \ _, _ => px)
138 |   Right contra   => (inh ** \ x, px => absurd (contra x px))
139 |
140 | EqUntil : (m : Nat) -> (a, b : Nat -> x) -> Type
141 | EqUntil m a b = (k : Nat) -> k `LTE` m -> a k === b k
142 |
143 | ------------------------------------------------------------------------------
144 | -- Closeness functions and extended naturals
145 | ------------------------------------------------------------------------------
146 |
147 | ||| A decreasing sequence of booleans
148 | Decreasing : (Nat -> Bool) -> Type
149 | Decreasing f = (n : Nat) -> So (f (S n)) -> So (f n)
150 |
151 | ||| Nat extended with a point at infinity
152 | record NatInf where
153 |   constructor MkNatInf
154 |   sequence     : Nat -> Bool
155 |   isDecreasing : Decreasing sequence
156 |
157 | repeat : x -> (Nat -> x)
158 | repeat v = const v
159 |
160 | Zero : NatInf
161 | Zero = MkNatInf (repeat False) (\ n, prf => prf)
162 |
163 | Omega : NatInf
164 | Omega = MkNatInf (repeat True) (\ n, prf => prf)
165 |
166 | (::) : x -> (Nat -> x) -> (Nat -> x)
167 | (v :: f) 0 = v
168 | (v :: f) (S n) = f n
169 |
170 | Succ : NatInf -> NatInf
171 | Succ f = MkNatInf (True :: f .sequence) decr where
172 |
173 |   decr : Decreasing (True :: f .sequence)
174 |   decr 0     = const Oh
175 |   decr (S n) = f .isDecreasing n
176 |
177 | fromNat : Nat -> NatInf
178 | fromNat 0 = Zero
179 | fromNat (S k) = Succ (fromNat k)
180 |
181 | soFromNat : k `LT` n -> So ((fromNat n) .sequence k)
182 | soFromNat p = case view p of
183 |   LTZero => Oh
184 |   LTSucc p => soFromNat p
185 |
186 | fromNatSo : {k, n : Nat} -> So ((fromNat n) .sequence k) -> k `LT` n
187 | fromNatSo {n = 0} hyp = absurd hyp
188 | fromNatSo {k = 0} {n = S n} hyp = LTESucc LTEZero
189 | fromNatSo {k = S k} {n = S n} hyp = LTESucc (fromNatSo hyp)
190 |
191 | LTE : (f, g : NatInf) -> Type
192 | f `LTE` g = (n : Nat) -> So (f .sequence n) -> So (g .sequence n)
193 |
194 | minimalZ : (f : NatInf) -> fromNat 0 `LTE` f
195 | minimalZ f n prf = absurd prf
196 |
197 | maximalInf : (f : NatInf) -> f `LTE` Omega
198 | maximalInf f n prf = Oh
199 |
200 | min : (f, g : NatInf) -> NatInf
201 | min (MkNatInf f prf) (MkNatInf g prg)
202 |   = MkNatInf (\ n => f n && g n) $ \ n, prfg =>
203 |     let (l, r) = soAnd prfg in
204 |     andSo (prf n l, prg n r)
205 |
206 | minLTE : (f, g : NatInf) -> min f g `LTE` f
207 | minLTE (MkNatInf f prf) (MkNatInf g prg)  n pr = fst (soAnd pr)
208 |
209 | max : (f, g : NatInf) -> NatInf
210 | max (MkNatInf f prf) (MkNatInf g prg)
211 |   = MkNatInf (\ n => f n || g n) $ \ n, prfg =>
212 |     orSo $ case soOr prfg of
213 |       Left pr => Left (prf n pr)
214 |       Right pr => Right (prg n pr)
215 |
216 | maxLTE : (f, g : NatInf) -> f `LTE` max f g
217 | maxLTE (MkNatInf f prf) (MkNatInf g prg) n pr = orSo (Left pr)
218 |
219 | record ClosenessFunction (0 x : Type) (c : (v, w : x) -> NatInf) where
220 |   constructor MkClosenessFunction
221 |   selfClose  : (v : x) -> c v v === Omega
222 |   closeSelf  : (v, w : x) -> c v w === Omega -> v === w
223 |   symmetric  : (v, w : x) -> c v w === c w v
224 |   ultrametic : (u, v, w : x) -> min (c u v) (c v w) `LTE` c u w
225 |
226 | ------------------------------------------------------------------------------
227 | -- Discrete closeness function
228 | ------------------------------------------------------------------------------
229 |
230 | Discrete : Type -> Type
231 | Discrete = DecEq
232 |
233 | dc : Discrete x => (v, w : x) -> NatInf
234 | dc v w = ifThenElse (isYes $ decEq v w) Omega Zero
235 |
236 | dcIsClosenessFunction : Discrete x => ClosenessFunction x PartI.dc
237 | dcIsClosenessFunction
238 |   = MkClosenessFunction selfClose closeSelf symmetric ultrametric
239 |
240 |   where
241 |
242 |   selfClose : (v : x) -> dc v v === Omega
243 |   selfClose v with (decEq v v)
244 |     _ | Yes pr = Refl
245 |     _ | No npr = absurd (npr Refl)
246 |
247 |   closeSelf : (v, w : x) -> dc v w === Omega -> v === w
248 |   closeSelf v w eq with (decEq v w)
249 |     _ | Yes pr = pr
250 |     _ | No npr = absurd (cong (($ 0) . sequence) eq)
251 |
252 |   symmetric : (v, w : x) -> dc v w === dc w v
253 |   symmetric v w with (decEq v w)
254 |     symmetric v v | Yes Refl = rewrite decEqSelfIsYes {x = v} in Refl
255 |     _ | No nprf with (decEq w v)
256 |       _ | Yes prf = absurd (nprf (sym prf))
257 |       _ | No _ = Refl
258 |
259 |   ultrametric : (u, v, w : x) -> min (dc u v) (dc v w) `LTE` dc u w
260 |   ultrametric u v w n with (decEq u w)
261 |     _ | Yes r = const Oh
262 |     _ | No nr with (decEq u v)
263 |       _ | Yes p with (decEq v w)
264 |         _ | Yes q = absurd (nr (trans p q))
265 |         _ | No nq = id
266 |       _ | No np with (decEq v w)
267 |         _ | Yes q = id
268 |         _ | No nq = id
269 |
270 | ------------------------------------------------------------------------------
271 | -- Discrete-sequence closeness function
272 | ------------------------------------------------------------------------------
273 |
274 | decEqUntil : Discrete x => (n : Nat) -> (f, g : Nat -> x) -> Dec (EqUntil n f g)
275 | decEqUntil n f g = decideLTEBounded (\ n => decEq (f n) (g n)) n
276 |
277 | fromYes : (d : Dec p) -> isYes d === True -> p
278 | fromYes (Yes prf) _ = prf
279 |
280 | decEqUntilPred :
281 |   Discrete x => (n : Nat) -> (f, g : Nat -> x) ->
282 |   isYes (decEqUntil (S n) f g) === True ->
283 |   isYes (decEqUntil n     f g) === True
284 | decEqUntilPred n f g eq with (decEqUntil n f g)
285 |   _ | Yes prf = Refl
286 |   _ | No nprf = let prf = fromYes (decEqUntil (S n) f g) eq in
287 |                 absurd (nprf $ \ l, bnd => prf l (lteSuccRight bnd))
288 |
289 | public export
290 | dsc : Discrete x => (f, g : Nat -> x) -> NatInf
291 | dsc f g = (MkNatInf Meas decr) where
292 |
293 |   Meas : Nat -> Bool
294 |   Meas = \ n => (ifThenElse (isYes $ decEqUntil n f g) Omega Zero) .sequence n
295 |
296 |   decr : Decreasing Meas
297 |   decr n with (decEqUntil (S n) f g) proof eq
298 |     _ | Yes eqSn = rewrite decEqUntilPred n f g (cong isYes eq) in id
299 |     _ | No neqSn = \case prf impossible
300 |
301 | interface IsSubSingleton x where
302 |   isSubSingleton : (v, w : x) -> v === w
303 |
304 | IsSubSingleton Void where
305 |   isSubSingleton p q = absurd p
306 |
307 | IsSubSingleton () where
308 |   isSubSingleton () () = Refl
309 |
310 | (IsSubSingleton a, IsSubSingleton b) => IsSubSingleton (a, b) where
311 |   isSubSingleton (p,q) (u,v) = cong2 (,) (isSubSingleton p u) (isSubSingleton q v)
312 |
313 | IsSubSingleton (So b) where
314 |   isSubSingleton Oh Oh = Refl
315 |
316 | -- K axiom
317 | IsSubSingleton (v === w) where
318 |   isSubSingleton Refl Refl = Refl
319 |
320 | 0 (~~~) : {0 b : a -> Type} -> (f, g : (x : a) ->  b x) -> Type
321 | f ~~~ g = (x : a) -> f x === g x
322 |
323 | 0 ExtensionalEquality : Type
324 | ExtensionalEquality
325 |   = {0 a : Type} -> {0 b : a -> Type} ->
326 |     {f, g : (x : a) -> b x} ->
327 |     f ~~~ g -> f === g
328 |
329 | interface Extensionality where
330 |   functionalExt : ExtensionalEquality
331 |
332 | {0 p : a -> Type} ->
333 |   Extensionality =>
334 |   ((x : a) -> IsSubSingleton (p x)) =>
335 |   IsSubSingleton ((x : a) -> p x) where
336 |   isSubSingleton v w = functionalExt (\ x => isSubSingleton (v x) (w x))
337 |
338 | -- Extensionality is needed for the No/No case
339 | Extensionality => IsSubSingleton p => IsSubSingleton (Dec p) where
340 |   isSubSingleton (Yes p) (Yes q) = cong Yes (isSubSingleton p q)
341 |   isSubSingleton (Yes p) (No nq) = absurd (nq p)
342 |   isSubSingleton (No np) (Yes q) = absurd (np q)
343 |   isSubSingleton (No np) (No nq) = cong No (isSubSingleton np nq)
344 |
345 | parameters {auto _ : Extensionality}
346 |
347 |   seqEquals : {f, g : Nat -> x} -> f ~~~ g -> f === g
348 |   seqEquals = functionalExt
349 |
350 |   decEqUntilSelfIsYes : Discrete x => (n : Nat) -> (f : Nat -> x) ->
351 |                            decEqUntil n f f === Yes (\ k, bnd => Refl)
352 |   decEqUntilSelfIsYes n f = isSubSingleton ? ?
353 |
354 |   NatInfEquals : {f, g : Nat -> Bool} ->
355 |                  {fdecr : Decreasing f} ->
356 |                  {gdecr : Decreasing g} ->
357 |                  f ~~~ g -> MkNatInf f fdecr === MkNatInf g gdecr
358 |   NatInfEquals {f} eq with (seqEquals eq)
359 |     _ | Refl = cong (MkNatInf f) (isSubSingleton ? ?)
360 |
361 |   dscIsClosenessFunction : Discrete x => ClosenessFunction (Nat -> x) PartI.dsc
362 |   dscIsClosenessFunction {x}
363 |     = MkClosenessFunction
364 |         selfClose
365 |         (\ v, w, eq => seqEquals (closeSelf v w eq))
366 |         (\ v, w => NatInfEquals (symmetric v w))
367 |         ultrametric
368 |
369 |     where
370 |
371 |     selfClose : (v : Nat -> x) -> dsc v v === Omega
372 |     selfClose v = NatInfEquals $ \ n => rewrite decEqUntilSelfIsYes n v in Refl
373 |
374 |     closeSelf : (v, w : Nat -> x) -> dsc v w === Omega -> v ~~~ w
375 |     closeSelf v w eq n with (cong (\ f => f .sequence n) eq)
376 |       _ | prf with (decEqUntil n v w)
377 |         _ | Yes eqn = eqn n reflexive
378 |         _ | No neqn = absurd prf
379 |
380 |     symmetric : (v, w : Nat -> x) -> (dsc v w) .sequence ~~~ (dsc w v) .sequence
381 |     symmetric v w n with (decEqUntil n v w)
382 |       _ | Yes p with (decEqUntil n w v)
383 |         _ | Yes q = Refl
384 |         _ | No nq = absurd (nq $ \ k, bnd => sym (p k bnd))
385 |       _ | No np with (decEqUntil n w v)
386 |         _ | Yes q = absurd (np $ \ k, bnd => sym (q k bnd))
387 |         _ | No nq = Refl
388 |
389 |     ultrametric : (u, v, w : Nat -> x) -> min (dsc u v) (dsc v w) `LTE` dsc u w
390 |     ultrametric u v w n with (decEqUntil n u w)
391 |       _ | Yes r = const Oh
392 |       _ | No nr with (decEqUntil n u v)
393 |         _ | Yes p with (decEqUntil n v w)
394 |           _ | Yes q = absurd (nr (\ k, bnd => trans (p k bnd) (q k bnd)))
395 |           _ | No nq = id
396 |         _ | No np with (decEqUntil n v w)
397 |           _ | Yes q = id
398 |           _ | No nq = id
399 |
400 | closeImpliesEqUntil : Discrete x =>
401 |   (n : Nat) -> (f, g : Nat -> x) ->
402 |   fromNat (S n) `LTE` dsc f g ->
403 |   EqUntil n f g
404 | closeImpliesEqUntil n f g prf with (prf n)
405 |   _ | prfn with (decEqUntil n f g)
406 |     _ | Yes eqn = eqn
407 |     _ | No neqn = absurd (prfn (soFromNat reflexive))
408 |
409 | eqUntilImpliesClose : Discrete x =>
410 |   (n : Nat) -> (f, g : Nat -> x) ->
411 |   EqUntil n f g ->
412 |   fromNat (S n) `LTE` dsc f g
413 | eqUntilImpliesClose n f g prf k hyp with (decEqUntil k f g)
414 |   _ | Yes p = Oh
415 |   _ | No np = let klten = fromLteSucc $ fromNatSo {k} {n = S n} hyp in
416 |               absurd (np $ \ k', bnd => prf k' (transitive bnd klten))
417 |
418 | buildUp : Discrete x => (n : Nat) -> (f, g : Nat -> x) ->
419 |   fromNat n `LTE` dsc f g ->
420 |   (v : x) ->
421 |   fromNat (S n) `LTE` dsc (v :: f) (v :: g)
422 | buildUp n f g hyp v
423 |   = eqUntilImpliesClose n (v :: f) (v :: g)
424 |   $ \ k, bnd => case bnd of
425 |     LTEZero => Refl
426 |     LTESucc bnd => closeImpliesEqUntil ? f g hyp ? bnd
427 |
428 | head : (Nat -> x) -> x
429 | head f = f Z
430 |
431 | tail : (Nat -> x) -> (Nat -> x)
432 | tail f = f . S
433 |
434 | parameters {auto _ : Extensionality}
435 |
436 |   eta : (f : Nat -> x) -> f === head f :: tail f
437 |   eta f = functionalExt $ \case
438 |             Z => Refl
439 |             S n => Refl
440 |
441 | ------------------------------------------------------------------------------
442 | -- Continuity and continuously searchable types
443 | ------------------------------------------------------------------------------
444 |
445 | ||| Uniform modulus of continuity
446 | ||| @ c   the notion of closeness used
447 | ||| @ p   the predicate of interest
448 | ||| @ mod the modulus being characterised
449 | 0 IsUModFor : (c : (v, w : x) -> NatInf) -> (p : Pred x) -> (mod : Nat) -> Type
450 | IsUModFor c p mod = (v, w : x) -> fromNat mod `LTE` c v w -> p v -> p w
451 |
452 | ||| Uniformly continuous predicate wrt a closeness function
453 | ||| @ c the notion of closeness used
454 | ||| @ p the uniformly continuous predicate
455 | record UContinuous {0 x : Type} (c : (v, w : x) -> NatInf) (p : Pred x) where
456 |   constructor MkUC
457 |   uModulus  : Nat
458 |   isUModFor : IsUModFor c p uModulus
459 |
460 | ||| A type equipped with
461 | ||| @ c a notion of closeness
462 | ||| is continuously searchable if for any
463 | ||| @ p a decidable predicate over that type
464 | ||| @ x can be found such that if there exists a
465 | ||| @ x0 satisfying p then x also satisfies p
466 | 0 IsCSearchable : (x : Type) -> ((v, w : x) -> NatInf) -> Type
467 | IsCSearchable x c
468 |   = (0 p : Pred x) -> UContinuous c p -> Decidable p ->
469 |     HilbertEpsilon p
470 |
471 | interface CSearchable x (0 c : (v, w : x) -> NatInf) where
472 |   csearch : IsCSearchable x c
473 |
474 | [DEMOTE] Searchable x => CSearchable x c where
475 |   csearch p uc pdec = search p pdec
476 |
477 | CSearchable Bool (PartI.dc {x = Bool}) where
478 |   csearch = csearch @{DEMOTE}
479 |
480 | discreteIsUContinuous :
481 |   {0 p : Pred x} -> Discrete x =>
482 |   Decidable p -> UContinuous PartI.dc p
483 | discreteIsUContinuous pdec = MkUC 1 isUContinuous where
484 |
485 |   isUContinuous : IsUModFor PartI.dc p 1
486 |   isUContinuous v w hyp pv with (decEq v w)
487 |     _ | Yes eq = replace {p} eq pv
488 |     _ | No neq = absurd (hyp 0 Oh)
489 |
490 | [PROMOTE] Discrete x => CSearchable x PartI.dc => Searchable x where
491 |   search p pdec = csearch p (discreteIsUContinuous pdec) pdec
492 |
493 | ------------------------------------------------------------------------------
494 | -- Main result
495 | ------------------------------------------------------------------------------
496 |
497 |
498 | -- Lemma 1
499 |
500 | nullModHilbert :
501 |   Decidable p -> IsUModFor c p 0 ->
502 |   (v : x ** p v) -> (v : x) -> p v
503 | nullModHilbert pdec pmod0 (v0 ** pv0) v = pmod0 v0 v (\ n => absurd) pv0
504 |
505 | trivial : UContinuous c (const ())
506 | trivial = MkUC 0 (\ _, _, _, _ => ())
507 |
508 | -- Lemma 2
509 |
510 |
511 | 0 tailPredicate : Pred (Nat -> x) -> x -> Pred (Nat -> x)
512 | tailPredicate p v = p . (v ::)
513 |
514 | parameters
515 |   {0 p : Pred (Nat -> x)}
516 |   {auto _ : Discrete x}
517 |   (pdec : Decidable p)
518 |
519 |   decTail : (v : x) -> Decidable (tailPredicate p v)
520 |   decTail v vs = pdec (v :: vs)
521 |
522 |   predModTail :
523 |     (mod : Nat) -> IsUModFor PartI.dsc p (S mod) ->
524 |     (v : x) -> IsUModFor PartI.dsc (tailPredicate p v) mod
525 |   predModTail mod hyp v f g prf pvf
526 |     = hyp (v :: f) (v :: g) (buildUp mod f g prf v) pvf
527 |
528 | [BYUCONTINUITY] Extensionality =>
529 |   Discrete x =>
530 |   CSearchable x PartI.dc =>
531 |   CSearchable (Nat -> x) (PartI.dsc {x}) where
532 |   csearch q quni qdec
533 |     = go (search @{PROMOTE})
534 |          qdec
535 |          (quni .uModulus)
536 |          (quni .isUModFor)
537 |
538 |     where
539 |
540 |     go : IsSearchable x ->
541 |          {0 p : Pred (Nat -> x)} -> Decidable p ->
542 |          (n : Nat) -> IsUModFor PartI.dsc p n ->
543 |          HilbertEpsilon p
544 |     go s pdec 0 hyp
545 |       = let f = const (searchableIsInhabited s) in
546 |         MkDPair f (\ v0, pv0 => nullModHilbert {c = dsc} pdec hyp (v0 ** pv0) f)
547 |     go s pdec (S mod) hyp
548 |       = let -- Stepping function generating a tail from the head
549 |             stepping : x -> (Nat -> x)
550 |             stepping i = fst (go s (decTail pdec i) mod (predModTail pdec mod hyp i))
551 |             -- Searching for the head
552 |             0 PH : Pred x
553 |             PH = \ v => p (v :: stepping v)
554 |             pHdec : Decidable PH
555 |             pHdec = \ v => pdec (v :: stepping v)
556 |             sH : HilbertEpsilon PH
557 |             sH = s PH pHdec
558 |             -- Searching for the tail given an arbitrary head
559 |             0 PT : x -> Pred (Nat -> x)
560 |             PT i = tailPredicate p i
561 |             pTdec : (v : x) -> Decidable (PT v)
562 |             pTdec i = decTail pdec i
563 |             sT : (v : x) -> HilbertEpsilon (PT v)
564 |             sT i = go s (pTdec i) mod (predModTail pdec mod hyp i)
565 |             -- build up the result
566 |             v : x; v = sH .fst
567 |             vs : Nat -> x; vs = (sT v) .fst
568 |          in MkDPair (v :: vs) $ \ vv0s, pvv0s =>
569 |              let v0 : x; v0 = head vv0s
570 |                  v0s : Nat -> x; v0s = tail vv0s
571 |              in sH .snd v0
572 |               $ (sT v0) .snd v0s
573 |               $ replace {p} (eta vv0s) pvv0s
574 |
575 | cantorIsCSearchable : Extensionality => IsCSearchable (Nat -> Bool) PartI.dsc
576 | cantorIsCSearchable = csearch @{BYUCONTINUITY}
577 |