14. Relations in Lean

In the last chapter, we noted that set theorists think of a binary relation \(R\) on a set \(A\) as a set of ordered pairs, so that \(R(a, b)\) really means \((a, b) \in R\). An alternative is to think of \(R\) as a function which, when applied to \(a\) and \(b\), returns the proposition that \(R(a, b)\) holds. This is the viewpoint adopted by Lean: a binary relation on a type A is a function A → A → Prop. Remember that the arrows associate to the right, so A → A → Prop really means A → (A → Prop). So, given a : A, R a is a predicate (the property of being related to A), and given a b : A, R a b is a proposition.

14.1. Order Relations

With first-order logic, we can say what it means for a relation to be reflexive, symmetric, transitive, antisymmetric, and so on:

namespace hidden

variable {A : Type}

def reflexive (R : A → A → Prop) : Prop :=
∀ x, R x x

def symmetric (R : A → A → Prop) : Prop :=
∀ x y, R x y → R y x

def transitive (R : A → A → Prop) : Prop :=
∀ x y z, R x y → R y z → R x z

def anti_symmetric (R : A → A → Prop) : Prop :=
∀ x y, R x y → R y x → x = y

end hidden

We can then use the notions freely. Notice that Lean will unfold the definitions when necessary, for example, treating reflexive R as ∀ x, R x x.

variable R : A → A → Prop

example (h : reflexive R) (x : A) : R x x := h x

example (h : symmetric R) (x y : A) (h1 : R x y) : R y x :=
h x y h1

example (h : transitive R) (x y z : A) (h1 : R x y) (h2 : R y z) :
  R x z :=
h x y z h1 h2

example (h : anti_symmetric R) (x y : A) (h1 : R x y)
    (h2 : R y x) :
  x = y :=
h x y h1 h2

In the command variable {A : Type}, we put curly braces around A to indicate that it is an implicit argument, which is to say, you do not have to write it explicitly; Lean can infer it from the argument R. That is why we can write reflexive R rather than reflexive A R: Lean knows that R is a binary relation on A, so it can infer that we mean reflexivity for binary relations on A.

Given h : transitive R, h1 : R x y, and h2 : R y z, it is annoying to have to write h x y z h1 h2 to prove R x z. After all, Lean should be able to infer that we are talking about transitivity at x, y, and z, from the fact that h1 is R x y and h2 is R y z. Indeed, we can replace that information by underscores:

variable R : A → A → Prop

example (h : transitive R) (x y z : A) (h1 : R x y)
    (h2 : R y z) :
  R x z :=
h _ _ _ h1 h2

But typing underscores is annoying, too. The best solution is to declare the arguments x y z to a transitivity hypothesis to be implicit as well:

variable {A : Type}

variable R : A → A → Prop

example (h : transitive R) (x y z : A) (h1 : R x y) (h2 : R y z) :
  R x z :=
h h1 h2

In fact, the notions reflexive, symmetric, transitive, and anti_symmetric are defined in Lean’s core library in exactly this way, so we are free to use them without defining them. That is why we put our temporary definitions of in a namespace hidden; that means that the full name of our version of reflexive is hidden.reflexive, which, therefore, doesn’t conflict with the one defined in the library.

In Section 13.1 we showed that a strict partial order—that is, a binary relation that is transitive and irreflexive—is also asymmetric. Here is a proof of that fact in Lean.

variable A : Type
variable R : A → A → Prop

example (h1 : irreflexive R) (h2 : transitive R) :
  ∀ x y, R x y → ¬ R y x :=
assume x y,
assume h3 : R x y,
assume h4 : R y x,
have h5 : R x x, from h2 h3 h4,
have h6 : ¬ R x x, from h1 x,
show false, from h6 h5

In mathematics, it is common to use infix notation and a symbol like ≤ to denote a partial order. Lean supports this practice:

section
parameter A : Type
parameter R : A → A → Prop

local infix < := R

example (h1 : irreflexive R) (h2 : transitive R) :
  ∀ x y, x < y → ¬ y < x :=
assume x y,
assume h3 : x < y,
assume h4 : y < x,
have h5 : x < x, from h2 h3 h4,
have h6 : ¬ x < x, from h1 x,
show false, from h6 h5

end

The parameter and parameters commands are similar to the variable and variables commands, except that parameters are fixed within a section. In other words, if you prove a theorem about R in the section above, you cannot apply that theorem to another relation, S, without closing the section. Since the parameter R is fixed, Lean allows us to define notation for R to be used locally in the section.

In the example below, having fixed a partial order, R, we define the corresponding strict partial order and prove that it is, indeed, a strict order.

