# Library Exercise_3_4_1_2

Require Import Setoid Utf8.
Require Import ZArith Omega.
Require Import Common Orders.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 3.4.1.2

Section Exercise_3_4_1_2.

## Problem

Decide whether the table to the left in Display (3.8) constitutes a linear order. Show that neither of the other tables are even preorders. The tables are:
```  m <= n    5m = n       |n - m| <= 1
-----     ------       ------------
m | n      m | n             m | n
--|--      --|--             --|--
0 | 0      0 | 0             0 | 0
0 | 1      1 | 5             1 | 0
1 | 1      2 | 10            0 | 1
0 | 2      3 | 15            1 | 1
1 | 2      4 | 20            2 | 1
2 | 2      5 | 25            1 | 2
0 | 3      6 | 30            2 | 2
```

Local Coercion Z.of_nat : >-> Z.

Local Notation "| a - b |" := (Z.abs_nat ((a:Z) - (b:Z))) (at level 10, a at next level, b at next level, no associativity).

Definition Exercise_3_4_1_2_left_relation : relation
:= fun m nm n.
Definition Exercise_3_4_1_2_middle_relation : relation
:= fun m n ⇒ 5 × m = n.
Definition Exercise_3_4_1_2_right_relation : relation
:= fun m n| n - m | 1.
Example Exercise_3_4_1_2_left_relation_linear_order
: LinearOrder Exercise_3_4_1_2_left_relation.
Proof.
split; compute; intros; omega.
Qed.
Example Exercise_3_4_1_2_middle_relation_not_reflexive
: ¬(Reflexive Exercise_3_4_1_2_middle_relation).
Proof.
intro H; specialize (H 1); compute in H; intuition.
Qed.
Example Exercise_3_4_1_2_right_relation_not_transitive
: ¬(Transitive Exercise_3_4_1_2_right_relation).
Proof.
intro H; specialize (H 0 1 2); compute in H; intuition.
Qed.
End Exercise_3_4_1_2.