Relations in Lean

What is a relation?

In a typical undergraduate mathematics course, a relation on a set \(A\) is defined to be a subset of \(A\times A\), the cartesian product of \(A\) with itself.

In the Lean approach, a relation on a type α is a function of type α → α → Prop. That is, a function that takes two terms x and y of type α and returns a Prop.

The Lean approach corresponds much more closely with the intuitive notion of relation than does the more traditional approach. Consider the following definition.

def near_to (x y : ℕ) : Prop := (x - y) < 5 ∧ (y - x) < 5

This defines a relation on natural numbers. It is reflexive and symmetric, but not transitive. Here’s a proof of reflexivity.

example : reflexive near_to :=
begin
  intro x, split; { rw nat.sub_self, norm_num }, 
end

What does this do? The definition of reflexive (which one finds by typing #print reflexive) is:

def reflexive : Π {β : Sort v}, (β → β → Prop) → Prop :=
λ {β : Sort v} (r : β → β → Prop), ∀ (x : β), r x x

So to prove that a relation on a type β is reflexive is precisely to show ∀ (x : β), r x x. Our proof begins by introducing a term x of type ℕ. To prove near_to x x is to show (x – x) < 5 ∧ (x – x) < 5. Each conjunct is dealt with identically.

As an exercise, fill in the sorrys in the following. Post your solutions as a comment!

example : symmetric near_to := sorry

example : ¬(transitive near_to) := sorry

Decidable relations

It would be nice if we could deduce simple numerical results with minimal effort. We’ll see how to do that and also introduce some nice notation.

The command below introduces the symbol ∼ to be used as an infix name for the relation near_to.

local infix `∼`:50 := near_to

With this notation, we’ll prove 5 is near to 7.

example : 5 ∼ 7 := by { split; norm_num }

Fine. But can’t Lean just see this obvious fact? It can if we can prove that near_to is a decidable_rel. That is, we must show for every x and y that near_to x y is decidable, a proposition for which there is an algorithm for determining its truth or falsity.

Fortunately, Lean provides a mechanism that can, in many cases, automatically derive that a relation (or Prop) is decidable. Having made the above definition, we can invoke the derive handler by adding the attribute [derive decidable_rel] to near_to. Make sure first to import tactic.

attribute [derive decidable_rel] near_to 

Alternatively, the previous definition could be decorated:

@[derive decidable_rel]
def near_to (x y : ℕ) : Prop := (x - y) < 5 ∧ (y - x) < 5

Via either method, Lean will derive that a typeclass instance of decidable_rel near_to. After this, the previous numerical result can be proved using dec_trivial,

example : 5 ∼ 7 := dec_trivial