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.
Wikipedia says 
A lot of the youtube channels I follow tend to involve somebody making
things, so of course one of the videos my SO and I watched a few days
ago was about 
And then, 10 minutes after we had left, realizing that I had written
down the password for the train website, since it was no longer saved on
the phone, but i had forgotten the bit of paper at home. We could have
gone back to take it, but decided not to bother, as we could also
hopefully buy paper-ish tickets at the train station (we could).
Later on, I also realized I had also forgotten my GPS tracker, so I have
no record of where we went exactly (but it s not hard to recognize it on
a map) nor on what the temperature was. It s a shame, but by that point
it was way too late to go back.
Anyway, that probably was when Murphy felt we had paid our respects, and
from then on everything went lovingly well!
Routing had been done on the 
And indeed, after a short while the paved road ended, but the path
continued on a wide and flat track, and was a welcome detour through
what looked like water works to prevent flood damage from a stream.
In a warmer season, with longer grass and ticks maybe the fact that I
was wearing a long skirt may have been an issue, but in winter it was
just fine.
And soon afterwards, we were in Porto Ceresio. I think I have been there
as a child, but I had no memory of it. On the other hand, it was about
as I expected: a tiny town with a lakeside street full of houses built
in the early 1900s when the area was an important tourism destination,
with older buildings a bit higher up on the hills (because streams
in this area will flood). And of course, getting there by foot rather
than by train we also saw the parts where real people live (but not
work: that s cross-border commuters country).
Soon after arriving in Porto Ceresio we stopped to eat our lunch on a
bench at the lakeside; up to then we had been pretty comfortable in the
clothing we had decided to wear: there was plenty of frost on the
ground, in the shade, but the sun was warm and the temperatures were
cleanly above freezing. Removing the gloves to eat, however, resulted in
quite cold hands, and we didn t want to stay still for longer than
strictly necessary.
So we spent another hour and a bit walking around Porto Ceresio like
proper tourists and taking pictures. There was an exhibition of nativity
scenes all around the streets, but to get a map one had to go to either
facebook or instagram, or wait for the opening hours of an office that
were later than the train we planned to get to go back home, so we only
saw maybe half of them, as we walked around: some were quite nice, some
were nativity scenes, and some showed that the school children must have
had some fun making them.
Another Christmas decoration were groups of creatures made of evergreen
branches that dotted the sidewalks around the lake: I took pictures of
the first couple of groups, and then after seeing a few more something
clicked in my brain, and I noticed that they were wrapped in green LED
strings, like chains, and they had a red ball that was supposed to be
the nose, but could just be around the mouth area, and suddenly I felt
the need to play 
Another thing that we noticed were some benches in the shape of books,
with book quotations on them; most were on reading-related topics, but
the one with the Constitution felt worth taking a picture of, especially
these days.
And then, our train was waiting at the station, and we had to go back
home for the afternoon; it was a nice outing, if a bit brief, and we
agreed to do it again, possibly with a bit of a detour to make the walk
a bit longer. And then maybe one day we ll train to do the whole 5-6
hour thing through the hills.
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.
Manor by Mingle - the hostel where we stayed at during our KL transit. Photo by Ravi Dwivedi. Released under the CC-BY-SA 4.0.
Dosa served at Adyar Ananda Bhavan. Photo by Ravi Dwivedi. Released under the CC-BY-SA 4.0.
Lockers at TBS bus station. Photo by Ravi Dwivedi. Released under the CC-BY-SA 4.0.
My boarding pass for the bus to the airport in Kuala Lumpur. Photo by Ravi Dwivedi. Released under the CC-BY-SA 4.0.
View of Kuala Lumpur from the aeroplane. Photo by Ravi Dwivedi. Released under the CC-BY-SA 4.0.
I bought a 
The Debian LTS Team, funded by [Freexian s Debian LTS offering]
(
Found this grafitti on the wall behind my house today:
