2 include "tutorial/chapter5.ma".
4 (*************************** Naive Set Theory *********************************)
6 (* Given a ``universe'' U (an arbitrary type U:Type), a naive but practical way
7 to deal with ``sets'' in U is simply to identify them with their characteristic
8 property, that is to as functions of type U → Prop.
10 For instance, the empty set is defined by the False predicate; a singleton set
11 {x} is defined by the property that its elements are equal to x. *)
13 definition empty_set ≝ λU:Type[0].λu:U.False.
14 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
15 interpretation "empty set" 'empty_set = (empty_set ?).
17 definition singleton ≝ λU.λx,u:U.x=u.
18 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
19 interpretation "singleton" 'singl x = (singleton ? x).
21 (* The membership relation is trivial: an element x$ is in the set (defined by
22 the property) P if and only if it enjoyes the property, that is, if it holds
25 definition member ≝ λU:Type[0].λu:U.λP:U→Prop.P u.
27 (* The operations of union, intersection, complementation and substraction are
28 defined in a straightforward way, in terms of logical operations: *)
30 definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a.
31 interpretation "union" 'union a b = (union ? a b).
33 definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∧ Q a.
34 interpretation "intersection" 'intersects a b = (intersection ? a b).
36 definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
37 interpretation "complement" 'not a = (complement ? a).
39 definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
40 interpretation "substraction" 'minus a b = (substraction ? a b).
42 (* More interesting are the notions of subset and equality. Given two sets P and
43 Q, P is a subset of Q when any element u in P is also in Q, that is when (P u)
46 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
48 (* Then, two sets P and Q are equal when P ⊆ Q and Q ⊆ P, or equivalently when
49 for any element u, P u ↔ Q u. *)
51 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
53 (* We shall use the infix notation ≐ for the previous notion of equality. *)
55 (* ≐ is typed as \doteq *)
56 notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
57 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
59 (* It is important to observe that the eqP is different from Leibniz equality of
60 chpater 3. As we already observed, Leibniz equality is a pretty syntactical (or
61 intensional) notion, that is a notion concerning the "connotation" of an object
62 and not its "denotation" (the shape assumed by the object, and not the
63 information it is supposed to convey). Intensionality stands in contrast with
64 "extensionality", referring to principles that judge objects to be equal if they
65 enjoy a given subset of external, observable properties (e.g. the property of
66 having the same elements). For instance given two sets A and B we can prove that
67 A ∪ B ≈ B ∪ A, since they have the same elements, but there is no way to prove
70 The main practical consequence is that, while we can always exploit a Leibniz
71 equality between two terms t1 and t2 for rewriting one into the other (in fact,
72 this is the essence of Leibniz equality), we cannot do the same for an
73 extensional equality (we could only rewrite inside propositions ``compatible''
74 with our external observation of the objects). *)
76 lemma eqP_sym: ∀U.∀A,B:U →Prop.
78 #U #A #B #eqAB #a @iff_sym @eqAB qed.
80 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
81 A ≐ B → B ≐ C → A ≐ C.
82 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
84 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
85 A ≐ C → A ∪ B ≐ C ∪ B.
86 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
88 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
89 B ≐ C → A ∪ B ≐ A ∪ C.
90 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
92 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
93 A ≐ C → A - B ≐ C - B.
94 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
96 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
97 B ≐ C → A - B ≐ A - C.
98 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
101 lemma union_empty_r: ∀U.∀A:U→Prop.
103 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
106 lemma union_comm : ∀U.∀A,B:U →Prop.
108 #U #A #B #a % * /2/ qed.
110 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
111 A ∪ B ∪ C ≐ A ∪ (B ∪ C).
112 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
115 (*distributivities *)
117 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
118 (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
119 #U #A #B #C #w % [* * /3/ | * * /3/]
122 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
123 (A ∪ B) - C ≐ (A - C) ∪ (B - C).
124 #U #A #B #C #w % [* * /3/ | * * /3/]
127 (************************ Sets with decidable equality ************************)
129 (* We say that a property P:A → Prop over a datatype A is decidable when we have
130 an effective way to assess the validity of P a for any a:A. As a consequence of
131 Goedel incompleteness theorem, not every predicate is decidable: for instance,
132 extensional equality on sets is not decidable, in general.
134 Decidability can be expressed in several possible ways. A convenient one is to
135 state it in terms of the computability of the characterisitc function of the
136 predicate P, that is in terms of the existence of a function Pb: A → bool such
140 Decidability is an important issue, and since equality is an essential
141 predicate, it is always interesting to try to understand when a given notion of
142 equality is decidable or not.
144 In particular, Leibniz equality on inductively generated datastructures is often
145 decidable, since we can simply write a decision algorithm by structural
146 induction on the terms. For instance we can define characteristic functions for
147 booleans and natural numbers in the following way: *)
149 definition beqb ≝ λb1,b2.
150 match b1 with [ true ⇒ b2 | false ⇒ notb b2].
154 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
155 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
158 (* It is so important to know if Leibniz equality for a given type is decidable
159 that turns out to be convenient to pack this information into a single algebraic
160 datastructure, called DeqSet: *)
162 record DeqSet : Type[1] ≝
164 eqb: carr → carr → bool;
165 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}.
167 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
168 interpretation "eqb" 'eqb a b = (eqb ? a b).
170 (* A DeqSet is simply a record composed by a carrier type carr, a boolean
171 function eqb: carr → carr → bool representing the decision algorithm, and a
172 proof eqb_true that the decision algorithm is correct. The :> symbol declares
173 carr as a coercion from a DeqSet to its carrier type. We use the infix notation
174 ``=='' for the decidable equality eqb of the carrier.
176 We can easily prove the following facts: *)
178 lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
179 * * % // normalize #H >H //
182 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
186 [% // | #m0 % normalize #H [destruct (H) | @False_ind destruct (H)]]
187 |#n0 #Hind #m cases m
188 [% normalize #H destruct (H) |#m0 >(eq_f … S) % #Heq [@eq_f @(Hind m0)//]
192 (* Then, we can build the following records: *)
193 definition DeqBool : DeqSet ≝ mk_DeqSet bool beqb beqb_true_to_eq.
194 definition DeqNat : DeqSet ≝ mk_DeqSet nat neqb neqb_true_to_eq.
196 (* Note that, since we declare a coercion from the DeqSet to its carrier, the
197 expression 0:DeqNat is well typed, and it is understood by the system as
198 0:carr DeqNat - that is, coercions are automatically insterted by the system, if
201 notation "\P H" non associative with precedence 90
202 for @{(proj1 … (eqb_true ???) $H)}.
204 notation "\b H" non associative with precedence 90
205 for @{(proj2 … (eqb_true ???) $H)}.
207 (****************************** Unification hints *****************************)
209 (* Suppose now to write an expression of the following kind:
211 that, after removing the notation, is equivalent to
213 The system knows that false is a boolean, so in order to accept the expression,
214 it should "figure out" some DeqSet having bool as carrier. This is not a trivial
215 operation: Matita should either try to synthetize it (that is a complex
216 operation known as narrowing) or look into its database of results for a
219 In this situations, we may suggest the intended solution to Matita using the
220 mechanism of unification hints \cite{hints}. The concrete syntax of unification
221 hints is a bit involved: we strongly recommend the user to include the file
222 "hints_declaration.ma" that allows you to write thing in a more convenient and
225 include "hints_declaration.ma".
227 (* For instance, the following declaration tells Matita that a solution of the
228 equation bool = carr X is X = DeqBool. *)
230 unification hint 0 ≔ ;
232 (* ---------------------------------------- *) ⊢
235 (* Using the previous notation (we suggest the reader to cut and paste it from
236 previous hints) the hint is expressed as an inference rule.
237 The conclusion of the rule is the unification problem that we intend to solve,
238 containing one or more variables $X_1,\dots X_b$. The premises of the rule are
239 the solutions we are suggesting to Matita. In general, unification hints should
240 only be used when there exists just one "intended" (canonical) solution for the
242 When you declare a unification hint, Matita verifies it correctness by
243 instantiating the unification problem with the hinted solution, and checking the
244 convertibility between the two sides of the equation. *)
247 example exhint: ∀b:bool. (b == false) = true → b = false.
251 (* In a similar way *)
253 unification hint 0 ≔ b1,b2:bool;
255 (* ---------------------------------------- *) ⊢
256 beqb b1 b2 ≡ eqb X b1 b2.
259 definition eq_pairs ≝
260 λA,B:DeqSet.λp1,p2:A×B.(fst … p1 == fst … p2) ∧ (snd … p1 == snd … p2).
262 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
263 eq_pairs A B p1 p2 = true ↔ p1 = p2.
264 #A #B * #a1 #b1 * #a2 #b2 %
265 [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
266 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
270 definition DeqProd ≝ λA,B:DeqSet.
271 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
273 unification hint 0 ≔ C1,C2;
277 (* ---------------------------------------- *) ⊢
280 unification hint 0 ≔ T1,T2,p1,p2;
282 (* ---------------------------------------- *) ⊢
283 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
285 example hint2: ∀b1,b2.
286 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
290 (******************************* Prop vs. bool ********************************)
292 (* It is probably time to make a discussion about "Prop" and "bool", and their
293 different roles in a the Calculus of Inductive Constructions.
295 Inhabitants of the sort "Prop" are logical propositions. In turn, logical
296 propositions P:Prop can be inhabitated by their proofs H:P. Since, in general,
297 the validity of a property P is not decidable, the role of the proof is to
298 provide a witness of the correctness of $P$ that the system can automatically
301 On the other hand, bool is just an inductive datatype with two constructors true
302 and false: these are terms, not types, and cannot be inhabited.
303 Logical connectives on bool are computable functions, defined by their truth
304 tables, using case analysis.
306 Prop and bool are, in a sense, complementary: the former is more suited for
307 abstract logical reasoning, while the latter allows, in some situations, for
308 brute-force evaluation.
309 Suppose for instance that we wish to prove that the 4 ≤ 3!. Starting from the
310 definition of the factorial function and properties of the less or equal
311 relation, the previous proof could take several steps. Suppose however we proved
312 the decidability of ≤, that is the existence of a boolean function leb
313 reflecting ≤ in the sense that
315 n ≤ m ⇔ leb n m = true
317 Then, we could reduce the verification of 4 ≤ 3! to that of leb 4 3! = true that
318 just requires a mere computation! *)
320 (******************************** Finite Sets *********************************)
322 (* A finite set is a record consisting of a DeqSet A, a list of elements of type
323 A enumerating all the elements of the set, and the proofs that the enumeration
324 does not contain repetitions and is complete. *)
326 let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
329 | cons a tl ⇒ (x == a) ∨ memb S x tl
332 let rec uniqueb (S:DeqSet) l on l : bool ≝
335 | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
338 lemma memb_append: ∀S,a,l1,l2.
339 memb S a (l1@l2) = true →
340 memb S a l1= true ∨ memb S a l2 = true.
341 #S #a #l1 elim l1 normalize [#l2 #H %2 //] #b #tl #Hind #l2
342 cases (a==b) normalize /2/
345 lemma memb_append_l1: ∀S,a,l1,l2.
346 memb S a l1= true → memb S a (l1@l2) = true.
347 #S #a #l1 elim l1 normalize
348 [#le #abs @False_ind /2/ |#b #tl #Hind #l2 cases (a==b) normalize /2/ ]
351 lemma memb_append_l2: ∀S,a,l1,l2.
352 memb S a l2= true → memb S a (l1@l2) = true.
353 #S #a #l1 elim l1 normalize //#b #tl #Hind #l2 cases (a==b) normalize /2/
356 lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
357 memb S2 (f a) (map … f l) = true.
358 #S1 #S2 #f #a #l elim l normalize [//]
359 #x #tl #memba cases (true_or_false (a==x))
360 [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
361 |#eqx >eqx cases (f a==f x) normalize /2/
365 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
366 memb S1 a1 l1 = true → memb S2 a2 l2 = true →
367 memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
368 #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
369 #x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
370 [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
371 |#membtl @memb_append_l2 @Hind //
375 lemma uniqueb_append: ∀A,l1,l2. uniqueb A l1 = true → uniqueb A l2 =true →
376 (∀a. memb A a l1 =true → ¬ memb A a l2 =true) → uniqueb A (l1@l2) = true.
377 #A #l1 elim l1 [normalize //] #a #tl #Hind #l2 #Hatl #Hl2
378 #Hmem normalize cut (memb A a (tl@l2)=false)
379 [2:#Hcut >Hcut normalize @Hind //
380 [@(andb_true_r … Hatl) |#x #Hmemx @Hmem @orb_true_r2 //]
381 |@(noteq_to_eqnot ? true) % #Happend cases (memb_append … Happend)
382 [#H1 @(absurd … H1) @sym_not_eq @eqnot_to_noteq
383 @sym_eq @(andb_true_l … Hatl)
384 |#H @(absurd … H) @Hmem normalize >(\b (refl ? a)) //
389 lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,b.
390 memb ? b (map ?? f l) = true → ∃a. memb ? a l = true ∧ f a = b.
392 [#b normalize #H destruct (H)
393 |#a #tl #Hind #b #H cases (orb_true_l … H)
394 [#eqb @(ex_intro … a) <(\P eqb) % // normalize >(\b (refl ? a)) //
395 |#memb cases (Hind … memb) #a * #mema #eqb
401 lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
402 memb ? (f a) (map ?? f l) = true → memb ? a l = true.
403 #A #B #f #l #a #injf elim l
405 |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
406 [#eqf @orb_true_r1 @(\b ?) >(injf … (\P eqf)) //
407 |#membtl @orb_true_r2 /2/
412 lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
413 uniqueb A l = true → uniqueb B (map ?? f l) = true .
414 #A #B #f #l #injf elim l
416 |#a #tl #Hind #Htl @true_to_andb_true
417 [@sym_eq @noteq_to_eqnot @sym_not_eq
418 @(not_to_not ?? (memb_map_inj … injf …) )
419 <(andb_true_l ?? Htl) /2/
420 |@Hind @(andb_true_r ?? Htl)
425 record FinSet : Type[1] ≝
426 { FinSetcarr:> DeqSet;
427 enum: list FinSetcarr;
428 enum_unique: uniqueb FinSetcarr enum = true;
429 enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
431 (* The library provides many operations for building new FinSet by composing
432 existing ones: for example, if A and B have type FinSet, then also option A,
433 A × B and A + B are finite sets. In all these cases, unification hints are used
434 to suggest the intended finite set structure associated with them, that makes
435 their use quite transparent to the user.*)
437 definition enum_prod ≝ λA,B:DeqSet.λl1:list A.λl2:list B.
438 compose ??? (pair A B) l1 l2.
440 lemma enum_prod_unique: ∀A,B,l1,l2.
441 uniqueb A l1 = true → uniqueb B l2 = true →
442 uniqueb ? (enum_prod A B l1 l2) = true.
444 #a #tl #Hind #l2 #H1 #H2 @uniqueb_append
445 [@unique_map_inj // #b1 #b2 #H3 destruct (H3) //
446 |@Hind // @(andb_true_r … H1)
447 |#p #H3 cases (memb_map_to_exists … H3) #b *
448 #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
449 [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
452 |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
453 [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
454 normalize >(\b (refl ? a)) //
455 |@orb_true_r2 @Hind2 @H4
463 lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2.
464 (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) →
465 ∀p. memb ? p (enum_prod A B l1 l2) = true.
466 #A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose //
470 λA,B:FinSet.mk_FinSet (DeqProd A B)
471 (enum_prod A B (enum A) (enum B))
472 (enum_prod_unique A B … (enum_unique A) (enum_unique B))
473 (enum_prod_complete A B … (enum_complete A) (enum_complete B)).
475 unification hint 0 ≔ C1,C2;
479 (* ---------------------------------------- *) ⊢
480 T1×T2 ≡ FinSetcarr X.
482 (* A particularly intersting case is that of the arrow type A → B. We may define
483 the graph of f:A → B, as the set (sigma type) of all pairs 〈a,b〉 such that
486 definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (fst … p) = snd … p.
488 (* In case the equality is decidable, we may effectively enumerate all elements
489 of the graph by simply filtering from pairs in A × B those satisfying the
490 test λp.f (fst … p) == snd … p: *)
492 definition graph_enum ≝ λA,B:FinSet.λf:A→B.
493 filter ? (λp.f (fst … p) == snd … p) (enum (FinProd A B)).
495 (* The proofs that this enumeration does not contain repetitions and
496 is complete are straightforward. *)