Notes on Lean

Equality🔗

First-order logic with equality imposes two axioms, reflexivity and substitution principle, on equality.[…]Substitution principle is also called Leibniz's law. These two axioms imply its remaining basic properties, including symmetry and transitivity. In Lean, reflexivity is the most fundamental property, as it is an interface to definitional equality.

The basic properties alone do not guarantee that equality is non-vacuous. When equality is considered on a fixed type, the basic properties may hold simply because all pairs of expressions of that type are equal. In Lean, equality is non-vacuous on most types.[…]Prop is a type on which equality is vacuous. This is stating the proof irrelevance.

In fact, an inductive type can be viewed as being freely generated by its constructors in the sense of constructor distinctness and injectivity. The former states that applications of distinct constructors are not equal, while the latter states that applications of the same constructor at distinct arguments are not equal.

The proofs of constructor distinctness and injectivity use the recursor of the inductive type together with the basic properties of equality.

Definitional equality and reflexivity🔗

We have made extensive use of rfl, which is simply the constructor Eq.refl of Eq, with both the arguments implicit. It proves reflexivity of equality.

def rfl.{u} : ∀ {α : Sort u} {a : α}, a = a :=
fun {α} {a} => Eq.refl a#print rfl

example : @rfl = @Eq.refl := rfl

example (α : Sort u) (a : α) : a = a := rfl

The applicability of rfl as a proof is entirely determined by the definitional equality implemented by the kernel. To demonstrate this, we define our own versions Eq and rfl.

inductive Eq' {α : Sort u} (a : α) : α → Prop where
  | refl : Eq' a a

def rfl' {α : Sort u} {a : α} := @Eq'.refl α a

These behave identically to Eq and rfl as far as definitional equality is concerned:

  1. Proof irrelevance

example
  (p : Prop) (proof₁ proof₂ : p) : Eq' proof₁ proof₂
:= rfl'

  1. Function \eta-equivalence

example
  (α : Sort u) (β : Sort v) (f : α → β) : Eq' (λ x ↦ f x) f
:= rfl'

  1. Structure \eta-equivalence

example
  (α : Type u) (β : Type v) (x : α × β)
  : Eq' ⟨x.1, x.2⟩  x
:= rfl'

  1. \beta-, \delta-, and \zeta-reductions

example
  (α : Sort u) (β : Sort v) (f : α → β) (a : α)
  : Eq' ((λ x ↦ f x) a) (f a)
:= rfl'

def ℕ_to_ℕ := ℕ → ℕ
example : Eq' ℕ_to_ℕ (ℕ → ℕ) := rfl'

example : Eq' (let t := ℕ; t → t) (ℕ → ℕ) := rfl'

  1. \iota-reduction

example (n : ℕ) :
  Eq' (@Nat.rec (λ _ ↦ ℕ) 0 (λ m _ ↦ m) (Nat.succ n)) n
:= rfl'

Moreover, the kernel performs reductions of different kinds until the normal form is obtained.

example (n : ℕ) :
  let pred (n : ℕ) := n - 1
  Eq' (pred (Nat.succ n)) n
:= rfl'

Of course, Eq' and rfl' also tell apart expressions that are not definitionally equal.

example : Eq' 0 1 := Type mismatch
  rfl'
has type
  Eq' ?m.8 ?m.8
but is expected to have type
  Eq' 0 1rfl'

Substitution principle🔗

Substitution principle is formulated as follows: if a = b and P a holds for a predicate P, then P b holds. We can prove it using the recursor

example :
  (α : Sort u) → (a : α) /- parameters -/ →
  (motive : (x : α) → a = x → Sort v) /- motive -/ →
  motive a (Eq.refl a) /- minor premise -/ →
  (b : α) /- index -/ →
  (h1 : a = b) /- major premise -/ →
  motive b h1 /- codomain -/
:= @Eq.rec

example
  (α : Sort u) (P : α → Prop) (a b : α)
  (h1 : a = b) (h2 : P a)
  : P b
:= @Eq.rec
  α a /- parameters -/
  (λ x _ ↦ P x) /- motive -/
  h2 /- minor premise -/
  b /- index -/
  h1 /- major premise -/

The proof works, since the codomain motive b h1 is P b,

example (α : Sort u) (P : α → Prop) (a b : α) (h1 : a = b) :
  let motive := (λ x _ ↦ P x)
  P b = motive b h1 := rfl

and since h2 has the type of the minor premise,

example (α : Sort u) (P : α → Prop) (a b : α) (h2 : P a) :
  let motive := (λ x _ ↦ P x)
  motive a (Eq.refl a) := h2

This type is simply the proposition P a,

