Library PropPreOrder


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

Set Implicit Arguments.

Generalizable All Variables.

Prop is pre-order


Section PropPreOrder.
  Global Instance Prop_PreOrder : @PreOrder Prop impl.
  firstorder.
  Qed.

  Global Instance PropHasMeets a b : MeetOf Prop_PreOrder a b
    := {| MeetElement := a b |}.
  abstract firstorder.
  Defined.

  Global Instance PropHasJoins a b : JoinOf Prop_PreOrder a b
    := {| JoinElement := a b |}.
  abstract firstorder.
  Defined.

  Global Instance PropHasIndexedMeets Index (Indexer : IndexProp)
  : IndexedMeetOf Indexer Prop_PreOrder
    := {| IndexedMeetElement := i, Indexer i |}.
  abstract firstorder.
  Defined.

  Global Instance PropHasIndexedJoins Index (Indexer : IndexProp)
  : IndexedJoinOf Indexer Prop_PreOrder
    := {| IndexedJoinElement := i, Indexer i |}.
  abstract firstorder.
  Defined.

  Global Instance PropHasEnsembleMeets (U : Ensemble Prop)
  : EnsembleMeetOf U Prop_PreOrder
    := {| EnsembleMeetElement := i, i Ui |}.
  abstract firstorder.
  Defined.

  Global Instance PropHasEnsembleJoins (U : Ensemble Prop)
  : EnsembleJoinOf U Prop_PreOrder
    := {| EnsembleJoinElement := i, i U i |}.
  abstract firstorder.
  Defined.
End PropPreOrder.