Library hydras.Prelude.DecPreOrder
From Coq Require Export Relations RelationClasses Setoid.
Class Total {A:Type}(R: relation A) :=
totalness : ∀ a b:A, R a b ∨ R b a.
From hydras Require Export STDPP_compat.
#[ global ] Instance comparison_eq_dec : EqDecision comparison.
#[ global ] Instance Total_Reflexive{A:Type}{R: relation A}(rt : Total R):
Reflexive R.
Module Semibundled.
Class TotalDec {A:Type}(R: relation A):=
{ total_dec :> Total R ;
dec_dec :> RelDecision R}.
A class of decidable total pre-orders
Class TotalDecPreOrder {A:Type}(le: relation A) :=
{
total_dec_pre_order :> PreOrder le;
total_dec_total :> TotalDec le
}.
End Semibundled.
when applied to a pre-order relation le, returns the equivalence and
the strict order associated to le
Definition preorder_equiv {A:Type}{le:relation A}
`{P:@PreOrder A le }(a b : A) :=
le a b ∧ le b a.
Definition lt {A:Type}{le:relation A} `{P:@PreOrder A le }(a b : A) :=
le a b ∧ ¬ le b a.
A class of total pre-orders
Class TotalPreOrder {A} (R : relation A) : Prop := {
total_pre_order_pre :> PreOrder R;
total_pre_order_total :> Total R
}.
Properties of decidable total pre-orders
Lemma lt_irreflexive {A:Type}{le:relation A}{P:PreOrder le}:
∀ a, ¬ lt a a.
Lemma lt_not_ge {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, lt a b → ¬ le b a.
Lemma not_le_ge {A} {le:relation A} {P0 : TotalPreOrder le} :
∀ a b, ¬ le a b → le b a.
Lemma le_not_gt {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, le a b → ¬ lt b a.
Lemma lt_not_equiv {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, lt a b → ¬ preorder_equiv a b.
Lemma equiv_not_lt {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, preorder_equiv a b → ¬ lt a b.
Lemma lt_le_trans {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b c, lt a b → le b c → lt a c.
Lemma le_lt_trans {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b c, le a b → lt b c → lt a c.
Lemma le_lt_weak {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, lt a b → le a b.
#[ global ] Instance lt_transitive {A:Type}{le:relation A}{P:PreOrder le}:
Transitive lt.
#[ global ] Instance equiv_equiv {A:Type}{le:relation A} `{P:@PreOrder A le }: Equivalence preorder_equiv.
Lemma le_lt_equiv_dec {A:Type} {le : relation A}
{P0: TotalPreOrder le} {dec : RelDecision le} (a b:A) :
le a b → {lt a b}+{preorder_equiv a b}.
Lemma not_le_gt {A:Type}(le : relation A)
(P0: TotalPreOrder le) (a b:A) : ¬ le a b → lt b a.
∀ a, ¬ lt a a.
Lemma lt_not_ge {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, lt a b → ¬ le b a.
Lemma not_le_ge {A} {le:relation A} {P0 : TotalPreOrder le} :
∀ a b, ¬ le a b → le b a.
Lemma le_not_gt {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, le a b → ¬ lt b a.
Lemma lt_not_equiv {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, lt a b → ¬ preorder_equiv a b.
Lemma equiv_not_lt {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, preorder_equiv a b → ¬ lt a b.
Lemma lt_le_trans {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b c, lt a b → le b c → lt a c.
Lemma le_lt_trans {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b c, le a b → lt b c → lt a c.
Lemma le_lt_weak {A:Type}{le:relation A}{P:PreOrder le}:
∀ a b, lt a b → le a b.
#[ global ] Instance lt_transitive {A:Type}{le:relation A}{P:PreOrder le}:
Transitive lt.
#[ global ] Instance equiv_equiv {A:Type}{le:relation A} `{P:@PreOrder A le }: Equivalence preorder_equiv.
Lemma le_lt_equiv_dec {A:Type} {le : relation A}
{P0: TotalPreOrder le} {dec : RelDecision le} (a b:A) :
le a b → {lt a b}+{preorder_equiv a b}.
Lemma not_le_gt {A:Type}(le : relation A)
(P0: TotalPreOrder le) (a b:A) : ¬ le a b → lt b a.