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 (************************ Sets with decidable equality ************************)
94 (* We say that a property P:A → Prop over a datatype A is decidable when we have
95 an effective way to assess the validity of P a for any a:A. As a consequence of
96 Goedel incompleteness theorem, not every predicate is decidable: for instance,
97 extensional equality on sets is not decidable, in general.
99 Decidability can be expressed in several possible ways. A convenient one is to
100 state it in terms of the computability of the characterisitc function of the
101 predicate P, that is in terms of the existence of a function Pb: A → bool such
105 Decidability is an important issue, and since equality is an essential
106 predicate, it is always interesting to try to understand when a given notion of
107 equality is decidable or not.
109 In particular, Leibniz equality on inductively generated datastructures is often
110 decidable, since we can simply write a decision algorithm by structural
111 induction on the terms. For instance we can define characteristic functions for
112 booleans and natural numbers in the following way: *)
114 definition beqb ≝ λb1,b2.
115 match b1 with [ true ⇒ b2 | false ⇒ notb b2].
119 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
120 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
123 (* It is so important to know if Leibniz equality for a given type is decidable
124 that turns out to be convenient to pack this information into a single algebraic
125 datastructure, called DeqSet: *)
127 record DeqSet : Type[1] ≝
129 eqb: carr → carr → bool;
130 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}.
132 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
133 interpretation "eqb" 'eqb a b = (eqb ? a b).
135 (* A DeqSet is simply a record composed by a carrier type carr, a boolean
136 function eqb: carr → carr → bool representing the decision algorithm, and a
137 proof eqb_true that the decision algorithm is correct. The :> symbol declares
138 carr as a coercion from a DeqSet to its carrier type. We use the infix notation
139 ``=='' for the decidable equality eqb of the carrier.
141 We can easily prove the following facts: *)
143 lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
144 * * % // normalize #H >H //
147 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
151 [% // | #m0 % normalize #H [destruct (H) | @False_ind destruct (H)]]
152 |#n0 #Hind #m cases m
153 [% normalize #H destruct (H) |#m0 >(eq_f … S) % #Heq [@eq_f @(Hind m0)//]
157 (* Then, we can build the following records: *)
158 definition DeqBool : DeqSet ≝ mk_DeqSet bool beqb beqb_true_to_eq.
159 definition DeqNat : DeqSet ≝ mk_DeqSet nat neqb neqb_true_to_eq.
161 (* Note that, since we declare a coercion from the DeqSet to its carrier, the
162 expression 0:DeqNat is well typed, and it is understood by the system as
163 0:carr DeqNat - that is, coercions are automatically insterted by the system, if
166 notation "\P H" non associative with precedence 90
167 for @{(proj1 … (eqb_true ???) $H)}.
169 notation "\b H" non associative with precedence 90
170 for @{(proj2 … (eqb_true ???) $H)}.
172 (****************************** Unification hints *****************************)
174 (* Suppose now to write an expression of the following kind:
176 that, after removing the notation, is equivalent to
178 The system knows that false is a boolean, so in order to accept the expression,
179 it should "figure out" some DeqSet having bool as carrier. This is not a trivial
180 operation: Matita should either try to synthetize it (that is a complex
181 operation known as narrowing) or look into its database of results for a
184 In this situations, we may suggest the intended solution to Matita using the
185 mechanism of unification hints \cite{hints}. The concrete syntax of unification
186 hints is a bit involved: we strongly recommend the user to include the file
187 "hints_declaration.ma" that allows you to write thing in a more convenient and
190 include "hints_declaration.ma".
192 (* For instance, the following declaration tells Matita that a solution of the
193 equation bool = carr X is X = DeqBool. *)
195 unification hint 0 ≔ ;
197 (* ---------------------------------------- *) ⊢
200 (* Using the previous notation (we suggest the reader to cut and paste it from
201 previous hints) the hint is expressed as an inference rule.
202 The conclusion of the rule is the unification problem that we intend to solve,
203 containing one or more variables $X_1,\dots X_b$. The premises of the rule are
204 the solutions we are suggesting to Matita. In general, unification hints should
205 only be used when there exists just one "intended" (canonical) solution for the
207 When you declare a unification hint, Matita verifies it correctness by
208 instantiating the unification problem with the hinted solution, and checking the
209 convertibility between the two sides of the equation. *)
212 example exhint: ∀b:bool. (b == false) = true → b = false.
216 (* In a similar way *)
218 unification hint 0 ≔ b1,b2:bool;
220 (* ---------------------------------------- *) ⊢
221 beqb b1 b2 ≡ eqb X b1 b2.
224 definition eq_pairs ≝
225 λA,B:DeqSet.λp1,p2:A×B.(fst … p1 == fst … p2) ∧ (snd … p1 == snd … p2).
227 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
228 eq_pairs A B p1 p2 = true ↔ p1 = p2.
229 #A #B * #a1 #b1 * #a2 #b2 %
230 [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
231 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
235 definition DeqProd ≝ λA,B:DeqSet.
236 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
238 unification hint 0 ≔ C1,C2;
242 (* ---------------------------------------- *) ⊢
245 unification hint 0 ≔ T1,T2,p1,p2;
247 (* ---------------------------------------- *) ⊢
248 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
250 example hint2: ∀b1,b2.
251 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
255 (******************************* Prop vs. bool ********************************)
257 (* It is probably time to make a discussion about "Prop" and "bool", and their
258 different roles in a the Calculus of Inductive Constructions.
260 Inhabitants of the sort "Prop" are logical propositions. In turn, logical
261 propositions P:Prop can be inhabitated by their proofs H:P. Since, in general,
262 the validity of a property P is not decidable, the role of the proof is to
263 provide a witness of the correctness of $P$ that the system can automatically
266 On the other hand, bool is just an inductive datatype with two constructors true
267 and false: these are terms, not types, and cannot be inhabited.
268 Logical connectives on bool are computable functions, defined by their truth
269 tables, using case analysis.
271 Prop and bool are, in a sense, complementary: the former is more suited for
272 abstract logical reasoning, while the latter allows, in some situations, for
273 brute-force evaluation.
274 Suppose for instance that we wish to prove that the 4 ≤ 3!. Starting from the
275 definition of the factorial function and properties of the less or equal
276 relation, the previous proof could take several steps. Suppose however we proved
277 the decidability of ≤, that is the existence of a boolean function leb
278 reflecting ≤ in the sense that
280 n ≤ m ⇔ leb n m = true
282 Then, we could reduce the verification of 4 ≤ 3! to that of leb 4 3! = true that
283 just requires a mere computation! *)
285 (******************************** Finite Sets *********************************)
287 (* A finite set is a record consisting of a DeqSet A, a list of elements of type
288 A enumerating all the elements of the set, and the proofs that the enumeration
289 does not contain repetitions and is complete. *)
291 let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
294 | cons a tl ⇒ (x == a) ∨ memb S x tl
297 let rec uniqueb (S:DeqSet) l on l : bool ≝
300 | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
303 lemma memb_append: ∀S,a,l1,l2.
304 memb S a (l1@l2) = true →
305 memb S a l1= true ∨ memb S a l2 = true.
306 #S #a #l1 elim l1 normalize [#l2 #H %2 //] #b #tl #Hind #l2
307 cases (a==b) normalize /2/
310 lemma memb_append_l1: ∀S,a,l1,l2.
311 memb S a l1= true → memb S a (l1@l2) = true.
312 #S #a #l1 elim l1 normalize
313 [#le #abs @False_ind /2/ |#b #tl #Hind #l2 cases (a==b) normalize /2/ ]
316 lemma memb_append_l2: ∀S,a,l1,l2.
317 memb S a l2= true → memb S a (l1@l2) = true.
318 #S #a #l1 elim l1 normalize //#b #tl #Hind #l2 cases (a==b) normalize /2/
321 lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
322 memb S2 (f a) (map … f l) = true.
323 #S1 #S2 #f #a #l elim l normalize [//]
324 #x #tl #memba cases (true_or_false (a==x))
325 [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
326 |#eqx >eqx cases (f a==f x) normalize /2/
330 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
331 memb S1 a1 l1 = true → memb S2 a2 l2 = true →
332 memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
333 #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
334 #x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
335 [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
336 |#membtl @memb_append_l2 @Hind //
340 lemma uniqueb_append: ∀A,l1,l2. uniqueb A l1 = true → uniqueb A l2 =true →
341 (∀a. memb A a l1 =true → ¬ memb A a l2 =true) → uniqueb A (l1@l2) = true.
342 #A #l1 elim l1 [normalize //] #a #tl #Hind #l2 #Hatl #Hl2
343 #Hmem normalize cut (memb A a (tl@l2)=false)
344 [2:#Hcut >Hcut normalize @Hind //
345 [@(andb_true_r … Hatl) |#x #Hmemx @Hmem @orb_true_r2 //]
346 |@(noteq_to_eqnot ? true) % #Happend cases (memb_append … Happend)
347 [#H1 @(absurd … H1) @sym_not_eq @eqnot_to_noteq
348 @sym_eq @(andb_true_l … Hatl)
349 |#H @(absurd … H) @Hmem normalize >(\b (refl ? a)) //
354 lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,b.
355 memb ? b (map ?? f l) = true → ∃a. memb ? a l = true ∧ f a = b.
357 [#b normalize #H destruct (H)
358 |#a #tl #Hind #b #H cases (orb_true_l … H)
359 [#eqb @(ex_intro … a) <(\P eqb) % // normalize >(\b (refl ? a)) //
360 |#memb cases (Hind … memb) #a * #mema #eqb
366 lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
367 memb ? (f a) (map ?? f l) = true → memb ? a l = true.
368 #A #B #f #l #a #injf elim l
370 |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
371 [#eqf @orb_true_r1 @(\b ?) >(injf … (\P eqf)) //
372 |#membtl @orb_true_r2 /2/
377 lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
378 uniqueb A l = true → uniqueb B (map ?? f l) = true .
379 #A #B #f #l #injf elim l
381 |#a #tl #Hind #Htl @true_to_andb_true
382 [@sym_eq @noteq_to_eqnot @sym_not_eq
383 @(not_to_not ?? (memb_map_inj … injf …) )
384 <(andb_true_l ?? Htl) /2/
385 |@Hind @(andb_true_r ?? Htl)
390 record FinSet : Type[1] ≝
391 { FinSetcarr:> DeqSet;
392 enum: list FinSetcarr;
393 enum_unique: uniqueb FinSetcarr enum = true;
394 enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
396 (* The library provides many operations for building new FinSet by composing
397 existing ones: for example, if A and B have type FinSet, then also option A,
398 A × B and A + B are finite sets. In all these cases, unification hints are used
399 to suggest the intended finite set structure associated with them, that makes
400 their use quite transparent to the user.*)
402 definition enum_prod ≝ λA,B:DeqSet.λl1:list A.λl2:list B.
403 compose ??? (pair A B) l1 l2.
405 lemma enum_prod_unique: ∀A,B,l1,l2.
406 uniqueb A l1 = true → uniqueb B l2 = true →
407 uniqueb ? (enum_prod A B l1 l2) = true.
409 #a #tl #Hind #l2 #H1 #H2 @uniqueb_append
410 [@unique_map_inj // #b1 #b2 #H3 destruct (H3) //
411 |@Hind // @(andb_true_r … H1)
412 |#p #H3 cases (memb_map_to_exists … H3) #b *
413 #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
414 [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
417 |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
418 [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
419 normalize >(\b (refl ? a)) //
420 |@orb_true_r2 @Hind2 @H4
428 lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2.
429 (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) →
430 ∀p. memb ? p (enum_prod A B l1 l2) = true.
431 #A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose //
435 λA,B:FinSet.mk_FinSet (DeqProd A B)
436 (enum_prod A B (enum A) (enum B))
437 (enum_prod_unique A B … (enum_unique A) (enum_unique B))
438 (enum_prod_complete A B … (enum_complete A) (enum_complete B)).
440 unification hint 0 ≔ C1,C2;
444 (* ---------------------------------------- *) ⊢
445 T1×T2 ≡ FinSetcarr X.
447 (* A particularly intersting case is that of the arrow type A → B. We may define
448 the graph of f:A → B, as the set (sigma type) of all pairs 〈a,b〉 such that
451 definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (fst … p) = snd … p.
453 (* In case the equality is decidable, we may effectively enumerate all elements
454 of the graph by simply filtering from pairs in A × B those satisfying the
455 test λp.f (fst … p) == snd … p: *)
457 definition graph_enum ≝ λA,B:FinSet.λf:A→B.
458 filter ? (λp.f (fst … p) == snd … p) (enum (FinProd A B)).
460 (* The proofs that this enumeration does not contain repetitions and
461 is complete are straightforward. *)