Lean uses something called type theory. This can be a little bit counterintuitive to mathematicians. For example there are lots of different kinds of 7. The core Lean library provides us with the natural number
7 = 7:nat, and the integer
7:int. If you have access to the maths library then (after e.g.
import topology.real or wherever they have put the reals nowadays, I heard it’s moving to
analysis.real) you have access to at least two further kinds of 7, namely
7:real, the rational number 7 and the real number 7. Mathematicians implicitly regard all of these 7’s as the same. Lean is a bit more wary about this kind of thing, although sometimes it will secretly change the type of something from nat to int to rational if it thinks that this is the only way to make things make any sense.
But I’m not here to talk about that, I’m here to talk about types. You can see the type of something with the
#check command. Let’s take a look at some types. Note that anything after the
-- signs means a comment.
#check 4 -- nat
#check nat -- Type
#check (7:int) -- int
#check int -- Type
#check Type -- kind of interesting. But not relevant to us.
If you’re using VS Code and you can find a little icon in the top right hand corner of one window that looks like four thin straight lines and says “Info View : Display Messages (Ctrl+Shift+Alt+Enter)” when you hover over it, then either by clicking on it or by typing Ctrl+Shift+Alt+Enter you can open a new little window where you can see the answers to all these checks. Alternatively you can just hover your cursor over the
#check to see the answer.
I think Type is a kind-of weird name for an *example* of a type, because there are types like
nat which are still types but which are not equal to Type. I guess the point is that Type is quite a general kind of type. If something has type Type, I like to think of it as a set. For example 4 is a number, not a set, so its type is
nat and not Type; but the set
nat of all natural numbers is a set, and indeed its type is Type.
Here are some more interesting types.
variable f: nat -> nat -- a function from the naturals to the naturals
#check f -- some sort of function type.
#check f 5 -- it's got type nat.
Note that we haven’t even defined the function f! So we wouldn’t actually be able to evaluate it, but even though it’s not been defined we can still figure out where it’s going from and to. This is called “type checking” I think. It’s some sort of basic sanity test which you can do in quite complicated situations to check that everything has the type it’s supposed to have.
Now here’s one of the most interesting types that there is.
#check (2+2=4) -- Prop
#check (forall x y : nat, x = y ) -- Prop
#check (forall x y : nat, x = x ) -- Prop
#check forall x y z n : nat, not ((x>=1) ∧ (y>=1) ∧ (z>=1) ∧ (n>=3) ∧ (x^n+y^n=z^n)) -- Prop
A “Prop” is a very common type, and it’s the type that true/false statements have.
It’s very easy to construct things of type
nat. For example any non-negative integer that you can think of has type
We just saw above that it’s also quite easy to construct things of type
Prop. For example
2+2=4 has type
Prop, as does the formulation of Fermat’s Last Theorem above.
But it turns out that
(2+2=4) is *also* a type!
So can we build something of type
Sure we can:
theorem t : (2+2=4) := by trivial
There’s a proof of the trivial theorem that 2+2=4. What this means in Lean is that
t is actually a thing of type
2+2=4, and it was constructed using the function
by trivial. You could use
theorem t2 : 2+2=4 :=
That’s a bit weird. Actually it’s not weird at all, it sort of makes things symmetric. For example
4 has type
nat has type
Type, which is some sort of generic type that begins with a capital letter. Similarly a proof of 2+2=4 has type
2+2=4, which has type
Prop, which is some sort of generic type that begins with a capital letter.
(forall x y : nat, x = y ) is simply not true, we can’t construct a proof of it. So there’s an example of a type for which we can’t construct any elements of that type! In fact there’s an even easier type with this property:
false is a
Prop which has been specifically designed so that it is impossible to construct anything of that type. Very counter-intuitive if you’re coming to this from a world like C++ or something, where types are actually designed so that you can build useful things of these types.
The difference between a theorem and an example in Lean is that theorems name the objects they’re constructing (proofs of propositions) and examples don’t. So we can prove
2+2=4 a third time like this:
example : 2+2=4 := by trivial
and here what we did was that we constructed an element of type
2+2=4, didn’t give it a name, and then threw it away.
When you are in the middle of a big proof, you have a bunch of hypotheses with names, and a goal. For example here’s a very elaborate proof of some easy fact.
example : forall x : nat, x <= x+x :=
have H : 0<=x,
-- at this point one could say "H is the hypothesis that 0 <= x"
-- but one could also say that H is an object of type 0<=x
-- or in other words a proof that 0<=x.
have H2 : x+0<=x+x,
have H3 : x+0 = x,
rewrite H3 at H2,
If you step through the proof, you can see that extra hypotheses slowly appear — these are objects representing proofs of mathematical true/false statements.
Functions are the same as logical implications.
Those of you who are paying attention might notice that Lean doesn’t distinguish between a mathematician’s “function arrow” and their “implies sign” . This is because, to a computer scientist, they’re the same thing! For example the squaring function on the natural numbers is
f : nat -> nat, and the input is a natural number (i.e. something of type nat) and the output is a natural number (i.e. something else of type nat). But if
Q are Propositions, then a function
f : P -> Q takes something of type
P and returns something of type
Q. Now something of type
P is a proof of
P, and something of type
Q is a proof of
Q, and this means that a function
P->Q is something which takes a proof of
P and returns a proof of
Q — so in particular it means that if
P is true (a notion which I am going to conflate with “provable”) then
Q must also be true! In particular we can really think of this function as a proof that .
This is called the Curry–Howard correspondence apparently.