]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/tutorial/chapter4.ma
- probe: new application to compute some data on the proof objects of
[helm.git] / matita / matita / lib / tutorial / chapter4.ma
1 (* 
2 Naif Set Theory
3
4 *)
5 include "basics/types.ma".
6 include "basics/bool.ma".
7 (* 
8 In this Chapter we shall develop a naif theory of sets represented as 
9 characteristic predicates over some universe A, that is as objects of type 
10 A→Prop. 
11 For instance the empty set is defined by the always false function: *)
12
13 definition empty_set ≝ λA:Type[0].λa:A.False.
14 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
15 interpretation "empty set" 'empty_set = (empty_set ?).
16
17 (* Similarly, a singleton set contaning containing an element a, is defined
18 by by the characteristic function asserting equality with a *)
19
20 definition singleton ≝ λA.λx,a:A.x=a.
21 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
22 interpretation "singleton" 'singl x = (singleton ? x).
23
24 (* The membership relation between an element of type A and a set S:A →Prop is
25 simply the predicate resulting from the application of S to a.
26 The operations of union, intersection, complement and substraction 
27 are easily defined in terms of the propositional connectives of dijunction,
28 conjunction and negation *)
29
30 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
31 interpretation "union" 'union a b = (union ? a b).
32
33 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
34 interpretation "intersection" 'intersects a b = (intersection ? a b).
35
36 definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
37 interpretation "complement" 'not a = (complement ? a).
38
39 definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
40 interpretation "substraction" 'minus a b = (substraction ? a b).
41
42 (* Finally, we use implication to define the inclusion relation between
43 sets *)
44
45 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
46 interpretation "subset" 'subseteq a b = (subset ? a b).
47
48 (* 
49 Set Equality
50
51 Two sets are equals if and only if they have the same elements, that is,
52 if the two characteristic functions are extensionally equivalent: *) 
53
54 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
55 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
56 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
57
58 (*
59 This notion of equality is different from the intensional equality of
60 functions; the fact it defines an equivalence relation must be explicitly 
61 proved: *)
62
63 lemma eqP_sym: ∀U.∀A,B:U →Prop. 
64   A =1 B → B =1 A.
65 #U #A #B #eqAB #a @iff_sym @eqAB qed.
66  
67 lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
68   A =1 B → B =1 C → A =1 C.
69 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
70
71 (* For the same reason, we must also prove that all the operations behave well
72 with respect to eqP: *)
73
74 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
75   A =1 C  → A ∪ B =1 C ∪ B.
76 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
77   
78 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
79   B =1 C  → A ∪ B =1 A ∪ C.
80 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
81   
82 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
83   A =1 C  → A ∩ B =1 C ∩ B.
84 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
85   
86 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
87   B =1 C  → A ∩ B =1 A ∩ C.
88 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
89
90 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
91   A =1 C  → A - B =1 C - B.
92 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
93   
94 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
95   B =1 C  → A - B =1 A - C.
96 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
97
98 (* 
99 Simple properties of sets
100
101 We can now prove several properties of the previous set-theoretic operations. 
102 In particular, union is commutative and associative, and the empty set is an 
103 identity element: *)
104
105 lemma union_empty_r: ∀U.∀A:U→Prop. 
106   A ∪ ∅ =1 A.
107 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
108 qed.
109
110 lemma union_comm : ∀U.∀A,B:U →Prop. 
111   A ∪ B =1 B ∪ A.
112 #U #A #B #a % * /2/ qed. 
113
114 lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
115   A ∪ B ∪ C =1 A ∪ (B ∪ C).
116 #S #A #B #C #w % [* [* /3/ | /3/ ] | * [/3/ | * /3/]
117 qed.   
118
119 (* In the same way we prove commutativity and associativity for set 
120 interesection *)
121
122 lemma cap_comm : ∀U.∀A,B:U →Prop. 
123   A ∩ B =1 B ∩ A.
124 #U #A #B #a % * /2/ qed. 
125
126 lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
127   A ∩ (B ∩ C) =1 (A ∩ B) ∩ C.
128 #U #A #B #C #w % [ * #Aw * /3/ | * * /3/ ]
129 qed.
130
131 (* We can also easily prove idempotency for union and intersection *)
132
133 lemma union_idemp: ∀U.∀A:U →Prop. 
134   A  ∪ A =1 A.
135 #U #A #a % [* // | /2/] qed. 
136
137 lemma cap_idemp: ∀U.∀A:U →Prop. 
138   A ∩ A =1 A.
139 #U #A #a % [* // | /2/] qed. 
140
141 (* We conclude our examples with a couple of distributivity theorems, and a 
142 characterization of substraction in terms of interesection and complementation. *)
143
144 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
145   (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
146 #U #A #B #C #w % [* * /3/ | * * /3/] 
147 qed.
148   
149 lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
150   (A ∪ B) - C =1 (A - C) ∪ (B - C).
151 #U #A #B #C #w % [* * /3/ | * * /3/] 
152 qed.
153
154 lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
155 #U #A #B #w normalize /2/
156 qed.
157
158 (* 
159 Bool vs. Prop
160
161 In several situation it is important to assume to have a decidable equality 
162 between elements of a set U, namely a boolean function eqb: U→U→bool such that
163 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y. 
164 A set equipped with such an equality is called a DeqSet: *)
165
166 record DeqSet : Type[1] ≝ { carr :> Type[0];
167    eqb: carr → carr → bool;
168    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
169 }.
170
171 (* We use the notation == to denote the decidable equality, to distinguish it
172 from the propositional equality. In particular, a term of the form a==b is a 
173 boolean, while a=b is a proposition. *)
174
175 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
176 interpretation "eqb" 'eqb a b = (eqb ? a b).
177
178 (* 
179 Small Scale Reflection
180
181 It is convenient to have a simple way to reflect a proof of the fact 
182 that (eqb a b) is true into a proof of the proposition (a = b); to this aim, 
183 we introduce two operators "\P" and "\b". *)
184
185 notation "\P H" non associative with precedence 90 
186   for @{(proj1 … (eqb_true ???) $H)}. 
187
188 notation "\b H" non associative with precedence 90 
189   for @{(proj2 … (eqb_true ???) $H)}. 
190   
191 (* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
192 \b h: eqb a b = true. Let us see an example of their use: the following 
193 statement asserts that we can reflect a proof that eqb a b is false into
194 a proof of the proposition a ≠ b. *)
195
196 lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
197   (eqb ? a b) = false ↔ a ≠ b.
198
199 (* We start the proof introducing the hypothesis, and then split the "if" and
200 "only if" cases *)
201  
202 #S #a #b % #H 
203
204 (* The latter is easily reduced to prove the goal true=false under the assumption
205 H1: a = b *)
206   [@(not_to_not … not_eq_true_false) #H1 
207   
208 (* since by assumption H false is equal to (a==b), by rewriting we obtain the goal 
209 true=(a==b) that is just the boolean version of H1 *) 
210
211   <H @sym_eq @(\b H1)
212
213 (* In the "if" case, we proceed by cases over the boolean equality (a==b); if 
214 (a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
215 true, then by reflection a=b, while by hypothesis a≠b *)
216   
217  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
218   ]
219 qed.
220  
221 (* We also introduce two operators "\Pf" and "\bf" to reflect a proof
222 of (a==b)=false into a proof of a≠b, and vice-versa *) 
223
224 notation "\Pf H" non associative with precedence 90 
225   for @{(proj1 … (eqb_false ???) $H)}. 
226
227 notation "\bf H" non associative with precedence 90 
228   for @{(proj2 … (eqb_false ???) $H)}. 
229
230 (* The following statement proves that propositional equality in a 
231 DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
232
233  lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
234 #S #a #b cases (true_or_false (eqb ? a b)) #H
235   [%1 @(\P H) | %2 @(\Pf H)]
236 qed.
237
238 (* 
239 Unification Hints
240
241 A simple example of a set with a decidable equality is bool. We first define 
242 the boolean equality beqb, that is just the xand function, then prove that 
243 beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by 
244 instantiating the DeqSet record with the previous information *)
245
246 definition beqb ≝ λb1,b2.
247   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
248
249 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
250
251 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
252 #b1 #b2 cases b1 cases b2 normalize /2/
253 qed. 
254
255 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
256
257 (* At this point, we would expect to be able to prove things like the
258 following: for any boolean b, if b==false is true then b=false. 
259 Unfortunately, this would not work, unless we declare b of type 
260 DeqBool (change the type in the following statement and see what 
261 happens). *)
262
263 example exhint: ∀b:DeqBool. (b==false) = true → b=false.
264 #b #H @(\P H) 
265 qed.
266
267 (* The point is that == expects in input a pair of objects whose type must be the 
268 carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference 
269 system has no knowledge of it (it is an information that has been supplied by the 
270 user, and stored somewhere in the library). More explicitly, the type inference 
271 inference system, would face an unification problem consisting to unify bool 
272 against the carrier of something (a metavaribale) and it has no way to synthetize 
273 the answer. To solve this kind of situations, matita provides a mechanism to hint 
274 the system the expected solution. A unification hint is a kind of rule, whose rhd 
275 is the unification problem, containing some metavariables X1, ..., Xn, and whose 
276 left hand side is the solution suggested to the system, in the form of equations 
277 Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
278 is, if it is a unifier for the given problem.
279 To make an example, in the previous case, the unification problem is bool = carr X,
280 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since 
281 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
282
283 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
284
285 unification hint  0 ≔ ; 
286     X ≟ mk_DeqSet bool beqb beqb_true
287 (* ---------------------------------------- *) ⊢ 
288     bool ≡ carr X.
289     
290 unification hint  0 ≔ b1,b2:bool; 
291     X ≟ mk_DeqSet bool beqb beqb_true
292 (* ---------------------------------------- *) ⊢ 
293     beqb b1 b2 ≡ eqb X b1 b2.
294     
295 (* After having provided the previous hints, we may rewrite example exhint 
296 declaring b of type bool. *)
297  
298 example exhint1: ∀b:bool. (b == false) = true → b = false. 
299 #b #H @(\P H)
300 qed.
301
302 (* The cartesian product of two DeqSets is still a DeqSet. To prove
303 this, we must as usual define the boolen equality function, and prove
304 it correctly reflects propositional equality. *)
305
306 definition eq_pairs ≝
307   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
308
309 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
310   eq_pairs A B p1 p2 = true ↔ p1 = p2.
311 #A #B * #a1 #b1 * #a2 #b2 %
312   [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
313   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
314   ]
315 qed.
316
317 definition DeqProd ≝ λA,B:DeqSet.
318   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
319
320 (* Having an unification problem of the kind T1×T2 = carr X, what kind 
321 of hint can we give to the system? We expect T1 to be the carrier of a
322 DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
323 This is expressed by the following hint: *)
324
325 unification hint  0 ≔ C1,C2; 
326     T1 ≟ carr C1,
327     T2 ≟ carr C2,
328     X ≟ DeqProd C1 C2
329 (* ---------------------------------------- *) ⊢ 
330     T1×T2 ≡ carr X.
331
332 unification hint  0 ≔ T1,T2,p1,p2; 
333     X ≟ DeqProd T1 T2
334 (* ---------------------------------------- *) ⊢ 
335     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
336
337 example hint2: ∀b1,b2. 
338   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
339 #b1 #b2 #H @(\P H).
340 qed-.