Skip to content
This repository has been archived by the owner on Oct 21, 2024. It is now read-only.

Latest commit

 

History

History
1261 lines (1022 loc) · 45.3 KB

12_Axioms.org

File metadata and controls

1261 lines (1022 loc) · 45.3 KB
Raw

Theorem Proving in Lean

Axioms and Computation

We have seen that the version of the Calculus of Inductive Constructions that has been implemented in Lean includes Pi types, and inductive types, and a nested hierarchy of universes with an impredicative, proof-irrelevant Prop at the bottom. In this chapter, we consider extensions of 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 ℕ, for example, denoting a natural number will reduce to a numeral.

To support classical reasoning, Lean’s standard library defines one choice axiom, which is justified on a set-theoretic interpretation of type theory. In the standard library, the law of the excluded middle is a consequence of this axiom. The library also imports two semi-constructive (or mildly classical) axioms, propositional extensionality and quotients. These are used, for example, to develop theories of sets and finite sets. Even some computationally inclined users may also wish to use the law of the excluded middle to reason about computation. Below we will describe the effects that these axioms have on computation aspects of the system.

However, the classical choice axiom (also known as the Hilbert operator) is entirely inimical to a computational interpretation of the system, which 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 depend on this construction lose their computational content, and in Lean we are required to mark such definitions as noncomputable to flag that fact.

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 a 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 Pi 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 ℕ 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 the 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 : A for any type A, 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, ignore intermediate typing constraints, and reduces terms until they reach a normal form. Current plans for Lean include the development of a fast evaluator along these lines.

Having adopted a proof-irrelevant Prop, one might consider it legitimate to use, for example, the law of the excluded middle, governing propositions. Of course, this, too, can block computation, but it does not block fast evaluation as described above. From a constructive point of view, the most objectionable classical axioms are “choice axioms” that allow us to extract “data” from any existential proposition, completely erasing the distinction between the proof-irrelevant and data-relevant parts of the theory. These are discussed in Section Choice Axioms below.

Propositional Extensionality

Propositional extensionality is the following axiom:

namespace hide

-- BEGIN
axiom propext {a b : Prop} : (a ↔ b) → a = b
-- END

end hide

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 the effect that equivalent propositions can be substituted for one another in any context:

namespace hide

axiom propext {a b : Prop} : (a ↔ b) → a = b

-- BEGIN
section
  open eq.ops
  variables a b c d e : Prop
  variable P : Prop → Prop

  example (H : a ↔ b) : (c ∧ a ∧ d → e) ↔ (c ∧ b ∧ d → e) :=
  propext H ▸ !iff.refl

  example (H : a ↔ b) (H1 : P a) : P b :=
  propext H ▸ H1
end
-- END

end hide

The first example could be proved more laboriously without propext using the fact that the propositional connectives respect propositional equivalence. The second example represents a more essential use of propext. In fact, it is equivalent to propext itself, a fact which we encourage you to prove.

Function Extensionality

Similar to propositional extensionality, function extensionality asserts that any two functions of type Π x : A, B x that agree on all their inputs are equal.

namespace hide

-- BEGIN
check @funext
-- ∀ {A : Type} {B : A → Type} {f₁ f₂ : Π x : A, B x}, (∀ x, f₁ x = f₂ x) → f₁ = f₂
-- END
end hide

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 X : Type we define the set X := X → Prop to denote the type of subsets of X, essentially identifying subsets with predicates. By combining funext and propext, we obtain an extensional theory of such sets:

import logic
open eq.ops

namespace hide

-- BEGIN
definition set (X : Type) := X → Prop

namespace set

variable {X : Type}

definition mem [reducible] (x : X) (a : set X) := a x
notation e ∈ a := mem e a

