04_Quantifiers_and_Equality.org

Theorem Proving in Lean

Quantifiers and Equality

The last chapter introduced you to methods that construct proofs of statements involving the propositional connectives. In this chapter, we extend the repertoire of logical constructions to include the universal and existential quantifiers, and the equality relation.

The Universal Quantifier

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

The universal quantifier, ∀x : A, p x is supposed to denote the assertion that “for every x : A, 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 : A is arbitrary, we obtain a proof ∀x : A, p x.

The elimination rule states:

Given a proof ∀x : A, p x and any term t : A, 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 Pi types:

Given a term t of type B x, in a context where x : A is arbitrary, we have (λx : A, t) : Πx : A, B x.

The elimination rule states:

Given a term s : Πx : A, B x and any term t : A, we have s t : B t.

In the case where p x has type Prop, if we replace Πx : A, B x with ∀x : A, p x, we can read these as the correct rules for building proofs involving the universal quantifier.

The Calculus of Inductive Constructions therefore identifies Π and ∀ in this way. If p is any expression, ∀x : A, p is nothing more than alternative notation for Πx : A, p, with the idea is that the former is more natural in cases where where p is a proposition. Typically, the expression p will depend on x : A. Recall that, in the case of ordinary function spaces, we could interpret A → B as the special case of Πx : A, B in which B 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.

import logic

section
  variables (A : Type) (p q : A → Prop)

  example : (∀x : A, p x ∧ q x) → ∀y : A, p y  :=
  assume H : ∀x : A, p x ∧ q x,
  take y : A,
  show p y, from and.elim_left (H y)
end

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 : A, p y is to take an arbitrary y, and prove p y. This is the introduction rule. Now, given that H has type ∀x : A, p x ∧ q x, 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, or chosen the variable z instead of y in the proof:

import logic

section
  variables (A : Type) (p q : A → Prop)

-- BEGIN
  example : (∀x : A, p x ∧ q x) → ∀y : A, p y  :=
  assume H : ∀x : A, p x ∧ q x,
  take z : A,
  show p z, from and.elim_left (H z)
-- END
end

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

section
  variables (A : Type) (r : A → A → Prop)
  variable trans_r : ∀x y z, r x y → r y z → r x z

  variables (a b c : A)
  variables (Hab : r a b) (Hbc : r b c)

  check trans_r
  check trans_r a b c
  check trans_r a b c Hab
  check trans_r a b c Hab Hbc
end

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 conlusion r a c.

In situtations 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:

section
  variables (A : Type) (r : A → A → Prop)
  variable (trans_r : ∀{x y z}, r x y → r y z → r x z)

  variables (a b c : A)
  variables (Hab : r a b) (Hbc : r b c)

  check trans_r
  check trans_r Hab
  check trans_r Hab Hbc
end

The advantage is that we can simply write trans_r Hab Hbc as a proof of r a c. The 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. In the output of the check command, an expression like ?z A r trans_r a b c Hab Hbc indicates an arbitrary value, that may depend on any of the values listed (in this case, all the variables in the section).

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

section
  variables (A : Type) (r : A → A → Prop)

  variable refl_r : ∀x, r x x
  variable symm_r : ∀{x y}, r x y → r y x
  variable trans_r : ∀{x y z}, r x y → r y z → r x z

  example (a b c d : A) (Hab : r a b) (Hcb : r c b) (Hcd : r c d) : r a d :=
  trans_r (trans_r Hab (symm_r Hcb)) Hcd
end

You might want to try to prove some of these equivalences:

import logic

section
  variables (A : Type) (p q : A → Prop)

  example : (∀x, p x ∧ q x) ↔ (∀x, p x) ∧ (∀x, q x) := sorry
  example : (∀x, p x → q x) → (∀x, p x) → (∀x, q x) := sorry
  example : (∀x, p x) ∨ (∀x, q x) → ∀x, p x ∨ q x := sorry
end

You should also try to understand why the reverse implication is not derivable in the last example.

It is often possible to bring a component outside a universal quantifier, when it does not depend on the quantified variable (one direction of the second of these requires classical logic):

section
  variables (A : Type) (p q : A → Prop)
  variable r : Prop

  example : A → (∀x : A, r) ↔ r := sorry
  example : (∀x, p x ∨ r) ↔ (∀x, p x) ∨ r := sorry
  example : (∀x, r → p x) ↔ (r → ∀x, p x) := sorry
end

As a final example, consider the “barber paradox”, that is, the claim that in a certain town there is a (male) barber that shaves all and only the men who do not shave themselves. Prove that this implies a contradiction:

section
  variables (men : Type) (barber : men) (shaves : men → men → Prop)

  example (H : ∀x : men, shaves barber x ↔ ¬shaves x x) : false := sorry
end

Equality

Let us now turn to one of the most fundamental relations defined in Lean’s library, namely, the equality relation. In the next chapter, 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:

import logic.eq

check eq.refl
check eq.symm
check eq.trans

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

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
eq.trans (eq.trans Hab (eq.symm Hcb)) Hcd

