In my “introduction to proof” course I teach the undergraduates about equivalence relations. What the students do not know, is that earlier on in the course I have secretly inserted examples of equivalence relations without ever letting on. For example, in the number theory section I prove that that if is a fixed positive integer, and are integers, then

and

And when we do equivalence relations I can then say “oh look! Congruence mod is an equivalence relation!”

I do the same trick with bijections. I prove that the identity function is a bijection, the inverse of a bijection is a bijection, and that the composite of two bijections is a bijection. Then later on I can say “oh look! ‘I biject with you’ is an equivalence relation!”

Coding up congruences mod in Lean is a joy to do, and one of my example files on this stuff even made it into mathlib!

But coding up the bijection equivalence relation into mathlib, one runs into an issue which is hard to explain to mathematicians. The problem is with symmetry — proving that the inverse of a bijection is a bijection. Say is a bijection, and . We’re trying to define the inverse function to and we want to figure out its value on . Lean has no trouble proving that there exists a unique element of such that applying to it gives . But when you try to access this element of while defining the inverse of , you get an intimidating error:

```
induction tactic failed, recursor 'Exists.dcases_on'
can only eliminate into Prop
```

Now Lean 3 does not have particularly friendly error messages, but as a Lean beginner I remember finding this one completely baffling. As far as type theory is concerned, there is a universe issue; the user just tried to define a function to `Type`

but the only function Lean could find was one into `Prop`

. A mathematician using Lean might know about Lean’s two kinds of universes — `Prop`

is the universe of true-false statements, where things like the statement of Fermat’s Last Theorem lives, and `Type`

is the universe of data, where things like the real numbers live. So what is going on? The problem is that is in `Prop`

, but the actual which exists is in `Type`

, and Lean is complaining that it does not have an *algorithm* to get hold of , and hence to move from the weak `Prop`

universe to the stronger `Type`

one.

Now of course to a mathematician this is just all ridiculous — the algorithm is “there is a unique — take that one”. The Lean beginner will learn that instead of applying the `cases`

tactic to `∃ (x : X), f x = y`

to get , they can apply the `choose`

tactic, and then one gets a new error

`definition 'g' is noncomputable, it depends on 'classical.some'`

which one fixes by writing `noncomputable theory`

at the top of the file. One is left with a feeling that Lean is kind of bewildering, and why was there so much fuss about applying the obvious algorithm “take the unique , duh”?

Recently on the Lean Zulip chat there has been talk amongst computationally-minded people about fancy things such as domain theory, topologies, the difference between `option`

and `roption`

, and difference lists. All of this has been slowly sinking into my head in some sort of way, and it culminated this morning in my actually seeing an explicit example (needs Zulip login) of a bijection between two sets where even a mathematician can see that there is some sort of issue with defining the inverse bijection. Thanks to Mario Carneiro for coming up with the example. The rest of this post explains it.

## The example.

The sets in question are as follows. Let . That’s easy enough.

Let be the set of infinite sequences where each `T,F`

(true or false), and with the property that for all we have . In words — if at some point in the sequence we see , then everything after that point is also .

Examples of elements of :

```
FFFFTTTTTTTTTTTTTTT...
FFFFFFFFFTTTTTTTTTT...
FFFFFFFFFFFFFFFFFFF...
TTTTTTTTTTTTTTTTTTT...
```

It is not hard to convince yourself that sequences in come in two flavours: either the sequence has some finite number of `F`

s and then everything afterwards is `T`

, or the sequence can be all `F`

s.

The bijection sends to the “all `F`

” sequence, and to the sequence which contains `F`

s and then reverts to `T`

forevermore. This is easily checked to be a bijection, and one even feels that it’s possible to write down the inverse. But how easy is it in practice?

Here’s the issue. Say I now give you a “black box” sequence in . It’s a function, I can guarantee that it’s in (I even have a proof!), and if you give me any I will return . We know that there is a unique with and it’s now your job to find it. What is your algorithm?

Initially you can start off by evaluating the function at some values. It turns out that is `F`

, that is `F`

and then that is `F`

. You realise that the you’re looking for is either a very large integer, or . But which one? You have what looks like complete access to , but you cannot work out which it corresponds to — indeed you cannot even say whether or not!

After a while, you get sick of this and say that actually you *haven’t* got complete access to and I am suppressing information. You complain that you don’t just want to evaluate at lots of numbers, you want to see the *actual definition*. So I reveal the definition: is defined to be

if there is a counterexample to the Goldbach conjecture which is at most , and `T`

`F`

otherwise. To put it another way — if the Goldbach conjecture is true then the sequence is all `F`

s and , but if it fails at some point then is the positive integer where it fails. I even show you the one-line proof that is an element of : if there’s a counterexample which is at most then clearly there’s a counterexample which is at most . Even with the definition, you are none the wiser!

## Conclusion.

When a function is marked as `noncomputable`