theorem setext {a b : set X} (H : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (take x, propext (H x))

end set
-- END
end hide

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

import standard
import logic
open eq.ops

namespace hide

definition set (X : Type) := X → Prop

namespace set

variable {X : Type}

definition mem [reducible] (x : X) (a : set X) := a x
notation e ∈ a := mem e a

theorem setext {a b : set X} (H : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
funext (take x, propext (H x))

-- BEGIN
definition empty [reducible] : set X := λ x, false
notation `∅` := empty

definition inter [reducible] (a b : set X) : set X := λ x, x ∈ a ∧ x ∈ b
notation a ∩ b := inter a b

theorem inter_self (a : set X) : a ∩ a = a :=
setext (take x, !and_self)

theorem inter_empty (a : set X) : a ∩ ∅ = ∅ :=
setext (take x, !and_false)

theorem empty_inter (a : set X) : ∅ ∩ a = ∅ :=
setext (take x, !false_and)

theorem inter.comm (a b : set X) : a ∩ b = b ∩ a :=
setext (take x, !and.comm)
-- END

end set
end hide

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

import data.nat
open nat algebra

definition f₁ (x : ℕ) := x
definition f₂ (x : ℕ) := 0 + x

theorem feq : f₁ = f₂ := funext (take x, eq.subst !zero_add rfl)
check eq.rec (0 : ℕ) feq    -- ℕ
eval eq.rec (0 : ℕ) feq     -- eq.rec 0 feq

First, we show that the two functions f₁ and f₂ are equal using function extensionality, and then we “cast” 0 of type ℕ by replacing f₁ by f₂ in the type. Of course, the cast is vacuous, because ℕ 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 ℕ 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.

In the next section, we will exhibit a similar example with the quotient construction. 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 A be any type, and let R be an equivalence relation on A. It is mathematically common to form the “quotient” A / R, that is, the type of elements of A “modulo” R. Set theoretically, one can view A / R as the set of equivalence classes of A modulo R. If f : A → B is any function that respects the equivalence relation in the sense that for every x y : A, R x y implies f x = f y, then f “lifts” to a function f' : A / R → B defined on each equivalence class [x] by f' [x] = f x. Lean’s standard library extends the Calculus of Inductive Constructions with additional constants that perform exactly these constructions, and installs this last equation as a definitional reduction rule.

First, it is useful to define the notion of a setoid, which is simply a type with an associated equivalence relation:

namespace hide

-- BEGIN
structure setoid [class] (A : Type) :=
(r : A → A → Prop) (iseqv : equivalence r)

namespace setoid
  infix `≈` := setoid.r

  variable {A : Type}
  variable [s : setoid A]
  include s

  theorem refl (a : A) : a ≈ a :=
  and.elim_left (@setoid.iseqv A s) a

  theorem symm {a b : A} : a ≈ b → b ≈ a :=
  λ H, and.elim_left (and.elim_right (@setoid.iseqv A s)) a b H

  theorem trans {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
  λ H₁ H₂, and.elim_right (and.elim_right (@setoid.iseqv A s)) a b c H₁ H₂
end setoid
-- END

end hide

Given a type A, a relation R on A, and a proof p that R is an equivalence relation, we can define setoid.mk p as an instance of the setoid class. Lean’s type class inference mechanism then allows us to use the generic notation ≈ for R, and to use the generic theorems setoid.refl, setoid.symm, setoid.trans to reason about R.

The quotient package consists of the following constructors:

namespace hide

-- BEGIN
open setoid
constant quot.{l}   : Π {A : Type.{l}}, setoid A → Type.{l}

namespace quot
  constant mk        : Π {A : Type}   [s : setoid A], A → quot s
  notation `⟦`:max a `⟧`:0 := mk a

  constant sound     : Π {A : Type}   [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
  constant lift      : Π {A B : Type} [s : setoid A] (f : A → B), (∀ a b, a ≈ b → f a = f b) → quot s → B
  constant ind       : ∀ {A : Type}   [s : setoid A] {B : quot s → Prop}, (∀ a, B ⟦a⟧) → ∀ q, B q
end quot
-- END

end hide

For any type A with associated equivalence relation R, first we declare a setoid instance s to associate R as “the” equivalence relation on A. Once we do that, quot s denotes the quotient type A / R, and given a : A, ⟦a⟧ denotes the “equivalence class” of a. The meaning of constants sound, lift, and ind are given by their types. In particular, lift is the function which lifts a function f : A → B that respects the equivalence relation to the function lift f : quot s → B which lifts f to A / R. After declaring the constants associated with the quotient type, the library file then calls an internal function, init_quotient, which installs the reduction that simplifies lift f ⟦a⟧ to f a.

To illustrate the use of quotients, let us define the type of ordered pairs. In the standard library, A × B represents the Cartesian product of the types A and B. We can view it as the type of pairs (a, b) where a : A and b : B. We can use quotient types to define the type of unordered pairs of type A. We can use the notation {a₁, a₂} to represent the unordered pair containing a₁ and a₂. Moreover, we want to be able to prove the equality {a₁, a₂} = {a₂, a₁}. We start this construction by defining a relation p ~ q on A × A.

import data.prod
open prod prod.ops quot

private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)

infix `~` := eqv

To make the proofs more compact, we open the namespaces eq and or. Thus, we can write symm, trans, inl and inr instead of eq.symm, eq.trans, or.inl and or.inr respectively. We also define the notation ⟨H₁, H₂⟩ for (and.intro H₁ H₂).

open eq or

local notation `⟨` H₁ `,` H₂ `⟩` := and.intro H₁ H₂

The next step is to prove that eqv is 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.

import data.prod
open prod prod.ops

private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)

infix `~` := eqv

open eq or

local notation `⟨` H₁ `,` H₂ `⟩` := and.intro H₁ H₂

-- BEGIN
private theorem eqv.refl {A : Type} : ∀ p : A × A, p ~ p :=
take p, inl ⟨rfl, rfl⟩

private theorem eqv.symm {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂) (b₁, b₂) (inl ⟨a₁b₁, a₂b₂⟩) := inl ⟨symm a₁b₁, symm a₂b₂⟩
| (a₁, a₂) (b₁, b₂) (inr ⟨a₁b₂, a₂b₁⟩) := inr ⟨symm a₂b₁, symm a₁b₂⟩

private theorem eqv.trans {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inl ⟨trans a₁b₁ b₁c₁, trans a₂b₂ b₂c₂⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inr ⟨trans a₁b₁ b₁c₂, trans a₂b₂ b₂c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inr ⟨trans a₁b₂ b₂c₂, trans a₂b₁ b₁c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inl ⟨trans a₁b₂ b₂c₁, trans a₂b₁ b₁c₂⟩

private theorem is_equivalence (A : Type) : equivalence (@eqv A) :=
mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)
-- END

Now that we have proved that eqv is an equivalence relation, we can construct a setoid (A × A), and use it to define the type uprod A of unordered pairs. Moreover, we define the unordered pair {a₁, a₂} as ⟦(a₁, a₂)⟧.

import data.prod
open prod prod.ops quot

private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)

infix `~` := eqv

open eq or

local notation `⟨` H₁ `,` H₂ `⟩` := and.intro H₁ H₂

private theorem eqv.refl {A : Type} : ∀ p : A × A, p ~ p :=
take p, inl ⟨rfl, rfl⟩

private theorem eqv.symm {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂) (b₁, b₂) (inl ⟨a₁b₁, a₂b₂⟩) := inl ⟨symm a₁b₁, symm a₂b₂⟩
| (a₁, a₂) (b₁, b₂) (inr ⟨a₁b₂, a₂b₁⟩) := inr ⟨symm a₂b₁, symm a₁b₂⟩

private theorem eqv.trans {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inl ⟨trans a₁b₁ b₁c₁, trans a₂b₂ b₂c₂⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inr ⟨trans a₁b₁ b₁c₂, trans a₂b₂ b₂c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inr ⟨trans a₁b₂ b₂c₂, trans a₂b₁ b₁c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inl ⟨trans a₁b₂ b₂c₁, trans a₂b₁ b₁c₂⟩

private theorem is_equivalence (A : Type) : equivalence (@eqv A) :=
mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)

-- BEGIN
definition uprod.setoid [instance] (A : Type) : setoid (A × A) :=
setoid.mk (@eqv A) (is_equivalence A)

definition uprod (A : Type) : Type :=
quot (uprod.setoid A)

namespace uprod
  definition mk {A : Type} (a₁ a₂ : A) : uprod A :=
  ⟦(a₁, a₂)⟧

  notation `{` a₁ `,` a₂ `}` := mk a₁ a₂
end uprod
-- END

Now, we can easily prove that {a₁, a₂} = {a₂, a₁} using the quot.sound since (a₁, a₂) ~ (a₂, a₁).

import data.prod
open prod prod.ops quot

private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)

