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}
module Searchable where

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

\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 costimers ℕ∞, 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.  Any
searchable set

\begin{code}

searchable : Set → Prp
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 = ∃-intro x₀ (λ r → two-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)

\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 : 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₁)
where
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
\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 : 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
where ε : (X → ₂) → X
ε p = ∃-witness(ε' p)

lemma : ∀(p : X → ₂) → p(ε p) ≡ ₁ → ∀(x : X) → p x ≡ ₁
lemma p = ∃-elim(ε' 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 : Set} →

searchable X → omniscient X

searchable-implies-omniscient {X} ε p = two-equality-cases case₀ case₁
where
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 → ₀))
\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 : Set} →

inhabited 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 (in₀(x , r)) = ∃-intro x (λ s → ⊥-elim(Lemma[b≡₀→b≠₁] r s))
lemma (in₁ f) = ∃-intro x₀ (λ r → f)
\end{code}

Some closure properties now:

\begin{code}

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
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 = ∃-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

\end{code}

Corollary: Binary products preserve searchability.

\begin{code}

binary-Tychonoff : {X Y : Set} →

searchable X → searchable Y → searchable(X × Y)

binary-Tychonoff ε δ = sums-preserve-searchability ε (λ i → δ)

open import Surjection

surjective-functions-preserve-searchability : {X Y : Set} →

∀{f : X → Y} → surjective f → searchable X → searchable Y

surjective-functions-preserve-searchability {X} {Y} {f} surjectivity-of-f ε q =
∃-intro y₀ h
where
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₁
where
fact : ∃ \(x : X) → f x ≡ a
fact = surjectivity-of-f 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)

\end{code}

Corollary:

\begin{code}

open import Image

image-of-searchable-is-searchable : {X Y : Set} →

∀(f : X → Y) → searchable X → searchable(image f)

image-of-searchable-is-searchable {X} {Y} f =
surjective-functions-preserve-searchability (corestriction-is-surjective f)

\end{code}