Library Stdlib.Sets.Relations_1_facts

Require Export Relations_1.

Local Ltac Tauto.intuition_solver ::= auto with sets.

Definition Complement (U:Type) (R:Relation U) : Relation U :=
  fun x y:U => ~ R x y.

Theorem Rsym_imp_notRsym :
 forall (U:Type) (R:Relation U),
   Symmetric U R -> Symmetric U (Complement U R).

Theorem Equiv_from_preorder :
 forall (U:Type) (R:Relation U),
   Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x).
#[global]
Hint Resolve Equiv_from_preorder : core.

Theorem Equiv_from_order :
 forall (U:Type) (R:Relation U),
   Order U R -> Equivalence U (fun x y:U => R x y /\ R y x).
#[global]
Hint Resolve Equiv_from_order : core.

Theorem contains_is_preorder :
 forall U:Type, Preorder (Relation U) (contains U).
#[global]
Hint Resolve contains_is_preorder : core.

Theorem same_relation_is_equivalence :
 forall U:Type, Equivalence (Relation U) (same_relation U).
#[global]
Hint Resolve same_relation_is_equivalence : core.

Theorem cong_reflexive_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Reflexive U R -> Reflexive U R'.

Theorem cong_symmetric_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Symmetric U R -> Symmetric U R'.

Theorem cong_antisymmetric_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.

Theorem cong_transitive_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Transitive U R -> Transitive U R'.