9. First Order Logic in Lean

9.1. Functions, Predicates, and Relations

In the last chapter, we discussed the language of first-order logic. We will see in the course of this book that Lean’s built-in logic is much more expressive; but it includes first-order logic, which is to say, anything that can be expressed (and proved) in first-order logic can be expressed (and proved) in Lean.

Lean is based on a foundational framework called type theory, in which every variable is assumed to range elements of some type. You can think of a type as being a “universe,” or a “domain of discourse,” in the sense of first-order logic.

For example, suppose we want to work with a first-order language with one constant symbol, one unary function symbol, one binary function symbol, one unary relation symbol, and one binary relation symbol. We can declare a new type U (for “universe”) and the relevant symbols as follows:

constant U : Type

constant c : U
constant f : U  U
constant g : U  U  U
constant P : U  Prop
constant R : U  U  Prop

We can then use them as follows:

variables x y : U

#check c
#check f c
#check g x y
#check g x (f c)

#check P (g x (f c))
#check R x y

The #check command tells us that the first four expressions have type U, and that the last two have type Prop. Roughly, this means that the first four expressions correspond to terms of first-order logic, and that the last two correspond to formulas.

Note all the following:

  • A unary function is represented as an object of type U U and a binary function is represented as an object of type U U U, using the same notation as for implication between propositions.
  • We write, for example, f x to denote the result of applying f to x, and g x y to denote the result of applying g to x and y, again just as we did when using modus ponens for first-order logic. Parentheses are needed in the expression g x (f c) to ensure that f c is parsed as a single argument.
  • A unary predicate is presented as an object of type U Prop and a binary function is represented as an object of type U U Prop. You can think of a binary relation R as being a function that assumes two arguments in the universe, U, and returns a proposition.
  • We write P x to denote the assertion that P holds of x, and R x y to denote that R holds of x and y.

You may reasonably wonder what difference there is between a constant and a variable in Lean. The following declarations also work:

variable U : Type

variable c : U
variable f : U  U
variable g : U  U  U
variable P : U  Prop
variable R : U  U  Prop

variables x y : U

#check c
#check f c
#check g x y
#check g x (f c)

#check P (g x (f c))
#check R x y

Although the examples function in much the same way, the constant and variable commands do very different things. The constant command declares a new object, axiomatically, and adds it to the list of objects Lean knows about. In contrast, when it is first executed, the variable command does not create anything. Rather, it tells Lean that whenever we enter an expression using the corresponding identifier, it should create a temporary variable of the corresponding type.

Many types are already declared in Lean’s standard library. For example, there is a type written nat or , that denotes the natural numbers:

#check nat
#check 

You can enter the unicode with \nat or \N. The two expressions mean the same thing.

Using this built-in type, we can model the language of arithmetic, as described in the last chapter, as follows:

namespace hide

constant mul :     
constant add :     
constant square :   
constant even :   Prop
constant odd :   Prop
constant prime :   Prop
constant divides :     Prop
constant lt :     Prop
constant zero : 
constant one : 

end hide

We have used the namespace command to avoid conflicts with identifiers that are already declared in the Lean library. We can again use the #check command to try them out:

variables w x y z : 

#check mul x y
#check add x y
#check square x
#check even x

In fact, all of the functions, predicates, and relations discussed here, except for the “square” function and “prime,” are defined in the core Lean library. They become available to us when we put the commands import data.nat and open nat at the top of a file in Lean.

constant square :   
constant prime :   Prop
constant even :   Prop

variables w x y z : 

#check even (x + y + z)  prime ((x + 1) * y * y)
#check ¬ (square (x + y * z) = w)  x + y < z
#check x < y  even x  even y  x + 1 < y

Here, we declare the constants square and prime axiomatically, but refer to the other operations and predicates in the Lean library. In this book, we will often proceed in this way, telling you explicitly what facts from the library you should use for exercises.

Again, note the following aspects of syntax:

  • In contrast to ordinary mathematical notation, in Lean, functions are applied without parentheses or commas. For example, we write square x and add x y instead of \(\mathit{square}(x)\) and \(\mathit{add}(x, y)\).
  • The same holds for predicates and relations: we write even x and lt x y instead of \(\mathit{even}(x)\) and \(\mathit{lt}(x, y)\), as one might do in symbolic logic.
  • The notation add : indicates that addition assumes two arguments, both natural numbers, and returns a natural number.
  • Similarly, the notation divides : Prop indicates that divides is a binary relation, which assumes two natural numbers as arguments and forms a proposition. In other words, divides x y expresses the assertion that x divides y.

Lean can help us distinguish between terms and formulas. If we #check the expression x + y + 1 in Lean, we are told it has type , which is to say, it denotes a natural number. If we #check the expression even (x + y + 1), we are told that it has type Prop, which is to say, it expresses a proposition.

In Chapter 7 we considered many-sorted logic, where one can have multiple universes. For example, we might want to use first-order logic for geometry, with quantifiers ranging over points and lines. In Lean, we can model this as by introducing a new type for each sort:

variables Point Line : Type
variable  lies_on : Point  Line  Prop

We can then express that two distinct points determine a line as follows:

#check  (p q : Point) (L M : Line),
        p  q  lies_on p L  lies_on q L  lies_on p M  lies_on q M  L = M

Notice that we have followed the convention of using iterated implication rather than conjunction in the antecedent. In fact, Lean is smart enough to infer what sorts of objects p, q, L, and M are from the fact that they are used with the relation on, so we could have written, more simply, this:

#check  p q L M, p  q  lies_on p L  lies_on q L  lies_on p M  lies_on q M  L = M

9.2. Using the Universal Quantifier

In Lean, you can enter the universal quantifier by writing \all. The motivating examples from Section 7.1 are rendered as follows:

constant prime :   Prop
constant even :   Prop
constant odd :   Prop

#check  x, (even x  odd x)  ¬ (even x  odd x)
#check  x, even x  2  x
#check  x, even x  even (x^2)
#check  x, even x  odd (x + 1)
#check  x, prime x  x > 2  odd x
#check  x y z, x  y  y  z  x  z

Remember that Lean expects a comma after the universal quantifier, and gives it the widest scope possible. For example, x, P Q is interpreted as x, (P Q), and we would write (∀ x, P) Q to limit the scope. If you prefer, you can use the plain ascii expression forall instead of the unicode .

In Lean, then, the pattern for proving a universal statement is rendered as follows:

variable U : Type
variable P : U  Prop

example :  x, P x :=
assume x,
show P x, from sorry

Read assume x as “fix an arbitrary value x of U.” Since we are allowed to rename bound variables at will, we can equivalently write either of the following:

variable U : Type
variable P : U  Prop

example :  y, P y :=
assume x,
show P x, from sorry

example :  x, P x :=
assume y,
show P y, from sorry

This constitutes the introduction rule for the universal quantifier. It is very similar to the introduction rule for implication: instead of using assume to temporarily introduce an assumption, we use assume to temporarily introduce a new object, y. (In fact, assume and assume are both alternate syntax for a single internal construct in Lean, which can also be denoted by λ.)

The elimination rule is, similarly, implemented as follows:

variable U : Type
variable P : U  Prop
variable h :  x, P x
variable a : U

example : P a :=
show P a, from h a

Observe the notation: P a is obtained by “applying” the hypothesis h to a. Once again, note the similarity to the elimination rule for implication.

Here is an example of how it is used:

variable U : Type
variables A B : U  Prop

example (h1 :  x, A x  B x) (h2 :  x, A x) :  x, B x :=
assume y,
have h3 : A y, from h2 y,
have h4 : A y  B y, from h1 y,
show B y, from h4 h3

Here is an even shorter version of the same proof, where we avoid using have:

example (h1 :  x, A x  B x) (h2 :  x, A x) :  x, B x :=
assume y,
show B y, from h1 y (h2 y)

You should talk through the steps, here. Applying h1 to y yields a proof of A y B y, which we then apply to h2 y, which is a proof of A y. The result is the proof of B y that we are after.

In the last chapter, we considered the following proof in natural deduction:

Here is the same proof rendered in Lean:

variable U : Type
variables A B : U  Prop

example : ( x, A x)  ( x, B x)  ( x, A x  B x) :=
assume hA :  x, A x,
assume hB :  x, B x,
assume y,
have Ay : A y, from hA y,
have By : B y, from hB y,
show A y  B y, from and.intro Ay By

