Terms, types, propositions

Statistical notation already distinguishes objects by kind. The expression $\hat{\tau }$ denotes a number, $\hat{\tau }(\cdot )$ denotes a function of the assignment, and $\mathbb{E}[\hat{\tau }]=\tau$ is a proposition about numbers. Lean records these distinctions as types.

Every Lean expression has a type. A proposition is also a type, and a proof is a term of that type. To check a proof, Lean computes the term’s type and verifies that it matches the stated proposition.

This chapter concentrates on reading statements: identifying their objects, assumptions, and conclusions. The examples are executable; running them shows the types and values discussed in the text.

Everything has a type

Two commands do all the exploring. #check reports the type of an expression without running it. #eval runs it.

#check (7 : ℕ)
#check (-3 : ℤ)
#check (2.5 : ℝ)
#check Real.sqrt

#eval (17 + 25 : ℕ)
#eval (10 : ℚ) / 4

#eval refuses on ℝ, and it is worth understanding why now rather than being surprised later. A real number in Lean is a Cauchy sequence up to equivalence: an infinite object with no finite normal form. There is nothing to print. This costs you nothing at all, because proofs do not evaluate — nobody ever needed the decimal expansion of $\mathrm{Var}(\hat{\tau })$ to prove a bound on it. When you want a number you can look at, work in ℚ; when you want mathematics, work in ℝ.

Types have types.

#check ℕ
#check ℝ
#check Prop
#check Type

#check ((2 : ℝ) + 2 = 4)

#check (rfl : (2 : ℕ) + 2 = 4)

The distinction that matters is Prop against Type. ℝ : Type — real numbers are data, and different real numbers are different. Prop is the type of statements, and (2 : ℝ) + 2 = 4 is a term of type Prop: not a number, not a Boolean, a claim.

The last #check in that block is the whole chapter in one line:

#check (rfl : (2 : ℕ) + 2 = 4)

We asked Lean for the type of the term rfl and told it to expect 2 + 2 = 4. It agreed. The proposition was used exactly as ℕ was used two lines earlier — as a type — and the proof was used exactly as 7 was — as a term of that type. This is the Curry–Howard correspondence, and after this paragraph I will stop naming it and start using it.

Definitions and functions

A def names a term. Nothing more.

def totalOfThree (y : Fin 3 → ℚ) : ℚ := y 0 + y 1 + y 2

def outcomes : Fin 3 → ℚ := ![2, 5, 11]

#eval outcomes 1
#eval totalOfThree outcomes
#check totalOfThree

theorem totalOfThree_apply (y : Fin 3 → ℚ) : totalOfThree y = y 0 + y 1 + y 2 := rfl

Note the type Fin 3 → ℚ standing in for “an outcome vector of length three”. Fin n is the type with exactly $n$ elements, so a function out of it is an $n$-vector indexed by unit, and an index is guaranteed in range by its type — there is no bounds check to write and no out-of-range case to handle. Chapter 3 takes this apart properly; for now, read Fin n → ℝ as $y\in {\mathbb{R}}^n$.

Function application is juxtaposition: f x, not f(x). Parentheses in Lean group, they do not apply, so f (x + 1) needs them and f x does not.

The last line of that block deserves a second look:

theorem totalOfThree_apply (y : Fin 3 → ℚ) : totalOfThree y = y 0 + y 1 + y 2 := rfl

rfl proves it because both sides reduce to the same term once the definition is unfolded. This is how you check that a definition means what you intended, and it is the cheapest sanity check available. It is also, as the last section of this chapter shows, how an empty theorem gets written by accident.

Every Lean function takes one argument.

def scale (c : ℚ) (y : Fin 3 → ℚ) : Fin 3 → ℚ := fun i => c * y i

#check scale
#check scale 2
#eval scale 2 ![1, 2, 3] 0

theorem scale_apply (y : Fin 3 → ℚ) : scale 2 y 2 = 2 * y 2 := rfl

#check scale prints the signature with its binders named, but the type it denotes is ℚ → (Fin 3 → ℚ) → (Fin 3 → ℚ), and → associates to the right, so that is ℚ → ((Fin 3 → ℚ) → (Fin 3 → ℚ)): give it a scalar and you get back a function waiting for a vector, which is what #check scale 2 reports. Partial application therefore always works, and you will see it constantly in Mathlib, where a lemma about f is applied to half its arguments and passed along as an argument itself.

example, theorem, and what rfl is not

example : (2 : ℕ) + 2 = 4 := rfl

theorem two_plus_two : (2 : ℕ) + 2 = 4 := rfl

