# Library Orders

Require Import Utf8 Setoid.
Require Import Ensembles.
Require Export Classes.RelationClasses Morphisms Bool.
Require Import Notations FunctionalExtensionality ProofIrrelevance.

Set Implicit Arguments.

Generalizable All Variables.

# Orders

Delimit Scope relation_scope with relation.
Bind Scope relation_scope with Relation_Definitions.relation.

Class Comparable {A} (R : Relation_Definitions.relation A) : Prop :=
comparability : x y, R x y R y x.

Class RelationDecidable {A} (R : Relation_Definitions.relation A) :=
Relation_dec : x y, {R x y} + {¬R x y}.

Definition dec_rel {A} R `{@RelationDecidable A R} x y :=
match Relation_dec x y with
| left _true
| right _false
end.

Arguments dec_rel {A} R {_} _ _.

Class LinearOrder {A} (R : Relation_Definitions.relation A) : Prop := {
LinearOrder_Reflexive :> RelationClasses.Reflexive R | 2 ;
LinearOrder_Transitive :> RelationClasses.Transitive R | 2 ;
LinearOrder_Comparable :> Comparable R | 2 }.

Definition Same_relation T (R R' : Relation_Definitions.relation T) : Prop :=
x y, R x y R' x y.

Equality is a pre-order
Program Instance eq_pre_order T : PreOrder (@eq T).

## Meets and joins

Definition is_meet S le `(PreOrder S le) (a b : S) : SProp
:= fun cle c a
le c b
d : S, le d ale d ble d c.

Definition is_join S le `(PreOrder _ le) (a b : S) : SProp
:= fun cle a c
le b c
d : S, le a dle b dle c d.

Class MeetOf {S} le `(PreOrder S le) (a b : S) :=
{ MeetElement :> S;
meet_is_meet : is_meet _ a b MeetElement }.

Class JoinOf {S} le `(PreOrder S le) (a b : S) :=
{ JoinElement :> S;
join_is_join : is_join _ a b JoinElement }.

Section IndexedMeetsAndJoins.
Variable T : Type.
Variable leq : Relation_Definitions.relation T.

Local Infix "≤" := leq.

Variable Index : Type.
Variable IndexToSet : IndexT.

Local Coercion IndexToSet : Index >-> T.

Definition is_indexed_meet `(PreOrder T leq) : TProp
:= fun c( i : Index, c i)
d : T,
( i : Index, d i)
→ d c.

Definition is_indexed_join `(PreOrder T leq) : TProp
:= fun c( i : Index, i c)
d : T,
( i : Index, i d)
→ c d.

Class IndexedMeetOf `(PreOrder T leq) :=
{ IndexedMeetElement :> T;
indexed_meet_is_meet : is_indexed_meet _ IndexedMeetElement }.

Class IndexedJoinOf `(PreOrder T leq) :=
{ IndexedJoinElement :> T;
indexed_join_is_join : is_indexed_join _ IndexedJoinElement }.
End IndexedMeetsAndJoins.

Section EnsemblesMeetsAndJoins.
Variable T : Type.
Variable leq : Relation_Definitions.relation T.

Local Infix "≤" := leq.

Variable U : Ensemble T.

Definition is_ensemble_meet `(PreOrder T leq) : TProp
:= fun c( i, i Uc i)
d : T,
( i, i Ud i)
→ d c.

Definition is_ensemble_join `(PreOrder T leq) : TProp
:= fun c( i, i Ui c)
d : T,
( i, i Ui d)
→ c d.

Class EnsembleMeetOf `(PreOrder T leq) :=
{ EnsembleMeetElement :> T;
ensemble_meet_is_meet : is_ensemble_meet _ EnsembleMeetElement }.

Class EnsembleJoinOf `(PreOrder T leq) :=
{ EnsembleJoinElement :> T;
ensemble_join_is_join : is_ensemble_join _ EnsembleJoinElement }.
End EnsemblesMeetsAndJoins.

## Opposite relations

Definition opposite_relation {T} :
Relation_Definitions.relation TRelation_Definitions.relation T
:= fun R ⇒ (fun x yR y x).

## Relation Homomorphisms

Record RelationHomomorphism
`(r : Relation_Definitions.relation T)
`(r' : Relation_Definitions.relation T') :=
{
RelationHomomorphism_Function :> TT';
RelationHomomorphism_Respectful
: respectful r r' RelationHomomorphism_Function RelationHomomorphism_Function
}.

Definition identity_relation_homomorphism `(r : Relation_Definitions.relation T)
: RelationHomomorphism r r.
(fun xx);
repeat intro; assumption.
Defined.

Definition compose_relation_homomorphisms
`(r : Relation_Definitions.relation T)
`(r' : Relation_Definitions.relation T')
`(r'' : Relation_Definitions.relation T'')
: RelationHomomorphism r' r''
→ RelationHomomorphism r r'
→ RelationHomomorphism r r''.
intros m1 m2.
(fun xm1 (m2 x)).
abstract (
repeat intro;
destruct m1, m2;
intuition
).
Defined.

Lemma RelationHomomorphism_Eq
`(m : @RelationHomomorphism T0 r0 T1 r1)
(m' : RelationHomomorphism r0 r1)
: ( x, m x = m' x)
→ m = m'.
intro H.
assert (H0 : RelationHomomorphism_Function m = RelationHomomorphism_Function m')
by (apply functional_extensionality_dep; assumption).
destruct m, m';
simpl in *;
subst;
f_equal;
apply ProofIrrelevance.proof_irrelevance.
Qed.