In Lean 4: Proving #10

Hello everyone,

In this post, I will — finally — explain how to construct a proof using Lean. Up until now, I wanted to cover the most fundamental concepts so that we could finally get to this part…

First of all, there is a way to know whether a proof is complete or not in Lean. When the proof is finished, Lean can recognize it and run your code. However, if you leave one of the steps incomplete or make a mistake, it will throw an error.

Once again, I will show this through an example:

import Mathlib.Tactic example {M : Type*} [AddCommMonoid M] (x y: M): x + y = y + x:= by apply add_comm x y

Available at this link: https://github.com/fizikzedenin-kodlari/LeanOnMath/blob/main/apply%20%236.lean

In this example, our proof was completed in a single step. That’s why I want to show this first, so that everything becomes crystal clear. When you type the code into this website https://live.lean-lang.org/, there shouldn’t be any problems as long as you pay attention to the whitespaces. Now, to cause an error, partially or completely delete the 3rd line.

Right now, I’ve changed the 3rd line to this: apply add_com. In other words, I deleted the x y at the end, and also one of the 'm's from comm. On the right side, there is a section called "Messages" that explains the issue to us. It says unknown identifier. It said this just because you were missing a single letter 'm'. First of all, situations like this can be quite frustrating. In fact, this is exactly why I mentioned the apply? tactic, which is essential for these kinds of moments.

I tried apply? and it suggested this to me:

exact AddCommMagma.add_comm x y

Alright, the code has changed a bit. This wasn’t exactly what I was looking for, but what I needed is right here. This is where I saw how to use add_comm. Delete the AddCommMagma. prefix and you will see that the code still works.

These parts might be confusing for beginners, but there is something I’ve learned from other programming languages so far: many commands do the exact same job. Over time, as you grasp the logic of the language, you will naturally figure out which parts you can delete anyway. Of course, you don’t have to delete it either.

After all, the best part of programming is: “If it works, don’t touch it!”

Let’s continue from here… First of all, the final version of the code evolved into this — and as I explained before, we can use exact, apply, and rw interchangeably from time to time. So, there are no surprises for us at this point. The final version of the code became: https://github.com/fizikzedenin-kodlari/LeanOnMath/blob/main/exact_%238.lean

import Mathlib.Tactic example {M : Type*} [AddCommMonoid M] (x y: M): x + y = y + x:= by exact add_comm x y

Now, let’s try something else: leave only exact on the 3rd line. When you try this, you will notice a red underline at the end of exact. In the clearest terms, this red underline means "the proof is incomplete; something is either missing or wrong." If there is no red underline anywhere in your code (colors like orange or yellow are considered acceptable), then your proof is complete. Congratulations!

Now, let’s get to why I said colors like orange and yellow are considered acceptable…

Change the last line to sorry.

import Mathlib.Tactic

example {M : Type*} [AddCommMonoid M] (x y: M): x + y = y + x:= by

sorry

When you do this, you will notice that the word example gets underlined in a color between yellow and orange. I called this "acceptable" because there is indeed something provable here, but you bypassed it for now by using sorry. Think of it as a reminder to come back to it later.

I would also like to draw your attention to the fact that a rectangle of the same color has been added to the immediate right of your code editor. When it was underlined in red, a red rectangle was added there as well.

Since our code is very short right now, the value of this feature might not be obvious. But let me tell you, as the code gets longer, you can easily find the places you left as sorry or that contain errors thanks to these indicators, without having to visually scan the entire code from top to bottom.

Stay with coding!

WhatsApp channel link to get instant updates on new posts: https://whatsapp.com/channel/0029VbDJCPQ4NVinQrRkA11O