in Lean it means that Lean has not been told a method for working it out for every input. The innocuous-looking statement “there exists a unique with , so choose that ” is clearly something which can be done abstractly, but there is no *method* for finding , even if we can prove that it must exist. There *can’t* be a method for finding it in general — any such method would translate into a method for proving Goldbach’s conjecture, the 3n+1 problem, Fermat’s Last Theorem, the twin primes conjecture and so on; these are hard problems. Indeed, one can prove using a diagonalisation argument that no algorithm can exist to invert this bijection. The inverse of our computable function certainly exists, but it is a *noncomputable function*. Lean can handle such functions, no problem, but it has to be told explicitly that it should be ignoring computability issues (e.g. with the line `noncomputable theory`

at the top of a file).

The fun thing is that one knows that there is the inverse of the relation arising from the bijection, and that this relation is total and functional, but can’t conclude that it contains the graph of a function.

LikeLike

Your example reminds me of Ed Nelson. What is the set of positive integers, to Lean? Is it closer to “finite length sequences of decimals” (call that D) or to “finite length sequences of tally marks” (call that T)?

I know nothing about Lean but I assume it would not return any error messages if you tried to define the bijection s:T –> D that counted up all the tally marks as a decimal. (e.g. 1111 –> 4), nor if you tried to define the inverse to s. I bet it would not even complain that this inverse is not “computable,” am I mistaken?

But it could never successfully compute the composite function s^{-1}(e(5000)), where e:D –> D is the function given by the formula e(d) = 10^d. Note there’s plenty of space in this text box to write down the answer to e(5000), though it would be a big eyesore. Nelson suspected that one could use this asymmetry between T and D to derive a contradiction from the Peano axioms.

LikeLike

In Lean we have both, but `nat` is the tally marks. The decimals are called `num` (and in fact they’re binary). The bijection between `nat` and `num` is indeed computable in both directions. “computable” in Lean has nothing to do with feasibility or practicality (a la P=NP), it’s just about whether an algorithm exists (Turing, Halting problem etc).

LikeLike

Pingback: Proofs are not programs | Xena

Why do you feel mislead by proofs-as-programs? Has someone tried to oversell the case to you? It is fairly well understood which kinds of proofs correspond to programs, and it’s not all of them, of course. There are researchers who push the boundaries of the slogan and try to extend it in various directions. This has brought a great deal of success to understanding the relationship between deduction and computation, but where did you hear claims on the basis of which you feel mislead?

LikeLike

This is a fair question. I guess I say a bit more about this in my follow-up post https://xenaproject.wordpress.com/2019/06/15/proofs-are-not-programs/ . Maybe the case was over-sold; but perhaps I just misunderstood the claims initially. I have been watching Xavier Leroy’s lectures https://www.college-de-france.fr/site/xavier-leroy/course-2018-11-21-10h00.htm here and the “proofs = programs” slogan comes up a lot. Of course it will be very well-known to people who properly understand the correspondence what the actual limitations of the claim are. I have read your work Andrej on constructivism https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/ and I must say that I found it far easier to understand fully once I had used Lean for a while (Lean forced me to think more carefully about the logic behind doing mathematics). What I want to argue is that the kind of mathematicians I hang out with (mostly number theorists and geometers) are doing mathematics which in areas which are highly respected by the community and which are resolutely and inherently non-constructive. I have no proof of this, but in my work formalising perfectoid spaces I had to switch Lean into “mathematician mode — no code generated but feel free to use excluded middle and the axiom of choice” sufficiently often for me to become convinced that, at least in my area, nonconstructivism is all over the place. I might be wrong. As far as I know, nobody has ever thought carefully about this, and I conjecture that this is because most people thinking about perfectoid spaces don’t know too much about constructive maths, and most people thinking about constructive maths don’t know too much about perfectoid spaces.

LikeLike

I think there are *two* things going on here:

(1) Constructive vs. non-constructive reasoning.

(2) Whether the axiom of unique choice is available constructively.

For both Lean and Coq, with propositions modeled by the built-in type Prop, the axiom of unique choice is not available when one is under the constructive regime.

However, this is not to say that unique choice is inherently non-constructive. If instead of using the type Prop one uses what Voevodsky calls hProp, which is simply the type of types with at most one element (as is done in HoTT/UF), then the axiom of choice just holds, even under the constructive regime, and doesn’t need to be postulated. And then you do get that a function has an inverse if and only if it is a bijection (I presume you are assuming the definition that says that a bijection is a function which is both and injection and a surjection).

But this wouldn’t help with the example you attribute to Carneiro, because the fact that the proposed function *is* a bijection requires non-constructive reasoning, *before* you attempt to invert it by applying unique choice. Technically, the fact that your function is a bijection is equivalent to what constructive mathematicians call LPO, which means that we can tell whether a sequence of the kind you are considering is eventuallyT or not, which, as you say, decides the Goldbach conjecture and many other things like it.

The obstacle to constructivity here is not unique choice but the the fact that the proof of bijectivity of your is not constructive in the first place.

LikeLike

When I said “the axiom of choice just holds” I meant to write “the axiom of unique choice just holds”. Sorry.

LikeLike

Thanks for this response! Yes, in Lean at least, a bijection is defined to be a function which is both an injection and a surjection.

LikeLike