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 an 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 that the former is more natural than the latter 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.

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)

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, 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, or chosen the variable z instead of y in the proof:

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

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

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          -- ∀ (x y z : A), r x y → r y z → r x z
check trans_r a b c
check trans_r a b c Hab
check trans_r a b c Hab Hbc

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:

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

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. The output of the check command contains expressions like ?z A r trans_r a b c Hab Hbc. Such an expression indicates an arbitrary value, that may depend on any of the values listed (in this case, all the variables in the local context).

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

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

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

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

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):

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

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:

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

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

It is the typing rule for Pi types, and the universal quantifier in particular, that distinguishes Prop from other types. Suppose we have A : Type.{i} and B : Type.{j}, where the expression B may depend on a variable x : A. Then Π x : A, B is an element of Type.{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 : A, B is an element of Type.{max i j}. In other words, the type of dependent functions from A to B “lives” in the universe with smallest index greater-than or equal to the indices of the universes of A and B. Suppose, however, that B is of Type.{0}, that is, an element of Prop. In that case, Π x : A, B is an element of Type.{0} as well, no matter which type universe A lives in. In other words, if B is a proposition depending on A, then ∀ x : A, B 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. In contrast to the standard kernel, such a Prop is absent from Lean’s kernel for homotopy type theory.

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 A is any type, we can form the type A → Prop of all predicates on A (the “power type of A”). The impredicativity of Prop means that we can form propositions that quantify over A → Prop. In particular, we can define predicates on A by quantifying over all predicates on A, which is exactly the type of circularity that was once considered problematic.

Equality

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

check eq.refl    -- ∀ (a : ?A), a = a
check eq.symm    -- ?a = ?b → ?b = ?a
check eq.trans   -- ?a = ?b → ?b = ?c → ?a = ?c

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

variables (A : Type) (a b c d : A)
premises (Hab : a = b) (Hcb : c = b) (Hcd : c = d)

example : a = d :=
eq.trans (eq.trans Hab (eq.symm Hcb)) Hcd

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

variables (A : Type) (a b c d : A)
premises (Hab : a = b) (Hcb : c = b) (Hcd : c = d)

-- BEGIN
open eq

example : a = d := trans (trans Hab (symm Hcb)) Hcd
-- END

Lean even defines convenient notation for writing proofs like this:

variables (A : Type) (a b c d : A)
premises (Hab : a = b) (Hcb : c = b) (Hcd : c = d)

-- BEGIN
open eq.ops

example : 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

variables (A B : Type)

example (f : A → B) (a : A) : (λ x, f x) a = f a := eq.refl _
example (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

variables (A B : Type)

-- BEGIN
example (f : A → B) (a : A) : (λ x, f x) a = f a := rfl
example (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 algebra

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 !left_distrib,
have H2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y),
  from (right_distrib x y x) ▸ !right_distrib ▸ H1,
!add.assoc⁻¹ ▸ H2

The exclamation mark infers explicit arguments to a theorem from the context. For more information, see Section More on Implicit Arguments. 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 equality. 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> (eq.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 algebra

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

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 algebra

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 calculational 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 algebra

-- 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  : left_distrib
    ... = x * x + y * x + (x + y) * y            : right_distrib
    ... = x * x + y * x + (x * y + y * y)        : 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 in the appropriate order the theorems left_distrib, mul.comm and add.comm and the theorems mul_sub_right_distrib and add_sub_add_left in the file data.nat.sub. Note that this exercise is slightly more involved than the previous example, because the subtraction on natural numbers is truncated, so that n - m is equal to 0 when m is greater than or equal to n.

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

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

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. If q does not mention w, then showing that q follows from p 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 algebra

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

theorem even_plus_even {a b : nat} (H1 : is_even a) (H2 : is_even b) : is_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)   : left_distrib)))

Lean provides syntactic sugar for exists.elim. The expression

obtain <var1> <var2>, from <expr1>,
<expr2>

translates to exists.elim <expr1> (λ <var1> <var2>, <expr2>). With this syntax, the example above can be presented in a more natural way:

import data.nat
open nat algebra

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

-- BEGIN
theorem even_plus_even {a b : nat} (H1 : is_even a) (H2 : is_even b) :
  is_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)   : left_distrib)
-- END

Just as the constructive “or” is stronger than the classical “or,” so, too, is the constructive “exists” stronger than the classical “exists”. For example, the following implication requires classical reasoning because, from a constructive standpoint, knowing that it is not the case that every x satisfies ¬ p is not the same as having a particular x that satisfies p.

open classical

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

