# Library Exercise_3_4_1_7

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

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 3.4.1.7

Section Exercise_3_4_1_7.

## Problem

Let S = {1, 2, 3, 4}. Find a preorder R S × S such that the set R is as small as possible. Is it a partial order? Is it a linear order?
Find a preorder R' S × S such that the set R' is as large as possible. Is it a partial order? Is it a linear order?

Let S := { n | 1 n 4 }.

Let R : relation S := fun n mproj1_sig n = proj1_sig m.
Let R' : relation S := fun n mTrue.

Local Ltac t :=
unfold R, R';
repeat match goal with
| _split
| _progress (compute in *; subst)
| _progress trivial
| _progress intuition
| _intro
| [ H : sig _ |- _ ] ⇒ destruct H
| _apply proof_irrelevance
| _omega
| _apply f_equal
end.

Instance Exercise_3_4_1_7_R_preorder : PreOrder R.
Proof.
t.
Qed.

Example Exercise_3_4_1_7_R'_preorder : PreOrder R'.
Proof.
t.
Qed.

Example Exercise_3_4_1_7_R_partial_order : PartialOrder _ R.
Proof.
t.
Qed.

Example Exercise_3_4_1_7_R_not_comparable : ¬(Comparable R).
Proof.
intro H.
assert (S1 : 1 1 4) by omega.
assert (S2 : 1 2 4) by omega.
specialize (H (exist _ 1 S1) (exist _ 2 S2)).
t.
Qed.

Example Exercise_3_4_1_7_R'_not_antisymmetric : ¬(Antisymmetric _ _ R').
Proof.
intro H.
assert (S1 : 1 1 4) by omega.
assert (S2 : 1 2 4) by omega.
specialize (H (exist _ 1 S1) (exist _ 2 S2) I I).
inversion H.
Qed.
End Exercise_3_4_1_7.