Declarations and Commands

At the "top level" of a Lean file, there are two things you can do: you can declare a new value or proof, or you can execute a command to take some action, usually involving checking or executing some code you've already written.

Declarations

Just like other programming languages, Lean lets you declare named values and functions. Unlike many other programming languages, you use the same keyword, def, to declare both!

Value Declarations

A value declaration specifies the name, type, and value of your declaration in the form def name : type := value:

def myNat : ℕ := 42
def myInt : ℤ := -42
def courseNumber : ℕ := 2 * 10 + 2 

Unlike the variables you may be used to from imperative programming languages, declarations in Lean are immutable—they can't be modified after they're made. (Attempting to redeclare myNat would trigger an error, while a line of code like myNat := 3 would be syntactically invalid.)

Function Declarations

Function declarations look similar to variable declarations, except they specify arguments that appear before the colon; these can be referenced in the value appearing on the right-hand side of the :=, which specifies the value that the function returns. The general format of a function declaration is def name (arg1 : type1) ... (argN : typeN) : returnType := functionBody. Here are a couple of examples:

def addAndSquare (m : ℤ) (n : ℤ) : ℤ :=
    (m + n) * (m + n)

def collatz (n : ℕ) : ℕ :=
    if n % 2 = 0
    then n / 2
    else 3 * n + 1

Theorem Declarations

Unlike other programming languages, however, Lean also allows us to declare theorems. These are a special kind of declaration: rather than naming a value or function, they give a name to a proof of a certain proposition. The syntax is similar to variable definitions, except that we use a different keyword and write a proposition where we would ordinarily write a type and a proof where we would ordinarily write a value:

theorem name : proposition := by
    proof
    done

Note that, like with functions, we can specify certain "arguments" to our theorems by placing them to the left of the colon—think of these like the variables you fix at the outset of a theorem statement in English such as in, "Let x be an integer.…" Here are some examples (we write sorry instead of supplying a proof; this is a special keyword that tells Lean that we don't yet have a proof where it's expecting one):

-- "Given propositions P and Q, if P ∧ Q, then Q ∧ P"
theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P := by
    sorry
    done

-- "For any natural numbers m, we have m + 0 = m"
theorem add_zero : ∀ (m : ℕ), m + 0 = m := by
    sorry
    done

Examples and Variables

Sometimes, you might see an example used instead of a theorem. examples are just theorems without names: the syntax is exactly the same, except that you omit the name in the declaration (and therefore can't refer to the proof later on). For instance, the first line in the declaration of and_swap above would become example (P Q : Prop) : P ∧ Q → Q ∧ P := ….

Another notational convenience you'll see is the variable declaration. These are not variables of the kind you're used to in languages like Python! (Those are closer to the defs discussed earlier.) Variable declarations have the form variable (name : type). This declaration tells Lean that, in the portion of the file following the variable declaration, whenever we refer to name, we're referring to an arbitrary value of type type. For instance, if we wanted to declare a series of theorems involving properties of arbitrary natural numbers, we might do the following:

-- "In what follows, n is an arbitrary natural number"
variable (n : ℕ)

-- "(An arbitrary natural number) n added to itself is at least as big as n"
theorem add_self_geq : n + n ≥ n := by
    sorry
    done

-- "(An arbitrary natural number) n squared is at least as big as n"
theorem square_geq : n * n ≥ n := by
    sorry
    done

Commands

In addition to defining new entities with declarations, you can also inspect existing ones using commands. Commands are instructions to Lean to perform some action on a specified expression. Lean will display the result of the command in the Infoview on the right-hand side of the screen—the same region that displays your proof state when writing a proof. There are three main commands we'll use in this course:

#check

The #check command tells Lean to display "what kind of thing" some expression represents. For instance, #check 22, #check 2 + 2, and #check 5 % 3 all output ℕ, since these are all natural numbers. #check 1 = 3 outputs Prop, indicating that 1 = 3 is a proposition. #check Nat.zero_le outputs ∀ (n : ℕ), 0 ≤ n, indicating that Nat.zero_le is a theorem that proves that particular proposition.

#truth_table

The #truth_table command tells Lean to generate the truth table for the provided propositional formula. Note that any propositional variables used in your formula must previously have been declared as variables in your file. (If you're not sure what this means, just stick to using the same propositional variable names used elsewhere in lectures and homework—usually P, Q, R and the like—and you should be fine.) For instance, if I have P Q : Prop and enter #truth_table P ∧ (P → Q), I'll get the following output:

P	Q	(P → Q)	(P ∧ (P → Q))
true	true	true	true
false	true	true	false
true	false	false	false
false	false	true	false

#eval

The #eval command tells Lean to evaluate an expression. (Note: this command will be used infrequently in this course, and parts of this description won't make sense until later in the semester!) For instance, #eval 3 + 4 outputs 7, while #eval (3 + 4) * 6 outputs 42. You can use this to evaluate the output of functions besides the standard arithmetic operators: for instance, if I have a function gcd that takes two integers and produces their greatest common divisor, then #eval gcd 18 42 will output 6.