Notes on Lean

Logic🔗

Proving a proposition in Lean amounts to constructing an expression whose type is that proposition. This is a manifestation of the Curry–Howard correspondence. More explicitly, the correspondence can be summarized by the following encoding of concepts from first-order logic:

Formation🔗

Proposition True is defined as an inductive type with a single constructor that takes no arguments.

inductive True : Prop
number of parameters: 0
constructors:
True.intro : True#print True

It can be defined as follows.

inductive True' : Prop where
  | intro : True'

Proposition False is defined as an inductive type without constructors.

inductive False : Prop
number of parameters: 0
constructors:#print False

inductive False' : Prop

Compound propositions in propositional calculus are formed by using the logical connectives: conjunction, disjunction, implication, biconditional, and negation. Recall that implication is encoded as a function type. Negation is a function

def Not : Prop → Prop :=
fun a ↦ a → False#print Not

def Not' (p : Prop) := p → False'

The remaining connectives are encoded as inductive types.

structure And (a b : Prop) : Prop
number of parameters: 2
fields:
  And.left : a
  And.right : b
constructor:
  And.intro {a b : Prop} (left : a) (right : b) : a ∧ b#print And
inductive Or : Prop → Prop → Prop
number of parameters: 2
constructors:
Or.inl : ∀ {a b : Prop}, a → a ∨ b
Or.inr : ∀ {a b : Prop}, b → a ∨ b#print Or
structure Iff (a b : Prop) : Prop
number of parameters: 2
fields:
  Iff.mp : a → b
  Iff.mpr : b → a
constructor:
  Iff.intro {a b : Prop} (mp : a → b) (mpr : b → a) : a ↔ b#print Iff

inductive And' (p q : Prop) : Prop where
  | intro (left : p) (right : q) : And' p q

inductive Or' (p q : Prop) : Prop where
  | inl (h : p) : Or' p q
  | inr (h : q) : Or' p q

inductive Iff' (p q : Prop) : Prop where
  | intro (mp : p → q) (mpr : q → p) : Iff' p q

Moreover, existential quantification is encoded as an inductive type.[…]This is an example of a dependent sum type.

inductive Exists.{u} : {α : Sort u} → (α → Prop) → Prop
number of parameters: 2
constructors:
Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p#print Exists

inductive Exists' {α : Sort u} (P : α → Prop) : Prop where
  | intro (a : α) (h : P a) : Exists' P

The following syntactic sugar is available for the standard versions.

example : ⊤ = True := rfl

example : ⊥ = False := rfl

example (p : Prop) : (¬p) = Not p := rfl

example (p q : Prop) : (p ∧ q) = And p q := rfl

example (p q : Prop) : (p ∨ q) = Or p q := rfl

example (p q : Prop) : (p ↔ q) = Iff p q := rfl

example (α : Sort u) (P : α → Prop) :
  (∃ a : α, P a) = Exists P := rfl

Introduction🔗

The proposition True' can be proven by the constructor.[…]Recall the anonymous constructor syntax.

example : True' := True'.intro
example : True' := ⟨⟩

The following notation is provided for the standard version.

example : trivial = True.intro := rfl

Since False' has no constructors, there are no expressions of type False'. It becomes meaningful via negation.

example : (Not' False') = (False' → False') := rfl

The function type α → α is inhabited for any type α by the identity function id. In particular, id proves Not' False'.

example : Not' False' := id

example (α : Sort u) : id = λ x : α ↦ x := rfl

The constructors of And', Or', and Iff' encode conjunction, disjunction, and biconditional introductions.

example (p q : Prop) (hl : p) (hr : q) : And' p q
  := ⟨hl, hr⟩

example (p q : Prop) (h : p) : Or' p q := Or'.inl h
example (p q : Prop) (h : q) : Or' p q := Or'.inr h

example (p q : Prop) (hl : p → q) (hr : q → p) : Iff' p q
  := ⟨hl, hr⟩

Moreover, the constructor of Exists' encodes existential generalization. We give two formulations.

example (α : Sort u) (P : α → Prop) (a : α)
  (h : P a) : Exists' P
:= Exists'.intro a h

example (α : Sort u) (P : α → Prop) (a : α)
  (h : P a) : Exists' P
:= ⟨a, h⟩

Elimination🔗

Propositions are subject to restricted elimination: they can be eliminated only into expressions of type Prop unless they have at most one constructor, whose arguments have type Prop or are shared with the type constructor.[…]For our immediate purposes, the only relevant shared arguments are parameters. The third argument of the type constructor of Acc illustrates the general case. This argument is shared with the only type constructor but it cannot be promoted to a parameter due to not satisfying the uniformity requirement. In contrast, constructorless inductive types, including False', can be eliminated into anything.

Principle of explosion🔗

