## 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`

Pingback: Decidable propositions I – exlean

zhangdef symmetric : ∀ {β : Sort v}, (β → β → Prop) → Prop :=

fun {β : Sort v} (r : β → β → Prop) => ∀ (x y : β), r x y → r y x

example : symmetric near_to := by

intro x y r

apply And.intro

exact r.right

exact r.left

def transitive : ∀ {β : Sort v}, (β → β → Prop) → Prop :=

fun {β : Sort v} (r : β → β → Prop) => ∀ (x y z : β), r x y → r y z → r x z

example : ¬(transitive near_to) := by

intro t

have h :

near_to 0 8

:=

t 0 4 8 (And.intro (by simp) (by simp)) (And.intro (by simp) (by simp))

have h₁ :

8 < 5 := h.right

contradiction