noncomputable def sampleMean (a b : ℝ) : ℝ := (a + b) / 2

theorem sampleMean_eq (a b : ℝ) : sampleMean a b = (a + b) / 2 := rfl

example states and proves something without naming it: use it to check your understanding. theorem gives it a name so later proofs can cite it. lemma is a synonym — Lean does not distinguish them, and any hierarchy you read into the two words is yours, not the compiler’s.

rfl is not a proof method, it is a term: the constructor of Eq saying “this thing equals itself”. It closes a goal exactly when both sides reduce to the same normal form. So it does closed arithmetic (2 + 2 and 4 both reduce to 4), and it unfolds definitions, and it does not do algebra: a + b = b + a is not an instance of “both sides are the same term”, and needs add_comm.

Propositions are types, proofs are terms

Here is the payoff for taking the correspondence seriously: → is one symbol doing two jobs, and they are the same job.

def constantOutcomes : Fin 3 → ℝ := fun _ => 4

theorem effect_nonneg_at_zero (y1 y0 : Fin 3 → ℝ) :
    (∀ i, y0 i ≤ y1 i) → y0 0 ≤ y1 0 :=
  fun h => h 0

As a type former, Fin 3 → ℝ is the type of outcome vectors. As a proposition former, p → q is implication. And the proof of an implication is written fun h => …, with the same keyword as an anonymous function, because it is an anonymous function: it takes a proof of the hypothesis and returns a proof of the conclusion. In effect_nonneg_at_zero the proof is fun h => h 0, which reads: given the assumption h, apply it at unit 0. Applying a hypothesis and applying a function are the same operation.

This unification is why the table below is short. Each connective has one way in and one way out; in every case the way in is “build a term” and the way out is “take the term apart”.

The rest of this section is that table with one worked example per row.

∀

theorem one_scale (y : Fin 3 → ℝ) : ∀ i, 1 * y i = y i :=
  fun i => one_mul (y i)

theorem one_scale_at_two (y : Fin 3 → ℝ) : 1 * y 2 = y 2 :=
  one_scale y 2

∀ i, P i is a dependent function type: a function from i to a proof of P i, where the type of the output depends on the input. That is the only difference between → and ∀, and it is why fun i => one_mul (y i) is a proof of ∀ i, 1 * y i = y i. To use a ∀, apply it, as one_scale y 2 does.

If you take one thing from this chapter, take this: in a statement, ∀ costs nothing and means everything. theorem HT_unbiased (D : Design n) … quantifies over every design in the universe. Chapter 8 makes that claim; the reason it is worth making is that the ∀ is genuinely unconstrained.

∃

theorem exists_treated : ∃ i : Fin 3, (![2, 5, 11] : Fin 3 → ℚ) i = 5 :=
  ⟨1, rfl⟩

theorem exists_pos_of_exists_eq_three (y : Fin 3 → ℝ) :
    (∃ i, y i = 3) → ∃ i, 0 < y i :=
  fun ⟨i, hi⟩ => ⟨i, by rw [hi]; norm_num⟩

The anonymous constructor ⟨_, _⟩ builds a term of any structure type, and ∃ i, P i is a structure with two fields: the witness and the proof. You must produce the unit. Lean will not accept “such a unit must exist” as an argument unless you have a term that says why. In exists_treated the witness is the unit 1 and the proof is rfl, which suffices because ![2, 5, 11] 1 evaluates to 5: once the witness is fixed there is nothing left but a computation.

Going the other way, an ∃ in a hypothesis is taken apart by pattern matching: fun ⟨i, hi⟩ => … binds the witness to i and its property to hi. The tactic spelling of the same move is obtain, in chapter 2.

The second theorem in that block does both moves in one term, and the middle of it is a small tactic script. Read it from the outside in.

1. fun ⟨i, hi⟩ => …

   The theorem’s hypothesis is ∃ i, y i = 3, so the proof is a function out of it, and the pattern ⟨i, hi⟩ takes that proof apart on the way in: i is whichever unit the hypothesis was about, hi is the proof that y i = 3. Nothing is known about i beyond hi.

   Goal

   y : Fin 3 → ℝ
   i : Fin 3
   hi : y i = 3
   ⊢ ∃ i, 0 < y i

2. ⟨i, …⟩

   The conclusion is again an ∃, so it again needs a witness and a proof. The witness is the unit we were just handed — the same i, because the unit whose outcome is 3 is exactly the unit whose outcome is positive. That leaves the property 0 < y i to prove.

   Goal

   y : Fin 3 → ℝ
   i : Fin 3
   hi : y i = 3
   ⊢ 0 < y i

