Martin Escardo 2011.

See my 2008 LMCS paper "Exhaustible sets in higher-type computation".
And also the work with Oliva on selection functions in proof theory.

Here we don't assume continuity axioms, but all functions are secretly
continuous, and searchable sets are secretly compact.


{-# OPTIONS --without-K #-}

module Searchable where

open import Two
open import CurryHoward
open import Equality
open import SetsAndFunctions


Because choice holds in MLTT, we can formulate searchability as
follows, rather than using selection functions (see searchable'

The drinker paradox says that in every pub there is a person x
such that if x drinks then everybody drinks.

In the definition below, p x ≡ ₁ means that x drinks, and the people
in the pub are the members of the set X. In general the DP is
non-constructive, as for example for the pub with set of costumers ℕ,
this would amount to LPO (limited principle of omniscience).  But it
is constructive for the larger pub with set of costumers ℕ∞, as shown
in the module ConvergentSequenceSearchable. Of course, it trivially
holds for finite sets.

In this module we investigate some closure properties of searchable
sets, and its relation to the principle of omniscience.  


searchable : Set  Prp
searchable X = ∀(p : X  )   \(x₀ : X)  p x₀    ∀(x : X)  p x  


Terminology: we call x₀ the universal witness.

For example, every finite set is searchable, and in particular the
set ₂ = { ₀ , ₁ } of binary numerals is searchable. To find x₀ : ₂
such that 

   (†) p x₀ ≡ ₁ → ∀(x : X) → p x ≡ ₁, 

we can check whether p ₀ ≡ ₁ and p ₁ ≡ ₁. 

     If this is the case, then ∀(x : X) → p x ≡ ₁ holds, which is
     the conclusion the implication (†), and hence we can take any
     x₀ : ₂ to make (†) hold.

     Otherwise, we can take any x₀ such that p x₀ ≡ ₀ so that the
     implication (†) holds vacuously.

That is, either the conclusion ∀(x : X) → p x ≡ ₁ of (†) holds, or
its premise p x₀ ≡ ₁ fails for suitable x₀.

However, there is a more direct proof: we claim that, without
checking the two possibilities, we can always take x₀ = p ₀.
(Cf. Section 8.1 of the LMCS'2008 paper.)


two-searchable : searchable 
two-searchable p = ∃-intro x₀  r  two-induction (lemma₀ r) (lemma₁ r))
    x₀ : 
    x₀ = p 
    claim : p x₀    p     p   
    claim r s = Lemma[fx≡y→x≡x'→fx'≡y] p r s

    lemma₀ : p x₀    p   
    lemma₀ r = two-equality-cases (claim r)  s  s)

    lemma₁ : p x₀    p   
    lemma₁ r = Lemma[fx≡y→x≡x'→fx'≡y] p r (lemma₀ r)

one-searchable : searchable 𝟙
one-searchable p = ∃-intro * f
  f : (r : p *  ) (x : 𝟙)  p x  
  f r * = r


In this module we prove some closure properties of searchable
sets. Before doing this, we investigate their general nature.

We first show that the universal witness x₀ is a root of p if and
only if p has a root.


_is-a-root-of_ : {X : Set}  X  (X  )  Prp
x is-a-root-of p = p x  

_has-a-root : {X : Set}  (X  )  Prp
p has-a-root =  \x  x is-a-root-of p

putative-root : {X : Set}  searchable X  ∀(p : X  )   \(x₀ : X)  p has-a-root  x₀ is-a-root-of p
putative-root {X} ε p = ∃-intro x₀ (∧-intro lemma₀ lemma₁)
  x₀ : X 
  x₀ = ∃-witness(ε p)
  lemma : ¬(∀(x : X)  p x  )  p x₀  
  lemma = Lemma[b≢₁→b≡₀]  contra-positive(∃-elim(ε p))

  lemma₀ : p has-a-root  x₀ is-a-root-of p
  lemma₀ (x , r) = lemma claim
   where claim : ¬(∀(x : X)  p x  )
         claim f = Lemma[b≡₁→b≢₀] (f x) r

  lemma₁ : x₀ is-a-root-of p  p has-a-root
  lemma₁ h = ∃-intro x₀ h 

We now relate our definition to the original definition using
selection functions. (Possible because choice holds in MLTT.)


_has-selection_ : (X : Set)  ((X  )  X)  Prp
X has-selection ε = ∀(p : X  )  p(ε p)    ∀(x : X)  p x  

searchable' : Set  Prp
searchable' X =  \(ε : (X  )  X)  X has-selection ε

searchable-implies-searchable' : {X : Set}  searchable X  searchable' X
searchable-implies-searchable' {X} ε' = ∃-intro ε lemma 
  ε : (X  )  X
  ε p = ∃-witness(ε' p)

  lemma : ∀(p : X  )  p(ε p)    ∀(x : X)  p x  
  lemma p = ∃-elim(ε' p)


In the following we will use ε (rather than ε' as above) to denote
a proof of a proposition of the form (searchable X).


open import Omniscience

searchable-implies-omniscient : {X : Set}  searchable X  omniscient X
searchable-implies-omniscient {X} ε p = two-equality-cases case₀ case₁
  x₀ : X
  x₀ = ∃-witness(ε p)

  lemma : p x₀    ∀(x : X)  p x   
  lemma = ∃-elim(ε p)

  case₀ : p x₀    ( \(x : X)  p x  )  (∀(x : X)  p x  )
  case₀ r = ∨-intro₀(∃-intro x₀ r)

  case₁ : p x₀    ( \(x : X)  p x  )  (∀(x : X)  p x  )
  case₁ r = ∨-intro₁(lemma r)

searchable-implies-inhabited : {X : Set}  searchable X  inhabited X
searchable-implies-inhabited ε = ∃-witness(ε x  ))

NB. The empty set is omniscient but of course not inhabited.

It seems unnatural to have a definition of searchability that forces
non-emptiness. There are two cases in which this is natural in our
context: when we show that the searchable sets are precisely the
images of the Cantor space (LMCS'2008), and when we prove the
countable Tychonoff theorem (LMCS'2008) - it is observed in
Escardo-Oliva MSCS'2010 that the inhabitedness of each factor is
absolutely essential. Apart from those cases, we could have
formulated searchability as omniscience (cf. Escardo-Oliva
CiE'2010). In fact:


inhabited-omniscient-implies-searchable : {X : Set}  inhabited X  omniscient X  searchable X
inhabited-omniscient-implies-searchable {X} x₀ φ p = lemma(φ p)
  lemma : ( \(x : X)  p x  )  (∀(x : X)  p x  )  
            \(x₀ : X)  p x₀    ∀(x : X)  p x  
  lemma (in₀(x , r)) = ∃-intro x  s  ⊥-elim(Lemma[b≡₀→b≢₁] r s))
  lemma (in₁ f) = ∃-intro x₀  r  f)

Some closure properties now:


sums-preserve-searchability : {X : Set}  {Y : X  Set}  

  searchable X  (∀(x : X)  searchable(Y x))  searchable(Σ \(x : X)  Y x)

sums-preserve-searchability {X} {Y} ε δ p = ∃-intro (x₀ , y₀) correctness
  lemma-next : ∀(x : X)   \(y₀ : Y x)  p(x , y₀)    ∀(y : Y x)  p(x , y)  
  lemma-next x = δ x  y  p(x , y))

  next : (x : X)  Y x
  next x = ∃-witness(lemma-next x)

  next-correctness : ∀(x : X)  p(x , next x)    ∀(y : Y x)  p(x , y)  
  next-correctness x = ∃-elim(lemma-next x)
  lemma-first :  \(x₀ : X)  p(x₀ , next x₀)    ∀(x : X)  p(x , next x)  
  lemma-first = ε x  p(x , next x))

  x₀ : X
  x₀ = ∃-witness lemma-first

  first-correctness : p(x₀ , next x₀)    ∀(x : X)  p(x , next x)  
  first-correctness = ∃-elim lemma-first

  y₀ : Y x₀
  y₀ = next x₀ 

  correctness : p(x₀ , y₀)    ∀(t : (Σ \(x : X)  Y x))  p t  
  correctness r (x , y) = next-correctness x (first-correctness r x) y


Corollary: Binary products preserve searchability:


binary-Tychonoff : {X Y : Set}  searchable X  searchable Y  searchable(X × Y)
binary-Tychonoff ε δ = sums-preserve-searchability ε  i  δ)


Corollary: binary coproducts preserve searchability:


open import AlternativeCoproduct

binary-sums-preserve-searchability : {X₀ X₁ : Set}  searchable X₀  searchable X₁  searchable(X₀ +' X₁)
binary-sums-preserve-searchability {X₀} {X₁} ε₀ ε₁ = sums-preserve-searchability two-searchable ε
  ε : (i : )  _
  ε  = ε₀
  ε  = ε₁



open import Retraction

retractions-preserve-searchability : {X Y : Set} 

 ∀{f : X  Y}  retraction f  searchable X  searchable Y

retractions-preserve-searchability {X} {Y} {f} f-retract ε q = 
 ∃-intro y₀ h
   p : X  
   p x = q(f x)

   x₀ : X 
   x₀ = ∃-witness(ε p)

   y₀ : Y
   y₀ = f x₀

   lemma : p x₀    ∀(x : X)  p x  
   lemma = ∃-elim(ε p)

   h : q y₀     (a : Y)  q a  
   h r a = Lemma[x≡y→x≡z→z≡y] fact₀ fact₁ 
     fact :  \(x : X)  f x  a 
     fact = f-retract a

     x : X
     x = ∃-witness fact

     fact₀ : q(f x)  
     fact₀ = lemma r x

     fact₁ : q(f x)  q a
     fact₁ = cong q (∃-elim fact)

retract-searchable : {X Y : Set}  retract Y of X  searchable X  searchable Y
retract-searchable (_ , φ) = retractions-preserve-searchability φ 

open import Isomorphism

iso-searchable : {X Y : Set}  X  Y  searchable X  searchable Y
iso-searchable (f , g , fg , gf) = retract-searchable (f ,  y  g y , fg y))

open import HSets

contractible-searchable : {X : Set}  contractible X  searchable X
contractible-searchable {X} (x , φ) p = x , g
  g : p x    (y : X)  p y  
  g r y = subst (φ y) r