infix `~` := eqv

open eq or

local notation `⟨` H₁ `,` H₂ `⟩` := and.intro H₁ H₂

private theorem eqv.refl {A : Type} : ∀ p : A × A, p ~ p :=
take p, inl ⟨rfl, rfl⟩

private theorem eqv.symm {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂) (b₁, b₂) (inl ⟨a₁b₁, a₂b₂⟩) := inl ⟨symm a₁b₁, symm a₂b₂⟩
| (a₁, a₂) (b₁, b₂) (inr ⟨a₁b₂, a₂b₁⟩) := inr ⟨symm a₂b₁, symm a₁b₂⟩

private theorem eqv.trans {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inl ⟨trans a₁b₁ b₁c₁, trans a₂b₂ b₂c₂⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inr ⟨trans a₁b₁ b₁c₂, trans a₂b₂ b₂c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inr ⟨trans a₁b₂ b₂c₂, trans a₂b₁ b₁c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inl ⟨trans a₁b₂ b₂c₁, trans a₂b₁ b₁c₂⟩

private theorem is_equivalence (A : Type) : equivalence (@eqv A) :=
mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)

definition uprod.setoid [instance] (A : Type) : setoid (A × A) :=
setoid.mk (@eqv A) (is_equivalence A)

definition uprod (A : Type) : Type :=
quot (uprod.setoid A)

