← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Sets/Classical_sets.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/Classical_sets.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: Classical_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
28
 
 
29
Require Export Ensembles.
 
30
Require Export Constructive_sets.
 
31
Require Export Classical_Type.
 
32
 
 
33
Section Ensembles_classical.
 
34
  Variable U : Type.
 
35
 
 
36
  Lemma not_included_empty_Inhabited :
 
37
    forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
 
38
  Proof.
 
39
    intros A NI.
 
40
    elim (not_all_ex_not U (fun x:U => ~ In U A x)).
 
41
    intros x H; apply Inhabited_intro with x.
 
42
    apply NNPP; auto with sets.
 
43
    red in |- *; intro.
 
44
    apply NI; red in |- *.
 
45
    intros x H'; elim (H x); trivial with sets.
 
46
  Qed.
 
47
 
 
48
  Lemma not_empty_Inhabited :
 
49
    forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
 
50
  Proof.
 
51
    intros; apply not_included_empty_Inhabited.
 
52
    red in |- *; auto with sets.
 
53
  Qed.
 
54
 
 
55
  Lemma Inhabited_Setminus :
 
56
    forall X Y:Ensemble U,
 
57
      Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
 
58
  Proof.
 
59
    intros X Y I NI. 
 
60
    elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
 
61
    intros x YX.
 
62
    apply Inhabited_intro with x.
 
63
    apply Setminus_intro.
 
64
    apply not_imply_elim with (In U X x); trivial with sets.
 
65
    auto with sets.
 
66
  Qed.
 
67
 
 
68
  Lemma Strict_super_set_contains_new_element :
 
69
    forall X Y:Ensemble U,
 
70
      Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
 
71
  Proof.
 
72
    auto 7 using Inhabited_Setminus with sets.
 
73
  Qed.
 
74
 
 
75
  Lemma Subtract_intro :
 
76
    forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
 
77
  Proof.
 
78
    unfold Subtract at 1 in |- *; auto with sets.
 
79
  Qed.
 
80
  Hint Resolve Subtract_intro : sets.
 
81
  
 
82
  Lemma Subtract_inv :
 
83
    forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
 
84
  Proof.
 
85
    intros A x y H'; elim H'; auto with sets.
 
86
  Qed.
 
87
 
 
88
  Lemma Included_Strict_Included :
 
89
    forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
 
90
  Proof.
 
91
    intros X Y H'; try assumption.
 
92
    elim (classic (X = Y)); auto with sets.
 
93
  Qed.
 
94
 
 
95
  Lemma Strict_Included_inv :
 
96
    forall X Y:Ensemble U,
 
97
      Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
 
98
  Proof.
 
99
    intros X Y H'; red in H'.
 
100
    split; [ tauto | idtac ].
 
101
    elim H'; intros H'0 H'1; try exact H'1; clear H'.
 
102
    apply Strict_super_set_contains_new_element; auto with sets.
 
103
  Qed.
 
104
 
 
105
  Lemma not_SIncl_empty :
 
106
    forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
 
107
  Proof.
 
108
    intro X; red in |- *; intro H'; try exact H'.
 
109
    lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
 
110
    intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
 
111
    intros x H'0; elim H'0.
 
112
    intro H'3; elim H'3.
 
113
  Qed.
 
114
 
 
115
  Lemma Complement_Complement :
 
116
    forall A:Ensemble U, Complement U (Complement U A) = A.
 
117
  Proof.
 
118
    unfold Complement in |- *; intros; apply Extensionality_Ensembles;
 
119
      auto with sets.
 
120
    red in |- *; split; auto with sets.
 
121
    red in |- *; intros; apply NNPP; auto with sets.
 
122
  Qed.
 
123
 
 
124
End Ensembles_classical.
 
125
 
 
126
 Hint Resolve Strict_super_set_contains_new_element Subtract_intro
 
127
  not_SIncl_empty: sets v62.