2. Lean🔗

2.1. Notes on Lean🔗

2.1.1. Lean as a programming language🔗

Lean is a functional programming language (i.e. it actually only consists of functions). This paradigm is in contrast to imperative programming such as Python, Java and C. Lean comes with many features you might be familiar with, such as a library for output and input, but is still young and many things need to be developed.

2.1.2. Dependent type theory🔗

In all programming languages, you have data types such as int, string and float. In Lean, these exist as well, but you can (and will in this course) define own data types. In all cases, we write x : α for a term x of type α, so we write False : Bool, 42 : ℕ, but also f : ℕ → ℝ (for a function from ℕ to ℝ, which is an own type) and 0 ≠ 1 : Prop (the proposition that 0 and 1 are different natural numbers), which is a proposition. Terms and types can depend on variables, e.g. in ∀ (n : ℕ), n < n + 1 : Prop and f : (n : ℕ) → (Fin n → ℝ) (where Fin n is the type which carries {0, ..., n-1}), which is a function f with domain ℕ such that f n ∈ ℝ^n.

As we see, these new data types are more abstract in the sense that Lean understands ℕ (and ℝ) as infinite types, which are not limited by floating point arithmetic. E.g., ℕ actually represents an infinite set that is characterized by containing 0, and if it contains n, then it also contains the successor of n (represented by succ n). Accordingly, the real numbers are defined by an equivalence relation on Cauchy sequences, which is quite elaborate. (Although ℝ is implemented as such a quotient within Lean, we will not have to deal with these implementation details when working with real numbers, since we will rely on results in Mathlib, the mathematical library, taking care of these details.)

2.1.3. Universes, Types and Terms🔗

In Lean, there are three levels of objects: universes, types and terms. We are concerned here with the last two. Of particular interest is the type Prop, which consists of statements that can be True or False. It includes mathematical statements, so either the hypotheses, or the goal of what is to be proven. A hypothesis in Lean has the form hP : P, which means P is true, and this statement is called hP. Synonomously, it meansthat P is true and hP is a proof of P. The hypotheses here have names P Q R S, and the proofs of the hypotheses hP hQ hR hS. All names can be arbitrary. Furthermore, there are hypotheses of the form P → Q, which is the statement that P implies Q. (Note the similarity to function notation as in f : ℝ → ℝ.)

2.1.4. Function definitions🔗

In Lean, the function f : ℕ → ℕ, x ↦ 2x is defined as

def f : ℕ → ℕ := fun x ↦ 2*x

(Write \mapsto for ↦.) It is assumed that the x is only introduced to define f. The application of f to an x : ℕ is then done using f x. (The notation f x is an abbreviation for f(x), since Lean is sparing with parenthesis.)

2.1.5. Equality🔗

Due to the multitude of types in Lean, we have to be careful about equality. In Lean, there are three types of equality:

Syntactic equality: If two terms are letter-for-letter equal, then they are syntactically equal. However, there are a few more situations in which two terms are syntactically equal. Namely, if one term is just an abbreviation for the other (for example, x = y is an abbreviation for Eq x y, where Eq is a function which takes two terms of the same type, and assigns True if they are the same and False otherwise), then these both terms are syntactically equal. Also equal are terms in which globally quantified variables have different letters. For example, ∀ x, ∃ y, f x y and ∀ y, ∃ x, f y x are syntactically equal.
Definitional equality: Some terms are equal by definition in Lean. For example, x : ℕ, x + 0 is by definition identical to x. However, 0 + x is not definitionally identical to x. This is apparently only due to the internal definition of addition of natural numbers in Lean.
Propositional equality: If there is a proof of x = y, then x and y are said to be propositionally equal. Similarly, terms P and Q are said to be propositionally equal if you can prove P ↔ Q. Some Lean tactics only work up to syntactic equality (such as rw), others (most) work up to definitional equality (such as apply, exact,...) This means that the tactic automatically transforms terms if they are syntactically or definitional equality.

There is a special kind of equality to be observed with sets and functions. For example, two functions are exactly the same if they return the same value for all values in the domain. This behavior is called extensionality in the theory of programming languages. (If extensionality applies, then, for example, two sorting algorithms are the same if they always produce the same result).

2.1.6. Different parentheses in `Lean`🔗

