4.1. The Universal Quantifier🔗

Notice that if α is any type, we can represent a unary predicate p on α as an object of type α → Prop. In that case, given x : α, p x denotes the assertion that p holds of x. Similarly, an object r : α → α → Prop denotes a binary relation on α: given x y : α, r x y denotes the assertion that x is related to y.

The universal quantifier, ∀ x : α, p x is supposed to denote the assertion that “for every x : α, p x” holds. As with the propositional connectives, in systems of natural deduction, “forall” is governed by an introduction and elimination rule. Informally, the introduction rule states:

Given a proof of p x, in a context where x : α is arbitrary, we obtain a proof ∀ x : α, p x.

The elimination rule states:

Given a proof ∀ x : α, p x and any term t : α, we obtain a proof of p t.

As was the case for implication, the propositions-as-types interpretation now comes into play. Remember the introduction and elimination rules for dependent arrow types:

Given a term t of type β x, in a context where x : α is arbitrary, we have (fun x : α => t) : (x : α) → β x.

The elimination rule states:

Given a term s : (x : α) → β x and any term t : α, we have s t : β t.

In the case where p x has type Prop, if we replace (x : α) → β x with ∀ x : α, p x, we can read these as the correct rules for building proofs involving the universal quantifier.

The Calculus of Constructions therefore identifies dependent arrow types with forall-expressions in this way. If p is any expression, ∀ x : α, p is nothing more than alternative notation for (x : α) → p, with the idea that the former is more natural than the latter in cases where p is a proposition. Typically, the expression p will depend on x : α. Recall that, in the case of ordinary function spaces, we could interpret α → β as the special case of (x : α) → β in which β does not depend on x. Similarly, we can think of an implication p → q between propositions as the special case of ∀ x : p, q in which the expression q does not depend on x.

Here is an example of how the propositions-as-types correspondence gets put into practice.

As a notational convention, we give the universal quantifier the widest scope possible, so parentheses are needed to limit the quantifier over x to the hypothesis in the example above. The canonical way to prove ∀ y : α, p y is to take an arbitrary y, and prove p y. This is the introduction rule. Now, given that h has type ∀ x : α, p x ∧ q x, the expression h y has type p y ∧ q y. This is the elimination rule. Taking the left conjunct gives the desired conclusion, p y.

Remember that expressions which differ up to renaming of bound variables are considered to be equivalent. So, for example, we could have used the same variable, x, in both the hypothesis and conclusion, and instantiated it by a different variable, z, in the proof:

As another example, here is how we can express the fact that a relation, r, is transitive:

trans_r : ∀ (x y z : α), r x y → r y z → r x z

trans_r a b c : r a b → r b c → r a c

trans_r a b c hab : r b c → r a c

trans_r a b c hab hbc : r a c

Think about what is going on here. When we instantiate trans_r at the values a b c, we end up with a proof of r a b → r b c → r a c. Applying this to the “hypothesis” hab : r a b, we get a proof of the implication r b c → r a c. Finally, applying it to the hypothesis hbc yields a proof of the conclusion r a c.

In situations like this, it can be tedious to supply the arguments a b c, when they can be inferred from hab hbc. For that reason, it is common to make these arguments implicit:

trans_r : r ?m.4 ?m.5 → r ?m.5 ?m.6 → r ?m.4 ?m.6

trans_r hab : r b ?m.6 → r a ?m.6

trans_r hab hbc : r a c

The advantage is that we can simply write trans_r hab hbc as a proof of r a c. A disadvantage is that Lean does not have enough information to infer the types of the arguments in the expressions trans_r and trans_r hab. The output of the first #check command is r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3, indicating that the implicit arguments are unspecified in this case.

Here is an example of how we can carry out elementary reasoning with an equivalence relation:

To get used to using universal quantifiers, you should try some of the exercises at the end of this section.

It is the typing rule for dependent arrow types, and the universal quantifier in particular, that distinguishes Prop from other types. Suppose we have α : Sort i and β : Sort j, where the expression β may depend on a variable x : α. Then (x : α) → β is an element of Sort (imax i j), where imax i j is the maximum of i and j if j is not 0, and 0 otherwise.

The idea is as follows. If j is not 0, then (x : α) → β is an element of Sort (max i j). In other words, the type of dependent functions from α to β “lives” in the universe whose index is the maximum of i and j. Suppose, however, that β is of Sort 0, that is, an element of Prop. In that case, (x : α) → β is an element of Sort 0 as well, no matter which type universe α lives in. In other words, if β is a proposition depending on α, then ∀ x : α, β is again a proposition. This reflects the interpretation of Prop as the type of propositions rather than data, and it is what makes Prop impredicative.