namespace uprod
  definition mk {A : Type} (a₁ a₂ : A) : uprod A :=
  ⟦(a₁, a₂)⟧

  notation `{` a₁ `,` a₂ `}` := mk a₁ a₂

-- BEGIN
  theorem mk_eq_mk {A : Type} (a₁ a₂ : A) : {a₁, a₂} = {a₂, a₁} :=
  quot.sound (inr ⟨rfl, rfl⟩)
-- END
end uprod

To complete the example, given a : A and u : uprod A, 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, in the lemma mem_respects. This is an idiom that is used extensively in the Lean standard library.

import data.prod
open prod prod.ops quot

private definition eqv {A : Type} (p₁ p₂ : A × A) : Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)

infix `~` := eqv

open eq or

local notation `⟨` H₁ `,` H₂ `⟩` := and.intro H₁ H₂

private theorem eqv.refl {A : Type} : ∀ p : A × A, p ~ p :=
take p, inl ⟨rfl, rfl⟩

private theorem eqv.symm {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂) (b₁, b₂) (inl ⟨a₁b₁, a₂b₂⟩) := inl ⟨symm a₁b₁, symm a₂b₂⟩
| (a₁, a₂) (b₁, b₂) (inr ⟨a₁b₂, a₂b₁⟩) := inr ⟨symm a₂b₁, symm a₁b₂⟩

private theorem eqv.trans {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inl ⟨trans a₁b₁ b₁c₁, trans a₂b₂ b₂c₂⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inl ⟨a₁b₁, a₂b₂⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inr ⟨trans a₁b₁ b₁c₂, trans a₂b₂ b₂c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inl ⟨b₁c₁, b₂c₂⟩) :=
  inr ⟨trans a₁b₂ b₂c₂, trans a₂b₁ b₁c₁⟩
| (a₁, a₂) (b₁, b₂) (c₁, c₂) (inr ⟨a₁b₂, a₂b₁⟩) (inr ⟨b₁c₂, b₂c₁⟩) :=
  inl ⟨trans a₁b₂ b₂c₁, trans a₂b₁ b₁c₂⟩

private theorem is_equivalence (A : Type) : equivalence (@eqv A) :=
mk_equivalence (@eqv A) (@eqv.refl A) (@eqv.symm A) (@eqv.trans A)

definition uprod.setoid [instance] (A : Type) : setoid (A × A) :=
setoid.mk (@eqv A) (is_equivalence A)

definition uprod (A : Type) : Type :=
quot (uprod.setoid A)

namespace uprod
  definition mk {A : Type} (a₁ a₂ : A) : uprod A :=
  ⟦(a₁, a₂)⟧

  notation `{` a₁ `,` a₂ `}` := mk a₁ a₂

  theorem mk_eq_mk {A : Type} (a₁ a₂ : A) : {a₁, a₂} = {a₂, a₁} :=
  quot.sound (inr ⟨rfl, rfl⟩)

