blob: cf73ce8b3af453d4af8b11fcdd4efc76f299e02c (
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
|
(************************************************************************)
(* 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: Relations_1_facts.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*)
Require Export Relations_1.
Definition Complement : (U: Type) (Relation U) -> (Relation U) :=
[U: Type] [R: (Relation U)] [x,y: U] ~ (R x y).
Theorem Rsym_imp_notRsym: (U: Type) (R: (Relation U)) (Symmetric U R) ->
(Symmetric U (Complement U R)).
Proof.
Unfold Symmetric Complement.
Intros U R H' x y H'0; Red; Intro H'1; Apply H'0; Auto with sets.
Qed.
Theorem Equiv_from_preorder :
(U: Type) (R: (Relation U)) (Preorder U R) ->
(Equivalence U [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; Intros x y h; Elim h; Intros H'3 H'4; Auto 10 with sets.
Red in H'1; Red; 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.
Hints Resolve Equiv_from_preorder.
Theorem Equiv_from_order :
(U: Type) (R: (Relation U)) (Order U R) ->
(Equivalence U [x,y: U] (R x y) /\ (R y x)).
Proof.
Intros U R H'; Elim H'; Auto 10 with sets.
Qed.
Hints Resolve Equiv_from_order.
Theorem contains_is_preorder :
(U: Type) (Preorder (Relation U) (contains U)).
Proof.
Auto 10 with sets.
Qed.
Hints Resolve contains_is_preorder.
Theorem same_relation_is_equivalence :
(U: Type) (Equivalence (Relation U) (same_relation U)).
Proof.
Unfold 1 same_relation; Auto 10 with sets.
Qed.
Hints Resolve same_relation_is_equivalence.
Theorem cong_reflexive_same_relation:
(U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Reflexive U R) ->
(Reflexive U R').
Proof.
Unfold same_relation; Intuition.
Qed.
Theorem cong_symmetric_same_relation:
(U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Symmetric U R) ->
(Symmetric U R').
Proof.
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:
(U:Type) (R, R':(Relation U)) (same_relation U R R') ->
(Antisymmetric U R) -> (Antisymmetric U R').
Proof.
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:
(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.
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.
|
