Proving trivial things with Lean [difficulty : quite easy]

If you want to learn Lean, you can do what I did and read a book and do all the exercises. I had a pdf copy which I would browse through, but if you try this route then I would thoroughly recommend having a computer with Lean installed to hand when reading, because if you don’t understand something you can experiment.

However, watching my teenage children learn has been an eye-opening experience. They seem far more focussed on just launching in and then googling when they get stuck. My children have learnt all manner of things in this way, from how to draw eyes to how to make animated computer art to how to write Machine Learning projects in Python. In short — they want to do the exercises before they have even opened the book.

This post is for those who want to learn Lean this way. Let’s see Lean working with mathematical statements in practice.

If you want to actually do some real learning, you must have access to a working version of Lean. If you don’t use Lean then all you will know at the end of this is that 2+2=4 and you knew that already. The simplest way to use Lean is just to run it in a web browser — click on that link and then just switch between tabs. A better way is to install it on a Windows/Mac/Linux computer, but this takes some time. Whatever you decide to do, here is some Lean code for you to cut and paste. Let’s start by proving that 2+2=4. Oh — Harrison said I should be using MathJax. Note to self: google for how to do this. Anyway, cut and paste this:


example: 2+2=4 :=
begin
trivial
end

or just click here (link opens in new window), and then click around and wait a few seconds for everything to load.

OK that was pretty trivial, although I am not particularly happy with how that code looks in this blog. Note to self — figure out a better way of displaying code.

If you’re using Lean online via your web browser, or VS Code, you should be able to move your cursor around this proof and see information about the state of the proof in another window (in VS Code hover your mouse over the symbols in the top right until you find the “display goal” one and click on it to open the window I’m talking about — in the browser version it’s just right there on the right).

You’ll see that in the middle of the argument we had a “goal”, which was “weird-sideways-T 2+2=4”. Then by the end we had no goals, which was because we had solved all the goals. The weird sideways T basically means: “anything to the left of it is something we are assuming, and anything to the right of it is something we are proving” (we didn’t have to assume anything here.)

Fiddle around and prove more things. That’s how we’re going to learn in this post. Try to prove that 2+3=5. Can we do big numbers? Can you prove 12321+12321=24642? Try to prove that 2+2=5. What happens? Can you prove that 3*3=9? That 5-4=1? Can you prove that 2-3=-1? This one is much harder that it looks! Can you prove that 2-3=0? Wait–what?

By default, Lean’s numbers are what a computer scientist might call “the natural numbers”, which apparently in their subject means \{0,1,2,3,4,\ldots\}. As a mathematician I was always taught that they started with 1 but never mind. Can you now see what is going on with 2-3 now? What do you think you will be able to prove that 7/3 is?

Even though you don’t have to, you can explicitly tell Lean that you’re talking about natural numbers, by writing (2:nat) instead of 2. If you’re using VS Code you can even write (2:\nat) and a really cool thing happens. Try it! The standard notation for the natural numbers is \mathbb{N}. It used to be \mathbf{N} in books, but when mathematicians wrote this on a blackboard it became \mathbb{N} (“blackboard bold”), and then at some point after LaTeX got popular in the 1990s the notation actually changed in books from the bold to the blackboard bold. Take a look at an old maths book at some point and notice that there’s probably no blackboard bold in it at all.

There is also standard notation for the integers in books — they’re called \mathbb{Z} and they are \{\ldots,-2,-1,-0,1,2,\ldots\}. There is also the rational numbers (\mathbb{Q}) and the real numbers (\mathbb{R}). However to get the rationals and the reals in Lean you’ll start having to import libraries so let’s not worry about that now.

Lean does understand negative numbers, but you will have to tell it explicitly that this is what we’re using. Try


example : (2:int)-(3:int)=(-1:int) :=
begin
trivial
end

That works, although it’s a bit ugly. You will get used to ugly. In fact you’ll begin to find it beautiful. When you’re bored of typing (2:int)+(2:int)=(4:int) you can see if \int works. You can also drop some of those ints. Try (2:int)+3=5. What about 2+(3:int)=(5:int). Not everything works! Why not? Remember that 2 by itself is a natural number not an integer. Hint: when adding two things together, Lean looks at the first one first — you have to start somewhere.

OK, let’s do algebra. We need a variable, and we will follow the time-honoured tradition by calling it x. Of course Lean wants us to know whether it is a nat or an int, because it’s fussy like that. So when we introduce the variable, we have to tell it. Try this.


variable x : int
example : x=x :=
begin
trivial
end

If you move the cursor up and down through the code you can see that in the middle we have a goal of x=x but we also have a hypothesis, which is that x is an integer. See the use of the colon? x:\mathbf{Z} means “x has type int“. We’re doing mathematics in a set-up called “type theory” so everything has a type. If you want to get distracted, then you can check the types of stuff with the #check command. Try this (some time after the variable command so Lean knows what x is)


#check 2
#check x
#check (2:int)
#check int

As I say, pretty much every object in Lean has a type. Did you notice that even int had a type? What is the type of the type of the type of the type of 2?

Anyway, let’s get back to algebra. See if you can prove that x+2=x+2. Can you prove that x+2=2+x though? Unfortunately, this apparently is non-trivial. We see on the right that our “trivial tactic failed”. Aah — so “trivial” is a tactic! There’s actually a whole section on tactics in the Lean reference manual, although actually that link is currently secret because the manual isn’t finished yet. The “trivial” tactic will only get you so far. There’s a much better tactic called “simp”, which is short for simple, which means that it will solve some goals which are bit more difficult than trivial. See if this works.


variable x : int
example : x+2=2+x :=
begin
simp
end

See how far you can get. You can even have more than one variable at once:


variables x y z: int
example : x+y+z=z+y+x :=
begin
simp
end

I think that’s enough for starters. Give it a go, get stuck, it’s quite confusing. Ask for help in the comments.

The bad news is that there aren’t that many powerful tactics at this point. The good news is that the Lean guys are writing new tactics all the time and adding them to Lean, so over the next few months maybe Lean will evolve and learn new moves tactics and by the end of term we will have caught them all done all the example sheet questions.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Learning Lean. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s