There are (essentially) three different types of parentheses in Lean statements. The simplest is (...), which, as in normal use, indicates parentheses in the sense of what belongs together. However, you have to learn how Lean brackets internally when no '()' are given. Operators like and (∧), or (∨), are right-associative, so e.g. P ∧ Q ∧ R := P ∧ (Q ∧ R). The application of functions in sequence, such as f : ℕ → ℝ and g : ℝ → ℝ , applied to n : ℕ is g (f n), because g expects an input of type ℝ, and this is what f n provides. You cannot omit (...), i.e. in this case the parenthesis is left-associative.

Now let's comment on the parentheses [...] and {...}. For example, #check@ gt_iff_lt (the statement that a>b holds if and only if b<a holds), where both types occur. This yields

gt_iff_lt : ∀ {α : Type u_1} [_inst_1 : has_lt α] {a b : α}, a > b ↔ b < a

When this result is applied, the statements in {...} and [...] are added by Lean itself. The statements in {...} depend on the type of the objects that have to be given, and can therefore be inferred. (Above, when applying gt_iff_lt, the variables a and b have to be given.) Therefore, their type is also known, and one does not have to α is not explicitly specified. Since the application is made to a concrete α (for example, ℕ), and Lean knows a lot about the natural numbers, the type class system can look up many properties of ℕ, and also finds that has_lt ℕ holds (i.e. on ℕ at least a partial order is defined).

2.1.7. Proving propositions and evaluating functions🔗

Although we almost exclusively prove propositions in tactic mode in these notes, it is instructive to know about the simplest example of how to turn the proof to term mode: There are two rules:

The tactic exact is the same as calling a function.
The tactic intro is like taking a variable, which will be the argument of a function which is evaluated in the next step.

Let us consider two examples:

The term proof

example (P : Prop) : False → P := False.elim

is the same as

example (P : Prop) : False → P := byP:Prop⊢ False → P
    exact False.elimAll goals completed! 🐙

The term proof

example (s t : Set ℝ) (hst : s ⊆ t) (x : ℝ) :
    x ∈ s → x ∈ t := fun hx ↦ hst hx

is the same as

example (s t : Set ℝ) (hst : s ⊆ t) (x : ℝ) :
    x ∈ s → x ∈ t := bys:Set ℝt:Set ℝhst:s ⊆ tx:ℝ⊢ x ∈ s → x ∈ t
    intro hxs:Set ℝt:Set ℝhst:s ⊆ tx:ℝhx:x ∈ s⊢ x ∈ t
    exact hst hxAll goals completed! 🐙

2.1.8. Two abbreviations🔗

There are at least two abbreviations used in Mathlib which you will encounter frequently.

If you have h : x = y and hx : P x (with P x : Prop), you can prove P y by replacing h in hx. The shorthand notation for this is h ▸ hx. (Write \t for ▸).

example (P : ℕ → Prop) (x y : ℕ) (h : x = y) (hx : P x) :
    P y := byP:ℕ → Propx:ℕy:ℕh:x = yhx:P x⊢ P y
  exact h ▸ hxAll goals completed! 🐙

Sometimes, bracketing is critical, and it appears frequently that it has the form apply first (second very long statement), and you might get lost since the closing brackets are far away from their opening counterparts. In this case, we write apply first <| second very long statement, which does not need a closing symbol.

example (P Q : Prop) (hP : P) (hnP : ¬P) : Q := byP:PropQ:ProphP:PhnP:¬P⊢ Q
    apply False.elim <| hnP hPAll goals completed! 🐙

2.2. Proofs in Lean🔗

2.2.1. Foundation🔗

In Lean every object has a type. Types itself fall into several categories, called universes. There are two main universes, called Prop and Type. Any mathematical statement comes with a claim and its proof. Say we want to claim something, such as Goldbach's conjecture:

theorem declaration uses 'sorry'goldbach : ∀ (n : ℕ) (h₁ : n > 2) (h₂ : Even n),
    ∃ (i j : ℕ), (Prime i) ∧ (Prime j) ∧ (n = i + j) := by⊢ ∀ n > 2, Even n → ∃ i j, Prime i ∧ Prime j ∧ n = i + j
  sorryAll goals completed! 🐙