Here is an alternative version, using the “anonymous” versions of have:

variable U : Type
variables A B : U  Prop

example : ( x, A x)  ( x, B x)  ( x, A x  B x) :=
assume hA :  x, A x,
assume hB :  x, B x,
assume y,
have A y, from hA y,
have B y, from hB y,
show A y  B y, from and.intro A y B y

The exercises below ask you to prove the barber paradox, which was discussed in the last chapter. You can do that using only propositional reasoning and the rules for the universal quantifer that we have just discussed.

9.3. Using the Existential Quantifier

In Lean, you can type the existential quantifier, , by writing \ex. If you prefer you can use the ascii equivalent, exists. The introduction rule is exists.intro and requires two arguments: a term, and a proof that that term satisfies the required property.

variable U : Type
variable P : U  Prop

example (y : U) (h : P y) :  x, P x :=
exists.intro y h

The elimination rule for the existential quantifier is given by exists.elim. It follows the form of the natural deduction rule: if we know ∃x, P x and we are trying to prove Q, it suffices to introduce a new variable, y, and prove Q under the assumption that P y holds.

variable U : Type
variable P : U  Prop
variable Q : Prop

example (h1 :  x, P x) (h2 :  x, P x  Q) : Q :=
exists.elim h1
  (assume (y : U) (h : P y),
    have h3 : P y  Q, from h2 y,
    show Q, from h3 h)

The following example uses both the introduction and the elimination rules for the existential quantifier.

variable U : Type
variables A B : U  Prop

example : ( x, A x  B x)   x, A x :=
assume h1 :  x, A x  B x,
exists.elim h1
  (assume y (h2 : A y  B y),
    have h3 : A y, from and.left h2,
    show  x, A x, from exists.intro y h3)

Notice the parentheses in the hypothesis; if we left them out, everything after the first x would be included in the scope of that quantifier. From the hypothesis, we obtain a y that satisfies A y B y, and hence A y in particular. So y is enough to witness the conclusion.

It is sometimes annoying to enclose the proof after an exists.elim in parenthesis, as we did here with the assume ... show block. To avoid that, we can use a bit of syntax from the programming world, and use a dollar sign instead. In Lean, an expression f $ t means the same thing as f (t), with the advantage that we do not have to remember to close the parenthesis. With this gadget, we can write the proof above as follows:

variable U : Type
variables A B : U  Prop

example : ( x, A x  B x)   x, A x :=
assume h1 :  x, A x  B x,
exists.elim h1 $
assume y (h2 : A y  B y),
have h3 : A y, from and.left h2,
show  x, A x, from exists.intro y h3

The following example is more involved:

example : ( x, A x  B x)  ( x, A x)  ( x, B x) :=
assume h1 :  x, A x  B x,
exists.elim h1 $
assume y (h2 : A y  B y),
or.elim h2
  (assume h3 : A y,
    have h4 :  x, A x, from exists.intro y h3,
    show ( x, A x)  ( x, B x), from or.inl h4)
  (assume h3 : B y,
    have h4 :  x, B x, from exists.intro y h3,
    show ( x, A x)  ( x, B x), from or.inr h4)

Note again the placement of parentheses in the statement.

In the last chapter, we considered the following natural deduction proof:

Here is a proof of the same implication in Lean:

variable U : Type
variables A B : U  Prop

example : ( x, A x  ¬ B x)  ¬  x, A x  B x :=
assume h1 :  x, A x  ¬ B x,
assume h2 :  x, A x  B x,
exists.elim h2 $
assume x (h3 : A x  B x),
have h4 : A x, from and.left h3,
have h5 : B x, from and.right h3,
have h6 : ¬ B x, from h1 x h4,
show false, from h6 h5

Here, we use exists.elim to introduce a value x satisfying A x B x. The name is arbitrary; we could just as well have used z:

example : ( x, A x  ¬ B x)  ¬  x, A x  B x :=
assume h1 :  x, A x  ¬ B x,
assume h2 :  x, A x  B x,
exists.elim h2 $
assume z (h3 : A z  B z),
have h4 : A z, from and.left h3,
have h5 : B z, from and.right h3,
have h6 : ¬ B z, from h1 z h4,
show false, from h6 h5

Here is another example of the exists-elimination rule:

