In Lean 4: #print and #check #12

Hello everyone,

In this post, I will talk about two tactics in the Lean 4 programming language. These tactics are used with commands from the Mathlib library.

First, let’s start with a simple example:

import Mathlib.Tactic

print add_comm

When you type it — as always, I mean in the https://live.lean-lang.org/ environment — you will see some output appearing on the right. When you look at the “expected type” section there, it will give you a very clear demonstration of what the add_comm command does.

Here is what it looks like on my end:

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

Now, on the 3rd line of the code, let’s add the command:

check add_comm

In the “expected type” section, here is what appears on my end again:

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

Note: If you click at the end of the line you typed, you determine which line’s output you want to see.

Now, let’s get to the difference:

When you look under the “messages” section on the right side, you should see some differences between #print and #check.

With the #check command, the output in the "expected type" and "messages" sections looks very similar. The real difference appears with the #print command. Since this theorem is short, you see a short output as well; longer theorems will have much longer outputs, but here is what currently appears on my end:

theorem add_comm.{u_1} : ∀ {G : Type u_1} [inst : AddCommMagma G] (a b : G), a + b = b + a :=
fun {G} [AddCommMagma G] => AddCommMagma.add_comm

As you progress in Lean 4, you will notice that this is actually the way the theorem is defined. Since it is very short and you are just at the beginning of your journey, it might not mean much to you right now; that is why I also want to show you something a bit longer:

To make it a bit longer, I added this to the 4th line:

print add_add_neg_add_cancel

Now, let’s look at what I got as an output in the “messages” section:

theorem add_add_neg_add_cancel.{u_3} : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a + b + (-b + c) = a + c :=
fun {G} [AddGroup G] a b c =>
  Eq.mpr (id (congrArg (fun _a => _a = a + c) (add_assoc a b (-b + c))))
    (Eq.mpr (id (congrArg (fun _a => a + _a = a + c) (Eq.symm (add_assoc b (-b) c))))
      (Eq.mpr (id (congrArg (fun _a => a + (_a + c) = a + c) (add_neg_cancel b)))
        (Eq.mpr (id (congrArg (fun _a => a + _a = a + c) (zero_add c))) (Eq.refl (a + c)))))

As you can see, it is longer, and there are much longer ones out there. In the “expected type” section, however, you can still see exactly how this command from Mathlib serves us. Here is what it looks like on my end:

⊢ ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a + b + (-b + c) = a + c

In other words, as you learn how to write proofs, you will understand much better what the outputs from #print actually mean. However, this is also a great way to check commands from the Mathlib library and see what they do. Because the pop-up windows usually disappear as soon as you move your cursor away, using this kind of approach will allow you to examine them comfortably.

Stay with coding!

The code can be accessed via this link: https://github.com/fizikzedenin-kodlari/LeanOnMath/blob/main/%23print%23check%2312.lean

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