3. rw [hi]

   Inside the brackets we switch to tactic mode with by. The remaining goal mentions y i, and hi says what y i is, so rewriting with it replaces y i by 3 and turns a claim about an unknown outcome into arithmetic.

   Goal

   y : Fin 3 → ℝ
   i : Fin 3
   hi : y i = 3
   ⊢ 0 < 3

4. norm_num

   0 < 3 is a fact about numerals, which is norm_num’s job. No goals remain.

That interleaving is normal and worth getting used to: the structure of a proof is usually clearest as a term, and the arithmetic in its leaves is usually shortest as a tactic. by is the door between them, and it can be opened anywhere a proof is expected.

∧ and ∨

theorem and_intro_example (y : Fin 3 → ℝ) (h0 : 0 ≤ y 0) (h1 : 0 ≤ y 1) :
    0 ≤ y 0 ∧ 0 ≤ y 1 :=
  ⟨h0, h1⟩

theorem and_elim_example (y : Fin 3 → ℝ) (h : 0 ≤ y 0 ∧ 0 ≤ y 1) : 0 ≤ y 1 :=
  h.2

Structurally, p ∧ q is an ordered pair. Build it with ⟨_, _⟩, project out of it with .1 and .2. There is no more to it.

theorem or_intro_example (i : Fin 3) (h : i ∈ ({0, 1} : Finset (Fin 3))) :
    i ∈ ({0, 1} : Finset (Fin 3)) ∨ i = 2 :=
  Or.inl h

theorem or_elim_example (y : Fin 3 → ℝ) (h : y 0 = 1 ∨ y 0 = 2) : 0 < y 0 :=
  Or.elim h (fun h1 => by rw [h1]; norm_num) (fun h2 => by rw [h2]; norm_num)

p ∨ q is the asymmetric one. To prove a disjunction you must say which side you have: Or.inl for the left, Or.inr for the right. To use one you must handle both sides, which is what Or.elim takes its two function arguments for. In this subject the disjunction is almost always “unit $i$ was treated, or it was not”, and the two-case structure of or_elim_example is the shape of every argument about an indicator.

or_intro_example is one application: the hypothesis h already proves the left disjunct, and Or.inl h labels it as such. The elimination takes more saying, because its two arguments are two little proofs.

1. Or.elim h (fun h1 => …) (fun h2 => …)

   h : y 0 = 1 ∨ y 0 = 2 gives no information about which equation holds, so the conclusion 0 < y 0 has to be established twice, once per side. Or.elim takes exactly that: a function turning a proof of the left disjunct into the conclusion, and a function doing the same for the right.

2. fun h1 => by rw [h1]; norm_num

   The left branch is handed h1 : y 0 = 1 and owes 0 < y 0. rw [h1] replaces y 0 by 1, leaving the numeric goal shown below, and norm_num settles it.

   Goal

   y : Fin 3 → ℝ
   h : y 0 = 1 ∨ y 0 = 2
   h1 : y 0 = 1
   ⊢ 0 < 1

3. fun h2 => by rw [h2]; norm_num

   The right branch is the same two tactics against the other equation: rw [h2] turns the goal into 0 < 2, and norm_num again finishes. Both branches produce a proof of the same proposition, which is why Or.elim can return one regardless of which side was true.

   Goal

   y : Fin 3 → ℝ
   h : y 0 = 1 ∨ y 0 = 2
   h2 : y 0 = 2
   ⊢ 0 < 2

¬

theorem not_neg_of_nonneg (x : ℝ) (h : 0 ≤ x) : ¬ (x < 0) :=
  fun hlt => absurd h (not_le.mpr hlt)