-- BEGIN
  private definition mem_fn {A : Type} (a : A) : A × A → Prop
  | (a₁, a₂) := a = a₁ ∨ a = a₂

  -- auxiliary lemma for proving mem_respects
  private lemma mem_swap {A : Type} {a : A} : ∀ {p : A × A}, mem_fn a p = mem_fn a (swap p)
  | (a₁, a₂) := propext (iff.intro
      (λ l : a = a₁ ∨ a = a₂, or.elim l (λ h₁, inr h₁) (λ h₂, inl h₂))
      (λ r : a = a₂ ∨ a = a₁, or.elim r (λ h₁, inr h₁) (λ h₂, inl h₂)))

  private lemma mem_respects {A : Type} : ∀ {p₁ p₂ : A × A} (a : A),  p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
  | (a₁, a₂) (b₁, b₂) a (inl ⟨a₁b₁, a₂b₂⟩) :=
    begin esimp at a₁b₁, esimp at a₂b₂, rewrite [a₁b₁, a₂b₂] end
  | (a₁, a₂) (b₁, b₂) a (inr ⟨a₁b₂, a₂b₁⟩) :=
    begin esimp at a₁b₂, esimp at a₂b₁, rewrite [a₁b₂, a₂b₁], apply mem_swap end

  definition mem {A : Type} (a : A) (u : uprod A) : Prop :=
  quot.lift_on u (λ p, mem_fn a p) (λ p₁ p₂ e, mem_respects a e)

  infix `∈` := mem

  theorem mem_mk_left {A : Type} (a b : A) : a ∈ {a, b} :=
  inl rfl

  theorem mem_mk_right {A : Type} (a b : A) : b ∈ {a, b} :=
  inr rfl

  theorem mem_or_mem_of_mem_mk {A : Type} {a b c : A} : c ∈ {a, b} → c = a ∨ c = b :=
  λ h, h
-- END
end uprod

The quotient construction can be used to derive function extensionality, and we have seen that the latter blocks computation. The following provides another example of the same phenomenon, similar to the one we discussed in the last section.

import data.finset
open finset quot list nat

definition s₁ : finset nat := to_finset [1, 2]
definition s₂ : finset nat := to_finset [2, 1]

theorem seq : s₁ = s₂ := dec_trivial
check eq.rec (0 : ℕ) seq
eval eq.rec (0 : ℕ) seq

Choice Axioms

The following axiom is used to support classical reasoning in Lean:

open subtype nonempty

namespace hide
-- BEGIN
axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
  { x | (∃ y : A, P y) → P x}
-- END
end hide

This asserts that given any predicate P on a nonempty type A, we can (magically) produce an element x with the property that if any element of A satisfies P, then x does. In the presence of classical logic, we could prove this from the slightly weaker axiom:

open subtype nonempty

namespace hide
-- BEGIN
axiom indefinite_description {A : Type} {P : A → Prop} (H : ∃ x, P x) :
  {x : A | P x}
-- END
end hide

This says that knowing that there is an element of A satisfying P is enough to produce one. This axiom essentially undoes the separation of data from propositions, because it allows us to extract a piece of data — an element of A satisfying P — from the proposition that such an element exists.

The axiom strong_indefinite_description is imported when you import logic.choice. Separating the x asserted to exist by the axiom from the property it satisfies allows us to define the Hilbert epsilon function:

import logic.quantifiers
open subtype nonempty

namespace hide

axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
  { x | (∃ y : A, P y) → P x}

-- BEGIN
noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
let u : {x | (∃ y, P y) → P x} :=
  strong_indefinite_description P H in
elt_of u

theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃ y, P y) :
    P (@epsilon A H P) :=
let u : {x | (∃ y, P y) → P x} :=
  strong_indefinite_description P H in
has_property u Hex

theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃ y, P y) :
    P (@epsilon A (nonempty_of_exists Hex) P) :=
epsilon_spec_aux (nonempty_of_exists Hex) P Hex
-- END

end hide

Assuming the type A is nonempty, epsilon P returns an element of A, with the property that if any element of A satisfies P, epsilon P does. Notice that the definition is preceded by the keyword noncomputable, to signal the fact that expressions depending on this definition will not compute to canonical normal forms, even under the more liberal evaluation scheme described above.