example (α : Sort u) (P : α → Prop) (a b : α) (h2 : P a) :
  let motive := (λ x _ ↦ P x)
  motive a (Eq.refl a) = P a := rfl

A short proof is obtained by letting Lean infer all implicit arguments.

example
  (α : Sort u) (P : α → Prop) (a b : α)
  (h1 : a = b) (h2 : P a)
  : P b
:= Eq.rec h2 h1

Proofs by pattern matching are translated to a similar use of Eq.rec as above.[…]We could replace rfl on the left of => with Eq.refl _. Using rfl avoids having to ignore the explicit parameter of Eq.refl.

example
  (α : Sort u) (P : α → Prop) (a b : α)
  (h1 : a = b) (h2 : P a)
  : P b
:=
  match h1 with
  | rfl => h2

Substitution principle is available as a theorem, with the predicate as an implicit parameter called motive, in line with Eq.rec.

example
  (α : Sort u) (P : α → Prop) (a b : α)
  (h1 : a = b) (h2 : P a)
  : P b
:= Eq.subst h1 h2

Named arguments allow specifying implicit parameters explicitly. 

example
  (α : Sort u) (P : α → Prop) (a b : α)
  (h1 : a = b) (h2 : P a)
  : P b
:= Eq.subst (motive := P) h1 h2

Basic properties of equality🔗

Equality is an equivalence relation, namely it is

  • reflexive: a = a for all a,

  • symmetric: if a = b then b = a for all a and b, and

  • transitive: if a = b and b = c then a = c for all a, b, and c.

With reflexivity already established, it remains to prove symmetry and transitivity.

example (α : Sort u) (a b : α) (h : a = b) : b = a
:= Eq.subst (motive := λ x ↦ x = a) h rfl

example (α : Sort u) (a b c : α) (h1 : a = b) (h2 : b = c)
  : a = c
:= Eq.subst h2 h1

In Lean, the following substitution is called congruence: if a = b and f is a function, then f a = f b.

example
  (α : Sort u) (β : Sort v) (a b : α) (f : α → β)
  (h : a = b)
  : f a = f b
:= Eq.subst (motive := λ x ↦ f a = f x) h rfl

Symmetry, transitivity, and congruence are available as theorems.

example (α : Sort u) (a b : α) (h : a = b) : b = a
:= Eq.symm h

example
  (α : Sort u) (a b c : α) (h1 : a = b) (h2 : b = c)
  : a = c
:= Eq.trans h1 h2

example
  (α : Sort u) (β : Sort v) (a b : α) (f : α → β)
  (h : a = b)
  : f a = f b
:= congrArg f h

Constructor distinctness🔗

Expressions given by distinct constructors of an inductive type are not equal. This constructor distinctness can be proven using the substitution principle. As an illustration, we show that 0 = n + 1 leads to a contradiction by applying the substitution principle to the predicate

def P (n : ℕ) : Prop
:=
  match n with
  | 0 => True
  | m + 1 => False

Indeed,

example (n : ℕ) (h : 0 = n + 1) : False :=
  let : P 0 := trivial
  Eq.subst h this

Recall that ¬ is syntactic sugar. Additional syntactic sugar is provided.

example (n : ℕ) :
  (¬(0 = n + 1)) = (0 = n + 1 → False)
:= rfl

example(n : ℕ) : (0 ≠ n + 1) = (0 = n + 1 → False) := rfl

Here is a reformulation of the above contradiction, with a proof that uses Nat.rec directly.

example (n : ℕ) : 0 ≠ n + 1
:=
  λ h : 0 = n + 1 ↦
  let P : ℕ → Prop := Nat.rec True (λ _ _ ↦ False)
  have : P 0 := trivial
  Eq.subst h this

Here is a proof by pattern matching.

example (n : ℕ) : 0 ≠ n + 1 := nofun

Constructor injectivity🔗

Applications of a constructor at distinct arguments are not equal. Equivalently, constructor injectivity holds: if two constructor applications are equal, then the arguments are equal as well. This can be proven using deconstruction together with congruence and transitivity.

example (n m : ℕ) (h : Nat.succ n = Nat.succ m) : n = m
:=
  let pred : Nat → Nat := Nat.rec 0 (λ k _ ↦ k)
  have hpp : pred (Nat.succ n) = pred (Nat.succ m)
    := congrArg pred h
  have hnp : n = pred (Nat.succ n) := rfl
  have hpm : pred (Nat.succ m) = m := rfl
  Eq.trans hnp (Eq.trans hpp hpm)

The keyword calc provides surface syntax for step-wise reasoning over transitive relations.[…]We use also a shorthand notation for pattern matching.