we speak about a term ∀ (n : ℕ) (h₁ : n > 2) (h₂ : Even n), ∃ (i j : ℕ), Prime i ∧ Prime ∧ (n = i + j) of type Prop, which constitutes its own type. A term of this type (which sould repalce the sorry in the above Lean code) is equivalent to a proof of Goldbach's conjecture.

This is to say:

Types as theorems, terms as proofs!

Constructing a term of type ℕ is easier (0 : ℕ) is accepted by Lean for this construction) than constructing a term of type ∀ (n : ℕ) (h₁ : n > 2) (h₂ : Even n), ∃ (i j : ℕ), (Prime i) ∧ (Prime j) ∧ (n = i + j), for which we would require proving Goldbach's conjecture and implementing the proof in Lean.

Since we are already speaking about fundamentals: For a large part, it is safe to think of Types as Sets. Recall that it leads to logical self-inconsistencies if we allow for something like the set/type of all sets/types. For this reason, the Type universe is split into levels, such as Type 0 : Type 1, saying that the type Type 0 (of all objects in level 0) is of Type 1, i.e., we are moving up a ladder when constructing more complex types. The coresponding idea goes back to von Neumann and Ernst Zermelo.

2.2.2. Mathlib🔗

The Lean-library which contains many mathematical results is called Mathlib. On its documentation page you can search for some results and concepts. (More precisely, you can search names of definitions, lemmas and theorems.) You will find results about e.g. Real numbers, Groups in algebra, Topology and Measure Theory.

Another way to search Mathlib is Moogle and Loogle (which you also have in vscode when clicking on the ∀ sign.)

2.2.3. First steps🔗

Let us start with some simple examples in order to explain the first tactics in Lean. We will deal here with

intro
exact
apply
rw
simp
apply?
have
refine
obtain

More tactics are found in Chapter xxx.

2.2.3.1. `intro`, `exact`, `apply` and `rw`

Let us start with a very simple example. If we want to prove the statement P → P (i.e. P implies P) we enter the following:

declaration uses 'sorry'example (P : Prop) : P → P := byP:Prop⊢ P → P
  sorryAll goals completed! 🐙

Depending on the position of the cursor, you will find the corresponding proof state. If the cursor is directly after by, the initial proof state is seen. It is important to know that behind ⊢ (called turnstile) stands the assertion, and everything above are hypotheses. (In the case shown, this is only the fact that P is an assertion/proposition.) This representation thus corresponds exactly to the assertion. If the cursor is after the sorry, there is now no goals, but the sorry tactic is only there to prove unproven assertions without further action, and a warning is issued in vscode. If you delete the sorry and replace it with an intro hP followed by exact hP, we get

example : P → P := byP:Sort ?u.7⊢ P → P
  intro hPP:Sort ?u.7hP:P⊢ P
  exact hPAll goals completed! 🐙

So we have transformed the statement P → P into a state where we have to assume hP : P and conclude P. The desired no goals appears.

The apply tactics is similar, but does not necessarily need to close the goal. Let us see how it works:

example (hPQ : P → Q) (hQR : Q → R) : P → R := byP:Sort ?u.23Q:Sort ?u.24R:Sort ?u.28hPQ:P → QhQR:Q → R⊢ P → R
  intro hPP:Sort ?u.23Q:Sort ?u.24R:Sort ?u.28hPQ:P → QhQR:Q → RhP:P⊢ R
  apply hQRP:Sort ?u.23Q:Sort ?u.24R:Sort ?u.28hPQ:P → QhQR:Q → RhP:P⊢ Q
  apply hPQP:Sort ?u.23Q:Sort ?u.24R:Sort ?u.28hPQ:P → QhQR:Q → RhP:P⊢ P
  exact hPAll goals completed! 🐙

Here, if the goal is R, and you have a proof hQR : Q → R, we only have to show Q and this transformation is done using apply hQR.

In fact, apply works iteratively. This means that apply hQR; apply hPQ; exact hP can be combined into

example (hPQ : P → Q) (hQR : Q → R) : P → R := byP:Sort ?u.23Q:Sort ?u.24R:Sort ?u.28hPQ:P → QhQR:Q → R⊢ P → R
  intro hPP:Sort ?u.23Q:Sort ?u.24R:Sort ?u.28hPQ:P → QhQR:Q → RhP:P⊢ R
  apply hQR (hPQ hP)All goals completed! 🐙