The term “predicative” stems from foundational developments around the turn of the twentieth century, when logicians such as Poincaré and Russell blamed set-theoretic paradoxes on the “vicious circles” that arise when we define a property by quantifying over a collection that includes the very property being defined. Notice that if α is any type, we can form the type α → Prop of all predicates on α (the “power type of α”). The impredicativity of Prop means that we can form propositions that quantify over α → Prop. In particular, we can define predicates on α by quantifying over all predicates on α, which is exactly the type of circularity that was once considered problematic.

4.2. Equality🔗

Let us now turn to one of the most fundamental relations defined in Lean's library, namely, the equality relation. In the chapter on inductive types, we will explain how equality is defined from the primitives of Lean's logical framework. In the meanwhile, here we explain how to use it.

Of course, a fundamental property of equality is that it is an equivalence relation:

Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

We can make the output easier to read by telling Lean not to insert the implicit arguments (which are displayed here as metavariables).

@Eq.refl : ∀ {α : Sort u} (a : α), a = a

@Eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a

@Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c

The inscription .{u} tells Lean to instantiate the constants at the universe u.

Thus, for example, we can specialize the example from the previous section to the equality relation:

We can also use the projection notation:

Reflexivity is more powerful than it looks. Recall that terms in the Calculus of Constructions have a computational interpretation, and that the logical framework treats terms with a common reduct as the same. As a result, some nontrivial identities can be proved by reflexivity:

This feature of the framework is so important that the library defines a notation rfl for Eq.refl _:

Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given h1 : a = b and h2 : p a, we can construct a proof for p b using substitution: Eq.subst h1 h2.

The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t.

The rule Eq.subst is used to define the following auxiliary rules, which carry out more explicit substitutions. They are designed to deal with applicative terms, that is, terms of form s t. Specifically, congrArg can be used to replace the argument, congrFun can be used to replace the term that is being applied, and congr can be used to replace both at once.

Lean's library contains a large number of common identities, such as these:

Note that Nat.mul_add and Nat.add_mul are alternative names for Nat.left_distrib and Nat.right_distrib, respectively. The properties above are stated for the natural numbers (type Nat).

Here is an example of a calculation in the natural numbers that uses substitution combined with associativity and distributivity.

Notice that the second implicit parameter to Eq.subst, which provides the context in which the substitution is to occur, has type α → Prop. Inferring this predicate therefore requires an instance of higher-order unification. In full generality, the problem of determining whether a higher-order unifier exists is undecidable, and Lean can at best provide imperfect and approximate solutions to the problem. As a result, Eq.subst doesn't always do what you want it to. The macro h ▸ e uses more effective heuristics for computing this implicit parameter, and often succeeds in situations where applying Eq.subst fails.

Because equational reasoning is so common and important, Lean provides a number of mechanisms to carry it out more effectively. The next section offers syntax that allow you to write calculational proofs in a more natural and perspicuous way. But, more importantly, equational reasoning is supported by a term rewriter, a simplifier, and other kinds of automation. The term rewriter and simplifier are described briefly in the next section, and then in greater detail in the next chapter.

4.3. Calculational Proofs🔗

A calculational proof is just a chain of intermediate results that are meant to be composed by basic principles such as the transitivity of equality. In Lean, a calculational proof starts with the keyword calc, and has the following syntax:

calc
  <expr>_0  'op_1'  <expr>_1  ':='  <proof>_1
  '_'       'op_2'  <expr>_2  ':='  <proof>_2
  ...
  '_'       'op_n'  <expr>_n  ':='  <proof>_n

Note that the calc relations all have the same indentation. Each <proof>_i is a proof for <expr>_{i-1} op_i <expr>_i.

We can also use _ in the first relation (right after <expr>_0) which is useful to align the sequence of relation/proof pairs:

calc <expr>_0
    '_' 'op_1' <expr>_1 ':=' <proof>_1
    '_' 'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_' 'op_n' <expr>_n ':=' <proof>_n

Here is an example:

This style of writing proofs is most effective when it is used in conjunction with the simp and rw tactics, which are discussed in greater detail in the next chapter. For example, using rw for rewrite, the proof above could be written as follows:

Essentially, the rw tactic uses a given equality (which can be a hypothesis, a theorem name, or a complex term) to “rewrite” the goal. If doing so reduces the goal to an identity t = t, the tactic applies reflexivity to prove it.

Rewrites can be applied sequentially, so that the proof above can be shortened to this:

Or even this:

The simp tactic, instead, rewrites the goal by applying the given identities repeatedly, in any order, anywhere they are applicable in a term. It also uses other rules that have been previously declared to the system, and applies commutativity wisely to avoid looping. As a result, we can also prove the theorem as follows:

We will discuss variations of rw and simp in the next chapter.

The calc command can be configured for any relation that supports some form of transitivity. It can even combine different relations.