In Lean 4: Basics #14

Hello everyone,

In this post, I will explain the working logic of Lean, starting with examples from the “Mathematics in Lean” book.

You can access the example via this link: https://github.com/fizikzedenin-kodlari/LeanOnMath/blob/main/example%2314.lean

import Mathlib.Tactic
example (a b c : ℝ) : a * b * c = b * ( a * c ) := by
  rw [mul_comm a b]   
  rw [mul_assoc b a c]

That is all for the example. Breaking it down line by line:

We are required to write the first line so that we can use commands such as mul_comm and mul_assoc from the Mathlib library.

As for the second line, it is as follows:

example (a b c : ℝ) : a * b * c = b * ( a * c ) := by

This is where the example begins. Breaking it down piece by piece:

(a b c : ℝ)

Let a, b, and c be real numbers.

a * b * c = b * ( a * c )

We want to prove that this equality holds.

:= by

…is the piece of code indicating that we are about to start the proof.

Moving on to the next line:

rw [mul_comm a b]

I have previously explained the rw tactic. On top of that explanation, we can now build new knowledge. The new thing you see here is: mul_comm

As you will see when you type the #check mul_comm command, we see the following in the "expected type" section:

⊢ ∀ {G : Type u_1} [inst : CommMagma G] (a b : G), a * b = b * a

Here, on the right side, we have the statement a b = b a. This is one of the things we need for our example. We chose to use this command precisely because it is what we need.

Since the things changing places in our example are a and b, we specified that in our command:

rw [mul_comm a b]

If our example had expressions like x and y instead of a and b, and they were the ones changing places, we would write it like this:

rw [mul_comm x y]

Now, let’s come to the last line:

rw [mul_assoc b a c]

The new thing you see here is: mul_assoc

When I type #check mul_assoc, it shows the following in the "expected type" section:

⊢ ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)

Looking at the right side again, the expression we see is:

a * b * c = a * (b * c)

What it does here is put b * c inside parentheses. We needed this as well, which is why we used it.

As you will notice, in this specific example, the code works whether you write mul_assoc b a c or just mul_assoc. This happens to be unique to this particular case. In other examples, you might be forced to specify the variables next to it.

For instance, if you try to do the same thing on the line above — meaning, if you just write mul_comm instead of mul_comm a b—Lean won't know which two variables to swap. You have to tell it yourself.

Writing the variables next to it guarantees your work, but as seen in the last line, even if you don’t write them, Lean won’t get confused sometimes because there is no other option it can possibly apply.

Note: When you start typing a command, a pop-up window will appear showing predicted code suggestions. You can add them by either clicking on them or pressing the Tab key on your keyboard.

Stay coding!

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