If we “open” the eq namespace, the names become shorter:

open eq

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
trans (trans Hab (symm Hcb)) Hcd

Lean even defines convenient notation for writing proofs like this:

open eq.ops

example (A : Type) (a b c d : A) (Hab : a = b) (Hcb : c = b) (Hcd : c = d) :
  a = d :=
Hab ⬝ Hcb⁻¹ ⬝ Hcd

You can use \tr to enter the transitivity dot, and \sy to enter the inverse/symmetry symbol.

Reflexivity is more powerful than it looks. Recall that terms in the Calculus of Inductive 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:

import data.nat data.prod
open nat prod

example (A B : Type) (f : A → B) (a : A) : (λx, f x) a = f a := eq.refl _
example (A B : Type) (a : A) (b : A) : pr1 (a, b) = a := eq.refl _
example : 2 + 3 = 5 := eq.refl _

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

import data.nat data.prod
open nat prod
-- BEGIN
example (A B : Type) (f : A → B) (a : A) : (λx, f x) a = f a := rfl
example (A B : Type) (a : A) (b : A) : pr1 (a, b) = a := rfl
example : 2 + 3 = 5 := rfl
-- END

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.

open eq.ops
-- BEGIN
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2

example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
H1 ▸ H2
-- END

The triangle in the second presentation is, once again, made available by opening eq.ops, and you can use \t to enter it. The term H1 ▸ H2 is just notation for eq.subst H1 H2. This notation is used extensively in the Lean standard library.

Here is an example of a calculation in the natural numbers that uses substitution combined with associativity, commutativity, and distributivity of the natural numbers. Of course, carrying out such calculations require being able to invoke such supporting theorems. You can find a number of identities involving the natural numbers in the associated library files, for example, in the module data.nat.basic. In the next chapter, we will have more to say about how to find theorems in Lean’s library.

import data.nat
open nat eq.ops

example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
have H1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y, from !mul.left_distrib,
have H2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y),
  from !mul.right_distrib ▸ !mul.right_distrib ▸ H1,
!add.assoc⁻¹ ▸ H2

Remember that the exclamation mark adds implicit arguments as necessary. In the statement of the example, remember that addition implicitly associates to the left, so the last step of the proof puts the right-hand side of H2 in the required form.

It is often important to be able to carry out substitutions like this by hand, but it is tedious to prove examples like the one above in this way. Fortunately, Lean provides an environment that provides better support for such calculations, which we will turn to now.

The Calculation Environment

A calculational proof is just a chain of intermediate results that are meant to be composed by basic principles such as the transitivity of ===. In Lean, a calculation 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

Each <proof>_i is a proof for <expr>_{i-1} op_i <expr>_i. The <proof>_i may also be of the form { <pr> }, where <pr> is a proof for some equality a = b. The form { <pr> } is just syntactic sugar for eq.subst <pr> (refl <expr>_{i-1}) In other words, we are claiming we can obtain <expr>_i by replacing a with b in <expr>_{i-1}.

Here is an example:

import data.nat
open nat

section
  variables (a b c d e : nat)
  variable H1 : a = b
  variable H2 : b = c + 1
  variable H3 : c = d
  variable H4 : e = 1 + d

  theorem T : a = e :=
  calc
    a     = b      : H1
      ... = c + 1  : H2
      ... = d + 1  : {H3}
      ... = 1 + d  : add.comm d 1
      ... =  e     : eq.symm H4
end

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

import data.nat
open nat

theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 :=
calc
  a     = b      : H1
    ... = c + 1  : H2
    ... = succ c : add_one c
    ... ≠ 0      : succ_ne_zero c

Lean offers some nice additional features. If the justification for a line of a calculations proof is foo, Lean will try adding implicit arguments if foo alone fails to do the job. If that doesn’t work, Lean will try the symmetric version, foo⁻¹, again adding arguments if necessary. If that doesn’t work, Lean proceeds to try {foo} and {foo⁻¹}, again, adding arguments if necessary. This can simplify the presentation of a calc proof considerably. Consider, for example, the following proof of the identity in the last section:

import data.nat
open nat

-- BEGIN
example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
calc
  (x + y) * (x + y) = (x + y) * x + (x + y) * y  : mul.left_distrib
    ... = x * x + y * x + (x + y) * y            : mul.right_distrib
    ... = x * x + y * x + (x * y + y * y)        : mul.right_distrib
    ... = x * x + y * x + x * y + y * y          : add.assoc
-- END

As an exercise, we suggest carrying out a similar expansion of (x - y) * (x - y), using the theorems mul_sub_right_distrib and mul_sub_left_distrib in the module data.nat.sub.

The Simplifier

[TO DO: this section needs to be written. Emphasize that the simplifier can be used in conjunction with calc.]

The Existential Quantifier

Finally, consider the existential quantifier, which can be written as either exists x : A, p x or ∃x : A, p x. Both versions are actually notationally convenient abbreviations for a more long-winded expression, Exists (λx : A, p x), defined in Lean’s library.