Just as indefinite_description is a weaker version of strong_indefinite_description, the some operator is a weaker version of the epsilon operator. It is sometimes easier to use. Assuming H : ∃ x, P x is a proof that some element of A satisfies P, some H denotes such an element.

import logic.quantifiers
open subtype nonempty

namespace hide

axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
  { x | (∃ y : A, P y) → P x}

noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
let u : {x | (∃ y, P y) → P x} :=
  strong_indefinite_description P H in
elt_of u

theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃ y, P y) :
    P (@epsilon A H P) :=
let u : {x | (∃ y, P y) → P x} :=
  strong_indefinite_description P H in
has_property u Hex

theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃ y, P y) :
    P (@epsilon A (nonempty_of_exists Hex) P) :=
epsilon_spec_aux (nonempty_of_exists Hex) P Hex

-- BEGIN
noncomputable definition some {A : Type} {P : A → Prop} (H : ∃ x, P x) : A :=
@epsilon A (nonempty_of_exists H) P

theorem some_spec {A : Type} {P : A → Prop} (H : ∃ x, P x) : P (some H) :=
epsilon_spec H
-- END

end hide

#

Excluded Middle

The law of the excluded middle is the following

open classical
namespace hide
-- BEGIN
check @em
-- ∀ (a : Prop), a ∨ ¬a
-- END
end hide

We can prove it using the choice axiom described in the previous section. This is a consequence of Diaconescu’s theorem which 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 strong_indefinite_description (Hilbert’s choice), propext (propositional extensionality) and funext (function extensionality). The standard library contains this proof, which we reproduce here.

First, we import the necessary axioms, fix a parameter, p, and define two predicates U and V:

-- BEGIN
import logic.eq
open classical eq.ops

section
parameter  p : Prop

definition U (x : Prop) : Prop := x = true ∨ p
definition V (x : Prop) : Prop := x = false ∨ p
-- END

end

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 epsilon to choose an element from each of U and V:

import logic.eq
open classical eq.ops

section
parameter  p : Prop

definition U (x : Prop) : Prop := x = true ∨ p
definition V (x : Prop) : Prop := x = false ∨ p

-- BEGIN
noncomputable definition u := epsilon U
noncomputable definition v := epsilon V

lemma u_def : U u :=
epsilon_spec (exists.intro true (or.inl rfl))

lemma v_def : V v :=
epsilon_spec (exists.intro false (or.inl rfl))
-- END

end

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:

import logic.eq
open classical eq.ops

section
parameter  p : Prop

definition U (x : Prop) : Prop := x = true ∨ p
definition V (x : Prop) : Prop := x = false ∨ p

noncomputable definition u := epsilon U
noncomputable definition v := epsilon V

lemma u_def : U u :=
epsilon_spec (exists.intro true (or.inl rfl))

lemma v_def : V v :=
epsilon_spec (exists.intro false (or.inl rfl))

-- BEGIN
lemma not_uv_or_p : ¬(u = v) ∨ p :=
or.elim u_def
  (assume Hut : u = true,
    or.elim v_def
      (assume Hvf : v = false,
        have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
        or.inl Hne)
      (assume Hp : p, or.inr Hp))
  (assume Hp : p, or.inr Hp)
-- END

end

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.

import logic.eq
open classical eq.ops

section
parameter  p : Prop

definition U (x : Prop) : Prop := x = true ∨ p
definition V (x : Prop) : Prop := x = false ∨ p

noncomputable definition u := epsilon U
noncomputable definition v := epsilon V

lemma u_def : U u :=
epsilon_spec (exists.intro true (or.inl rfl))

lemma v_def : V v :=
epsilon_spec (exists.intro false (or.inl rfl))

lemma not_uv_or_p : ¬(u = v) ∨ p :=
or.elim u_def
  (assume Hut : u = true,
    or.elim v_def
      (assume Hvf : v = false,
        have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
        or.inl Hne)
      (assume Hp : p, or.inr Hp))
  (assume Hp : p, or.inr Hp)

-- BEGIN
lemma p_implies_uv : p → u = v :=
assume Hp : p,
have Hpred : U = V, from
  funext (take x : Prop,
    have Hl : (x = true ∨ p) → (x = false ∨ p), from
      assume A, or.inr Hp,
    have Hr : (x = false ∨ p) → (x = true ∨ p), from
      assume A, or.inr Hp,
    show (x = true ∨ p) = (x = false ∨ p), from
      propext (iff.intro Hl Hr)),