Both False and False' are uninhabited, that is, there are no expressions of either type. Uninhabited propositions encode contradictions. From a contradiction, any proposition can be derived by the principle of explosion. The recursor False.rec encodes the principle of explosion.

recursor False.rec.{u} : (motive : False → Sort u) → (t : False) → motive t
number of parameters: 0
number of indices: 0
number of motives: 1
number of minors: 0
rules:#print False.rec

example : False → False' := False.rec

The arguments of the recursor are implicit, and Lean infers them from the context. The type of @False.rec is

example :
  (motive : False → Sort u) /- motive -/ →
  (h : False) /- major premise -/ →
  motive h /- codomain -/
:= @False.rec

and an explicit version of the above proof reads

example : False → False' := @False.rec λ _ ↦ False'

Here @False.rec is evaluated partially, and the only argument λ _ ↦ False' is the motive. The proof works, since the partially applied function has the domain False, given by major premise, and since its codomain motive h is False',

example (h : False) :
  let motive := λ _ ↦ False'
  False' = motive h := rfl

Recall that pattern matching is implemented using recursors. The nomatch expression is a pattern match with zero cases, and nofun is shorthand for a function that applies nomatch to its arguments. 

example : False → False' := λ h ↦ nomatch h
example : False → False' := nofun

The principle of explosion applies starting from False' as well.

example : False' → False := False'.rec
example : False' → False := nofun

Conjunction elimination🔗

Deconstruction via pattern matching enables proofs of statements involving compound hypotheses. We illustrate conjunction elimination.

