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.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-} 

module Searchable where

open import Two
open import SpartanMLTT

\end{code}

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

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.  

\begin{code}

searchable : U  U
searchable X = (p : X  𝟚)  Σ \(x₀ : X)  p x₀    (x : X)  p x  

\end{code}

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.)

\begin{code}

two-searchable : searchable 𝟚
two-searchable p = x₀ ,  r  𝟚-induction (lemma₀ r) (lemma₁ r))
 where 
    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 = * , f
 where 
  f : (r : p *  ) (x : 𝟙)  p x  
  f r * = r

\end{code}

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.

\begin{code}

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


_has-a-root : {X : U}  (X  𝟚)  U
p has-a-root = Σ \x  x is-a-root-of p


putative-root : {X : U}  searchable X  (p : X  𝟚)  Σ \(x₀ : X)  (p has-a-root)  (x₀ is-a-root-of p)
putative-root {X} ε p = x₀ , (lemma₀ , lemma₁)
 where 
  x₀ : X 
  x₀ = pr₁(ε p)
  
  lemma : ¬((x : X)  p x  )  p x₀  
  lemma = Lemma[b≢₁→b≡₀]  contra-positive(pr₂(ε 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 = x₀ , h 
\end{code}

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

\begin{code}

_has-selection_ : (X : U)  ((X  𝟚)  X)  U
X has-selection ε = (p : X  𝟚)  p(ε p)    (x : X)  p x  


searchable' : U  U
searchable' X = Σ \(ε : (X  𝟚)  X)  X has-selection ε


searchable-implies-searchable' : {X : U}  searchable X  searchable' X
searchable-implies-searchable' {X} ε' = ε , lemma 
 where 
  ε : (X  𝟚)  X
  ε p = pr₁(ε' p)

  lemma : (p : X  𝟚)  p(ε p)    (x : X)  p x  
  lemma p = pr₂(ε' p)

\end{code}

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

\begin{code}

open import Omniscience

searchable-implies-omniscient : {X : U}  searchable X  omniscient X
searchable-implies-omniscient {X} ε p = two-equality-cases case₀ case₁
 where 
  x₀ : X
  x₀ = pr₁(ε p)

  lemma : p x₀    (x : X)  p x   
  lemma = pr₂(ε p)

  case₀ : p x₀    (Σ \(x : X)  p x  ) + ((x : X)  p x  )
  case₀ r = inl(x₀ , r)

  case₁ : p x₀    (Σ \(x : X)  p x  ) + ((x : X)  p x  )
  case₁ r = inr(lemma r)


searchable-implies-inhabited : {X : U}  searchable X  X
searchable-implies-inhabited ε = pr₁(ε x  ))
\end{code}

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:

\begin{code}

inhabited-omniscient-implies-searchable : {X : U}  X  omniscient X  searchable X
inhabited-omniscient-implies-searchable {X} x₀ φ p = lemma(φ p)
 where
  lemma : (Σ \(x : X)  p x  ) + ((x : X)  p x  )  
           Σ \(x₀ : X)  p x₀    (x : X)  p x  
  lemma (inl(x , r)) = x ,  s  ∅-elim(Lemma[b≡₀→b≢₁] r s))
  lemma (inr f) = x₀ ,  r  f)
\end{code}

Some closure properties now:

\begin{code}

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

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

sums-preserve-searchability {X} {Y} ε δ p = (x₀ , y₀) , correctness
 where 
  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 = pr₁(lemma-next x)

  next-correctness : (x : X)  p(x , next x)    (y : Y x)  p(x , y)  
  next-correctness x = pr₂(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₀ = pr₁ lemma-first

  first-correctness : p(x₀ , next x₀)    (x : X)  p(x , next x)  
  first-correctness = pr₂ 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

\end{code}

Corollary: Binary products preserve searchability:

\begin{code}

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

\end{code}

Corollary: binary coproducts preserve searchability:

\begin{code}

open import AlternativeCoproduct

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

\end{code}

\begin{code}

open import Retraction

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

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

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

   x₀ : X 
   x₀ = pr₁(ε p)

   y₀ : Y
   y₀ = f x₀

   lemma : p x₀    (x : X)  p x  
   lemma = pr₂(ε p)

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

     x : X
     x = pr₁ fact

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

     fact₁ : q(f x)  q a
     fact₁ = ap q (pr₂ fact)


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

open import Equivalence

equiv-searchable : {X Y : U}  X  Y  searchable X  searchable Y
equiv-searchable (f , (g , fg) , (h , hf)) = retract-searchable (f ,  y  g y , fg y))

open import Sets

contractible-searchable : {X : U}  contractible X  searchable X
contractible-searchable {X} (x , φ) p = x , g
 where
  g : p x    (y : X)  p y  
  g r y = transport  v  p v  ) (φ y) r

\end{code}