# Library Exercise_3_4_1_8

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.8

Section Exercise_3_4_1_8.

## Problem

List all the preorder relations possible on the set {1, 2}.
For any n , how many linear orders exist on the set {1, 2, 3, ..., n}. Does your formula work when n = 0?

Let finite_set n := { m | 1 m n }.
Let finite_set_relation n : Relation_Definitions.relation Relation_Definitions.relation (finite_set n)
:= fun r ⇒ (fun x yr (proj1_sig x) (proj1_sig y)).

Local Ltac t :=
unfold finite_set, finite_set_relation;
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.

Example Exercise_3_4_1_8_R1 : Relation_Definitions.relation (finite_set 2) :=
finite_set_relation (@eq ).
Example Exercise_3_4_1_8_R2 : Relation_Definitions.relation (finite_set 2) :=
finite_set_relation (fun x yx y).
Example Exercise_3_4_1_8_R3 : Relation_Definitions.relation (finite_set 2) :=
finite_set_relation (fun x yy x).
Example Exercise_3_4_1_8_R4 : Relation_Definitions.relation (finite_set 2) :=
fun _ _True.

Example Exercise_3_4_1_8_R1_preorder : PreOrder Exercise_3_4_1_8_R1.
Proof. t. Qed.
Example Exercise_3_4_1_8_R2_preorder : PreOrder Exercise_3_4_1_8_R2.
Proof. t. Qed.
Example Exercise_3_4_1_8_R3_preorder : PreOrder Exercise_3_4_1_8_R3.
Proof. t. Qed.
Example Exercise_3_4_1_8_R4_preorder : PreOrder Exercise_3_4_1_8_R4.
Proof. t. Qed.
End Exercise_3_4_1_8.