(Here, hPQ hP is a proof for Q, since we apply P → Q to a proof of P, which gives Q.)

We note that the above example is equivalent to

example : ∀ (P : Prop), P → P := by⊢ ∀ (P : Prop), P → P
  intro PP:Prop⊢ P → P
  intro hPP:ProphP:P⊢ P
  exact hPAll goals completed! 🐙

So if we have a ∀ in the goal, we make progress by using intro.

Sometimes, we have statements of equality x = y or P ↔ Q, so we would like to use the one instead of the other. This works using rw:

example (hQ : Q) (hPQ : P ↔ Q) : P := byQ:PropP:ProphQ:QhPQ:P ↔ Q⊢ P
    rw [hPQ]Q:PropP:ProphQ:QhPQ:P ↔ Q⊢ Q
    exact hQAll goals completed! 🐙

Here, we use rw to transform the goal P to the rewritten goal Q. If we want to use rw reversely, we write rw [← hPQ], and we can use rw also in hypothesis by writing e.g. rw [hPQ] at hP. Here is an example.

example (hQ : Q) (hPQ : P ↔ Q) : P := byQ:PropP:ProphQ:QhPQ:P ↔ Q⊢ P
    rw [← hPQ] at hQQ:PropP:ProphQ:PhPQ:P ↔ Q⊢ P
    exact hQAll goals completed! 🐙

2.2.3.2. `apply?` and `simp`

Of course, we want to make use of known facts when proving new ones. There are two main search functions built into our work: simp? and apply?. The first is based on simp, which works using a collection of simplification rules, which are searchable using simp?. Here is an example:

example : (0 < 1) := by⊢ 0 < 1
  Try this: simp only [Nat.lt_one_iff, pos_of_gt]simp?All goals completed! 🐙

Lean suggests Try this: simp only [Nat.lt_one_iff, pos_of_gt], which is taken to our code when we click on it.

In fact, the same example can be solved using library search using apply?. Here, Lean searches its library for possible results, and often outputs very many results and the remaining goals. Here, it is simple:

example : (0 < 1) := by⊢ 0 < 1
  Try this: exact Nat.one_posapply?All goals completed! 🐙

where Lean suggests Try this: exact Nat.one_pos.

2.2.3.3. `have`, `refine`, and `use`

In order to have some proper example, let us introduce Even and Odd. In fact, for a definition of Even, we can type

def Even.{u_2} : {α : Type u_2} → [inst : Add α] → α → Prop :=
fun {α} [Add α] a => ∃ r, a = r + r#print Even

which results in

def Even.{u_2} : {α : Type u_2} → [inst : Add α] → α → Prop :=
fun {α} [Add α] a => ∃ r, a = r + r

Assume we cannot prove our goal in one step, but need some intermediate result. In this case, we have the have tactics. We simply claim what we need as an intermediate step. At the moment, we leave the rest using sorry.

declaration uses 'sorry'example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    sorryAll goals completed! 🐙
  sorryAll goals completed! 🐙

We come to our intermediate result later, but first want to use it in the rest of the proof. However, we have to disentangle the ∃ statement in h. Often, we have to take apart what we are given. Note that ∃ (n : ℕ), Even n consists of (n : ℕ) and a proof of Odd , i.e. a pair of objects, and pairs in Lean are gives using ⟨_, _⟩. We use obtain in order to get the two elements of the pair:

declaration uses 'sorry'example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    sorryAll goals completed! 🐙
  obtain ⟨n, hn⟩ := hintron:ℕhn:Even n⊢ ∃ n, Even (n * n)
  sorryAll goals completed! 🐙

Recall that hn itself is an ∃-statement. This means we can use a nested version:

declaration uses 'sorry'example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    sorryAll goals completed! 🐙
  obtain ⟨n, ⟨k, hk⟩⟩ := hintro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n, Even (n * n)
  sorryAll goals completed! 🐙

Now we can use that n is Even and therefore would like to use that n * n = (2*k) * (2*k) = 4*k*k for showing that n * n is even. In order to see what we have to show, let us simplify using the definition of Even:

declaration uses 'sorry'example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    sorryAll goals completed! 🐙
  obtain ⟨n, ⟨k, hk⟩⟩ := hintro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n, Even (n * n)
  simp [Even]intro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n r, n * n = r + r
  sorryAll goals completed! 🐙

Now we can use n from above, and r = 2*k*k. This works with use:

declaration uses 'sorry'example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    sorryAll goals completed! 🐙
  obtain ⟨n, ⟨k, hk⟩⟩ := hintro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n, Even (n * n)
  simp [Even]intro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n r, n * n = r + r
  use nhn:ℕk:ℕhk:n = k + k⊢ ∃ r, n * n = r + r
  use 2*k*khn:ℕk:ℕhk:n = k + k⊢ n * n = 2 * k * k + 2 * k * k
  sorryAll goals completed! 🐙

The rest should be easy, since it only remains a calculation. Here, we use rw and the ring tactics, which can do calculations within a ring (in fact in a monoid):

declaration uses 'sorry'example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    sorryAll goals completed! 🐙
  obtain ⟨n, ⟨k, hk⟩⟩ := hintro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n, Even (n * n)
  simp [Even]intro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n r, n * n = r + r
  use nhn:ℕk:ℕhk:n = k + k⊢ ∃ r, n * n = r + r
  use 2*k*khn:ℕk:ℕhk:n = k + k⊢ n * n = 2 * k * k + 2 * k * k
  rw [hk]hn:ℕk:ℕhk:n = k + k⊢ (k + k) * (k + k) = 2 * k * k + 2 * k * k
  ringAll goals completed! 🐙

It remains to show the intermediate step. Here, we have to give Lean a pair, i.e. some n as well as a proof that Even n. This can not only be done using use as above, but also using refine, which is able to make a pair from two separate objects. Assume ww want to use that Even 48, but do not have a proof yet. Then we write a ?_, which stands for a hole in the proof which is to be filled in later:

declaration uses 'sorry'example : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even n
  refine ⟨48, ?_⟩⊢ Even 48
  sorryAll goals completed! 🐙

For a proof of Even 48, we need to find 24 and a proof that 48 = 24 + 24. Let us again work with ?_:

example : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even n
  refine ⟨48, ⟨24, ?_⟩⟩⊢ 48 = 24 + 24
  ringAll goals completed! 🐙

(In fact, the last step can also be solved by rfl, which means that the goal is true by definition.)

In total, we have the full example:

example : ∃ (n : ℕ), Even (n * n) := by⊢ ∃ n, Even (n * n)
  have h : ∃ (n : ℕ), Even n := by⊢ ∃ n, Even (n * n)
    refine ⟨48, ⟨24, by⊢ 48 = 24 + 24 rflAll goals completed! 🐙⟩⟩
  obtain ⟨n, ⟨k, hk⟩⟩ := hintro.intron:ℕk:ℕhk:n = k + k⊢ ∃ n, Even (n * n)
  use n, 2*k^2hn:ℕk:ℕhk:n = k + k⊢ n * n = 2 * k ^ 2 + 2 * k ^ 2
  rw [hk]hn:ℕk:ℕhk:n = k + k⊢ (k + k) * (k + k) = 2 * k ^ 2 + 2 * k ^ 2
  ringAll goals completed! 🐙

2.2.4. Names of `Mathlib` Results🔗

Names like zero_add, add_zero, one_mul, add_assoc, succ_ne_zero, lt_of_succ_le,... seem cryptic. It is clear that individual relatively understandable abbreviations (zero, one, mul, add, succ,...) are separated by _. In general, the following two rules apply to naming:

The goal of the statement to be proven is described; if hypotheses are added in the name, then with of_. The statement lt_of_succ_le is therefore an < statement, where succ ≤ applies. In fact:

Nat.lt_of_succ_le {n m : ℕ} (h : n.succ ≤ m) : n < m#check Nat.lt_of_succ_le

results in

Nat.lt_of_succ_le {n m : ℕ} (h : n.succ ≤ m) : n < m

This way, you can often guess the names of statements that you want to use.

2.2.5. Holes in proofs🔗

What is a hole in a proof? It is a missing argument...

2.2.6. Exercises🔗

It is now time to move to the exercises. So, proceed to vscode (or gitpod), copy the exercises folder and start coding. Further hints on tactics etc is given within the exercises. Tactics are given in alphabetical order in the next chapter.