# Axioms and Computation

We have seen that the version of the Calculus of Constructions that
has been implemented in Lean includes dependent function types,
inductive types, and a hierarchy of universes that starts with an
impredicative, proof-irrelevant `Prop`

at the bottom. In this
chapter, we consider ways of extending the CIC with additional axioms
and rules. Extending a foundational system in such a way is often
convenient; it can make it possible to prove more theorems, as well as
make it easier to prove theorems that could have been proved
otherwise. But there can be negative consequences of adding additional
axioms, consequences which may go beyond concerns about their
correctness. In particular, the use of axioms bears on the
computational content of definitions and theorems, in ways we will
explore here.

Lean is designed to support both computational and classical
reasoning. Users that are so inclined can stick to a "computationally
pure" fragment, which guarantees that closed expressions in the system
evaluate to canonical normal forms. In particular, any closed
computationally pure expression of type `Nat`

, for example, will
reduce to a numeral.

Lean's standard library defines an additional axiom, propositional
extensionality, and a quotient construction which in turn implies the
principle of function extensionality. These extensions are used, for
example, to develop theories of sets and finite sets. We will see
below that using these theorems can block evaluation in Lean's kernel,
so that closed terms of type `Nat`

no longer evaluate to numerals. But
Lean erases types and propositional information when compiling
definitions to bytecode for its virtual machine evaluator, and since
these axioms only add new propositions, they are compatible with that
computational interpretation. Even computationally inclined users may
wish to use the classical law of the excluded middle to reason about
computation. This also blocks evaluation in the kernel, but it is
compatible with compilation to bytecode.

The standard library also defines a choice principle that is entirely
antithetical to a computational interpretation, since it magically
produces "data" from a proposition asserting its existence. Its use is
essential to some classical constructions, and users can import it
when needed. But expressions that use this construction to produce
data do not have computational content, and in Lean we are required to
mark such definitions as `noncomputable`

to flag that fact.

