Lean for All

Day 18: Hidden arguments🔗

Find the arguments a statement does not show: curly braces, square brackets, and variables Lean adds by itself.

Some functions work for every type. This one applies a function twice:

def twice {α : Type} (f : α → α) (x : α) : α := f (f x) 16#eval twice (fun n => n + 3) 10 
16

α (the Greek letter alpha) stands for any type: Nat, Int, lists, anything. fun n => n + 3 is a function without a name: “take n, give n + 3”. Applied twice to 10, it gives 16.

{α : Type} is in curly braces, so it is an implicit argument: you never write it, Lean works it out (here from 10, it sees α is Nat). In a theorem, curly braces still mean for every. They only change who fills the value in.

To see everything, put @ in front of a name. Then all hidden arguments become visible, and you may give them yourself:

def twice {α : Type} (f : α → α) (x : α) : α := f (f x) @twice : {α : Type} → (α → α) → α → α#check @twice 16#eval @twice Nat (fun n => n + 3) 10 @List.length_append : ∀ {α : Type u_1} {as bs : List α}, (as ++ bs).length = as.length + bs.length#check @List.length_append 
@twice : {α : Type} → (α → α) → α → α
16
@List.length_append : ∀ {α : Type u_1} {as bs : List α}, (as ++ bs).length = as.length + bs.length

The last line shows a library theorem in full:

∀ {α : Type u_1} {as bs : List α}, (as ++ bs).length = as.length + bs.length

For every type α and all lists as and bs with entries in α, …

(Type u_1 is a technical detail: read it as “some type”.)

Square brackets are a second kind of hidden argument:

def addSelf {α : Type} [Add α] (x : α) : α := x + x 10#eval addSelf 5 -6#eval addSelf (-3 : Int) 
10
-6

[Add α] reads “α must have an addition”. Lean finds that addition by itself: for Nat the usual one, for Int the integer one. Such an argument is called a type class argument.

For an auditor, this means + in a general statement is “whatever addition the type has”. Usually that is the familiar one, but a file can supply its own.

The most surprising hidden argument: in core Lean, a name you never declared silently becomes “for every”. This is called autoImplicit.

theorem t (h : a > 5) : a > 3 := a:Nath:a > 5⊢ a > 3 All goals completed! 🐙 @t : ∀ {a : Nat}, a > 5 → a > 3#check @t 
@t : ∀ {a : Nat}, a > 5 → a > 3

a is declared nowhere, yet Lean accepts it and reads ∀ {a : Nat}, a > 5 → a > 3. Here that is harmless. But a typo also becomes a variable:

theorem length_self : lenght = lenght := rfl @length_self : ∀ {α : Sort u_1} {lenght : α}, lenght = lenght#check @length_self 
@length_self : ∀ {α : Sort u_1} {lenght : α}, lenght = lenght

lenght is not a function about length. It is a new hidden variable, and the theorem only says that something equals itself. Mathlib switches autoImplicit off, so there such code is rejected.

When a name in a statement is declared nowhere, it is a hidden “for every”, or a typo.

Check yourself🔗