12. 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 executable code, 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 compiled code.
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 compilation, 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 code generation, whereas the third is not amenable to computational interpretation. We will spell out the details more precisely below.
12.1. 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 prf : 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 prevent the generation
of executable code, as described above. It is only the choice
principles discussed in the section on choice that completely erase the
distinction between the proof-irrelevant and data-relevant parts of
the theory.
12.2. Propositional Extensionality
Propositional extensionality is the following axiom:
axiom propext {a b : Prop} : (a ↔ b) → a = b
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
\{\ast\}, for some distinguished element \ast. The axiom has the
effect that equivalent propositions can be substituted for one another
in any context:
12.3. 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:
funext.{u, v}
{α : Sort u} {β : α → Sort v}
{f g : (x : α) → β x}
(h : ∀ (x : α), f x = g x) :
f = g
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 u 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 _ => 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 _ => Iff.intro
(fun ⟨_, h⟩ => h)
(fun h => False.elim h)
theorem empty_inter (a : Set α) : ∅ ∩ a = ∅ :=
setext fun _ => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => False.elim h)
theorem inter.comm (a b : Set α) : a ∩ b = b ∩ a :=
setext fun _ => 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 valCurrent 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.
12.4. 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:
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 → β
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 numbers equivalent to 4
#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 := a:Natb:Nath:mod7Rel a b⊢ f a = f b
a:Natb:Nath:a % 7 = b % 7⊢ a % 7 = 0 ↔ b % 7 = 0
All goals completed! 🐙
#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:
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
fun 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:
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
Given a type α, a relation r
on α, and a proof iseqv
that r is an equivalence relation, we can define an
instance of the Setoid class.
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
theorem Quotient.exact:
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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_fnau 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.
set_option linter.unusedVariables false
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ (b₁, b₂).fst = (a₁, a₂).fst ∧ (b₁, b₂).snd = (a₁, a₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ (b₁, b₂).fst = (a₁, a₂).snd ∧ (b₁, b₂).snd = (a₁, a₂).fst All goals completed! 🐙)
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 (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).sndb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₁:(b₁, b₂).fst = (c₁, c₂).fstb₂c₂:(b₁, b₂).snd = (c₁, c₂).snd⊢ (a₁, a₂).fst = (c₁, c₂).snd ∧ (a₁, a₂).snd = (c₁, c₂).fst All goals completed! 🐙)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (α:Type u_1a₁:αa₂:αb₁:αb₂:αc₁:αc₂:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fstb₁c₂:(b₁, b₂).fst = (c₁, c₂).sndb₂c₁:(b₁, b₂).snd = (c₁, c₂).fst⊢ (a₁, a₂).fst = (c₁, c₂).fst ∧ (a₁, a₂).snd = (c₁, c₂).snd All goals completed! 🐙)
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⟩)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) = mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) = mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) ↔ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) → mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) → mem_fn a (a₁, a₂)
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a (a₁, a₂) → mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) intro
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a (a₁, a₂)h:a = a₁⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a (a₁, a₂)h:a = a₂⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:α⊢ mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst) → mem_fn a (a₁, a₂) intro
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)h:a = (a₁, a₂).snd⊢ mem_fn a (a₁, a₂) All goals completed! 🐙
α:Type u_1a:αa₁:αa₂:αx✝:mem_fn a ((a₁, a₂).snd, (a₁, a₂).fst)h:a = (a₁, a₂).fst⊢ mem_fn a (a₁, a₂) All goals completed! 🐙
private theorem mem_respects : {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂) α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₁:(a₁, a₂).fst = (b₁, b₂).fsta₂b₂:(a₁, a₂).snd = (b₁, b₂).snd⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂)
All goals completed! 🐙
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂) α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:(a₁, a₂).fst = (b₁, b₂).snda₂b₁:(a₁, a₂).snd = (b₁, b₂).fst⊢ mem_fn a (a₁, a₂) = mem_fn a (b₁, b₂)
α:Type u_1a₁:αa₂:αb₁:αb₂:αa:αa₁b₂:a₁ = b₂a₂b₁:a₂ = b₁⊢ mem_fn a (b₂, b₁) = mem_fn a (b₁, b₂)
All goals completed! 🐙
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 (.mk _ 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:
variable {α : Sort u} {β : α → Sort v}
def extfun (α : Sort u) (β : α → Sort v) := Quot (fun (f g : (x : α) → β x) => ∀ x, f x = g x)
def extfun_app {α β} (f : extfun α β) (x : α) : β x :=
Quot.lift (· x) (α✝:Sort uβ✝:α✝ → Sort vα:Sort ?u.9β:α → Sort ?u.8f:extfun α βx:α⊢ ∀ (a b : (x : α) → β x), (∀ (x : α), a x = b x) → a x = b x α✝:Sort uβ✝:α✝ → Sort vα:Sort ?u.9β:α → Sort ?u.8f:extfun α βx:αa✝¹:(x : α) → β xb✝:(x : α) → β xa✝:∀ (x : α), a✝¹ x = b✝ x⊢ a✝¹ x = b✝ x; All goals completed! 🐙) f
example (f₁ f₂ : (x : α) → β x) (h : ∀ x, f₁ x = f₂ x) :=
calc f₁
_ = extfun_app (.mk _ f₁) := rfl
_ = extfun_app (.mk _ f₂) := α:Sort uβ:α → Sort vf₁:(x : α) → β xf₂:(x : α) → β xh:∀ (x : α), f₁ x = f₂ x⊢ extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₁) = extfun_app (Quot.mk (fun f g => ∀ (x : α), f x = g x) f₂) α:Sort uβ:α → Sort vf₁:(x : α) → β xf₂:(x : α) → β xh:∀ (x : α), f₁ x = f₂ x⊢ ∀ (x : α), f₁ x = f₂ x; All goals completed! 🐙
_ = f₂ := rfl
As a result, f₁ is equal to f₂.
12.5. Choice
To state the final axiom defined in the standard library, we need the
Nonempty type, which is defined as follows:
class inductive Nonempty (α : Sort u) : Prop where
| intro (val : α) : Nonempty α
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:
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:
noncomputable def indefiniteDescription {α : Sort u}
(p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
Because it depends on choice, Lean cannot generate executable code 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:
variable {α : Sort u} {p : α → Prop}
noncomputable def choose (h : ∃ x, p x) : α :=
(indefiniteDescription p h).val
theorem choose_spec (h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property
The choice principle also erases the distinction between the
property of being Nonempty and the more constructive property of
being Inhabited:
open Classical
noncomputable def inhabited_of_nonempty (h : Nonempty α) : Inhabited α :=
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:
strongIndefiniteDescription {α : Sort u} (p : α → Prop)
(h : 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:
epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
epsilon_spec {α : Sort u} {p : α → Prop}
(hex : ∃ (y : α), p y) :
p (@epsilon _ hex.nonempty p)
12.6. The Law of the Excluded Middle
The law of the excluded middle is the following:
Classical.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:
open Classical
theorem em (p : Prop) : p ∨ ¬p := p:Prop⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ p⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ p⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U x⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V x⊢ p ∨ ¬p
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 choose to choose an element from each of U and V:
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exU⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exV⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U u⊢ p ∨ ¬p
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V v⊢ p ∨ ¬p
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:
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ p⊢ p ∨ ¬p
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.
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ pp_implies_uv:p → u = v⊢ p ∨ ¬p
Putting these last two facts together yields the desired conclusion:
match not_uv_or_p with
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ pp_implies_uv:p → u = vhne:u ≠ v⊢ p ∨ ¬p
All goals completed! 🐙
p:PropU:Prop → Prop := fun x => x = True ∨ pV:Prop → Prop := fun x => x = False ∨ pexU:∃ x, U xexV:∃ x, V xu:Prop := choose exUv:Prop := choose exVu_def:U uv_def:V vnot_uv_or_p:u ≠ v ∨ pp_implies_uv:p → u = vh:p⊢ p ∨ ¬p
All goals completed! 🐙
Consequences of excluded middle include double-negation elimination, proof by cases, and proof by contradiction, all of which are described in the section on classical logic. The law of the excluded middle and propositional extensionality imply propositional completeness:
open Classical
theorem propComplete (a : Prop) : a = True ∨ a = False :=
match em a with
| Or.inl ha =>
Or.inl (propext (Iff.intro (fun _ => True.intro) (fun _ => ha)))
| Or.inr hn =>
Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
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 : α, 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
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 := rfl
_ = 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.