summaryrefslogtreecommitdiff
path: root/theories/Sets/Relations_1_facts.v
blob: fd83b0e0df6035b105ffaafdec3a1ba222780b08 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         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.  *)
(****************************************************************************)

(*i $Id$ i*)

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).
Proof.
unfold Symmetric, Complement in |- *.
intros U R H' x y H'0; red in |- *; 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).
Proof.
intros U R H'; elim H'; intros H'0 H'1.
apply Definition_of_equivalence.
red in H'0; auto 10 with sets.
2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
red in H'1; red in |- *; auto 10 with sets.
intros x y z h; elim h; intros H'3 H'4; clear h.
intro h; elim h; intros H'5 H'6; clear h.
split; apply H'1 with y; auto 10 with sets.
Qed.
Hint Resolve Equiv_from_preorder.

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).
Proof.
intros U R H'; elim H'; auto 10 with sets.
Qed.
Hint Resolve Equiv_from_order.

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

Theorem same_relation_is_equivalence :
 forall U:Type, Equivalence (Relation U) (same_relation U).
Proof.
unfold same_relation at 1 in |- *; auto 10 with sets.
Qed.
Hint Resolve same_relation_is_equivalence.

Theorem cong_reflexive_same_relation :
 forall (U:Type) (R R':Relation U),
   same_relation U R R' -> Reflexive U R -> Reflexive U R'.
Proof.
unfold same_relation in |- *; 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'.
Proof.
  compute in |- *; 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'.
Proof.
  compute in |- *; 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'.
Proof.
intros U R R' H' H'0; red in |- *.
elim H'.
intros H'1 H'2 x y z H'3 H'4; apply H'2.
apply H'0 with y; auto with sets.
Qed.