Equality🔗

First-order logic with equality imposes two axiom schemas, reflexivity and substitution principle, on equality.[…]Substitution principle is also called Leibniz's law. We explain how they correspond to the introduction rule and to a special case of the elimination rule of the inductive type Eq.

Two basic facts about inductive types, constructor distinctness and injectivity, are proved using the substitution principle. We treat them in turn.

Formation🔗

Equality is encoded by the inductive type Eq.

inductive Eq.{u_1} : {α : Sort u_1} → α → α → Prop
number of parameters: 2
constructors:
Eq.refl : ∀ {α : Sort u_1} (a : α), a = a#print Eq

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

We define our own version of Eq.

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

Introduction🔗

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

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

We define our own version.

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

It proves reflexivity of equality.

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

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

The applicability of rfl as a proof is entirely determined by the definitional equality implemented by the kernel, and rfl' behaves identically to rfl with respect to all its aspects, summarized below.

Proof irrelevance

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

Function \eta-equivalence

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

Structure \eta-equivalence

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

\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'

\iota-reduction

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

Quotient reduction[…]We will return to this.

example (α : Sort u) (β : Sort v) (s : Setoid α)
  (f : α → β) (x : α)
  (h : ∀ (x y : α), x ≈ y → f x = f y)
  : Eq' (Quotient.lift f h ⟦x⟧) (f x)
:= 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'

Elimination🔗

Rather than using the recursor of Eq directly, equality is typically eliminated by using the substitution principle formulated as follows: if a = b and P a holds for a predicate P, then P b holds.[…]We could demonstrate the substitution principle just as well using our version Eq', but Eq comes with the syntactic sugar = which improves readability. 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 recursor permits any universe as the codomain of the motive, while the substitution principle is more special: it has the proposition P b as its codomain.

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.

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

Occasionally, it might be necessary to provide explicit motive. This can be done using a named argument.

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

Setting the option pp.explicit to true makes #print show all implicit arguments.

set_option pp.explicit true in
theorem Document.Equality.subst.{u} : ∀ (α : Sort u) (P : α → Prop) (a b : α), @Eq α a b → P a → P b :=
fun α P a b h1 h2 ↦ @Eq.subst α P a b h1 h2#print subst

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 two substitutions are called congruences

congruence in argument: if a = b and f is a function, then f a = f b,
congruence in function: if f = g for two functions, then f a = g a.

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

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

Symmetry, transitivity, and the two congruences 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

example
  (α : Sort u) (β : Sort v) (a : α) (f g : α → β)
  (h : f = g)
  : f a = g a
:= congrFun h a

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 :=
  have : 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

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

example
  (α : Type u) (β : Type v) (p q : α × β)
  (h : p = q)
  : p.fst = q.fst ∧ p.snd = q.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