2 include "tutorial/chapter5.ma".
3 include "basics/core_notation/singl_1.ma".
5 (*************************** Naive Set Theory *********************************)
7 (* Given a ``universe'' U (an arbitrary type U:Type), a naive but practical way
8 to deal with ``sets'' in U is simply to identify them with their characteristic
9 property, that is to as functions of type U → Prop.
11 For instance, the empty set is defined by the False predicate; a singleton set
12 {x} is defined by the property that its elements are equal to x. *)
14 definition empty_set ≝ λU:Type[0].λu:U.False.
15 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
16 interpretation "empty set" 'empty_set = (empty_set ?).
18 definition singleton ≝ λU.λx,u:U.x=u.
19 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
20 interpretation "singleton" 'singl x = (singleton ? x).
22 (* The membership relation is trivial: an element x$ is in the set (defined by
23 the property) P if and only if it enjoyes the property, that is, if it holds
26 definition member ≝ λU:Type[0].λu:U.λP:U→Prop.P u.
28 (* The operations of union, intersection, complementation and substraction are
29 defined in a straightforward way, in terms of logical operations: *)
31 definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a.
32 interpretation "union" 'union a b = (union ? a b).
34 definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∧ Q a.
35 interpretation "intersection" 'intersects a b = (intersection ? a b).
37 definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
38 interpretation "complement" 'not a = (complement ? a).
40 definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
41 interpretation "substraction" 'minus a b = (substraction ? a b).
43 (* More interesting are the notions of subset and equality. Given two sets P and
44 Q, P is a subset of Q when any element u in P is also in Q, that is when (P u)
47 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
49 (* Then, two sets P and Q are equal when P ⊆ Q and Q ⊆ P, or equivalently when
50 for any element u, P u ↔ Q u. *)
52 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
54 (* We shall use the infix notation ≐ for the previous notion of equality. *)
56 (* ≐ is typed as \doteq *)
57 notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
58 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
60 (* It is important to observe that the eqP is different from Leibniz equality of
61 chpater 3. As we already observed, Leibniz equality is a pretty syntactical (or
62 intensional) notion, that is a notion concerning the "connotation" of an object
63 and not its "denotation" (the shape assumed by the object, and not the
64 information it is supposed to convey). Intensionality stands in contrast with
65 "extensionality", referring to principles that judge objects to be equal if they
66 enjoy a given subset of external, observable properties (e.g. the property of
67 having the same elements). For instance given two sets A and B we can prove that
68 A ∪ B ≈ B ∪ A, since they have the same elements, but there is no way to prove
71 The main practical consequence is that, while we can always exploit a Leibniz
72 equality between two terms t1 and t2 for rewriting one into the other (in fact,
73 this is the essence of Leibniz equality), we cannot do the same for an
74 extensional equality (we could only rewrite inside propositions ``compatible''
75 with our external observation of the objects). *)
77 lemma eqP_sym: ∀U.∀A,B:U →Prop.
79 #U #A #B #eqAB #a @iff_sym @eqAB qed.
81 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
82 A ≐ B → B ≐ C → A ≐ C.
83 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
85 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
86 A ≐ C → A ∪ B ≐ C ∪ B.
87 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
89 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
90 B ≐ C → A ∪ B ≐ A ∪ C.
91 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
93 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
94 A ≐ C → A - B ≐ C - B.
95 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
97 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
98 B ≐ C → A - B ≐ A - C.
99 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
102 lemma union_empty_r: ∀U.∀A:U→Prop.
104 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
107 lemma union_comm : ∀U.∀A,B:U →Prop.
109 #U #A #B #a % * /2/ qed.
111 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
112 A ∪ B ∪ C ≐ A ∪ (B ∪ C).
113 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
116 (*distributivities *)
118 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
119 (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
120 #U #A #B #C #w % [* * /3/ | * * /3/]
123 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
124 (A ∪ B) - C ≐ (A - C) ∪ (B - C).
125 #U #A #B #C #w % [* * /3/ | * * /3/]
128 (************************ Sets with decidable equality ************************)
130 (* We say that a property P:A → Prop over a datatype A is decidable when we have
131 an effective way to assess the validity of P a for any a:A. As a consequence of
132 Goedel incompleteness theorem, not every predicate is decidable: for instance,
133 extensional equality on sets is not decidable, in general.
135 Decidability can be expressed in several possible ways. A convenient one is to
136 state it in terms of the computability of the characterisitc function of the
137 predicate P, that is in terms of the existence of a function Pb: A → bool such
141 Decidability is an important issue, and since equality is an essential
142 predicate, it is always interesting to try to understand when a given notion of
143 equality is decidable or not.
145 In particular, Leibniz equality on inductively generated datastructures is often
146 decidable, since we can simply write a decision algorithm by structural
147 induction on the terms. For instance we can define characteristic functions for
148 booleans and natural numbers in the following way: *)
150 definition beqb ≝ λb1,b2.
151 match b1 with [ true ⇒ b2 | false ⇒ notb b2].
155 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
156 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
159 (* It is so important to know if Leibniz equality for a given type is decidable
160 that turns out to be convenient to pack this information into a single algebraic
161 datastructure, called DeqSet: *)
163 record DeqSet : Type[1] ≝
165 eqb: carr → carr → bool;
166 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}.
168 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
169 interpretation "eqb" 'eqb a b = (eqb ? a b).
171 (* A DeqSet is simply a record composed by a carrier type carr, a boolean
172 function eqb: carr → carr → bool representing the decision algorithm, and a
173 proof eqb_true that the decision algorithm is correct. The :> symbol declares
174 carr as a coercion from a DeqSet to its carrier type. We use the infix notation
175 ``=='' for the decidable equality eqb of the carrier.
177 We can easily prove the following facts: *)
179 lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
180 * * % // normalize #H >H //
183 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
187 [% // | #m0 % normalize #H [destruct (H) | @False_ind destruct (H)]]
188 |#n0 #Hind #m cases m
189 [% normalize #H destruct (H) |#m0 >(eq_f … S) % #Heq [@eq_f @(Hind m0)//]
193 (* Then, we can build the following records: *)
194 definition DeqBool : DeqSet ≝ mk_DeqSet bool beqb beqb_true_to_eq.
195 definition DeqNat : DeqSet ≝ mk_DeqSet nat neqb neqb_true_to_eq.
197 (* Note that, since we declare a coercion from the DeqSet to its carrier, the
198 expression 0:DeqNat is well typed, and it is understood by the system as
199 0:carr DeqNat - that is, coercions are automatically insterted by the system, if
202 notation "\P H" non associative with precedence 90
203 for @{(proj1 … (eqb_true ???) $H)}.
205 notation "\b H" non associative with precedence 90
206 for @{(proj2 … (eqb_true ???) $H)}.
208 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
209 (eqb ? a b) = false ↔ a ≠ b.
211 [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
212 |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
216 notation "\Pf H" non associative with precedence 90
217 for @{(proj1 … (eqb_false ???) $H)}.
219 notation "\bf H" non associative with precedence 90
220 for @{(proj2 … (eqb_false ???) $H)}.
222 (****************************** Unification hints *****************************)
224 (* Suppose now to write an expression of the following kind:
226 that, after removing the notation, is equivalent to
228 The system knows that false is a boolean, so in order to accept the expression,
229 it should "figure out" some DeqSet having bool as carrier. This is not a trivial
230 operation: Matita should either try to synthetize it (that is a complex
231 operation known as narrowing) or look into its database of results for a
234 In this situations, we may suggest the intended solution to Matita using the
235 mechanism of unification hints \cite{hints}. The concrete syntax of unification
236 hints is a bit involved: we strongly recommend the user to include the file
237 "hints_declaration.ma" that allows you to write thing in a more convenient and
240 include "hints_declaration.ma".
242 (* For instance, the following declaration tells Matita that a solution of the
243 equation bool = carr X is X = DeqBool. *)
245 unification hint 0 ≔ ;
247 (* ---------------------------------------- *) ⊢
250 (* Using the previous notation (we suggest the reader to cut and paste it from
251 previous hints) the hint is expressed as an inference rule.
252 The conclusion of the rule is the unification problem that we intend to solve,
253 containing one or more variables $X_1,\dots X_b$. The premises of the rule are
254 the solutions we are suggesting to Matita. In general, unification hints should
255 only be used when there exists just one "intended" (canonical) solution for the
257 When you declare a unification hint, Matita verifies it correctness by
258 instantiating the unification problem with the hinted solution, and checking the
259 convertibility between the two sides of the equation. *)
262 example exhint: ∀b:bool. (b == false) = true → b = false.
266 (* In a similar way *)
268 unification hint 0 ≔ b1,b2:bool;
270 (* ---------------------------------------- *) ⊢
271 beqb b1 b2 ≡ eqb X b1 b2.
274 definition eq_pairs ≝
275 λA,B:DeqSet.λp1,p2:A×B.(fst … p1 == fst … p2) ∧ (snd … p1 == snd … p2).
277 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
278 eq_pairs A B p1 p2 = true ↔ p1 = p2.
279 #A #B * #a1 #b1 * #a2 #b2 %
280 [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
281 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
285 definition DeqProd ≝ λA,B:DeqSet.
286 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
288 unification hint 0 ≔ C1,C2;
292 (* ---------------------------------------- *) ⊢
295 unification hint 0 ≔ T1,T2,p1,p2;
297 (* ---------------------------------------- *) ⊢
298 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
300 example hint2: ∀b1,b2.
301 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
305 (******************************* Prop vs. bool ********************************)
307 (* It is probably time to make a discussion about "Prop" and "bool", and their
308 different roles in a the Calculus of Inductive Constructions.
310 Inhabitants of the sort "Prop" are logical propositions. In turn, logical
311 propositions P:Prop can be inhabitated by their proofs H:P. Since, in general,
312 the validity of a property P is not decidable, the role of the proof is to
313 provide a witness of the correctness of $P$ that the system can automatically
316 On the other hand, bool is just an inductive datatype with two constructors true
317 and false: these are terms, not types, and cannot be inhabited.
318 Logical connectives on bool are computable functions, defined by their truth
319 tables, using case analysis.
321 Prop and bool are, in a sense, complementary: the former is more suited for
322 abstract logical reasoning, while the latter allows, in some situations, for
323 brute-force evaluation.
324 Suppose for instance that we wish to prove that the 4 ≤ 3!. Starting from the
325 definition of the factorial function and properties of the less or equal
326 relation, the previous proof could take several steps. Suppose however we proved
327 the decidability of ≤, that is the existence of a boolean function leb
328 reflecting ≤ in the sense that
330 n ≤ m ⇔ leb n m = true
332 Then, we could reduce the verification of 4 ≤ 3! to that of leb 4 3! = true that
333 just requires a mere computation! *)
335 (******************************** Finite Sets *********************************)
337 (* A finite set is a record consisting of a DeqSet A, a list of elements of type
338 A enumerating all the elements of the set, and the proofs that the enumeration
339 does not contain repetitions and is complete. *)
341 let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
344 | cons a tl ⇒ (x == a) ∨ memb S x tl
347 lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
348 #S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
351 lemma memb_cons: ∀S,a,b,l.
352 memb S a l = true → memb S a (b::l) = true.
353 #S #a #b #l normalize cases (a==b) normalize //
356 lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
357 #S #a #x normalize cases (true_or_false … (a==x)) #H
358 [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
361 let rec uniqueb (S:DeqSet) l on l : bool ≝
364 | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
367 lemma memb_append: ∀S,a,l1,l2.
368 memb S a (l1@l2) = true →
369 memb S a l1= true ∨ memb S a l2 = true.
370 #S #a #l1 elim l1 normalize [#l2 #H %2 //] #b #tl #Hind #l2
371 cases (a==b) normalize /2/
374 lemma memb_append_l1: ∀S,a,l1,l2.
375 memb S a l1= true → memb S a (l1@l2) = true.
376 #S #a #l1 elim l1 normalize
377 [#le #abs @False_ind /2/ |#b #tl #Hind #l2 cases (a==b) normalize /2/ ]
380 lemma memb_append_l2: ∀S,a,l1,l2.
381 memb S a l2= true → memb S a (l1@l2) = true.
382 #S #a #l1 elim l1 normalize //#b #tl #Hind #l2 cases (a==b) normalize /2/
385 lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
386 memb S2 (f a) (map … f l) = true.
387 #S1 #S2 #f #a #l elim l normalize [//]
388 #x #tl #memba cases (true_or_false (a==x))
389 [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
390 |#eqx >eqx cases (f a==f x) normalize /2/
394 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
395 memb S1 a1 l1 = true → memb S2 a2 l2 = true →
396 memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
397 #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
398 #x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
399 [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
400 |#membtl @memb_append_l2 @Hind //
404 lemma uniqueb_append: ∀A,l1,l2. uniqueb A l1 = true → uniqueb A l2 =true →
405 (∀a. memb A a l1 =true → ¬ memb A a l2 =true) → uniqueb A (l1@l2) = true.
406 #A #l1 elim l1 [normalize //] #a #tl #Hind #l2 #Hatl #Hl2
407 #Hmem normalize cut (memb A a (tl@l2)=false)
408 [2:#Hcut >Hcut normalize @Hind //
409 [@(andb_true_r … Hatl) |#x #Hmemx @Hmem @orb_true_r2 //]
410 |@(noteq_to_eqnot ? true) % #Happend cases (memb_append … Happend)
411 [#H1 @(absurd … H1) @sym_not_eq @eqnot_to_noteq
412 @sym_eq @(andb_true_l … Hatl)
413 |#H @(absurd … H) @Hmem normalize >(\b (refl ? a)) //
418 lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,b.
419 memb ? b (map ?? f l) = true → ∃a. memb ? a l = true ∧ f a = b.
421 [#b normalize #H destruct (H)
422 |#a #tl #Hind #b #H cases (orb_true_l … H)
423 [#eqb @(ex_intro … a) <(\P eqb) % //
424 |#memb cases (Hind … memb) #a * #mema #eqb
430 lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
431 memb ? (f a) (map ?? f l) = true → memb ? a l = true.
432 #A #B #f #l #a #injf elim l
434 |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
435 [#eqf @orb_true_r1 @(\b ?) >(injf … (\P eqf)) //
436 |#membtl @orb_true_r2 /2/
441 lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
442 uniqueb A l = true → uniqueb B (map ?? f l) = true .
443 #A #B #f #l #injf elim l
445 |#a #tl #Hind #Htl @true_to_andb_true
446 [@sym_eq @noteq_to_eqnot @sym_not_eq
447 @(not_to_not ?? (memb_map_inj … injf …) )
448 <(andb_true_l ?? Htl) /2/
449 |@Hind @(andb_true_r ?? Htl)
454 record FinSet : Type[1] ≝
455 { FinSetcarr:> DeqSet;
456 enum: list FinSetcarr;
457 enum_unique: uniqueb FinSetcarr enum = true;
458 enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
460 (* The library provides many operations for building new FinSet by composing
461 existing ones: for example, if A and B have type FinSet, then also option A,
462 A × B and A + B are finite sets. In all these cases, unification hints are used
463 to suggest the intended finite set structure associated with them, that makes
464 their use quite transparent to the user.*)
466 definition enum_prod ≝ λA,B:DeqSet.λl1:list A.λl2:list B.
467 compose ??? (pair A B) l1 l2.
469 lemma enum_prod_unique: ∀A,B,l1,l2.
470 uniqueb A l1 = true → uniqueb B l2 = true →
471 uniqueb ? (enum_prod A B l1 l2) = true.
473 #a #tl #Hind #l2 #H1 #H2 @uniqueb_append
474 [@unique_map_inj // #b1 #b2 #H3 destruct (H3) //
475 |@Hind // @(andb_true_r … H1)
476 |#p #H3 cases (memb_map_to_exists … H3) #b *
477 #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
478 [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
481 |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
482 [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
483 normalize >(\b (refl ? a)) //
484 |@orb_true_r2 @Hind2 @H4
492 lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2.
493 (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) →
494 ∀p. memb ? p (enum_prod A B l1 l2) = true.
495 #A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose //
499 λA,B:FinSet.mk_FinSet (DeqProd A B)
500 (enum_prod A B (enum A) (enum B))
501 (enum_prod_unique A B … (enum_unique A) (enum_unique B))
502 (enum_prod_complete A B … (enum_complete A) (enum_complete B)).
504 unification hint 0 ≔ C1,C2;
508 (* ---------------------------------------- *) ⊢
509 T1×T2 ≡ FinSetcarr X.
511 (* A particularly intersting case is that of the arrow type A → B. We may define
512 the graph of f:A → B, as the set (sigma type) of all pairs 〈a,b〉 such that
515 definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (fst … p) = snd … p.
517 (* In case the equality is decidable, we may effectively enumerate all elements
518 of the graph by simply filtering from pairs in A × B those satisfying the
519 test λp.f (fst … p) == snd … p: *)
521 definition graph_enum ≝ λA,B:FinSet.λf:A→B.
522 filter ? (λp.f (fst … p) == snd … p) (enum (FinProd A B)).
524 (* The proofs that this enumeration does not contain repetitions and
525 is complete are straightforward. *)