As you should by now expect, the library includes both an introduction rule and an elimination rule. The introduction rule is straightforward: to prove ∃x : A, p x, it suffices to provide a suitable term t and a proof of p t. Here are some examples:

import data.nat
open nat

example : ∃x, x > 0 :=
have H : 1 > 0, from succ_pos 0,
exists.intro 1 H

example (x : ℕ) (H : x > 0) : ∃y, y < x :=
exists.intro 0 H

example (x y z : ℕ) (Hxy : x < y) (Hyz : y < z) : ∃w, x < w ∧ w < z :=
exists.intro y (and.intro Hxy Hyz)

check @exists.intro

Note that exists.intro has implicit arguments: Lean has to infer the predicate p : A → Prop in the conclusion ∃x, p x. This is not a trivial affair. For example, if we have have Hg : g 0 0 = 0 and write exists.intro 0 Hg, there are many possible values for the predicate p, corresponding to the theorems ∃x, g x x = x, ∃x, g x x = 0, ∃x, g x 0 = x, etc. Lean uses the context to infer which one is appropriate. This is illustrated in the following example, in which we set the option pp.implicit to true to ask Lean’s pretty-printer to show the implicit arguments.

import data.nat
open nat

section
  variable g : ℕ → ℕ → ℕ
  variable Hg : g 0 0 = 0

  theorem gex1 : ∃ x, g x x = x := exists.intro 0 Hg
  theorem gex2 : ∃ x, g x 0 = x := exists.intro 0 Hg
  theorem gex3 : ∃ x, g 0 0 = x := exists.intro 0 Hg
  theorem gex4 : ∃ x, g x x = 0 := exists.intro 0 Hg

  set_option pp.implicit true  -- display implicit arguments
  check gex1
  check gex2
  check gex3
  check gex4
end

We can view exists.intro as an information-hiding operation: we are “hiding” the witness to the body of the assertion. The existential elimination rule, exists.elim, performs the opposite operation. It allows us to prove a proposition q from ∃x : A, p x, by showing that q follows from p w for an arbitrary value w. Roughly speaking, since we know there is an x satisfying p x, we can give it a name, say, w. Showing that q follows from p w, where q does not mention w, is tantamount to showing the q follows from the existence of any such x.

(It may be helpful to compare the exists-elimination rule to the or-elimination rule. The assertion ∃x : A, p x can be thought of as a big disjunction of the propositions p a, as a ranges over all the elements of A.)

Notice that exists introduction and elimination are very similar to the sigma introduction sigma.mk and elimination. The difference is that given a : A and h : p a, exists.intro a h has type (∃x : A, p x) : Prop and sigma.mk a h has type (Σx : A, p x) : Type. The similarity between ∃ and Σ is another instance of the Curry-Howard isomorphism.

In the following example, we define even a as ∃b, a = 2*b, and then we show that the sum of two even numbers is an even number.

import data.nat
open nat

definition even (a : nat) := ∃b, a = 2*b

theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
exists.elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
exists.elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
  exists.intro (w1 + w2)
    (calc
      a + b = 2*w1 + b      : Hw1
        ... = 2*w1 + 2*w2   : Hw2
        ... = 2*(w1 + w2)   : mul.left_distrib)))

Lean provides syntactic sugar for exists.elim, with expressions of the form obtain _, from _, _. With this syntax, the example above can be presented in a more natural way: :

import data.nat
open nat

definition even (a : nat) := ∃b, a = 2*b

theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) :
  even (a + b) :=
obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
obtain (w2 : nat) (Hw2 : b = 2*w2), from H2,
exists.intro (w1 + w2)
  (calc
    a + b = 2*w1 + b      : Hw1
      ... = 2*w1 + 2*w2   : Hw2
      ... = 2*(w1 + w2)   : mul.left_distrib)

What follows are some common identities involving the existential quantifier. We encourage you to prove as many as you can. Be careful: many of them are nonconstructive, and require the use of the law of the excluded middle.

import logic

section
  variables (A : Type) (p q : A → Prop)
  variable r : Prop

  example : (∃x, p x ∨ q x) ↔ (∃x, p x) ∨ (∃x, q x) := sorry

  example : (∃x : A, r) ↔ r := sorry
  example : (∃x, p x ∧ r) ↔ (∃x, p x) ∧ r := sorry
  example : (∀x, p x → r) ↔ (∃x, p x) → r := sorry
  example : (∃x, p x → r) ↔ (∀x, p x → r) := sorry
  example : (∃x, r → p x) ↔ (r → ∃x, p x) := sorry

  example : (∃x, p x) ↔ (∀x, ¬p x) := sorry
  example : (∀x, p x) ↔ (∃x, ¬p x) := sorry
  example : (¬∃x, p x) ↔ (∀x, ¬p x) := sorry
  example : (¬∀x, p x) ↔ (∃x, ¬p x) := sorry
end