variable U : Type
variable u : U
variable P : Prop

example : (x : U, P)  P :=
iff.intro
  (assume h1 : x, P,
    exists.elim h1 $
    assume x (h2 : P),
    h2)
  (assume h1 : P,
    exists.intro u h1)

It is subtle: the proof does not go through if we do not declare a variable u of type U, even though u does not appear in the statement of the theorem. The semantics of first-order logic, discussed in the next chapter, presuppose that the universe is nonempty. In Lean, however, it is possible for a type to be empty, and so the proof above depends on the fact that there is an element u in U.

These features are all illustrated in the following example:

variable U : Type
variables P R : U  Prop
variable Q : Prop

example (h1 : x, P x  R x) (h2 : x, P x  R x  Q) : Q :=
let y, hPy, hRy := h1 in
show Q, from h2 y hPy hRy

9.4. Equality and calculational proofs

In Lean, reflexivity, symmetry, and transitivity are called eq.refl, eq.symm, and eq.trans, and the second substitution rule is called eq.subst. Their uses are illustrated below.

variable A : Type

variables x y z : A
variable P : A  Prop

example : x = x :=
show x = x, from eq.refl x

example : y = x :=
have h : x = y, from sorry,
show y = x, from eq.symm h

example : x = z :=
have h1 : x = y, from sorry,
have h2 : y = z, from sorry,
show x = z, from eq.trans h1 h2

example : P y :=
have h1 : x = y, from sorry,
have h2 : P x, from sorry,
show P y, from eq.subst h1 h2

The rule eq.refl above assumes x as an argument, because there is no hypothesis to infer it from. All the other rules assume their premises as arguments. Here is an example of equational reasoning:

variables (A : Type) (x y z : A)

example : y = x  y = z  x = z :=
assume h1 : y = x,
assume h2 : y = z,
have h3 : x = y, from eq.symm h1,
show x = z, from eq.trans h3 h2

This proof can be written more concisely:

example : y = x  y = z  x = z :=
assume h1 h2, eq.trans (eq.symm h1) h2

Because calculation is so important in mathematics, however, Lean provides more efficient ways of carrying them out. One is the rewrite tactic. Typing begin and end in a Lean proof puts Lean into “tactic mode,” which means that Lean then expects a list of instructions. The command rewrite then uses identities to change the goal. For example, the previous proof could be written as follows:

example : y = x  y = z  x = z :=
assume h1 : y = x,
assume h2 : y = z,
show x = z,
  begin
    rewrite h1,
    apply h2
  end

The rewrite tactic can be abbreviated rw.

The first command changes the goal x = z to y = z; the minus sign before h1 tells Lean to use the equation in the reverse direction. After that, we can finish the goal by applying h2.

An alternative is to rewrite the goal using h1 and h2, which reduces the goal to x = x. When that happens, rewrite automatically applies reflexivity.

example : y = x  y = z  x = z :=
assume h1 : y = x,
assume h2 : y = z,
show x = z,
  begin
    rw h1,
    rw h2
  end

In fact, a sequence of rewrites can be combined, using square brackets:

example : y = x  y = z  x = z :=
assume h1 : y = x,
assume h2 : y = z,
show x = z,
  begin
    rw [h1, h2]
  end

And when you reduce a proof to a single tactic, you can use by instead of begin ... end.

example : y = x  y = z  x = z :=
assume h1 : y = x,
assume h2 : y = z,
show x = z, by rw [h1, h2]

We will see in the coming chapters that in ordinary mathematical proofs, one commonly carries out calculations in a format like this:

\[\begin{split}t_1 &= t_2 \\ \ldots & = t_3 \\ \ldots &= t_4 \\ \ldots &= t_5\end{split}\]

Lean has a mechanism to model calculational proofs like this. Whenever a proof of an equation is expected, you can provide a proof using the identifier calc, following by a chain of equalities and justification, in the following form:

calc
  e1 = e2    : justification 1
    ... = e3 : justification 2
    ... = e4 : justification 3
    ... = e5 : justification 4

The chain can go on as long as needed. Each justification is the name of the assumption or theorem that is used. For example, the previous proof could be written as follows:

example : y = x  y = z  x = z :=
assume h1 : y = x,
assume h2 : y = z,
calc
    x = y : eq.symm h1
  ... = z : h2