example (n m : ℕ) (h : Nat.succ n = Nat.succ m) : n = m
:=
  let pred
  | 0 => 0
  | x + 1 => x
  calc
    n = pred (Nat.succ n) := rfl
    _ = pred (Nat.succ m) := congrArg pred h
    _ = m := rfl

Lean generates an injectivity theorem for each constructor taking fields, unless those fields appear in the constructor's codomain.

example (n m : ℕ) (h : Nat.succ n = Nat.succ m) : n = m
:= Nat.succ.inj h

inductive Nat' : Type where
  | zero : Nat'
  | succ : Nat' → Nat'

example (n m : Nat') (h : Nat'.succ n = Nat'.succ m) : n = m
:= Nat'.succ.inj h

For constructors with multiple arguments, injectivity yields equalities for each argument.

example
  (α : Type u) (β : Type v) (pair₁ pair₂ : α × β)
  (h : pair₁ = pair₂)
  : pair₁.fst = pair₂.fst ∧ pair₁.snd = pair₂.snd
:= Prod.mk.inj h

No injectivity theorem is generated for Eq.refl since it has no fields.

#print Unknown constant `Eq.refl.inj`Eq.refl.inj

Further proofs🔗

We will give proofs of symmetry, transitivity, and congruence directly using Eq.rec.

Symmetry🔗

example :
  (α : Sort u) → (a : α) /- parameters -/ →
  (motive : (x : α) → a = x → Sort v) /- motive -/ →
  motive a (Eq.refl a) /- minor premise -/ →
  (b : α) /- index -/ →
  (h : a = b) /- major premise -/ →
  motive b h /- codomain -/
:= @Eq.rec

example (α : Sort u) (a b : α) (h : a = b) : b = a
:= @Eq.rec
  α a /- parameters -/
  (λ x _ ↦ x = a) /- motive -/
  rfl /- minor premise -/
  b /- index -/
  h /- major premise -/

The proof works, since the codomain motive b h is b = a,

example (α : Sort u) (a b : α) (h : a = b) :
  let motive := (λ x _ ↦ x = a)
  (b = a) = motive b h := rfl

and since rfl has the type of the minor premise,

example (α : Sort u) (a : α) :
  let motive := (λ x _ ↦ x = a)
  motive a (Eq.refl a) := rfl

This type is simply the proposition a = a,

example (α : Sort u) (a : α) :
  let motive := (λ x _ ↦ x = a)
  (a = a) = motive a (Eq.refl a) := rfl

It admits the proof rfl.

A short proof is obtained by letting Lean infer all implicit arguments.

example (α : Sort u) (a b : α) (h : a = b) : b = a
:= Eq.rec rfl h

Proofs by pattern matching are translated to a similar use of Eq.rec as above.

example (α : Sort u) (a b : α) (h : a = b) : b = a
:=
  match h with
  | rfl => rfl

Transitivity🔗

example :
  (α : Sort u) → (b : α) /- parameters -/ →
  (motive : (x : α) → b = x → Sort v) /- motive -/ →
  motive b (Eq.refl b) /- minor premise -/ →
  (c : α) /- index -/ →
  (h2 : b = c) /- major premise -/ →
  motive c h2 /- codomain -/
:= @Eq.rec

example
  (α : Sort u) (a b c : α) (h1 : a = b) (h2 : b = c)
  : a = c
:= @Eq.rec
  α b /- parameters -/
  (λ x _ ↦ a = x) /- motive -/
  h1 /- minor premise -/
  c /- index -/
  h2 /- major premise -/

The motive λ x _ ↦ a = x is different from the one in the proof of symmetry: its body is a = x while for symmetry it was x = a. The proof works, since the codomain motive c h2 is a = c,

example (α : Sort u) (a b c : α) (h2 : b = c) :
  let motive := (λ x _ ↦ a = x)
  (a = c) = motive c h2 := rfl

and since h1 : a = b has the type of the minor premise,

example (α : Sort u) (a b : α) (h1 : a = b) :
  let motive := (λ x _ ↦ a = x)
  motive b (Eq.refl b) := h1

Indeed,

example (α : Sort u) (a b : α) :
  let motive := (λ x _ ↦ a = x)
  (a = b) = motive b (Eq.refl b) := rfl

A short proof is obtained by letting Lean infer all implicit arguments.

example
  (α : Sort u) (a b c : α) (h1 : a = b) (h2 : b = c)
  : a = c
:= Eq.rec h1 h2

A proof by pattern matching is translated to a similar use of Eq.rec as above.

example
  (α : Sort u) (a b c : α) (h1 : a = b) (h2 : b = c)
  : a = c
:=
  match h2 with
  | rfl => h1

Congruence🔗

example
  (α : Sort u) (β : Sort v) (a b : α) (f : α → β)
  (h : a = b)
  : f a = f b
:= Eq.rec rfl h