section
parameters {A : Type} (R : A → A → Prop)
parameter (reflR : reflexive R)
parameter (transR : transitive R)
parameter (antisymmR : ∀ {a b : A}, R a b → R b a → a = b)

local infix ≤ := R

definition R' (a b : A) : Prop := a ≤ b ∧ a ≠ b

local infix < := R'

theorem irreflR (a : A) : ¬ a < a :=
assume : a < a,
have a ≠ a, from and.right this,
have a = a, from rfl,
show false, from ‹a ≠ a› ‹a = a›

theorem transR {a b c : A} (h₁ : a < b) (h₂ : b < c) : a < c :=
have a ≤ b, from and.left h₁,
have a ≠ b, from and.right h₁,
have b ≤ c, from and.left h₂,
have b ≠ c, from and.right h₂,
have a ≤ c, from transR ‹a ≤ b› ‹b ≤ c›,
have a ≠ c, from
    assume : a = c,
    have c ≤ b, from eq.subst ‹a = c› ‹a ≤ b›,
    have b = c, from antisymmR ‹b ≤ c› ‹c ≤ b›,
    show false, from ‹b ≠ c› ‹b = c›,
show a < c, from and.intro ‹a ≤ c› ‹a ≠ c›
end

Notice that we have used suggestive names reflR, transR, antisymmR instead of h1, h2, h3 to help remember which hypothesis is which. The proof also uses anonymous have and assume, referring back to them with the French quotes, \f< anf \f>. Remember also that eq.subst ‹a = c› ‹a ≤ b› is a proof of the fact that amounts for substituting c for a in a ≤ b. You can also use the equivalent notation ‹a = c› ▸ ‹a ≤ b›, where the triangle is written \t.

In Section Section 13.1, we also noted that you can define a (weak) partial order from a strict one. We ask you to do this formally in the exercises below.

Here is one more example. Suppose R is a binary relation on a type A, and we define S x y to mean that both R x y and R y x holds. Below we show that the resulting relation is reflexive and symmetric.

section
parameter A : Type
parameter R : A → A → Prop

variable h1 : transitive R
variable h2 : reflexive R

def S (x y : A) := R x y ∧ R y x

example : reflexive S :=
assume x,
have R x x, from h2 x,
show S x x, from and.intro this this

example : symmetric S :=
assume x y,
assume h : S x y,
have h1 : R x y, from h.left,
have h2 : R y x, from h.right,
show S y x, from ⟨h.right, h.left⟩

end

In the exercises below, we ask you to show that S is transitive as well.

In the first example, we use the anonymous assume and have, and then refer back to the have with the keyword this. In the second example, we abbreviate and.left h and and.right h as h.left and h.right, respectively. We also abbreviate and.intro h.right h.left with an anonymous constructor, writing ⟨h.right, h.left⟩. Lean figures out that we are trying to prove a conjunction, and figures out that and.intro is the relevant introduction principle. You can type the corner brackets with \< and \>, respectively.

14.2. Orderings on Numbers

Conveniently, Lean has the normal orderings on the natural numbers, integers, and so on defined already.

open nat
variables n m : ℕ

#check 0 ≤ n
#check n < n + 1

example : 0 ≤ n := nat.zero_le n
example : n < n + 1 := lt_succ_self n

example (h : n + 1 ≤ m) : n < m + 1 :=
have h1 : n < n + 1, from lt_succ_self n,
have h2 : n < m, from lt_of_lt_of_le h1 h,
have h3 : m < m + 1, from lt_succ_self m,
show n < m + 1, from lt_trans h2 h3

There are many theorems in Lean that are useful for proving facts about inequality relations. We list some common ones here.

variables (A : Type) [partial_order A]
variables a b c : A

#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_trans : a < b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (le_of_lt : a < b → a ≤ b)

Here the declaration at the top says that A has the structure of a partial order. There are also properties that are specific to some domains, like the natural numbers:

variable n : ℕ

#check (nat.zero_le : ∀ n : ℕ, 0 ≤ n)
#check (nat.lt_succ_self : ∀ n : ℕ, n < n + 1)
#check (nat.le_succ : ∀ n : ℕ, n ≤ n + 1)

14.3. Equivalence Relations

In Section 13.3 we saw that an equivalence relation is a binary relation on some domain \(A\) that is reflexive, symmetric, and transitive. We will see such relations in Lean in a moment, but first let’s define another kind of relation called a preorder, which is a binary relation that is reflexive and transitive.

namespace hidden

variable {A : Type}

