Library EnsemblePreOrder


Require Import Utf8.
Require Export Orders Ensembles Coq.Program.Basics.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

Ensembles form a pre-order


Section EnsemblePreOrder.
  Variable T : Type.

  Global Instance Ensemble_PreOrder : @PreOrder (Ensemble T) (Included _).
  firstorder.
  Qed.

  Hint Extern 1 ⇒ constructor.
  Hint Extern 1 ⇒ destruct_head_hnf @Intersection.
  Hint Extern 1 ⇒ destruct_head_hnf @Union.
  Hint Extern 2 ⇒ left.
  Hint Extern 2 ⇒ right.

  Global Instance EnsembleHasMeets a b : MeetOf Ensemble_PreOrder a b
    := {| MeetElement := a b |}.
  abstract firstorder.
  Defined.

  Global Instance EnsembleHasJoins a b : JoinOf Ensemble_PreOrder a b
    := {| JoinElement := a b |}.
  abstract firstorder.
  Defined.

  Global Instance EnsembleHasIndexedMeets Index (Indexer : IndexEnsemble T)
  : IndexedMeetOf Indexer Ensemble_PreOrder
    := {| IndexedMeetElement := (fun t i, t Indexer i) |}.
  abstract firstorder.
  Defined.

  Global Instance EnsembleHasIndexedJoins Index (Indexer : IndexEnsemble T)
  : IndexedJoinOf Indexer Ensemble_PreOrder
    := {| IndexedJoinElement := (fun t i, t Indexer i) |}.
  abstract firstorder.
  Defined.

  Global Instance EnsembleHasEnsembleMeets (U : Ensemble (Ensemble T))
  : EnsembleMeetOf U Ensemble_PreOrder
    := {| EnsembleMeetElement := (fun t S, S Ut S) |}.
  abstract firstorder.
  Defined.

  Global Instance EnsembleHasEnsembleJoins (U : Ensemble (Ensemble T))
  : EnsembleJoinOf U Ensemble_PreOrder
    := {| EnsembleJoinElement := (fun t S, S U t S) |}.
  abstract firstorder.
  Defined.
End EnsemblePreOrder.