Seemingly Impossible Lean Programs  ^[draft]

It should come as no surprise that an exhaustive search over a finite set can be performed algorithmically by enumeration. On the other hand, it is impossible to perform such an exhaustive enumeration over the natural numbers or the integers, as these sets are infinite. However, somewhat paradoxically, there are infinite sets that can be exhaustively searched in finite time. More precisely, there is at least one infinite set $X$ with the property that for any given Boolean-valued function $p$ on $X$, it is possible to algorithmically verify within finite time whether $p$ holds for all elements of $X$ or to produce a counter-example if one exists. Moreover, there is a characterisation of the sets that can be exhaustively searched algorithmically in finite time as those that are topologically compact (under the so-called intrinsic topology). Both the title and the contents of this post are based on this post by Martín Hötzel Escardó on the blog Mathematics and Computation. The accompanying code is written in Lean4, unlike the original post which uses Haskell.

The primary example of an infinite exhaustively searchable type in this post will be the set of conatural numbers, defined as the set of decreasing infinite binary sequences. There is an embedding of the natural numbers into the conatural numbers, taking each natural number $n$ to the sequence with $n$ ones in the beginning followed by infinitely many zeros. The set also contains a special point - an infinite sequence of ones - which does not corresponding to any natural number.

/-- The conatural numbers -
    the set of infinite decreasing binary sequences. -/
def InfNat := {f : ℕ → Bool // ∀ n, f n.succ → f n}
-- a conventient notation
notation "ℕ∞" => InfNat

/-- The image of `0`, which corresponds to
    the constant sequence with the value `false`. -/
def zero : ℕ∞ := ⟨fun n => false, fun _ => id⟩

/-- The successor of a conatural number, defined as
    the sequence obtained by appending `true` at the front. -/
def succ : ℕ∞ → ℕ∞
  | ⟨f, inc⟩ =>
    ⟨fun
      | .zero => true
      | .succ a => f a,
    fun
      | .zero => fun _ => rfl
      | .succ _ => inc _⟩

/-- The special point at infinity, which is defined as
    the constant sequence with the value `true` -/
def inf : ℕ∞ := ⟨fun n => true, fun _ => id⟩