summaryrefslogtreecommitdiff
path: root/theories/Sets/Classical_sets.v
blob: 701d9f8a834918b1ad8407f9cc1c4a3458f92e38 (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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \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: Classical_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)

Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical_Type.

Section Ensembles_classical.
  Variable U : Type.

  Lemma not_included_empty_Inhabited :
    forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
  Proof.
    intros A NI.
    elim (not_all_ex_not U (fun x:U => ~ In U A x)).
    intros x H; apply Inhabited_intro with x.
    apply NNPP; auto with sets.
    red in |- *; intro.
    apply NI; red in |- *.
    intros x H'; elim (H x); trivial with sets.
  Qed.

  Lemma not_empty_Inhabited :
    forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
  Proof.
    intros; apply not_included_empty_Inhabited.
    red in |- *; auto with sets.
  Qed.

  Lemma Inhabited_Setminus :
    forall X Y:Ensemble U,
      Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
  Proof.
    intros X Y I NI.
    elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI).
    intros x YX.
    apply Inhabited_intro with x.
    apply Setminus_intro.
    apply not_imply_elim with (In U X x); trivial with sets.
    auto with sets.
  Qed.

  Lemma Strict_super_set_contains_new_element :
    forall X Y:Ensemble U,
      Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
  Proof.
    auto 7 using Inhabited_Setminus with sets.
  Qed.

  Lemma Subtract_intro :
    forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
  Proof.
    unfold Subtract at 1 in |- *; auto with sets.
  Qed.
  Hint Resolve Subtract_intro : sets.

  Lemma Subtract_inv :
    forall (A:Ensemble U) (x y:U), In U (Subtract U A x) y -> In U A y /\ x <> y.
  Proof.
    intros A x y H'; elim H'; auto with sets.
  Qed.

  Lemma Included_Strict_Included :
    forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
  Proof.
    intros X Y H'; try assumption.
    elim (classic (X = Y)); auto with sets.
  Qed.

  Lemma Strict_Included_inv :
    forall X Y:Ensemble U,
      Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
  Proof.
    intros X Y H'; red in H'.
    split; [ tauto | idtac ].
    elim H'; intros H'0 H'1; try exact H'1; clear H'.
    apply Strict_super_set_contains_new_element; auto with sets.
  Qed.

  Lemma not_SIncl_empty :
    forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
  Proof.
    intro X; red in |- *; intro H'; try exact H'.
    lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
    intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
    intros x H'0; elim H'0.
    intro H'3; elim H'3.
  Qed.

  Lemma Complement_Complement :
    forall A:Ensemble U, Complement U (Complement U A) = A.
  Proof.
    unfold Complement in |- *; intros; apply Extensionality_Ensembles;
      auto with sets.
    red in |- *; split; auto with sets.
    red in |- *; intros; apply NNPP; auto with sets.
  Qed.

End Ensembles_classical.

 Hint Resolve Strict_super_set_contains_new_element Subtract_intro
  not_SIncl_empty: sets v62.