# Library CoLoR.Util.Relation.Preorder

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Solange Coupet-Grimal and William Delobel, 2006-01-09
Various properties of preorders

Section PreOrderFacts.
Variable A : Type.
Variable leA : relation A.

Definition eqA : relation A := fun (f g : A) => leA f g /\ leA g f.
Definition ltA : (relation A) := fun (f g : A) => leA f g /\ ~ eqA f g.

Variable leA_preorder : preorder A leA.

Lemma eqA_equivalence : equivalence A eqA.

Lemma ltA_antisym : forall (a b : A), ltA a b -> ltA b a -> False.

Lemma ltA_trans : transitive A ltA.

Lemma leA_dec_to_eqA_dec : (forall (a b : A), leA a b \/ ~ leA a b) ->
forall (a b : A), eqA a b \/ ~ eqA a b.

Lemma ltA_eqA_compat_r : forall (a b b' :A), eqA b b' -> ltA a b -> ltA a b'.

Lemma ltA_eqA_compat_l : forall (a b b' :A), eqA b b' -> ltA b a -> ltA b' a.

Section Decidability.

Variable leA_dec : forall a b, {leA a b} + {~leA a b}.

Lemma eqA_dec : forall a b, {eqA a b} + {~eqA a b}.

Lemma ltA_dec : forall a b, {ltA a b} + {~ltA a b}.

End Decidability.

End PreOrderFacts.