In 2007, Martin Escardo wrote a often-read
blog post about Seemingly impossible functional programs . One such seemingly impossible function is
find, which takes a predicate on infinite sequences of bits, and returns an infinite sequence for which that predicate hold (unless the predicate is just always false, in which case it returns some arbitrary sequence).
Inspired by conversations with and experiments by Massin Guerdi at the dinner of
LeaningIn 2025 in Berlin (yes, this blog post has been in my pipeline for far too long), I wanted to play around these concepts in Lean.
Let s represent infinite sequences of bits as functions from
Nat to
Bit, and give them a nice name, and some basic functionality, including a binary operator for consing an element to the front:
import Mathlib.Data.Nat.Find
abbrev Bit := Bool
def Cantor : Type := Nat Bit
def Cantor.head (a : Cantor) : Bit := a 0
def Cantor.tail (a : Cantor) : Cantor := fun i => a (i + 1)
@[simp, grind] def Cantor.cons (x : Bit) (a : Cantor) : Cantor
0 => x
i+1 => a i
infix:60 " # " => Cantor.cons
With this in place, we can write Escardo s function in Lean. His blog post discusses a few variants; I ll focus on just one of them:
mutual
partial def forsome (p : Cantor Bool) : Bool :=
p (find p)
partial def find (p : Cantor Bool) : Cantor :=
have b := forsome (fun a => p (true # a))
(b # find (fun a => p (b # a)))
end
We define
find together with
forsome, which checks if the predicate
p holds for any sequence. Using that
find sets the first element of the result to
true if there exists a squence starting with
true, else to
false, and then tries to find the rest of the sequence.
It is a bit of a brian twiter that this code works, but it does:
def fifth_false : Cantor Bool := fun a => not (a 5)
/-- info: [true, true, true, true, true, false, true, true, true, true] -/
#guard_msgs in
#eval List.ofFn (fun (i : Fin 10) => find fifth_false i)
Of course, in Lean we don t just want to define these functions, but we want to prove that they do what we expect them to do.
Above we defined them as
partial functions, even though we hope that they are not actually partial: The
partial keyword means that we don t have to do a termination proof, but also that we cannot prove anything about these functions.
So can we convince Lean that these functions are total after all? We can, but it s a bit of a puzzle, and we have to adjust the definitions.
First of all, these seemingly impossible functions are only possible because we assume that the predicate we pass to it,
p, is computable and total. This is where the whole magic comes from, and I recommend to read Escardo s blog posts and papers for more on this fascinating topic. In particular, you will learn that a predicate on
Cantor that is computable and total necessarily only looks at some initial fragment of the sequence. The length of that prefix is called the modulus . So if we hope to prove termination of
find and
forsome, we have to restrict their argument
p to only such computable predicates.
To that end I introduce
HasModulus and the subtype of predicates on
Cantor that have such a modulus:
-- Extensional (!) modulus of uniform continuity
def HasModulus (p : Cantor ) := n, a b : Cantor, ( i < n, a i = b i) p a = p b
@[ext] structure CantorPred where
pred : Cantor Bool
hasModulus : HasModulus pred
The modulus of such a predicate is now the least prefix lenght that determines the predicate. In particular, if the modulus is zero, the predicate is constant:
namespace CantorPred
variable (p : CantorPred)
noncomputable def modulus : Nat :=
open Classical in Nat.find p.hasModulus
theorem eq_of_modulus : a b : Cantor, ( i < p.modulus, a i = b i) p a = p b := by
open Classical in
unfold modulus
exact Nat.find_spec p.hasModulus
theorem eq_of_modulus_eq_0 (hm : p.modulus = 0) : a b, p a = p b := by
intro a b
apply p.eq_of_modulus
simp [hm]
Because we want to work with
CantorPred and not
Cantor Bool I have to define some operations on that new type; in particular the cons element before predicate operation that we saw above in
find:
def comp_cons (b : Bit) : CantorPred where
pred := fun a => p (b # a)
hasModulus := by
obtain n, h_n := p.hasModulus
cases n with
zero => exists 0; grind
succ m =>
exists m
intro a b heq
simp
apply h_n
intro i hi
cases i
rfl
grind
@[simp, grind =] theorem comp_cons_pred (x : Bit) (a : Cantor) :
(p.comp_cons x) a = p (x # a) := rfl
For this operation we know that the modulus decreases (if it wasn t already zero):
theorem comp_cons_modulus (x : Bit) :
(p.comp_cons x).modulus p.modulus - 1 := by
open Classical in
apply Nat.find_le
intro a b hab
apply p.eq_of_modulus
cases hh : p.modulus
simp
intro i hi
cases i
grind
grind
grind_pattern comp_cons_modulus => (p.comp_cons x).modulus
We can rewrite the
find function above to use these operations:
mutual
partial def forsome (p : CantorPred) : Bool := p (find p)
partial def find (p : CantorPred) : Cantor := fun i =>
have b := forsome (p.comp_cons true)
(b # find (p.comp_cons b)) i
end
I have also eta-expanded the
Cantor function returned by
find; there is now a
fun i => i around the body. We ll shortly see why that is needed.
Now have everything in place to attempt a termination proof. Before we do that proof, we could step back and try to come up with an informal termination argument.
- The recursive call from
forsome to find doesn t decrease any argument at all. This is ok if all calls from find to forsome are decreasing.
- The recursive call from
find to find decreases the index i as the recursive call is behind the Cantor.cons operation that shifts the index. Good.
- The recursive call from
find to forsome decreases the modulus of the argument p, if it wasn t already zero.
But if was zero, it does not decrease it! But if it zero, then the call from forsome to find doesn t actually need to call find, because then p doesn t look at its argument.
We can express all this reasoning as a termination measure in the form of a lexicographic triple. The
0 and
1 in the middle component mean that for zero modulus, we can call
forsome from
find for free .
mutual
def forsome (p : CantorPred) : Bool := p (find p)
termination_by (p.modulus, if p.modulus = 0 then 0 else 1, 0)
decreasing_by grind
def find (p : CantorPred) : Cantor := fun i =>
have b := forsome (p.comp_cons true)
(b # find (p.comp_cons b)) i
termination_by i => (p.modulus, if p.modulus = 0 then 1 else 0, i)
decreasing_by all_goals grind
end
The termination proof doesn t go through just yet: Lean is not able to see that
(_ # p) i will call
p with
i - 1, and it does not see that
p (find p) only uses
find p if the modulus of
p is non-zero. We can use the
wf_preprocess feature to tell it about that:
The following theorem replaces a call to
p f, where
p is a function parameter, with the slightly more complex but provably equivalent expression on the right, where the call to
f is no in the
else branch of an
if-then-else and thus has
p.modulus = 0 in scope:
@[wf_preprocess]
theorem coe_wf (p : CantorPred) :
(wfParam p) f = p (if _ : p.modulus = 0 then fun _ => false else f) := by
split
next h => apply p.eq_of_modulus_eq_0 h
next => rfl
And similarly we replace
(_ # p) i with a variant that extend the context with information on how
p is called:
def cantor_cons' (x : Bit) (i : Nat) (a : j, j + 1 = i Bit) : Bit :=
match i with
0 => x
j + 1 => a j (by grind)
@[wf_preprocess] theorem cantor_cons_congr (b : Bit) (a : Cantor) (i : Nat) :
(b # a) i = cantor_cons' b i (fun j _ => a j) := by cases i <;> rfl
After these declarations, the above definition of
forsome and
find goes through!
It remains to now prove that they do what they should, by a simple induction on the modulus of
p:
@[simp, grind =] theorem tail_cons_eq (a : Cantor) : (x # a).tail = a := by
funext i; simp [Cantor.tail, Cantor.cons]
@[simp, grind =] theorem head_cons_tail_eq (a : Cantor) : a.head # a.tail = a := by
funext i; cases i <;> rfl
theorem find_correct (p : CantorPred) (h_exists : a, p a) : p (find p) := by
by_cases h0 : p.modulus = 0
obtain a, h_a := h_exists
rw [ h_a]
apply p.eq_of_modulus_eq_0 h0
rw [find.eq_unfold, forsome.eq_unfold]
dsimp -zeta
extract_lets b
change p (_ # _)
by_cases htrue : a, p (true # a)
next =>
have := find_correct (p.comp_cons true) htrue
grind
next =>
have : b = false := by grind
clear_value b; subst b
have hfalse : a, p (false # a) := by
obtain a, h_a := h_exists
cases h : a.head
exists Cantor.tail a
grind
exfalso
apply htrue
exists Cantor.tail a
grind
clear h_exists
exact find_correct (p.comp_cons false) hfalse
termination_by p.modulus
decreasing_by all_goals grind
theorem forsome_correct (p : CantorPred) :
forsome p ( a, p a) where
mp hfind := by unfold forsome at hfind; exists find p
mpr hex := by unfold forsome; exact find_correct p hex
This is pretty nice! However there is more to do. For example, Escardo has a massively faster variant of
find that we can implement as a partial function in Lean:
def findBit (p : Bit Bool) : Bit :=
if p false then false else true
def branch (x : Bit) (l r : Cantor) : Cantor :=
fun n =>
if n = 0 then x
else if 2 n then r ((n - 2) / 2)
else l ((n - 1) / 2)
mutual
partial def forsome (p : Cantor -> Bool) : Bool :=
p (find p)
partial def find (p : Cantor -> Bool) : Cantor :=
let x := findBit (fun x => forsome (fun l => forsome (fun r => p (branch x l r))))
let l := find (fun l => forsome (fun r => p (branch x l r)))
let r := find (fun r => p (branch x l r))
branch x l r
end
But can we get this past Lean s termination checker? In order to prove that the modulus of
p is decreasing, we d have to know that, for example,
find (fun r => p (branch x l r)) is behaving nicely. Unforunately, it is rather hard to do termination proof for a function that relies on the behaviour of the function itself.
So I ll leave this open as a future exercise.
I have dumped the code for this post at
https://github.com/nomeata/lean-cantor.
Passively lit coding
The expected record surpass for the uniform distribution
The expected record surpass for the normal distribution
The expected record surpass for the gamma distribution
Squasher in action
Microsoft Minesweeper
Norman Ramsey shows a formula
Our most favorite camp spot
The IDE
A chatbot
