-
Notifications
You must be signed in to change notification settings - Fork 2
/
Ensf_inclus.v
161 lines (137 loc) · 5.35 KB
/
Ensf_inclus.v
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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
(* This program is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1 *)
(* of the License, or (at your option) any later version. *)
(* *)
(* This program is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU Lesser General Public *)
(* License along with this program; if not, write to the Free *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA *)
(* Contribution to the Coq Library V6.3 (July 1999) *)
(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet Coq *)
(* *)
(* INRIA ENS-CNRS *)
(* Rocquencourt Lyon *)
(* *)
(* Coq V5.10 *)
(* Nov 25th 1994 *)
(* *)
(****************************************************************************)
(* Ensf_inclus.v *)
(****************************************************************************)
(* Formal Language Theory *)
(* *)
(* Judicael Courant - Jean-Christophe Filliatre *)
(* *)
(* Developped in V5.8 June-July 1993 *)
(* Ported to V5.10 October 1994 *)
(****************************************************************************)
Require Import Ensf_types.
Require Import Ensf_dans.
Require Import Ensf_union.
Require Import Ensf_produit.
(* *)
(* INCLUSION *)
(* On definit le predicat (inclus E F) par (dans x E)->(dans x F). *)
(* On montre ensuite facilement les resultats suivants : *)
(* -- inclus empty A *)
(* -- inclus A A *)
(* -- (inclus a b)->(inclus c d) *)
(* ->(inclus (prodcart a c) (prodcart b d) *)
(* *)
Definition inclus (A B : Ensf) : Prop := forall x : Elt, dans x A -> dans x B.
Hint Unfold inclus.
Lemma empty_inclus : forall x : Ensf, inclus empty x.
unfold inclus in |- *; intros.
absurd (dans x0 empty); auto.
Qed.
Hint Resolve empty_inclus.
Lemma refl_inclus : forall x : Ensf, inclus x x.
auto.
Qed.
Hint Resolve refl_inclus.
Lemma inclus_trans :
forall a b c : Ensf, inclus a b -> inclus b c -> inclus a c.
auto.
Qed.
Lemma cart_inclus :
forall a b c d : Ensf,
inclus a b -> inclus c d -> inclus (prodcart a c) (prodcart b d).
unfold inclus in |- *.
intros.
cut
(exists x1 : Elt,
(exists x2 : Elt, dans x1 a /\ dans x2 c /\ x = couple x1 x2)).
2: apply coupl3; auto.
intro H2; elim H2; clear H2.
intros x1 H2; elim H2; clear H2.
intros x2 H2; elim H2; clear H2.
intros H2 H3; elim H3; clear H3.
intros H3 H4.
rewrite H4.
auto.
Qed.
Hint Resolve cart_inclus.
Lemma inclus_add :
forall (a b : Ensf) (y : Elt), inclus a b -> inclus a (add y b).
auto.
Qed.
Hint Resolve inclus_add.
Lemma singl_inclus_add :
forall (e : Elt) (a : Ensf), inclus (singleton e) (add e a).
unfold inclus in |- *.
intros e a x H.
cut (x = e); auto.
intro H0.
rewrite H0; auto.
Qed.
Hint Resolve singl_inclus_add.
Lemma inclus_singl :
forall (e : Elt) (a : Ensf), inclus (singleton e) a -> dans e a.
auto.
Qed.
Lemma add_inclus :
forall (x : Elt) (a b : Ensf), dans x b -> inclus a b -> inclus (add x a) b.
unfold inclus in |- *.
intros.
cut (x = x0 \/ dans x0 a).
2: apply dans_add; auto.
intro H2; elim H2; clear H2.
intro H2; rewrite <- H2; auto.
auto.
Qed.
Hint Resolve add_inclus.
Lemma dans_trans :
forall (x : Elt) (a b : Ensf), dans x a -> inclus a b -> dans x b.
auto.
Qed.
Lemma union_inclus :
forall a b c : Ensf, inclus a c -> inclus b c -> inclus (union a b) c.
unfold inclus in |- *.
intros.
cut (dans x a \/ dans x b); auto.
intro H2; elim H2; auto.
Qed.
Hint Resolve union_inclus.
Lemma inclus_g : forall a b : Ensf, inclus a (union a b).
auto.
Qed.
Lemma inclus_d : forall a b : Ensf, inclus b (union a b).
auto.
Qed.
Lemma inclus_g2 : forall A B C : Ensf, inclus A B -> inclus A (union B C).
auto.
Qed.
Hint Resolve inclus_g2.
Lemma inclus_d2 : forall A B C : Ensf, inclus A C -> inclus A (union B C).
auto.
Qed.
Hint Resolve inclus_d2.