def preorder (R : A → A → Prop) : Prop :=
reflexive R ∧ transitive R

end hidden

Lean’s library provides a different formulation of preorders, so, in order to use the same name, we have to put it in the hidden namespace. Lean’s library defines other properties of relations, such as these:

namespace hidden

variables {A : Type} (R : A → A → Prop)

def equivalence := reflexive R ∧ symmetric R ∧ transitive R

def total := ∀ x y, R x y ∨ R y x

def irreflexive := ∀ x, ¬ R x x

def anti_symmetric := ∀ ⦃x y⦄, R x y → R y x → x = y

end hidden

You can ask Lean to print their definitions:

#print equivalence
#print total
#print irreflexive
#print anti_symmetric

Building on our previous definition of a preorder, we can describe a partial order as an antisymmetric preorder, and show that an equivalence relation as a symmetric preorder.

namespace hidden

variable {A : Type}

def preorder (R : A → A → Prop) : Prop :=
reflexive R ∧ transitive R

def partial_order (R : A → A → Prop) : Prop :=
preorder R ∧ anti_symmetric R

example (R : A → A → Prop):
  equivalence R ↔ preorder R ∧ symmetric R :=
iff.intro
  (assume h1 : equivalence R,
    have h2 : reflexive R, from and.left h1,
    have h3 : symmetric R, from and.left (and.right h1),
    have h4 : transitive R, from and.right (and.right h1),
    show preorder R ∧ symmetric R,
      from and.intro (and.intro h2 h4) h3)
  (assume h1 : preorder R ∧ symmetric R,
    have h2 : preorder R, from and.left h1,
    show equivalence R,
      from and.intro (and.left h2)
             (and.intro (and.right h1) (and.right h2)))

end hidden

In Section 13.3 we claimed that there is yet another way to define an equivalence relation, namely, as a binary relation satisfying the following two properties:

  • \(\forall a \; (a \equiv a)\)

  • \(\forall {a, b, c} \; (a \equiv b \wedge c \equiv b \to a \equiv c)\)

Let’s prove this in Lean. Remember that the parameters and local infix commands serve to fix a relation R and introduce the notation ≈ to denote it. (You can type ≈ as \~~.) In the assumptions reflexive (≈) and symmetric (≈), the notation (≈) denotes R.

section
parameters {A : Type} (R : A → A → Prop)
local infix ≈ := R

variable (h1 : reflexive (≈))
variable (h2 : ∀ {a b c}, a ≈ b ∧ c ≈ b → a ≈ c)

example : symmetric (≈) :=
assume a b (h : a ≈ b),
have b ≈ b ∧ a ≈ b, from and.intro (h1 b) h,
show b ≈ a, from h2 this

example : transitive (≈) :=
assume a b c (h3 : a ≈ b) (h4 : b ≈ c),
have c ≈ b, from h2 (and.intro (h1 c) h4),
have a ≈ b ∧ c ≈ b, from and.intro h3 this,
show a ≈ c, from h2 this

end

14.4. Exercises

  1. Replace the sorry commands in the following proofs to show that we can create a partial order R'​ out of a strict partial order R.

    section
parameters {A : Type} {R : A → A → Prop}
parameter (irreflR : irreflexive R)
parameter (transR : transitive R)

local infix < := R

def R' (a b : A) : Prop := R a b ∨ a = b
local infix ≤ := R'

theorem reflR' (a : A) : a ≤ a := sorry

theorem transR' {a b c : A} (h1 : a ≤ b) (h2 : b ≤ c):
  a ≤ c :=
sorry

theorem antisymmR' {a b : A} (h1 : a ≤ b) (h2 : b ≤ a) :
  a = b :=
sorry

end

  2. Replace the sorry by a proof.

    section
parameters {A : Type} {R : A → A → Prop}
parameter (reflR : reflexive R)
parameter (transR : transitive R)

def S (a b : A) : Prop := R a b ∧ R b a

example : transitive S :=
sorry

end

  3. Only one of the following two theorems is provable. Figure out which one is true, and replace the sorry command with a complete proof.

    section
  parameters {A : Type} {a b c : A} {R : A → A → Prop}
  parameter (Rab : R a b)
  parameter (Rbc : R b c)
  parameter (nRac : ¬ R a c)

  -- Prove one of the following two theorems:

  theorem R_is_strict_partial_order :
    irreflexive R ∧ transitive R :=
  sorry

  theorem R_is_not_strict_partial_order :
    ¬(irreflexive R ∧ transitive R) :=
  sorry
end

  4. Complete the following proof.

    open nat

example : 1 ≤ 4 :=
sorry