As usual, the syntax is finicky; notice that there are no commas in the calc expression, and the colons and dots need to be entered exactly in that form. All that varies are the expressions e1, e2, e3, ... and the justifications themselves.

The calc environment is most powerful when used in conjunction with rewrite, since we can then rewrite expressions with facts from the library. For example, Lean’s library has a number of basic identities for the integers, such as these:

variables x y z : int

example : x + 0 = x :=
add_zero x

example : 0 + x = x :=
zero_add x

example : (x + y) + z = x + (y + z) :=
add_assoc x y z

example : x + y = y + x :=
add_comm x y

example : (x * y) * z = x * (y * z) :=
mul_assoc x y z

example : x * y = y * x :=
mul_comm x y

example : x * (y + z) = x * y + x * z :=
left_distrib x y z

example : (x + y) * z = x * z + y * z :=
right_distrib x y z

You can also write the type of integers as , entered with either \Z or \int. Notice that, for example, add_comm is the theorem x y, x + y = y + x. So to instantiate it to s + t = t + s, you write add_comm s t. Using these axioms, here is the calculation above rendered in Lean, as a theorem about the integers:

example (x y z : int) : (x + y) + z = (x + z) + y :=
calc
   (x + y) + z = x + (y + z) : add_assoc x y z
           ... = x + (z + y) : eq.subst (add_comm y z) rfl
           ... = (x + z) + y : eq.symm (add_assoc x z y)

Using rewrite is more efficient, though at times we have to provide information to specify where the rules are used:

example (x y z : int) : (x + y) + z = (x + z) + y :=
calc
  (x + y) + z = x + (y + z) : by rw add_assoc
          ... = x + (z + y) : by rw [add_comm y z]
          ... = (x + z) + y : by rw add_assoc

In that case, we can use a single rewrite:

example (x y z : int) : (x + y) + z = (x + z) + y :=
by rw [add_assoc, add_comm y z, add_assoc]

If you #check the proof before the sequence of rewrites is sufficient, the error message will display the remaining goal.

Here is another example:

variables a b d c : int

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
calc
  (a + b) * (c + d) = (a + b) * c + (a + b) * d : by rw left_distrib
    ... = (a * c + b * c) + (a + b) * d         : by rw right_distrib
    ... = (a * c + b * c) + (a * d + b * d)     : by rw right_distrib
    ... = a * c + b * c + a * d + b * d         : by rw add_assoc

Once again, we can get by with a shorter proof:

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
by rw [left_distrib, right_distrib, right_distrib, add_assoc]

