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.
I have officially reached the 6-week mark, the halfway point of my Outreachy internship. The time has flown by incredibly fast, yet it feels short because there is still so much exciting work to do.
. I am an intern here at Outreachy working with Debian OpenQA Image testing team. The work consists of testing Images with OpenQA. The internship has reached midpoint and here are some of the highlights that I have had so far.
NB: The context menu allows to switch the fonts on systems where the above snippet has not (yet) been installed. So good enough for a one-off.
This allows for convenient storage. Since it's too cold outside right now, cultivation will have to wait
until spring. This also just needs mycelium one can just buy, and some material fungus digests.
They can also be fed coffee grounds, and harvest of the fruit body is possible circa every two weeks.
KDE
Donate
. I am an intern at Outreachy and contributing to the Debian Images Testing project since October 2025. This project is Open Source and everyone can contribute to it in any way. The project uses Open QA to automatically install Operating System Images and test them . We have a community 
Screenshot of Wikipedia edit metadata on Special:RecentChanges with RCFilters enabled. Highlighted edits with a colored circle to the left side of other metadata are flagged by ORES. Different circle and highlight colors (white, yellow, orange, and red in the figure) correspond to different levels of confidence that the edit is damaging. RCFilters does not specifically flag edits by new accounts or unregistered editors, but does support filtering changes by editor types.
Charts showing the probability that an edit will be reverted as a function of ORES scores in the neighborhood of the discontinuous threshold that triggers the RCfilters flag. The jump in the increase in reversion chances is larger for registered editors compared to unregistered editors at both thresholds.
.
![[RSS 1.0 Feed]](common/rss10.png){kind=small}
![[RSS 2.0 Feed]](common/rss20.png){kind=small}
![[Atom Feed]](common/atom.png){kind=small}
![[FOAF Subscriptions]](common/foaf.png){kind=small}
![[OPML Subscriptions]](common/opml.png){kind=small}
![[Hacker]](common/hacker.png){kind=small}
![[Planet]](common/planet.png){kind=small}
