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}