{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Uncountability.Impossible where

Seemingly impossible programs and proofs#

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
import Padova2025.ProvingBasics.Equality.Booleans as B

A root of a decidable predicate P : X → Bool is a value x : X such that P x ≡ false (as with roots of ℕ-valued functions). Let us call a type X searchable iff every decidable predicate P : X → Bool has a root or alternatively is constantly true.

Searchable : Set → Set
Searchable X = (P : X → Bool) → (∃[ x ] P x ≡ false) ⊎ ((x : X) → P x ≡ true)

In classical mathematics, every type is trivially searchable. But as long as we do not postulate classical mathematics, this searchability condition expresses in Agda a much stronger claim—namely that, given a predicate P, we can decide by means of an algorithm which alternative holds.

Equivalent (for inhabited types) is the following property related to the drinker paradox.

HasDrinkers : Set → Set
HasDrinkers X = (P : X → Bool) → ∃[ a ] (P a ≡ true → ((x : X) → P x ≡ true))

false≢true : false ≢ true
false≢true ()

Exercise 1HasDrinkers⇒Searchable

HasDrinkers⇒Searchable : {X : Set} → HasDrinkers X → Searchable X
HasDrinkers⇒Searchable = {!!}

The reference solution uses: find _,_ false left true right refl

Your solution

Reference solution

HasDrinkers⇒Searchable : {X : Set} → HasDrinkers X → Searchable X
HasDrinkers⇒Searchable find P with find P
... | a , p with P a in eq
... | false = left  (a , eq)
... | true  = right (p refl)

Exercise 2Searchable⇒HasDrinkers

Searchable⇒HasDrinkers : {X : Set} → X → Searchable X → HasDrinkers X
Searchable⇒HasDrinkers = {!!}

The reference solution uses: left _,_ ⊥-elim false≢true trans sym right

Your solution

Reference solution

Searchable⇒HasDrinkers : {X : Set} → X → Searchable X → HasDrinkers X
Searchable⇒HasDrinkers x₀ dec P with dec P
... | left  (x , eq) = x  , λ eq' → ⊥-elim (false≢true (trans (sym eq) eq'))
... | right f        = x₀ , λ _   → f

Exercise: The Booleans are searchable#

Finite types such as Bool are searchable: To decide whether a predicate has a root, we can inspect every element of the type in turn.

Exercise 3Bool-searchable

Bool-searchable : Searchable Bool
Bool-searchable P with P false in eq | P true in eq'
... | false | y     = {!!}
... | true  | false = {!!}
... | true  | true  = {!!}

The reference solution uses: left _,_ right

Your solution

Reference solution

Bool-searchable : Searchable Bool
Bool-searchable P with P false in eq | P true in eq'
... | false | y     = left  (false , eq)
... | true  | false = left  (true  , eq')
... | true  | true  = right λ { false → eq ; true → eq' }

There is also a slick proof involving the ideas of the cryptic is-tautology₁' function from the module on equality results on Booleans.

Exercise 4Bool-hasDrinkers

Bool-hasDrinkers : HasDrinkers Bool
Bool-hasDrinkers P = P false , {!!}

The reference solution uses: part₂

Your solution

Reference solution

Bool-hasDrinkers : HasDrinkers Bool
Bool-hasDrinkers P = P false , B.part₂ P

Infinite yet searchable types?#

open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Operators
open import Padova2025.ProvingBasics.Termination.Gas
open import Padova2025.Explorations.Uncountability.Applications

Amazingly, beyond the finite types, there do exist infinite types which are searchable.

In any flavor of constructive mathematics where function extensionality is available, such as Cubical Agda, the “one-point compactification of the natural numbers”, roughly speaking ℕ with an added point ∞, is searchable.
In some flavors, even the Cantor space is searchable—its uncountability notwithstanding.

This shocking fact has been thoroughly explored by Martín Escardó. To jump into this fascinating area, have a look at this classic post on Andrej Bauer’s blog, this Agda code or these slides.

A miniature toy version (blithely employing a recursion which will be but cannot be shown to be terminating) is available in the following module.

open import Padova2025.Explorations.Uncountability.Impossible.Toy

This module exports a function root : (Cantor → Bool) → Maybe List which should either return just xs with xs the first five terms of a root of the input predicate (more terms could also be generated as needed), or nothing in case no root exists. When applied to predicates defined in the empty context, not using any assumptions or postulates, the root function always works correctly, though this meta-assertion is not provable in Agda.

More precisely, the recursion employed be the root function terminates in case the input function is uniformly continuous. It is a meta-theorem about certain flavors of Martin-Löf type theory that every term of type Cantor → Bool in the empty context is indeed uniformly continuous, and one can entertain the idea that this result also holds for Agda (which however strictly speaking is ill-specified). See this note by Thierry Coquand and Guilhem Jaber for details and the PhD thesis of Martin Baillon for many new results and pointers to the literature.

Try it yourself: Fill in the hole as you wish; press C-c C-v; enter root example; observe the results. For instance, if example xs is defined as not (xs zero) || xs one || not (xs two), then root example will reduce to just (true ∷ false ∷ true ∷ false ∷ false ∷ []).

Exercise 5example

example : Cantor → Bool
example xs = {!!}

The reference solution uses: true

Your solution

Reference solution

example : Cantor → Bool
example xs = true