theorem anything_from_contradiction (n : ℕ) (h : 0 < n) (h' : n = 0) : 1 = 2 :=
  absurd h (by rw [h']; exact lt_irrefl 0)

¬ p is not primitive. It is notation for p → False, where False is the proposition with no proofs. So a proof of ¬ p is a function turning a proof of p into a contradiction, and it is introduced with fun like any other function.

That is the whole of the first theorem. Its conclusion ¬ (x < 0) is an implication, so the proof begins with fun, and the body has to manufacture a False out of two facts that cannot both hold.

1. fun hlt => …

   ¬ (x < 0) is (x < 0) → False, so fun introduces a hypothesis hlt asserting the thing we are denying, and what remains to produce is False. Together with the theorem’s own h : 0 ≤ x, the context now contains both halves of a contradiction.

   Goal

   x : ℝ
   h : 0 ≤ x
   hlt : x < 0
   ⊢ False

2. not_le.mpr hlt

   not_le states ¬ (a ≤ b) ↔ b < a. At a := 0, b := x that reads ¬ (0 ≤ x) ↔ x < 0, so its right-to-left direction turns hlt : x < 0 into a proof of ¬ (0 ≤ x) — the negation of exactly the hypothesis we were given.

3. absurd h (not_le.mpr hlt)

   absurd : p → ¬ p → q consumes a proof and its negation and returns anything; here p is 0 ≤ x and q is False. Applying a ¬ p to a p would have done the same job — (not_le.mpr hlt) h — and absurd is the readable spelling.

The second theorem in that block is the one to remember:

theorem anything_from_contradiction (n : ℕ) (h : 0 < n) (h' : n = 0) : 1 = 2

From contradictory hypotheses, anything follows — absurd : p → ¬p → q, with q arbitrary. A formalization whose hypotheses cannot all hold is provable and says nothing whatsoever. This is not a hypothetical failure mode; it is the single most common way an autoformalized theorem is wrong while being green in the editor, and chapter 5 turns it into a checklist item.

The proof is one application of absurd with a two-tactic script inside it, and the script is where the two hypotheses are brought into collision.

1. absurd h …

   Take p := 0 < n, which h proves, and q := (1 = 2), which is the goal — q is unconstrained, so the conclusion never has to be looked at. What is still owed is a proof of ¬ (0 < n), and that is the bracket.

2. rw [h']

   The second hypothesis h' : n = 0 is the other half of the contradiction. Rewriting with it inside the goal ¬ (0 < n) replaces n by 0, so what has to be denied is now a closed arithmetic statement rather than one about an unknown n.

   Goal

   n : ℕ
   h : 0 < n
   h' : n = 0
   ⊢ ¬0 < 0

3. exact lt_irrefl 0

   lt_irrefl a : ¬ (a < a) is irreflexivity of <, and at a := 0 it is literally the goal. Note where the work happened: nothing about 1 = 2 was ever proved, and nothing could be — the theorem is true only because its hypotheses are jointly impossible.

↔

theorem nonneg_iff_zero_le (x : ℝ) : 0 ≤ x ↔ ¬ (x < 0) :=
  Iff.intro (fun h => not_lt.mpr h) (fun h => not_lt.mp h)

theorem use_iff (x : ℝ) (h : 0 ≤ x) : ¬ (x < 0) :=
  (nonneg_iff_zero_le x).mp h

p ↔ q is a structure with two fields, the two implications. .mp is left-to-right (modus ponens), .mpr is right-to-left (reverse). You will use these constantly, because a large fraction of Mathlib’s usable content is stated as ↔ — sub_eq_zero, not_lt, div_lt_one, Nat.cast_ne_zero — and picking the right projection is half of applying it.

Which projection you want is decided by the goal, not by the lemma. Both directions of nonneg_iff_zero_le are one use of the same Mathlib ↔, read in opposite directions.

1. Iff.intro (fun h => …) (fun h => …)

   Iff.intro is the anonymous constructor under its own name: the first argument is the forward implication 0 ≤ x → ¬ (x < 0), the second the backward one. ⟨_, _⟩ would have built the same term.

2. fun h => not_lt.mpr h

   not_lt states ¬ (a < b) ↔ b ≤ a. The forward direction has to produce ¬ (x < 0) from h : 0 ≤ x, so instantiate the lemma at a := x, b := 0, where it reads ¬ (x < 0) ↔ 0 ≤ x. The proposition we have sits on the right and the one we want on the left, which is what .mpr is for.

3. fun h => not_lt.mp h

   The backward direction is the same instance of the same lemma with the two sides swapping roles, so it is .mp. This is why an ↔ in Mathlib is worth twice what an implication is: one lemma, both directions, and the only thing to get right is which projection turns what you have into what you want.

use_iff then shows the same lemma being used rather than proved: (nonneg_iff_zero_le x).mp h supplies the explicit argument x, so that the ↔ is about this particular real number, and projects out the direction that takes h : 0 ≤ x to the conclusion.

Implicit and instance arguments

Three kinds of brackets appear in a Lean signature, and the difference is who supplies the argument.

theorem first_eq_first {α : Type} {n : ℕ} (y : Fin (n + 1) → α) : y 0 = y 0 := rfl

#check @first_eq_first
#check @add_comm

(x : ℝ) is explicit: you write it. {α : Type} is implicit: Lean works it out from the other arguments, which is why you write first_eq_first y and never mention α or n. @ makes every implicit argument explicit again, and #check @some_lemma is the fastest way to see what a Mathlib lemma really takes — worth doing before every use of a lemma you have not used before.

def totalOver {M : Type} [AddCommMonoid M] (y : Fin 3 → M) : M := y 0 + y 1 + y 2

#eval totalOver (![1, 2, 3] : Fin 3 → ℕ)
#check @totalOver

[AddCommMonoid M] is an instance argument, filled by a search over a database of registered instances. This is how one ∑ works for ℕ, ℝ, matrices and functions at once: the notation is defined for any type with a registered commutative addition, and Lean finds the registration.

Exercises

Every exercise below is a statement with its proof replaced by sorry. Do them in term mode, with at most a by norm_num tucked inside a bracket, because the point is to feel that a proof is a term you build rather than a sequence of commands you run. Tactics are chapter 2.

def effect (y1 y0 : Fin 2 → ℚ) (i : Fin 2) : ℚ := y1 i - y0 i

theorem ex_effect_apply (y1 y0 : Fin 2 → ℚ) : effect y1 y0 1 = y1 1 - y0 1 :=
  sorry

def effect (y1 y0 : Fin 2 → ℚ) (i : Fin 2) : ℚ := y1 i - y0 i

theorem ex_effect_apply (y1 y0 : Fin 2 → ℚ) : effect y1 y0 1 = y1 1 - y0 1 :=
  rfl

theorem ex_and_comm (y1 y0 : Fin 2 → ℝ) (h : y0 0 ≤ y1 0 ∧ y0 1 ≤ y1 1) :
    y0 1 ≤ y1 1 ∧ y0 0 ≤ y1 0 :=
  sorry

theorem ex_and_comm (y1 y0 : Fin 2 → ℝ) (h : y0 0 ≤ y1 0 ∧ y0 1 ≤ y1 1) :
    y0 1 ≤ y1 1 ∧ y0 0 ≤ y1 0 :=
  ⟨h.2, h.1⟩

theorem ex_exists_effect :
    ∃ i : Fin 3, (![1, 5, 2] : Fin 3 → ℚ) i - (![1, 3, 2] : Fin 3 → ℚ) i = 2 :=
  sorry

theorem ex_exists_effect :
    ∃ i : Fin 3, (![1, 5, 2] : Fin 3 → ℚ) i - (![1, 3, 2] : Fin 3 → ℚ) i = 2 :=
  ⟨1, by norm_num⟩

theorem ex_constant_effect (y1 y0 : Fin 3 → ℝ) (c : ℝ) (h : ∀ i, y1 i - y0 i = c) :
    y1 0 - y0 0 = y1 1 - y0 1 :=
  sorry

theorem ex_constant_effect (y1 y0 : Fin 3 → ℝ) (c : ℝ) (h : ∀ i, y1 i - y0 i = c) :
    y1 0 - y0 0 = y1 1 - y0 1 :=
  (h 0).trans (h 1).symm

theorem ex_obs_nonneg (yobs y1 y0 : ℝ) (h1 : 0 ≤ y1) (h0 : 0 ≤ y0)
    (h : yobs = y1 ∨ yobs = y0) : 0 ≤ yobs :=
  sorry

theorem ex_obs_nonneg (yobs y1 y0 : ℝ) (h1 : 0 ≤ y1) (h0 : 0 ≤ y0)
    (h : yobs = y1 ∨ yobs = y0) : 0 ≤ yobs :=
  Or.elim h (fun e => e ▸ h1) (fun e => e ▸ h0)

theorem ex_error_iff (est tau : ℝ) : est = tau ↔ est - tau = 0 :=
  sorry

theorem ex_error_iff (est tau : ℝ) : est = tau ↔ est - tau = 0 :=
  Iff.intro (fun h => by rw [h, sub_self]) (fun h => sub_eq_zero.mp h)

theorem ex_curry (p q r : Prop) : (p → q → r) → (p ∧ q → r) :=
  sorry

theorem ex_curry (p q r : Prop) : (p → q → r) → (p ∧ q → r) :=
  fun f h => f h.1 h.2

theorem ex_not_not (p : Prop) : p → ¬ ¬ p :=
  sorry

theorem ex_not_not (p : Prop) : p → ¬ ¬ p :=
  fun hp hnp => hnp hp

Reading autoformalized Lean

Two failures you can already diagnose, with nothing in them but this chapter.

Both failures share a shape, and it is the shape to look for: the statement is true, and the truth has nothing to do with the mathematics you asked about. Lean will not warn you, because there is nothing wrong. The only defense is reading the statement, which is why this chapter came before the one on how to prove things.

Next: the goal state, and the tactics that move it.