← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Sets/Relations_1_facts.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Sets/Relations_1_facts.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
(****************************************************************************)
 
9
(*                                                                          *)
 
10
(*                         Naive Set Theory in Coq                          *)
 
11
(*                                                                          *)
 
12
(*                     INRIA                        INRIA                   *)
 
13
(*              Rocquencourt                        Sophia-Antipolis        *)
 
14
(*                                                                          *)
 
15
(*                                 Coq V6.1                                 *)
 
16
(*                                                                          *)
 
17
(*                               Gilles Kahn                                *)
 
18
(*                               Gerard Huet                                *)
 
19
(*                                                                          *)
 
20
(*                                                                          *)
 
21
(*                                                                          *)
 
22
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
 
23
(* to the Newton Institute for providing an exceptional work environment    *)
 
24
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 
25
(****************************************************************************)
 
26
 
 
27
(*i $Id: Relations_1_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
28
 
 
29
Require Export Relations_1.
 
30
 
 
31
Definition Complement (U:Type) (R:Relation U) : Relation U :=
 
32
  fun x y:U => ~ R x y.
 
33
 
 
34
Theorem Rsym_imp_notRsym :
 
35
 forall (U:Type) (R:Relation U),
 
36
   Symmetric U R -> Symmetric U (Complement U R).
 
37
Proof.
 
38
unfold Symmetric, Complement in |- *.
 
39
intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets.
 
40
Qed.
 
41
 
 
42
Theorem Equiv_from_preorder :
 
43
 forall (U:Type) (R:Relation U),
 
44
   Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x).
 
45
Proof.
 
46
intros U R H'; elim H'; intros H'0 H'1.
 
47
apply Definition_of_equivalence.
 
48
red in H'0; auto 10 with sets.
 
49
2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
 
50
red in H'1; red in |- *; auto 10 with sets.
 
51
intros x y z h; elim h; intros H'3 H'4; clear h.
 
52
intro h; elim h; intros H'5 H'6; clear h.
 
53
split; apply H'1 with y; auto 10 with sets.
 
54
Qed.
 
55
Hint Resolve Equiv_from_preorder.
 
56
 
 
57
Theorem Equiv_from_order :
 
58
 forall (U:Type) (R:Relation U),
 
59
   Order U R -> Equivalence U (fun x y:U => R x y /\ R y x).
 
60
Proof.
 
61
intros U R H'; elim H'; auto 10 with sets.
 
62
Qed.
 
63
Hint Resolve Equiv_from_order.
 
64
 
 
65
Theorem contains_is_preorder :
 
66
 forall U:Type, Preorder (Relation U) (contains U).
 
67
Proof.
 
68
auto 10 with sets.
 
69
Qed.
 
70
Hint Resolve contains_is_preorder.
 
71
 
 
72
Theorem same_relation_is_equivalence :
 
73
 forall U:Type, Equivalence (Relation U) (same_relation U).
 
74
Proof.
 
75
unfold same_relation at 1 in |- *; auto 10 with sets.
 
76
Qed.
 
77
Hint Resolve same_relation_is_equivalence.
 
78
 
 
79
Theorem cong_reflexive_same_relation :
 
80
 forall (U:Type) (R R':Relation U),
 
81
   same_relation U R R' -> Reflexive U R -> Reflexive U R'.
 
82
Proof.
 
83
unfold same_relation in |- *; intuition.
 
84
Qed.
 
85
 
 
86
Theorem cong_symmetric_same_relation :
 
87
 forall (U:Type) (R R':Relation U),
 
88
   same_relation U R R' -> Symmetric U R -> Symmetric U R'.
 
89
Proof.
 
90
  compute in |- *; intros; elim H; intros; clear H;
 
91
   apply (H3 y x (H0 x y (H2 x y H1))).
 
92
(*Intuition.*)
 
93
Qed.
 
94
 
 
95
Theorem cong_antisymmetric_same_relation :
 
96
 forall (U:Type) (R R':Relation U),
 
97
   same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
 
98
Proof.
 
99
  compute in |- *; intros; elim H; intros; clear H;
 
100
   apply (H0 x y (H3 x y H1) (H3 y x H2)).
 
101
(*Intuition.*)
 
102
Qed.
 
103
 
 
104
Theorem cong_transitive_same_relation :
 
105
 forall (U:Type) (R R':Relation U),
 
106
   same_relation U R R' -> Transitive U R -> Transitive U R'.
 
107
Proof.
 
108
intros U R R' H' H'0; red in |- *.
 
109
elim H'.
 
110
intros H'1 H'2 x y z H'3 H'4; apply H'2.
 
111
apply H'0 with y; auto with sets.
 
112
Qed.
 
 
b'\\ No newline at end of file'