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.