Using a clever trick (known as Diaconescu's theorem), one can use propositional extensionality, function extensionality, and choice to derive the law of the excluded middle. As noted above, however, use of the law of the excluded middle is still compatible with bytecode compilation and code extraction, as are other classical principles, as long as they are not used to manufacture data.

To summarize, then, on top of the underlying framework of universes, dependent function types, and inductive types, the standard library adds three additional components:

- the axiom of propositional extensionality
- a quotient construction, which implies function extensionality
- a choice principle, which produces data from an existential proposition.

The first two of these block normalization within Lean, but are compatible with bytecode evaluation, whereas the third is not amenable to computational interpretation. We will spell out the details more precisely below.

## Historical and Philosophical Context

For most of its history, mathematics was essentially computational:
geometry dealt with constructions of geometric objects, algebra was
concerned with algorithmic solutions to systems of equations, and
analysis provided means to compute the future behavior of systems
evolving over time. From the proof of a theorem to the effect that
"for every `x`

, there is a `y`

such that ...", it was generally
straightforward to extract an algorithm to compute such a `y`

given
`x`

.

In the nineteenth century, however, increases in the complexity of
mathematical arguments pushed mathematicians to develop new styles of
reasoning that suppress algorithmic information and invoke
descriptions of mathematical objects that abstract away the details of
how those objects are represented. The goal was to obtain a powerful
"conceptual" understanding without getting bogged down in
computational details, but this had the effect of admitting
mathematical theorems that are simply *false* on a direct
computational reading.

There is still fairly uniform agreement today that computation is
important to mathematics. But there are different views as to how best
to address computational concerns. From a *constructive* point of
view, it is a mistake to separate mathematics from its computational
roots; every meaningful mathematical theorem should have a direct
computational interpretation. From a *classical* point of view, it is
more fruitful to maintain a separation of concerns: we can use one
language and body of methods to write computer programs, while
maintaining the freedom to use nonconstructive theories and methods
to reason about them. Lean is designed to support both of these
approaches. Core parts of the library are developed constructively,
but the system also provides support for carrying out classical
mathematical reasoning.

Computationally, the purest part of dependent type theory avoids the
use of `Prop`

entirely. Inductive types and dependent function types
can be viewed as data types, and terms of these types can be
"evaluated" by applying reduction rules until no more rules can be
applied. In principle, any closed term (that is, term with no free
variables) of type `Nat`

should evaluate to a numeral, `succ (... (succ zero)...)`

.

Introducing a proof-irrelevant `Prop`

and marking theorems
irreducible represents a first step towards separation of
concerns. The intention is that elements of a type `p : Prop`

should
play no role in computation, and so the particular construction of a
term `t : p`

is "irrelevant" in that sense. One can still define
computational objects that incorporate elements of type `Prop`

; the
point is that these elements can help us reason about the effects of
the computation, but can be ignored when we extract "code" from the
term. Elements of type `Prop`

are not entirely innocuous,
however. They include equations `s = t : α`

for any type `α`

, and
such equations can be used as casts, to type check terms. Below, we
will see examples of how such casts can block computation in the
system. However, computation is still possible under an evaluation
scheme that erases propositional content, ignores intermediate typing
constraints, and reduces terms until they reach a normal form. This is
precisely what Lean's virtual machine does.

Having adopted a proof-irrelevant `Prop`

, one might consider it
legitimate to use, for example, the law of the excluded middle,
`p ∨ ¬p`

, where `p`

is any proposition. Of course, this, too, can block
computation according to the rules of CIC, but it does not block
bytecode evaluation, as described above. It is only the choice
principles discussed in :numref:`choice`

that completely erase the
distinction between the proof-irrelevant and data-relevant parts of
the theory.

## Propositional Extensionality

Propositional extensionality is the following axiom:

```
namespace Hidden
axiom propext {a b : Prop} : (a ↔ b) → a = b
end Hidden
```

It asserts that when two propositions imply one another, they are
actually equal. This is consistent with set-theoretic interpretations
in which any element `a : Prop`

is either empty or the singleton set
`{*}`

, for some distinguished element `*`

. The axiom has the
effect that equivalent propositions can be substituted for one another
in any context:

```
theorem thm₁ (a b c d e : Prop) (h : a ↔ b) : (c ∧ a ∧ d → e) ↔ (c ∧ b ∧ d → e) :=
propext h ▸ Iff.refl _
theorem thm₂ (a b : Prop) (p : Prop → Prop) (h : a ↔ b) (h₁ : p a) : p b :=
propext h ▸ h₁
```

## Function Extensionality

Similar to propositional extensionality, function extensionality
asserts that any two functions of type `(x : α) → β x`

that agree on
all their inputs are equal:

```
universe u v
#check (@funext :
{α : Type u}
→ {β : α → Type u}
→ {f g : (x : α) → β x}
→ (∀ (x : α), f x = g x)
→ f = g)
#print funext
```

From a classical, set-theoretic perspective, this is exactly what it means for two functions to be equal. This is known as an "extensional" view of functions. From a constructive perspective, however, it is sometimes more natural to think of functions as algorithms, or computer programs, that are presented in some explicit way. It is certainly the case that two computer programs can compute the same answer for every input despite the fact that they are syntactically quite different. In much the same way, you might want to maintain a view of functions that does not force you to identify two functions that have the same input / output behavior. This is known as an "intensional" view of functions.

In fact, function extensionality follows from the existence of
quotients, which we describe in the next section. In the Lean standard
library, therefore, `funext`

is thus
proved from the quotient construction.

Suppose that for `α : Type`

we define the `Set α := α → Prop`

to
denote the type of subsets of `α`

, essentially identifying subsets
with predicates. By combining `funext`

and `propext`

, we obtain an
extensional theory of such sets:

```
def Set (α : Type u) := α → Prop
namespace Set
def mem (x : α) (a : Set α) := a x
infix:50 (priority := high) "∈" => mem
theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x => propext (h x))
end Set
```

We can then proceed to define the empty set and set intersection, for example, and prove set identities:

```
def Set (α : Type u) := α → Prop
namespace Set
def mem (x : α) (a : Set α) := a x
infix:50 (priority := high) "∈" => mem
theorem setext {a b : Set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (fun x => propext (h x))
def empty : Set α := fun x => False
notation (priority := high) "∅" => empty
def inter (a b : Set α) : Set α :=
fun x => x ∈ a ∧ x ∈ b
infix:70 " ∩ " => inter
theorem inter_self (a : Set α) : a ∩ a = a :=
setext fun x => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => ⟨h, h⟩)
theorem inter_empty (a : Set α) : a ∩ ∅ = ∅ :=
setext fun x => Iff.intro
(fun ⟨_, h⟩ => h)
(fun h => False.elim h)
theorem empty_inter (a : Set α) : ∅ ∩ a = ∅ :=
setext fun x => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => False.elim h)
theorem inter.comm (a b : Set α) : a ∩ b = b ∩ a :=
setext fun x => Iff.intro
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
end Set
```

The following is an example of how function extensionality blocks computation inside the Lean kernel:

```
def f (x : Nat) := x
def g (x : Nat) := 0 + x
theorem f_eq_g : f = g :=
funext fun x => (Nat.zero_add x).symm
def val : Nat :=
Eq.recOn (motive := fun _ _ => Nat) f_eq_g 0
-- does not reduce to 0
#reduce val
-- evaluates to 0
#eval val
```

First, we show that the two functions `f`

and `g`

are equal using
function extensionality, and then we cast `0`

of type `Nat`

by
replacing `f`

by `g`

in the type. Of course, the cast is
vacuous, because `Nat`

does not depend on `f`

. But that is enough
to do the damage: under the computational rules of the system, we now
have a closed term of `Nat`

that does not reduce to a numeral. In this
case, we may be tempted to reduce the expression to `0`

. But in
nontrivial examples, eliminating cast changes the type of the term,
which might make an ambient expression type incorrect. The virtual
machine, however, has no trouble evaluating the expression to
`0`

. Here is a similarly contrived example that shows how
`propext`

can get in the way:

```
theorem tteq : (True ∧ True) = True :=
propext (Iff.intro (fun ⟨h, _⟩ => h) (fun h => ⟨h, h⟩))
def val : Nat :=
Eq.recOn (motive := fun _ _ => Nat) tteq 0
-- does not reduce to 0
#reduce val
-- evaluates to 0
#eval val
```

Current research programs, including work on *observational type
theory* and *cubical type theory*, aim to extend type theory in ways
that permit reductions for casts involving function extensionality,
quotients, and more. But the solutions are not so clear-cut, and the
rules of Lean's underlying calculus do not sanction such reductions.

In a sense, however, a cast does not change the meaning of an
expression. Rather, it is a mechanism to reason about the expression's
type. Given an appropriate semantics, it then makes sense to reduce
terms in ways that preserve their meaning, ignoring the intermediate
bookkeeping needed to make the reductions type-correct. In that case,
adding new axioms in `Prop`

does not matter; by proof irrelevance,
an expression in `Prop`

carries no information, and can be safely
ignored by the reduction procedures.

## Quotients

Let `α`

be any type, and let `r`

be an equivalence relation on
`α`

. It is mathematically common to form the "quotient" `α / r`

,
that is, the type of elements of `α`

"modulo" `r`

. Set
theoretically, one can view `α / r`

as the set of equivalence
classes of `α`

modulo `r`

. If `f : α → β`

is any function that
respects the equivalence relation in the sense that for every
`x y : α`

, `r x y`

implies `f x = f y`

, then `f`

"lifts" to a function
`f' : α / r → β`

defined on each equivalence class `⟦x⟧`

by
`f' ⟦x⟧ = f x`

. Lean's standard library extends the Calculus of
Constructions with additional constants that perform exactly these
constructions, and installs this last equation as a definitional
reduction rule.

In its most basic form, the quotient construction does not even
require `r`

to be an equivalence relation. The following constants
are built into Lean:

```
namespace Hidden
universe u v
axiom Quot : {α : Sort u} → (α → α → Prop) → Sort u
axiom Quot.mk : {α : Sort u} → (r : α → α → Prop) → α → Quot r
axiom Quot.ind :
∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop},
(∀ a, β (Quot.mk r a)) → (q : Quot r) → β q
axiom Quot.lift :
{α : Sort u} → {r : α → α → Prop} → {β : Sort u} → (f : α → β)
→ (∀ a b, r a b → f a = f b) → Quot r → β
end Hidden
```

The first one forms a type `Quot r`

given a type `α`

by any binary
relation `r`

on `α`

. The second maps `α`

to `Quot α`

, so that
if `r : α → α → Prop`

and `a : α`

, then `Quot.mk r a`

is an
element of `Quot r`

. The third principle, `Quot.ind`

, says that
every element of `Quot.mk r a`

is of this form. As for
`Quot.lift`

, given a function `f : α → β`

, if `h`

is a proof
that `f`

respects the relation `r`

, then `Quot.lift f h`

is the
corresponding function on `Quot r`

. The idea is that for each
element `a`

in `α`

, the function `Quot.lift f h`

maps
`Quot.mk r a`

(the `r`

-class containing `a`

) to `f a`

, wherein `h`

shows that this function is well defined. In fact, the computation
principle is declared as a reduction rule, as the proof below makes
clear.

```
def mod7Rel (x y : Nat) : Prop :=
x % 7 = y % 7
-- the quotient type
#check (Quot mod7Rel : Type)
-- the class of a
#check (Quot.mk mod7Rel 4 : Quot mod7Rel)
def f (x : Nat) : Bool :=
x % 7 = 0
theorem f_respects (a b : Nat) (h : mod7Rel a b) : f a = f b := by
simp [mod7Rel, f] at *
rw [h]
#check (Quot.lift f f_respects : Quot mod7Rel → Bool)
-- the computation principle
example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
rfl
```

The four constants, `Quot`

, `Quot.mk`

, `Quot.ind`

, and
`Quot.lift`

in and of themselves are not very strong. You can check
that the `Quot.ind`

is satisfied if we take `Quot r`

to be simply
`α`

, and take `Quot.lift`

to be the identity function (ignoring
`h`

). For that reason, these four constants are not viewed as
additional axioms.

They are, like inductively defined types and the associated constructors and recursors, viewed as part of the logical framework.

What makes the `Quot`

construction into a bona fide quotient is the
following additional axiom:

```
namespace Hidden
universe u v
axiom Quot.sound :
∀ {α : Type u} {r : α → α → Prop} {a b : α},
r a b → Quot.mk r a = Quot.mk r b
end Hidden
```

This is the axiom that asserts that any two elements of `α`

that are
related by `r`

become identified in the quotient. If a theorem or
definition makes use of `Quot.sound`

, it will show up in the
`#print axioms`

command.

Of course, the quotient construction is most commonly used in
situations when `r`

is an equivalence relation. Given `r`

as
above, if we define `r'`

according to the rule `r' a b`

iff
`Quot.mk r a = Quot.mk r b`

, then it's clear that `r'`

is an
equivalence relation. Indeed, `r'`

is the *kernel* of the function
`a ↦ quot.mk r a`

. The axiom `Quot.sound`

says that `r a b`

implies `r' a b`

. Using `Quot.lift`

and `Quot.ind`

, we can show
that `r'`

is the smallest equivalence relation containing `r`

, in
the sense that if `r''`

is any equivalence relation containing
`r`

, then `r' a b`

implies `r'' a b`

. In particular, if `r`

was an equivalence relation to start with, then for all `a`

and
`b`

we have `r a b`

iff `r' a b`

.

To support this common use case, the standard library defines the
notion of a *setoid*, which is simply a type with an associated
equivalence relation:

```
namespace Hidden
class Setoid (α : Sort u) where
r : α → α → Prop
iseqv : Equivalence r
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
namespace Setoid
variable {α : Sort u} [Setoid α]
theorem refl (a : α) : a ≈ a :=
iseqv.refl a
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
iseqv.symm hab
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
iseqv.trans hab hbc
end Setoid
end Hidden
```

Given a type `α`

, a relation `r`

on `α`

, and a proof `p`

that `r`

is an equivalence relation, we can define `Setoid.mk r p`

as an instance of the setoid class.

```
namespace Hidden
def Quotient {α : Sort u} (s : Setoid α) :=
@Quot α Setoid.r
end Hidden
```

The constants `Quotient.mk`

, `Quotient.ind`

, `Quotient.lift`

,
and `Quotient.sound`

are nothing more than the specializations of
the corresponding elements of `Quot`

. The fact that type class
inference can find the setoid associated to a type `α`

brings a
number of benefits. First, we can use the notation `a ≈ b`

(entered
with `\approx`

) for `Setoid.r a b`

, where the instance of
`Setoid`

is implicit in the notation `Setoid.r`

. We can use the
generic theorems `Setoid.refl`

, `Setoid.symm`

, `Setoid.trans`

to
reason about the relation. Specifically with quotients we can use the
generic notation `⟦a⟧`

for `Quot.mk Setoid.r`

where the instance
of `Setoid`

is implicit in the notation `Setoid.r`

, as well as the
theorem `Quotient.exact`

:

```
universe u
#check (@Quotient.exact :
∀ {α : Sort u} {s : Setoid α} {a b : α},
Quotient.mk s a = Quotient.mk s b → a ≈ b)
```

Together with `Quotient.sound`

, this implies that the elements of
the quotient correspond exactly to the equivalence classes of elements
in `α`

.

Recall that in the standard library, `α × β`

represents the
Cartesian product of the types `α`

and `β`

. To illustrate the use
of quotients, let us define the type of *unordered* pairs of elements
of a type `α`

as a quotient of the type `α × α`

. First, we define
the relevant equivalence relation:

```
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
```

The next step is to prove that `eqv`

is in fact an equivalence
relation, which is to say, it is reflexive, symmetric and
transitive. We can prove these three facts in a convenient and
readable way by using dependent pattern matching to perform
case-analysis and break the hypotheses into pieces that are then
reassembled to produce the conclusion.

```
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (by simp_all)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (by simp_all)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
```

Now that we have proved that `eqv`

is an equivalence relation, we
can construct a `Setoid (α × α)`

, and use it to define the type
`UProd α`

of unordered pairs.

```
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (by simp_all)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (by simp_all)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
r := eqv
iseqv := is_equivalence
def UProd (α : Type u) : Type u :=
Quotient (uprodSetoid α)
namespace UProd
def mk {α : Type} (a₁ a₂ : α) : UProd α :=
Quotient.mk' (a₁, a₂)
notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
end UProd
```

Notice that we locally define the notation `{a₁, a₂}`

for unordered
pairs as `Quotient.mk (a₁, a₂)`

. This is useful for illustrative
purposes, but it is not a good idea in general, since the notation
will shadow other uses of curly brackets, such as for records and
sets.

We can easily prove that `{a₁, a₂} = {a₂, a₁}`

using `Quot.sound`

,
since we have `(a₁, a₂) ~ (a₂, a₁)`

.

```
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (by simp_all)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (by simp_all)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
r := eqv
iseqv := is_equivalence
def UProd (α : Type u) : Type u :=
Quotient (uprodSetoid α)
namespace UProd
def mk {α : Type} (a₁ a₂ : α) : UProd α :=
Quotient.mk' (a₁, a₂)
notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
Quot.sound (Or.inr ⟨rfl, rfl⟩)
end UProd
```

To complete the example, given `a : α`

and `u : uprod α`

, we
define the proposition `a ∈ u`

which should hold if `a`

is one of
the elements of the unordered pair `u`

. First, we define a similar
proposition `mem_fn a u`

on (ordered) pairs; then we show that
`mem_fn`

respects the equivalence relation `eqv`

with the lemma
`mem_respects`

. This is an idiom that is used extensively in the
Lean standard library.

```
private def eqv (p₁ p₂ : α × α) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50 " ~ " => eqv
private theorem eqv.refl (p : α × α) : p ~ p :=
Or.inl ⟨rfl, rfl⟩
private theorem eqv.symm : ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (by simp_all)
private theorem eqv.trans : ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (by simp_all)
private theorem is_equivalence : Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instance uprodSetoid (α : Type u) : Setoid (α × α) where
r := eqv
iseqv := is_equivalence
def UProd (α : Type u) : Type u :=
Quotient (uprodSetoid α)
namespace UProd
def mk {α : Type} (a₁ a₂ : α) : UProd α :=
Quotient.mk' (a₁, a₂)
notation "{ " a₁ ", " a₂ " }" => mk a₁ a₂
theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
Quot.sound (Or.inr ⟨rfl, rfl⟩)
private def mem_fn (a : α) : α × α → Prop
| (a₁, a₂) => a = a₁ ∨ a = a₂
-- auxiliary lemma for proving mem_respects
private theorem mem_swap {a : α} :
∀ {p : α × α}, mem_fn a p = mem_fn a (⟨p.2, p.1⟩)
| (a₁, a₂) => by
apply propext
apply Iff.intro
. intro
| Or.inl h => exact Or.inr h
| Or.inr h => exact Or.inl h
. intro
| Or.inl h => exact Or.inr h
| Or.inr h => exact Or.inl h
private theorem mem_respects
: {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
| (a₁, a₂), (b₁, b₂), a, Or.inl ⟨a₁b₁, a₂b₂⟩ => by simp_all
| (a₁, a₂), (b₁, b₂), a, Or.inr ⟨a₁b₂, a₂b₁⟩ => by simp_all; apply mem_swap
def mem (a : α) (u : UProd α) : Prop :=
Quot.liftOn u (fun p => mem_fn a p) (fun p₁ p₂ e => mem_respects a e)
infix:50 (priority := high) " ∈ " => mem
theorem mem_mk_left (a b : α) : a ∈ {a, b} :=
Or.inl rfl
theorem mem_mk_right (a b : α) : b ∈ {a, b} :=
Or.inr rfl
theorem mem_or_mem_of_mem_mk {a b c : α} : c ∈ {a, b} → c = a ∨ c = b :=
fun h => h
end UProd
```

For convenience, the standard library also defines `Quotient.lift₂`

for lifting binary functions, and `Quotient.ind₂`

for induction on
two variables.

We close this section with some hints as to why the quotient
construction implies function extensionality. It is not hard to show
that extensional equality on the `(x : α) → β x`

is an equivalence
relation, and so we can consider the type `extfun α β`

of functions
"up to equivalence." Of course, application respects that equivalence
in the sense that if `f₁`

is equivalent to `f₂`

, then `f₁ a`

is
equal to `f₂ a`

. Thus application gives rise to a function
`extfun_app : extfun α β → (x : α) → β x`

. But for every `f`

,
`extfun_app ⟦f⟧`

is definitionally equal to `fun x => f x`

, which is
in turn definitionally equal to `f`

. So, when `f₁`

and `f₂`

are
extensionally equal, we have the following chain of equalities:

```
f₁ = extfun_app ⟦f₁⟧ = extfun_app ⟦f₂⟧ = f₂
```

As a result, `f₁`

is equal to `f₂`

.

## Choice

To state the final axiom defined in the standard library, we need the
`Nonempty`

type, which is defined as follows:

```
namespace Hidden
class inductive Nonempty (α : Sort u) : Prop where
| intro (val : α) : Nonempty α
end Hidden
```

Because `Nonempty α`

has type `Prop`

and its constructor contains data, it can only eliminate to `Prop`

.
In fact, `Nonempty α`

is equivalent to `∃ x : α, True`

:

```
example (α : Type u) : Nonempty α ↔ ∃ x : α, True :=
Iff.intro (fun ⟨a⟩ => ⟨a, trivial⟩) (fun ⟨a, h⟩ => ⟨a⟩)
```

Our axiom of choice is now expressed simply as follows:

```
namespace Hidden
universe u
axiom choice {α : Sort u} : Nonempty α → α
end Hidden
```

Given only the assertion `h`

that `α`

is nonempty, `choice h`

magically produces an element of `α`

. Of course, this blocks any
meaningful computation: by the interpretation of `Prop`

, `h`

contains no information at all as to how to find such an element.

This is found in the `Classical`

namespace, so the full name of the
theorem is `Classical.choice`

. The choice principle is equivalent to
the principle of *indefinite description*, which can be expressed with
subtypes as follows:

```
namespace Hidden
universe u
axiom choice {α : Sort u} : Nonempty α → α
noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
(h : ∃ x, p x) : {x // p x} :=
choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
end Hidden
```

Because it depends on `choice`

, Lean cannot generate bytecode for
`indefiniteDescription`

, and so requires us to mark the definition
as `noncomputable`

. Also in the `Classical`

namespace, the
function `choose`

and the property `choose_spec`

decompose the two
parts of the output of `indefiniteDescription`

:

```
open Classical
namespace Hidden
noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
(indefiniteDescription p h).val
theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property
end Hidden
```

The `choice`

principle also erases the distinction between the
property of being `Nonempty`

and the more constructive property of
being `Inhabited`

:

```
open Classical
theorem inhabited_of_nonempty : Nonempty α → Inhabited α :=
fun h => choice (let ⟨a⟩ := h; ⟨⟨a⟩⟩)
```

In the next section, we will see that `propext`

, `funext`

, and
`choice`

, taken together, imply the law of the excluded middle and
the decidability of all propositions. Using those, one can strengthen
the principle of indefinite description as follows:

```
open Classical
universe u
#check (@strongIndefiniteDescription :
{α : Sort u} → (p : α → Prop)
→ Nonempty α → {x // (∃ (y : α), p y) → p x})
```

Assuming the ambient type `α`

is nonempty,
`strongIndefiniteDescription p`

produces an element of `α`

satisfying `p`

if there is one. The data component of this
definition is conventionally known as *Hilbert's epsilon function*:

```
open Classical
universe u
#check (@epsilon :
{α : Sort u} → [Nonempty α]
→ (α → Prop) → α)
#check (@epsilon_spec :
∀ {α : Sort u} {p : α → Prop} (hex : ∃ (y : α), p y),
p (@epsilon _ (nonempty_of_exists hex) p))
```

## The Law of the Excluded Middle

The law of the excluded middle is the following

```
open Classical
#check (@em : ∀ (p : Prop), p ∨ ¬p)
```

Diaconescu's theorem states
that the axiom of choice is sufficient to derive the law of excluded
middle. More precisely, it shows that the law of the excluded middle
follows from `Classical.choice`

, `propext`

, and `funext`

. We
sketch the proof that is found in the standard library.

First, we import the necessary axioms, and define two predicates `U`

and `V`

:

```
namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
sorry
end Hidden
```

If `p`

is true, then every element of `Prop`

is in both `U`

and `V`

.
If `p`

is false, then `U`

is the singleton `true`

, and `V`

is the singleton `false`

.

Next, we use `some`

to choose an element from each of `U`

and `V`

:

```
namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
sorry
end Hidden
```

Each of `U`

and `V`

is a disjunction, so `u_def`

and `v_def`

represent four cases. In one of these cases, `u = True`

and
`v = False`

, and in all the other cases, `p`

is true. Thus we have:

```
namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
Or.inl hne
sorry
end Hidden
```

On the other hand, if `p`

is true, then, by function extensionality
and propositional extensionality, `U`

and `V`

are equal. By the
definition of `u`

and `v`

, this implies that they are equal as well.

```
namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
Or.inl hne
have p_implies_uv : p → u = v :=
fun hp =>
have hpred : U = V :=
funext fun x =>
have hl : (x = True ∨ p) → (x = False ∨ p) :=
fun _ => Or.inr hp
have hr : (x = False ∨ p) → (x = True ∨ p) :=
fun _ => Or.inr hp
show (x = True ∨ p) = (x = False ∨ p) from
propext (Iff.intro hl hr)
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
rw [hpred]; intros; rfl
show u = v from h₀ _ _
sorry
end Hidden
```

Putting these last two facts together yields the desired conclusion:

```
namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
Or.inl hne
have p_implies_uv : p → u = v :=
fun hp =>
have hpred : U = V :=
funext fun x =>
have hl : (x = True ∨ p) → (x = False ∨ p) :=
fun _ => Or.inr hp
have hr : (x = False ∨ p) → (x = True ∨ p) :=
fun _ => Or.inr hp
show (x = True ∨ p) = (x = False ∨ p) from
propext (Iff.intro hl hr)
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
rw [hpred]; intros; rfl
show u = v from h₀ _ _
match not_uv_or_p with
| Or.inl hne => Or.inr (mt p_implies_uv hne)
| Or.inr h => Or.inl h
end Hidden
```

Consequences of excluded middle include double-negation elimination, proof by cases, and proof by contradiction, all of which are described in the Section Classical Logic. The law of the excluded middle and propositional extensionality imply propositional completeness:

```
namespace Hidden
open Classical
theorem propComplete (a : Prop) : a = True ∨ a = False :=
match em a with
| Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
| Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
end Hidden
```

Together with choice, we also get the stronger principle that every
proposition is decidable. Recall that the class of `Decidable`

propositions is defined as follows:

```
namespace Hidden
class inductive Decidable (p : Prop) where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p
end Hidden
```

In contrast to `p ∨ ¬ p`

, which can only eliminate to `Prop`

, the
type `Decidable p`

is equivalent to the sum type `Sum p (¬ p)`

, which
can eliminate to any type. It is this data that is needed to write an
if-then-else expression.

As an example of classical reasoning, we use `choose`

to show that if
`f : α → β`

is injective and `α`

is inhabited, then `f`

has a
left inverse. To define the left inverse `linv`

, we use a dependent
if-then-else expression. Recall that `if h : c then t else e`

is
notation for `dite c (fun h : c => t) (fun h : ¬ c => e)`

. In the definition
of `linv`

, choice is used twice: first, to show that
`(∃ a : A, f a = b)`

is "decidable," and then to choose an `a`

such that
`f a = b`

. Notice that `propDecidable`

is a scoped instance and is activated
by the `open Classical`

command. We use this instance to justify
the if-then-else expression. (See also the discussion in
Section Decidable Propositions).

```
open Classical
noncomputable def linv [Inhabited α] (f : α → β) : β → α :=
fun b : β => if ex : (∃ a : α, f a = b) then choose ex else default
theorem linv_comp_self {f : α → β} [Inhabited α]
(inj : ∀ {a b}, f a = f b → a = b)
: linv f ∘ f = id :=
funext fun a =>
have ex : ∃ a₁ : α, f a₁ = f a := ⟨a, rfl⟩
have feq : f (choose ex) = f a := choose_spec ex
calc linv f (f a)
_ = choose ex := dif_pos ex
_ = a := inj feq
```

From a classical point of view, `linv`

is a function. From a
constructive point of view, it is unacceptable; because there is no
way to implement such a function in general, the construction is not
informative.