example (p q : Prop) (h : And' p q) : p
:=
  match h with
  | And'.intro hp _ => hp

This is just the projection associated to the first field of And'.[…]Recall that we considered the analogous projection for Prod' earlier. Here are two alternative proofs.

example (p q : Prop) (h : And' p q) : p
:=
  let ⟨hp, _⟩ := h
  hp

example (p q : Prop) (h : And' p q) : p
:=
  let ⟨_, _⟩ := h
  ‹p›

Here is a proof that bypasses the user-facing surface syntax and employs the recursor And'.rec directly.

example (p q : Prop) (h : And' p q) : p
:= And'.rec (λ hp _ ↦ hp) h

Let us write this proof more explicitly. The recursor of And' has the type

example :
  (p q : Prop) /- parameters -/ →
  {motive : And' p q → Sort u} /- motive -/ →

  -- minor premises:
  ((hl : p) → (hr : q) → motive (And'.intro hl hr)) →

  (h : And' p q) /- major premise -/ →
  motive h /- codomain -/
:= @And'.rec

The minor premise corresponds to the only constructor intro. The explicit proof

example (p q : Prop) (h : And' p q) : p
:= @And'.rec
  p q /- parameters -/
  (λ _ ↦ p) /- motive -/
  (λ hp _ ↦ hp) /- minor premise -/
  h /- major premise -/

works, since the codomain motive h is p,

example (p q : Prop) (h : And' p q) :
  let motive := λ _ ↦ p
  p = motive h := rfl

and since λ hp _ ↦ hp has the type p → q → p of the minor premise,

example (p q : Prop) (h : And' p q) :
  let motive := λ _ ↦ p
  ((hl : p) → (hr : q) → motive (And'.intro hl hr)) :=
    λ hp _ ↦ hp

example (p q : Prop) (h : And' p q) :
  let motive := λ _ ↦ p
  ((hl : p) → (hr : q) → motive (And'.intro hl hr))
    = (p → q → p)
:= rfl

The standard And is a structure with fields left and right.

example (h : p ∧ q) : p := h.left

Commutativity of disjunction🔗

Let us now turn to disjunction and consider its commutativity. Deconstruction of a disjunctive hypothesis results in two cases. We give two formulations.

example (h : Or' p q) : Or' q p
:=
  match h with
  | Or'.inl hp => Or'.inr hp
  | Or'.inr hq => Or'.inl hq

example (h : Or' p q) : Or' q p
:=
  match h with
  | Or'.inl _ => Or'.inr ‹p›
  | Or'.inr _ => Or'.inl ‹q›

This is a proof by case analysis: h was either constructed with inl or with inr. In the former case, we construct a new Or' expression using inr, and in the latter case inl is used. In other words, we swap the roles of inl and inr.

Here is a proof that uses the recursor Or'.rec directly.

example (p q : Prop) (h : Or' p q) : Or' q p
:= Or'.rec
  (λ hp ↦ Or'.inr hp)
  (λ hq ↦ Or'.inl hq)
  h

An explicit version reads

example :
  (p q : Prop) /- parameters -/ →
  (motive : Or' p q → Prop) /- motive -/ →

  -- minor premises:
  ((h : p) → motive (Or'.inl h)) /- inl -/ →
  ((h : q) → motive (Or'.inr h)) /- inr -/ →

  (h : Or' p q) /- major premise -/ →
  motive h /- codomain -/
:= @Or'.rec


example (p q : Prop) (h : Or' p q) : Or' q p
:= @Or'.rec
  p q /- parameters -/
  (λ _ ↦ Or' q p) /- motive -/

  -- minor premises:
  (λ hp ↦ Or'.inr hp) /- inl -/
  (λ hq ↦ Or'.inl hq) /- inr -/

  h /- major premise -/

The proof works since the codomain motive h is Or' q p,

example (p q : Prop) (h : Or' p q) :
  let motive := λ _ ↦ Or' q p
  Or' q p = motive h := rfl

and since λ hp ↦ Or'.inr hp and λ hq ↦ Or'.inl hq have the types of the minor premises associated to inl and inr, respectively. Indeed,

example (p q : Prop) (h : Or' p q) :
  let motive := λ (_ : Or' p q) ↦ Or' q p
  ((h : p) → motive (Or'.inl h)) := λ hp ↦ Or'.inr hp

example (p q : Prop) (h : Or' p q) :
  let motive := λ (_ : Or' p q) ↦ Or' q p
  ((h : q) → motive (Or'.inr h)) := λ hq ↦ Or'.inl hq

Here

example (p q : Prop) (h : Or' p q) :
  let motive := λ (_ : Or' p q) ↦ Or' q p
  ((h : p) → motive (Or'.inl h)) = (p → Or' q p) := rfl

example (p q : Prop) (h : Or' p q) :
  let motive := λ (_ : Or' p q) ↦ Or' q p
  ((h : q) → motive (Or'.inr h)) = (q → Or' q p) := rfl

Restricted elimination🔗

Inspecting the type of Or.rec, we see that Or.rec differs from all other recursors we have seen so far in that its motive's codomain is not an arbitrary universe Sort u but Prop. This is a manifestation of restricted elimination.

Restricted elimination can be understood as the flipside of proof irrelevance. Indeed, without such restriction, proof irrelevance would lead to inconsistency via

example (p : Prop) (proof₁ proof₂ : p) (f : p → Sort u)
  : f proof₁ = f proof₂
:= rfl

For instance, True ∨ True admits two proofs using distinct constructors

def proof₁ : True ∨ True := Or.inl trivial
def proof₂ : True ∨ True := Or.inr trivial

These proofs are definitionally equal. Consequently,

example (f : True ∨ True → Sort u) : f proof₁ = f proof₂
:= rfl

The following function violates restricted elimination.

def bad (h : True ∨ True) := Tactic `cases` failed with a nested error:
Tactic `induction` failed: recursor `Or.casesOn` can only eliminate into `Prop`

motive:True ∨ True → Sort ?u.224h_1:(h : True) → motive ⋯h_2:(h : True) → motive ⋯h✝:True ∨ True⊢ motive h✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nilmatch h with
  | Or.inl _ => 0
  | Or.inr _ => 1

If it were allowed, then taking bad as f in the above example would lead to 0 = 1.

Existential instantiation🔗

Deconstruction enables existential instantiation. We give three formulations.

example (q : Prop) (α : Sort u) (P : α → Prop)
  (h1 : Exists' P) (h2 : ∀ a : α, P a → q) : q
:=
  let ⟨a, h⟩ := h1
  h2 a h

example (q : Prop) (α : Sort u) (P : α → Prop)
  (h1 : Exists' P) (h2 : ∀ a : α, P a → q) : q
:=
  match h1 with
  | Exists'.intro a h => h2 a h

example (q : Prop) (α : Sort u) (P : α → Prop)
  (h1 : Exists' P) (h2 : ∀ a : α, P a → q) : q
:=
  Exists'.rec (λ a h ↦ h2 a h) h1

Propositions of form Exists' p can be eliminated only into expressions of type Prop, as seen from the motive in

recursor Exists'.rec.{u} : ∀ {α : Sort u} {P : α → Prop} {motive : Exists' P → Prop},
  (∀ (a : α) (h : P a), motive ⋯) → ∀ (t : Exists' P), motive t
number of parameters: 2
number of indices: 0
number of motives: 1
number of minors: 1
rules:
for Exists'.intro (2 fields): fun {α} P motive intro a h ↦ intro a h#print Exists'.rec

The field a : α of Exists'.intro does not have type Prop and is not shared with the type constructor.

Equality🔗

Two propositions are equal if and only if they are equivalent. The implication from equality to equivalence can be proven using the substitution principle for equality. We return to this principle.

example (p q : Prop) (h : p = q) : p ↔ q :=
  have : p ↔ p := ⟨id, id⟩
  Eq.subst h this

The opposite implication is an axiom. Axioms are propositions postulated without proof. The kernel postulates a small number of axioms including propext. We return to axioms in general.

axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b#print propext

example (p q : Prop) (h : p ↔ q) : p = q := propext h