(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

Require Export Relations_1.

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).
forall (U : Type) (R : Relation U),
Symmetric U R -> Symmetric U (Complement U R)
Proof.
forall (U : Type) (R : Relation U),
Symmetric U R -> Symmetric U (Complement U R)
unfold Symmetric, Complement.
forall (U : Type) (R : Relation U),
(forall x y : U, R x y -> R y x) ->
forall x y : U, ~ R x y -> ~ R y x
intros U R H' x y H'0; red; intro H'1; apply H'0; auto with sets.
Qed.

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).
forall (U : Type) (R : Relation U),
Preorder U R ->
Equivalence U (fun x y : U => R x y /\ R y x)
Proof.
forall (U : Type) (R : Relation U),
Preorder U R ->
Equivalence U (fun x y : U => R x y /\ R y x)
intros U R H'; elim H'; intros H'0 H'1.
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Equivalence U (fun x y : U => R x y /\ R y x)
apply Definition_of_equivalence.
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Reflexive U (fun x y : U => R x y /\ R y x)
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Transitive U (fun x y : U => R x y /\ R y x)
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Symmetric U (fun x y : U => R x y /\ R y x)
-
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Reflexive U (fun x y : U => R x y /\ R y x) red in H'0; auto 10 with sets.
-
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Transitive U (fun x y : U => R x y /\ R y x) red in H'1; red; auto 10 with sets.
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:forall x y z : U, R x y -> R y z -> R x z
forall x y z : U,
R x y /\ R y x -> R y z /\ R z y -> R x z /\ R z x
  intros x y z h; elim h; intros H'3 H'4; clear h.
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:forall x0 y0 z0 : U, R x0 y0 -> R y0 z0 -> R x0 z0
x, y, z:U
H'3:R x y
H'4:R y x
R y z /\ R z y -> R x z /\ R z x
  intro h; elim h; intros H'5 H'6; clear h.
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:forall x0 y0 z0 : U, R x0 y0 -> R y0 z0 -> R x0 z0
x, y, z:U
H'3:R x y
H'4:R y x
H'5:R y z
H'6:R z y
R x z /\ R z x
  split; apply H'1 with y; auto 10 with sets.
-
U:Type
R:Relation U
H':Preorder U R
H'0:Reflexive U R
H'1:Transitive U R
Symmetric U (fun x y : U => R x y /\ R y x) red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
Qed.
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).
forall (U : Type) (R : Relation U),
Order U R ->
Equivalence U (fun x y : U => R x y /\ R y x)
Proof.
forall (U : Type) (R : Relation U),
Order U R ->
Equivalence U (fun x y : U => R x y /\ R y x)
intros U R H'; elim H'; auto 10 with sets.
Qed.
Hint Resolve Equiv_from_order : core.

Theorem contains_is_preorder :
 forall U:Type, Preorder (Relation U) (contains U).
forall U : Type, Preorder (Relation U) (contains U)
Proof.
forall U : Type, Preorder (Relation U) (contains U)
auto 10 with sets.
Qed.
Hint Resolve contains_is_preorder : core.

Theorem same_relation_is_equivalence :
 forall U:Type, Equivalence (Relation U) (same_relation U).
forall U : Type,
Equivalence (Relation U) (same_relation U)
Proof.
forall U : Type,
Equivalence (Relation U) (same_relation U)
unfold same_relation at 1; auto 10 with sets.
Qed.
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'.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Reflexive U R -> Reflexive U R'
Proof.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Reflexive U R -> Reflexive U R'
unfold same_relation; intuition.
Qed.

Theorem cong_symmetric_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Symmetric U R -> Symmetric U R'.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Symmetric U R -> Symmetric U R'
Proof.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Symmetric U R -> Symmetric U R'
  compute; intros; elim H; intros; clear H;
   apply (H3 y x (H0 x y (H2 x y H1))).
(*Intuition.*)
Qed.

Theorem cong_antisymmetric_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Antisymmetric U R -> Antisymmetric U R'
Proof.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Antisymmetric U R -> Antisymmetric U R'
  compute; intros; elim H; intros; clear H;
   apply (H0 x y (H3 x y H1) (H3 y x H2)).
(*Intuition.*)
Qed.

Theorem cong_transitive_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Transitive U R -> Transitive U R'.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Transitive U R -> Transitive U R'
Proof.
forall (U : Type) (R R' : Relation U),
same_relation U R R' ->
Transitive U R -> Transitive U R'
intros U R R' H' H'0; red.
U:Type
R, R':Relation U
H':same_relation U R R'
H'0:Transitive U R
forall x y z : U, R' x y -> R' y z -> R' x z
elim H'.
U:Type
R, R':Relation U
H':same_relation U R R'
H'0:Transitive U R
contains U R R' ->
contains U R' R ->
forall x y z : U, R' x y -> R' y z -> R' x z
intros H'1 H'2 x y z H'3 H'4; apply H'2.
U:Type
R, R':Relation U
H':same_relation U R R'
H'0:Transitive U R
H'1:contains U R R'
H'2:contains U R' R
x, y, z:U
H'3:R' x y
H'4:R' y z
R x z
apply H'0 with y; auto with sets.
Qed.