example (H : ¬ ∀ x, ¬ p x) : ∃ x, p x :=
by_contradiction
  (assume H1 : ¬ ∃ x, p x,
    have H2 : ∀ x, ¬ p x, from
      take x,
      assume H3 : p x,
      have H4 : ∃ x, p x, from exists.intro x H3,
      show false, from H1 H4,
    show false, from H H2)

What follows are some common identities involving the existential quantifier. We encourage you to prove as many as you can. We are also leaving it to you to determine which are nonconstructive, and hence require some form of classical reasoning.

open classical

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

example : (∃ x : A, r) → r := sorry
example : r → (∃ x : A, r) := sorry
example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r := sorry
example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q 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

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

Notice that the declaration variable a : A amounts to the assumption that there is at least one element of type A. This assumption is needed in the second example, as well as in the last two.

Here are solutions to two of the more difficult ones:

open classical

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

-- BEGIN
example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
iff.intro
  (assume H : ∃ x, p x ∨ q x,
    obtain a (H1 : p a ∨ q a), from H,
    or.elim H1
      (assume Hpa : p a, or.inl (exists.intro a Hpa))
      (assume Hqa : q a, or.inr (exists.intro a Hqa)))
  (assume H : (∃ x, p x) ∨ (∃ x, q x),
    or.elim H
      (assume Hp : ∃ x, p x,
        obtain a Hpa, from Hp,
        exists.intro a (or.inl Hpa))
      (assume Hq : ∃ x, q x,
        obtain a Hqa, from Hq,
        exists.intro a (or.inr Hqa)))

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
  (assume H1 : ∃ x, p x → r,
    assume H2 : ∀ x, p x,
    obtain b (Hb : p b → r), from H1,
    show r, from  Hb (H2 b))
  (assume H1 : (∀ x, p x) → r,
    show ∃ x, p x → r, from
      by_cases
        (assume Hap : ∀ x, p x, exists.intro a (λ H', H1 Hap))
        (assume Hnap : ¬ ∀ x, p x,
          by_contradiction
            (assume Hnex : ¬ ∃ x, p x → r,
              have Hap : ∀ x, p x, from
                take x,
                by_contradiction
                  (assume Hnp : ¬ p x,
                    have Hex : ∃ x, p x → r,
                      from exists.intro x (assume Hp, absurd Hp Hnp),
                    show false, from Hnex Hex),
              show false, from Hnap Hap)))
-- END

More on the Proof Language

We have seen that keywords like assume, take, have, show, and obtain make it possible to write formal proof terms that mirror the structure of informal mathematical proofs. In this section, we discuss some additional features of the proof language that are often convenient.

To start with, we can use anonymous “have” expressions to introduce an auxiliary goal without having to label it. We can refer to the last expression introduced in this way using the keyword this:

import data.nat
open nat algebra

variable f : ℕ → ℕ
premise H : ∀ x : ℕ, f x ≤ f (x + 1)

example : f 0 ≤ f 3 :=
have f 0 ≤ f 1, from H 0,
have f 0 ≤ f 2, from le.trans this (H 1),
show f 0 ≤ f 3, from le.trans this (H 2)

Often proofs move from one fact to the next, so this can be effective in eliminating the clutter of lots of labels.

One can also refer to any element or hypothesis in the context, anonymous or not, by enclosing the type in backticks:

import data.nat
open nat algebra

variable f : ℕ → ℕ
premise H : ∀ x : ℕ, f x ≤ f (x + 1)

-- BEGIN
example : f 0 ≤ f 3 :=
have f 0 ≤ f 1, from H 0,
have f 0 ≤ f 2, from le.trans `f 0 ≤ f 1` (H 1),
show f 0 ≤ f 3, from le.trans `f 0 ≤ f 2` (H 2)
-- END

In the last line, for example, the expression `f 0 ≤ f 2` means “find any element of the context that has type f 0 ≤ f 2.” In other words, we state the assertion rather than name the variable that witnesses its truth. This can be done anywhere later in the proof:

import data.nat
open nat algebra

variable f : ℕ → ℕ
premise H : ∀ x : ℕ, f x ≤ f (x + 1)

-- BEGIN
example : f 0 ≤ f 3 :=
have f 0 ≤ f 1, from H 0,
have f 1 ≤ f 2, from H 1,
have f 2 ≤ f 3, from H 2,
show f 0 ≤ f 3, from le.trans `f 0 ≤ f 1` (le.trans `f 1 ≤ f 2` `f 2 ≤ f 3`)
-- END

The suppose keyword acts as an anonymous assume:

import data.nat
open nat algebra

variable f : ℕ → ℕ
premise H : ∀ x : ℕ, f x ≤ f (x + 1)

-- BEGIN
example : f 0 ≥ f 1 → f 0 = f 1 :=
suppose f 0 ≥ f 1,
show f 0 = f 1, from le.antisymm (H 0) this
-- END

Notice that there is an asymmetry: you can use have with or without a label, but if you do not wish to name the assumption, you must use suppose rather than assume. The reason is that Lean allows us to write assume H to introduce a hypothesis without specifying it, leaving it to the system to infer to relevant assumption. An anonymous assume would thus lead to ambiguities when parsing expressions.

As with the anonymous have, when you use suppose to introduce an assumption, that assumption can also be invoked later in the proof by enclosing it in backticks.

import data.nat
open nat algebra

variable f : ℕ → ℕ
premise H : ∀ x : ℕ, f x ≤ f (x + 1)

-- BEGIN
example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
suppose f 0 ≥ f 1,
suppose f 1 ≥ f 2,
have f 0 ≥ f 2, from le.trans `f 2 ≤ f 1` `f 1 ≤ f 0`,
have f 0 ≤ f 2, from le.trans (H 0) (H 1),
show f 0 = f 2, from le.antisymm this `f 0 ≥ f 2`
-- END

Notice that le.antisymm is the assertion that if a ≤ b and b ≤ a then a = b, and a ≥ b is definitionally equal to b ≤ a.

One can also do an anonymous assume by enclosing the statement in backticks.

import data.nat
open nat algebra

variable f : ℕ → ℕ
premise H : ∀ x : ℕ, f x ≤ f (x + 1)

-- BEGIN
example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
assume `f 0 ≥ f 1`,
assume `f 1 ≥ f 2`,
have f 0 ≥ f 2, from le.trans `f 2 ≤ f 1` `f 1 ≤ f 0`,
have f 0 ≤ f 2, from le.trans (H 0) (H 1),
show f 0 = f 2, from le.antisymm this `f 0 ≥ f 2`
-- END

This is slightly weaker than using suppose, because we can no longer use the identifier this. But the mechanism is more general: it can be used with other binders, like take and obtains.

If more than one element of the context has the named type, the expression is ambiguous:

definition imp_self (p : Prop) : p → p :=
assume `p`, `p`

print imp_self

definition imp_self2 (p : Prop) : p → p → p :=
assume `p` `p`, `p`

print imp_self2

The output shows that in the second example, it is the second argument that is chosen. Using anonymous binders when data is involved looks somewhat odd:

import data.nat
open nat algebra

-- BEGIN
definition idnat : ℕ → ℕ :=
take `ℕ`, `ℕ`

print idnat

definition idnat2 : ℕ → ℕ → ℕ :=
take `ℕ` `ℕ`, `ℕ`

print idnat2
eval idnat2 0 1  -- returns 1
-- END

But with propositions it is usually quite natural. Here is an example of an anonymous binder used with the obtain construction, continuing the examples above.

import data.nat
open nat algebra

-- BEGIN
variable f : ℕ → ℕ

example (H : ∀ x : ℕ, f x ≤ f (x + 1)) (H' : ∃ x, f (x + 1) ≤ f x) :
  ∃ x, f (x + 1) = f x :=
obtain x `f (x + 1) ≤ f x`, from H',
exists.intro x
  (show f (x + 1) = f x, from le.antisymm `f (x + 1) ≤ f x` (H x))
-- END

The following proof that the square root of two is irrational can be found in the standard library. It provides a nice example of the way that proof terms can be structured and made readable using the devices we have discussed here.

import data.nat
open nat
  
theorem sqrt_two_irrational {a b : ℕ} (co : coprime a b) : a^2 ≠ 2 * b^2 :=
assume H : a^2 = 2 * b^2,
have even (a^2),
  from even_of_exists (exists.intro _ H),
have even a,
  from even_of_even_pow this,
obtain (c : ℕ) (aeq : a = 2 * c),
  from exists_of_even this,
have 2 * (2 * c^2) = 2 * b^2,
  by rewrite [-H, aeq, *pow_two, mul.assoc, mul.left_comm c],
have 2 * c^2 = b^2,
  from eq_of_mul_eq_mul_left dec_trivial this,
have even (b^2),
  from even_of_exists (exists.intro _ (eq.symm this)),
have even b,
  from even_of_even_pow this,
have 2 ∣ gcd a b,
  from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
have 2 ∣ (1 : ℕ),
  by rewrite [gcd_eq_one_of_coprime co at this]; exact this,
show false, from absurd `2 ∣ 1` dec_trivial

#