9.5. Exercises

  1. Fill in the sorry.

    section
      variable A : Type
      variable f : A  A
      variable P : A  Prop
      variable  h :  x, P x  P (f x)
    
      -- Show the following:
      example :  y, P y  P (f (f y)) :=
      sorry
    end
    
  2. Fill in the sorry.

    section
      variable U : Type
      variables A B : U  Prop
    
      example : ( x, A x  B x)   x, A x :=
      sorry
    end
    
  3. Fill in the sorry.

    section
      variable U : Type
      variables A B C : U  Prop
    
      variable h1 :  x, A x  B x
      variable h2 :  x, A x  C x
      variable h3 :  x, B x  C x
    
      example :  x, C x :=
      sorry
    end
    
  4. Fill in the sorry’s below, to prove the barber paradox.

    open classical   -- not needed, but you can use it
    
    -- This is an exercise from Chapter 4. Use it as an axiom here.
    axiom not_iff_not_self (P : Prop) : ¬ (P  ¬ P)
    
    example (Q : Prop) : ¬ (Q  ¬ Q) :=
    not_iff_not_self Q
    
    section
      variable Person : Type
      variable shaves : Person  Person  Prop
      variable barber : Person
      variable h :  x, shaves barber x  ¬ shaves x x
    
      -- Show the following:
      example : false :=
      sorry
    end
    
  5. Fill in the sorry.

    section
      variable U : Type
      variables A B : U  Prop
    
      example : ( x, A x)   x, A x  B x :=
      sorry
    end
    
  6. Fill in the sorry.

    section
      variable U : Type
      variables A B : U  Prop
    
      variable h1 :  x, A x  B x
      variable h2 :  x, A x
    
      example :  x, B x :=
      sorry
    end
    
  7. Fill in the sorry.

    variable  U : Type
    variables A B C : U  Prop
    
    example (h1 :  x, A x  B x) (h2 :  x, B x  C x) :
         x, A x  C x :=
    sorry
    
  8. Complete these proofs.

    variable  U : Type
    variables A B C : U  Prop
    
    example : (¬  x, A x)   x, ¬ A x :=
    sorry
    
    example : ( x, ¬ A x)  ¬  x, A x :=
    sorry
    
  9. Fill in the sorry.

    variable  U : Type
    variables R : U  U  Prop
    
    example : ( x,  y, R x y)   y,  x, R x y :=
    sorry
    
  10. The following exercise shows that in the presence of reflexivity, the rules for symmetry and transitivity are equivalent to a single rule.

    theorem foo {A : Type} {a b c : A} : a = b  c = b  a = c :=
    sorry
    
    -- notice that you can now use foo as a rule. The curly braces mean that
    -- you do not have to give A, a, b, or c
    
    section
      variable A : Type
      variables a b c : A
    
      example (h1 : a = b) (h2 : c = b) : a = c :=
      foo h1 h2
    end
    
    section
      variable {A : Type}
      variables {a b c : A}
    
      -- replace the sorry with a proof, using foo and rfl, without using eq.symm.
      theorem my_symm (h : b = a) : a = b :=
      sorry
    
      -- now use foo, rfl, and my_symm to prove transitivity
      theorem my_trans (h1 : a = b) (h2 : b = c) : a = c :=
      sorry
    end
    
  11. Replace each “sorry” below by the correct axiom from the list.

    -- these are the axioms for a commutative ring
    
    #check @add_assoc
    #check @add_comm
    #check @add_zero
    #check @zero_add
    #check @mul_assoc
    #check @mul_comm
    #check @mul_one
    #check @one_mul
    #check @left_distrib
    #check @right_distrib
    #check @add_left_neg
    #check @add_right_neg
    #check @sub_eq_add_neg
    
    variables x y z : int
    
    theorem t1 : x - x = 0 :=
    calc
    x - x = x + -x : by rw sub_eq_add_neg
        ... = 0      : by rw add_right_neg
    
    theorem t2 (h : x + y = x + z) : y = z :=
    calc
    y     = 0 + y        : by rw zero_add
        ... = (-x + x) + y : by rw add_left_neg
        ... = -x + (x + y) : by rw add_assoc
        ... = -x + (x + z) : by rw h
        ... = (-x + x) + z : by rw add_assoc
        ... = 0 + z        : by rw add_left_neg
        ... = z            : by rw zero_add
    
    theorem t3 (h : x + y = z + y) : x = z :=
    calc
    x     = x + 0        : sorry
        ... = x + (y + -y) : sorry
        ... = (x + y) + -y : sorry
        ... = (z + y) + -y : by rw h
        ... = z + (y + -y) : sorry
        ... = z + 0        : sorry
        ... = z            : sorry
    
    theorem t4 (h : x + y = 0) : x = -y :=
    calc
    x     = x + 0        : by rw add_zero
        ... = x + (y + -y) : by rw add_right_neg
        ... = (x + y) + -y : by rw add_assoc
        ... = 0 + -y       : by rw h
        ... = -y           : by rw zero_add
    
    theorem t5 : x * 0 = 0 :=
    have h1 : x * 0 + x * 0 = x * 0 + 0, from
    calc
        x * 0 + x * 0 = x * (0 + 0) : sorry
                ... = x * 0       : sorry
                ... = x * 0 + 0   : sorry,
    show x * 0 = 0, from t2 _ _ _ h1
    
    theorem t6 : x * (-y) = -(x * y) :=
    have h1 : x * (-y) + x * y = 0, from
    calc
        x * (-y) + x * y = x * (-y + y) : sorry
                    ... = x * 0        : sorry
                    ... = 0            : by rw t5 x,
    show x * (-y) = -(x * y), from t4 _ _ h1
    
    theorem t7 : x + x = 2 * x :=
    calc
    x + x = 1 * x + 1 * x : by rw one_mul
        ... = (1 + 1) * x   : sorry
        ... = 2 * x         : rfl