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.