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 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
208 (eqb ? a b) = false ↔ a ≠ b.
210 [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
211 |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
215 notation "\Pf H" non associative with precedence 90
216 for @{(proj1 … (eqb_false ???) $H)}.
218 notation "\bf H" non associative with precedence 90
219 for @{(proj2 … (eqb_false ???) $H)}.
221 (****************************** Unification hints *****************************)
223 (* Suppose now to write an expression of the following kind:
225 that, after removing the notation, is equivalent to
227 The system knows that false is a boolean, so in order to accept the expression,
228 it should "figure out" some DeqSet having bool as carrier. This is not a trivial
229 operation: Matita should either try to synthetize it (that is a complex
230 operation known as narrowing) or look into its database of results for a
233 In this situations, we may suggest the intended solution to Matita using the
234 mechanism of unification hints \cite{hints}. The concrete syntax of unification
235 hints is a bit involved: we strongly recommend the user to include the file
236 "hints_declaration.ma" that allows you to write thing in a more convenient and
239 include "hints_declaration.ma".
241 (* For instance, the following declaration tells Matita that a solution of the
242 equation bool = carr X is X = DeqBool. *)
244 unification hint 0 ≔ ;
246 (* ---------------------------------------- *) ⊢
249 (* Using the previous notation (we suggest the reader to cut and paste it from
250 previous hints) the hint is expressed as an inference rule.
251 The conclusion of the rule is the unification problem that we intend to solve,
252 containing one or more variables $X_1,\dots X_b$. The premises of the rule are
253 the solutions we are suggesting to Matita. In general, unification hints should
254 only be used when there exists just one "intended" (canonical) solution for the
256 When you declare a unification hint, Matita verifies it correctness by
257 instantiating the unification problem with the hinted solution, and checking the
258 convertibility between the two sides of the equation. *)
261 example exhint: ∀b:bool. (b == false) = true → b = false.
265 (* In a similar way *)
267 unification hint 0 ≔ b1,b2:bool;
269 (* ---------------------------------------- *) ⊢
270 beqb b1 b2 ≡ eqb X b1 b2.
273 definition eq_pairs ≝
274 λA,B:DeqSet.λp1,p2:A×B.(fst … p1 == fst … p2) ∧ (snd … p1 == snd … p2).
276 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
277 eq_pairs A B p1 p2 = true ↔ p1 = p2.
278 #A #B * #a1 #b1 * #a2 #b2 %
279 [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
280 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
284 definition DeqProd ≝ λA,B:DeqSet.
285 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
287 unification hint 0 ≔ C1,C2;
291 (* ---------------------------------------- *) ⊢
294 unification hint 0 ≔ T1,T2,p1,p2;
296 (* ---------------------------------------- *) ⊢
297 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
299 example hint2: ∀b1,b2.
300 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
304 (******************************* Prop vs. bool ********************************)
306 (* It is probably time to make a discussion about "Prop" and "bool", and their
307 different roles in a the Calculus of Inductive Constructions.
309 Inhabitants of the sort "Prop" are logical propositions. In turn, logical
310 propositions P:Prop can be inhabitated by their proofs H:P. Since, in general,
311 the validity of a property P is not decidable, the role of the proof is to
312 provide a witness of the correctness of $P$ that the system can automatically
315 On the other hand, bool is just an inductive datatype with two constructors true
316 and false: these are terms, not types, and cannot be inhabited.
317 Logical connectives on bool are computable functions, defined by their truth
318 tables, using case analysis.
320 Prop and bool are, in a sense, complementary: the former is more suited for
321 abstract logical reasoning, while the latter allows, in some situations, for
322 brute-force evaluation.
323 Suppose for instance that we wish to prove that the 4 ≤ 3!. Starting from the
324 definition of the factorial function and properties of the less or equal
325 relation, the previous proof could take several steps. Suppose however we proved
326 the decidability of ≤, that is the existence of a boolean function leb
327 reflecting ≤ in the sense that
329 n ≤ m ⇔ leb n m = true
331 Then, we could reduce the verification of 4 ≤ 3! to that of leb 4 3! = true that
332 just requires a mere computation! *)
334 (******************************** Finite Sets *********************************)
336 (* A finite set is a record consisting of a DeqSet A, a list of elements of type
337 A enumerating all the elements of the set, and the proofs that the enumeration
338 does not contain repetitions and is complete. *)
340 let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
343 | cons a tl ⇒ (x == a) ∨ memb S x tl
346 lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
347 #S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
350 lemma memb_cons: ∀S,a,b,l.
351 memb S a l = true → memb S a (b::l) = true.
352 #S #a #b #l normalize cases (a==b) normalize //
355 lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
356 #S #a #x normalize cases (true_or_false … (a==x)) #H
357 [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
360 let rec uniqueb (S:DeqSet) l on l : bool ≝
363 | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
366 lemma memb_append: ∀S,a,l1,l2.
367 memb S a (l1@l2) = true →
368 memb S a l1= true ∨ memb S a l2 = true.
369 #S #a #l1 elim l1 normalize [#l2 #H %2 //] #b #tl #Hind #l2
370 cases (a==b) normalize /2/
373 lemma memb_append_l1: ∀S,a,l1,l2.
374 memb S a l1= true → memb S a (l1@l2) = true.
375 #S #a #l1 elim l1 normalize
376 [#le #abs @False_ind /2/ |#b #tl #Hind #l2 cases (a==b) normalize /2/ ]
379 lemma memb_append_l2: ∀S,a,l1,l2.
380 memb S a l2= true → memb S a (l1@l2) = true.
381 #S #a #l1 elim l1 normalize //#b #tl #Hind #l2 cases (a==b) normalize /2/
384 lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
385 memb S2 (f a) (map … f l) = true.
386 #S1 #S2 #f #a #l elim l normalize [//]
387 #x #tl #memba cases (true_or_false (a==x))
388 [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
389 |#eqx >eqx cases (f a==f x) normalize /2/
393 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
394 memb S1 a1 l1 = true → memb S2 a2 l2 = true →
395 memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
396 #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
397 #x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
398 [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
399 |#membtl @memb_append_l2 @Hind //
403 lemma uniqueb_append: ∀A,l1,l2. uniqueb A l1 = true → uniqueb A l2 =true →
404 (∀a. memb A a l1 =true → ¬ memb A a l2 =true) → uniqueb A (l1@l2) = true.
405 #A #l1 elim l1 [normalize //] #a #tl #Hind #l2 #Hatl #Hl2
406 #Hmem normalize cut (memb A a (tl@l2)=false)
407 [2:#Hcut >Hcut normalize @Hind //
408 [@(andb_true_r … Hatl) |#x #Hmemx @Hmem @orb_true_r2 //]
409 |@(noteq_to_eqnot ? true) % #Happend cases (memb_append … Happend)
410 [#H1 @(absurd … H1) @sym_not_eq @eqnot_to_noteq
411 @sym_eq @(andb_true_l … Hatl)
412 |#H @(absurd … H) @Hmem normalize >(\b (refl ? a)) //
417 lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,b.
418 memb ? b (map ?? f l) = true → ∃a. memb ? a l = true ∧ f a = b.
420 [#b normalize #H destruct (H)
421 |#a #tl #Hind #b #H cases (orb_true_l … H)
422 [#eqb @(ex_intro … a) <(\P eqb) % //
423 |#memb cases (Hind … memb) #a * #mema #eqb
429 lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
430 memb ? (f a) (map ?? f l) = true → memb ? a l = true.
431 #A #B #f #l #a #injf elim l
433 |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
434 [#eqf @orb_true_r1 @(\b ?) >(injf … (\P eqf)) //
435 |#membtl @orb_true_r2 /2/
440 lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
441 uniqueb A l = true → uniqueb B (map ?? f l) = true .
442 #A #B #f #l #injf elim l
444 |#a #tl #Hind #Htl @true_to_andb_true
445 [@sym_eq @noteq_to_eqnot @sym_not_eq
446 @(not_to_not ?? (memb_map_inj … injf …) )
447 <(andb_true_l ?? Htl) /2/
448 |@Hind @(andb_true_r ?? Htl)
453 record FinSet : Type[1] ≝
454 { FinSetcarr:> DeqSet;
455 enum: list FinSetcarr;
456 enum_unique: uniqueb FinSetcarr enum = true;
457 enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
459 (* The library provides many operations for building new FinSet by composing
460 existing ones: for example, if A and B have type FinSet, then also option A,
461 A × B and A + B are finite sets. In all these cases, unification hints are used
462 to suggest the intended finite set structure associated with them, that makes
463 their use quite transparent to the user.*)
465 definition enum_prod ≝ λA,B:DeqSet.λl1:list A.λl2:list B.
466 compose ??? (pair A B) l1 l2.
468 lemma enum_prod_unique: ∀A,B,l1,l2.
469 uniqueb A l1 = true → uniqueb B l2 = true →
470 uniqueb ? (enum_prod A B l1 l2) = true.
472 #a #tl #Hind #l2 #H1 #H2 @uniqueb_append
473 [@unique_map_inj // #b1 #b2 #H3 destruct (H3) //
474 |@Hind // @(andb_true_r … H1)
475 |#p #H3 cases (memb_map_to_exists … H3) #b *
476 #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
477 [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
480 |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
481 [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
482 normalize >(\b (refl ? a)) //
483 |@orb_true_r2 @Hind2 @H4
491 lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2.
492 (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) →
493 ∀p. memb ? p (enum_prod A B l1 l2) = true.
494 #A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose //
498 λA,B:FinSet.mk_FinSet (DeqProd A B)
499 (enum_prod A B (enum A) (enum B))
500 (enum_prod_unique A B … (enum_unique A) (enum_unique B))
501 (enum_prod_complete A B … (enum_complete A) (enum_complete B)).
503 unification hint 0 ≔ C1,C2;
507 (* ---------------------------------------- *) ⊢
508 T1×T2 ≡ FinSetcarr X.
510 (* A particularly intersting case is that of the arrow type A → B. We may define
511 the graph of f:A → B, as the set (sigma type) of all pairs 〈a,b〉 such that
514 definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (fst … p) = snd … p.
516 (* In case the equality is decidable, we may effectively enumerate all elements
517 of the graph by simply filtering from pairs in A × B those satisfying the
518 test λp.f (fst … p) == snd … p: *)
520 definition graph_enum ≝ λA,B:FinSet.λf:A→B.
521 filter ? (λp.f (fst … p) == snd … p) (enum (FinProd A B)).
523 (* The proofs that this enumeration does not contain repetitions and
524 is complete are straightforward. *)