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.