have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
show u = v, from H'
-- END

end

Putting these last two facts together yields the desired conclusion:

import logic.eq
open classical eq.ops

section
parameter  p : Prop

definition U (x : Prop) : Prop := x = true ∨ p
definition V (x : Prop) : Prop := x = false ∨ p

noncomputable definition u := epsilon U
noncomputable definition v := epsilon V

lemma u_def : U u :=
epsilon_spec (exists.intro true (or.inl rfl))

lemma v_def : V v :=
epsilon_spec (exists.intro false (or.inl rfl))

lemma not_uv_or_p : ¬(u = v) ∨ p :=
or.elim u_def
  (assume Hut : u = true,
    or.elim v_def
      (assume Hvf : v = false,
        have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
        or.inl Hne)
      (assume Hp : p, or.inr Hp))
  (assume Hp : p, or.inr Hp)

lemma p_implies_uv : p → u = v :=
assume Hp : p,
have Hpred : U = V, from
  funext (take x : Prop,
    have Hl : (x = true ∨ p) → (x = false ∨ p), from
      assume A, or.inr Hp,
    have Hr : (x = false ∨ p) → (x = true ∨ p), from
      assume A, or.inr Hp,
    show (x = true ∨ p) = (x = false ∨ p), from
      propext (iff.intro Hl Hr)),
have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
show u = v, from H'

-- BEGIN
theorem EM : p ∨ ¬p :=
have H : ¬(u = v) → ¬p, from mt p_implies_uv,
or.elim not_uv_or_p
  (assume Hne : ¬(u = v), or.inr (H Hne))
  (assume Hp : p, or.inl Hp)
-- END

end

Consequences of excluded middle include double-negation elimination, proof by cases, and proof by contradiction, all of which are described in Section Classical Logic.

The law of the excluded middle and propositional extensionality imply propositional completeness:

open classical

namespace hide

-- BEGIN
theorem prop_complete (a : Prop) : a = true ∨ a = false :=
or.elim (em a)
  (λ t, or.inl (propext (iff.intro (λ h, trivial) (λ h, t))))
  (λ f, or.inr (propext (iff.intro (λ h, absurd h f) (λ h, false.elim h))))
-- END

end hide

Propositional Decidability

Taken together, the law of the excluded middle and the axiom of indefinite description imply that every proposition is decidable. The following is the contained in logic.choice:

open classical decidable inhabited nonempty

namespace hide

-- BEGIN
noncomputable definition decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) :=
inhabited_of_nonempty
  (or.elim (em a)
    (assume Ha, nonempty.intro (inl Ha))
    (assume Hna, nonempty.intro (inr Hna)))

noncomputable definition prop_decidable [instance] (a : Prop) : decidable a :=
arbitrary (decidable a)
-- END

end hide

The definition decidable_inhabited uses the law of the excluded middle to show that decidable a is inhabited for any a. It is marked as an instance, and is silently used for for synthesizing the implicit argument in arbitrary (decidable a).

As an example, we use some to prove that if f : A → B is injective and A is inhabited, then f has a left inverse. To define the left inverse linv, we use the “dependent if-then-else” expression. Recall that if h : c then t else e is notation for dite c (λ h : c, t) (λ h : ¬ c, e). In the definition of linv, the strong_indefinite_description 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. From a classical point of view, linv is a function. From a constructive point of view, it is unacceptable; since there is no way to implement such a function in general, the construction is not informative.

open classical function

noncomputable definition linv {A B : Type} [h : inhabited A] (f : A → B) : B → A :=
λ b : B, if ex : (∃ a : A, f a = b) then some ex else arbitrary A

theorem has_left_inverse_of_injective {A B : Type} {f : A → B}
        : inhabited A → injective f → ∃ g, g ∘ f = id :=
assume h   : inhabited A,
assume inj : ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂,
have is_linv  : (linv f) ∘ f = id, from
  funext (λ a,
    assert ex  : ∃ a₁ : A, f a₁ = f a,   from exists.intro a rfl,
    have   feq : f (some ex) = f a,      from !some_spec,
    calc linv f (f a) = some ex   :  dif_pos ex
               ...    = a         :  inj _ _ feq),
exists.intro (linv f) is_linv

Constructive Choice

In the standard library, we say a type A is encodable if there are functions f : A → nat and g : nat → option A such that for all a : A, g (f a) = some a. Here is the precise definition:

namespace hide
open option
-- BEGIN
structure encodable [class] (A : Type) :=
(encode : A → nat) (decode : nat → option A) (encodek : ∀ a, decode (encode a) = some a)
-- END

end hide

The standard library shows that indefinite_description axiom is actually a theorem for any encodable type A and decidable predicate p : A → Prop. It provides the following definition and theorem, which are concrete realizations of some and some_spec, respectively.

import data.encodable
open encodable subtype
-- BEGIN
check @choose
-- choose : Π {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p], (∃ (x : A), p x) → A
check @choose_spec
-- choose_spec : ∀ {A : Type} {p : A → Prop} [c : encodable A] [d : decidable_pred p] (ex : ∃ (x : A), p x), p (choose ex)
-- END

The construction is straightforward: it finds a : A satisfying p by enumerating the elements of A and testing whether they satisfy p or not. We can show that this search always terminates because we have the assumption ∃ (x : A), p x.

We can use this to provide a constructive version of the theorem has_left_inverse_of_injective. We remark this is not the only possible version. The constructive version contains more hypotheses than the classical version. In Bishop’s terminology, it avoids “pseudo-generality.” Considering the classical construction, it is clear that once we have choose, we can construct the left inverse as long as we can decide whether b is in the image of a function f : A → B.

import data.encodable
open encodable function

section
  parameters {A B : Type}
  parameter  (f : A → B)
  parameter  [inhA : inhabited A]
  parameter  [dex  : ∀ b, decidable (∃ a, f a = b)]
  parameter  [encA : encodable A]
  parameter  [deqB : decidable_eq B]
  include inhA dex encA deqB

  definition finv : B → A :=
  λ b : B, if ex : (∃ a, f a = b) then choose ex else arbitrary A

  theorem has_left_inverse_of_injective : injective f → has_left_inverse f :=
  assume inj : ∀ a₁ a₂, f a₁ = f a₂ → a₁ = a₂,
  have is_linv : ∀ a, finv (f a) = a, from
    (take a,
      assert ex  : ∃ a₁, f a₁ = f a, from exists.intro a rfl,
      have   feq : f (choose ex) = f a, from !choose_spec,
      calc finv (f a) = choose ex :  dif_pos ex
               ...    = a         :  inj _ _ feq),
  exists.intro finv is_linv
end

The argument is essentially the same as the classical one; we have simply replaced the classical some with the constructive choice function choose, and added three extra hypotheses: dex, encA and deqB. The first one makes sure we can decide whether a value b is in the image of f or not, and the last two are needed to use choose.

The standard library contains many encodable types and shows that many types have decidable equality. The hypothesis dex can be satisfied in many cases. For example, it is trivially satisfied if f is surjective. It is also satisfied whenever A is finite.

import data.encodable
open encodable function

-- BEGIN
section
  parameters {A B : Type} (f : A → B)

  definition decidable_in_image_of_surjective : surjective f → ∀ b, decidable (∃ a, f a = b) :=
  assume s : surjective f, take b,
  decidable.inl (s b)

  definition decidable_in_image_of_fintype_of_deceq [instance]
             [finA : fintype A] [deqB : decidable_eq B] : ∀ b, decidable (∃ a, f a = b) :=
  take b, decidable_exists_finite
end
-- END

Tracking used axioms

The Lean standard library contains only 3 axioms: quot.sound, propext and strong_indefinite_description. Most of the library depends only on the first two. The command print axioms displays all axioms that have been asserted/imported into the current logical context. Similarly, the command print axioms decl_name prints all axioms the declaration decl_name depends on.

IMPORTANT: in the Lean web version, we erase the proof of most theorems. The idea is to reduce the size of the file that must be downloaded to run Lean on your web browser. So, the result of the print axioms commands is not precise on the web version. Please use the Lean native application if you are interested in using these commands.

import data.finset data.set
-- BEGIN
print axioms
print axioms nat.add
print axioms finset.union
print axioms set.empty_union
print axioms classical.some
-- END