X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter6.ma;h=a5355b5fa990fdea2185197ca25a45553ff5e5d9;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=150b07b76f62099d9b3c7a66de6acb7c44454480;hpb=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma
index 150b07b76..a5355b5fa 100644
--- a/matita/matita/lib/tutorial/chapter6.ma
+++ b/matita/matita/lib/tutorial/chapter6.ma
@@ -1,193 +1,525 @@
-(*
-Formal Languages
 
-In this chapter we shall apply our notion of DeqSet, and the list operations 
-defined in Chapter 4 to formal languages. A formal language is an arbitrary set
-of words over a given alphabet, that we shall represent as a predicate over words. 
-*)
 include "tutorial/chapter5.ma".
+include "basics/core_notation/singl_1.ma".
 
-(* A word (or string) over an alphabet S is just a list of elements of S.*)
-definition word ≝ λS:DeqSet.list S.
+(*************************** Naive Set Theory *********************************)
 
-(* For any alphabet there is only one word of length 0, the empty word, which is 
-denoted by ϵ .*) 
+(* Given a ``universe'' U (an arbitrary type U:Type), a naive but practical way 
+to deal with ``sets'' in U is simply to identify them with their characteristic 
+property, that is to as functions of type U → Prop. 
 
-notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
-interpretation "epsilon" 'epsilon = (nil ?).
+For instance, the empty set is defined by the False predicate; a singleton set 
+{x} is defined by the property that its elements are equal to x. *)
 
-(* The operation that consists in appending two words to form a new word, whose 
-length is the sum of the lengths of the original words is called concatenation.
-String concatenation is just the append operation over lists, hence there is no
-point to define it. Similarly, many of its properties, such as the fact that 
-concatenating a word with the empty word gives the original word, follow by 
-general results over lists.
-*)
+definition empty_set ≝ λU:Type[0].λu:U.False.
+notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
+interpretation "empty set" 'empty_set = (empty_set ?).
 
-(*
-Operations over languages
+definition singleton ≝ λU.λx,u:U.x=u.
+(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
+interpretation "singleton" 'singl x = (singleton ? x).
+
+(* The membership relation is trivial: an element x$ is in the set (defined by 
+the property) P if and only if it enjoyes the property, that is, if it holds
+(P x). *)
+
+definition member ≝ λU:Type[0].λu:U.λP:U→Prop.P u.
 
-Languages inherit all the basic operations for sets, namely union, intersection, 
-complementation, substraction, and so on. In addition, we may define some new 
-operations induced by string concatenation, and in particular the concatenation 
-A · B of two languages A and B, the so called Kleene's star A* of A and the 
-derivative of a language A w.r.t. a given character a. *)
+(* The operations of union, intersection, complementation and substraction are 
+defined in a straightforward way, in terms of logical operations: *)
 
-definition cat : ∀S,l1,l2,w.Prop ≝ 
-  λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a.
+interpretation "union" 'union a b = (union ? a b).
 
-notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
-interpretation "cat lang" 'middot a b = (cat ? a b).
+definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∧ Q a.
+interpretation "intersection" 'intersects a b = (intersection ? a b).
 
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
 
-(* Given a language l, the Kleene's star of l, denoted by l*, is the set of 
-finite-length strings that can be generated by concatenating arbitrary strings of 
-l. In other words, w belongs to l* is and only if there exists a list of strings 
-w1,w2,...wk all belonging to l, such that l = w1w2...wk. 
-We need to define the latter operations. The following flatten function takes in 
-input a list of words and concatenates them together. *)
+definition substraction ≝  λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
 
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+(* More interesting are the notions of subset and equality. Given two sets P and 
+Q, P is a subset of Q when any element u in P is also in Q, that is when (P u) 
+implies (Q u). *)
 
-(* Given a list of words l and a language r, (conjunct l r) is true if and only if
-all words in l are in r, that is for every w in l, r w holds. *)
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
 
-let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
+(* Then, two sets P and Q are equal when P ⊆ Q and Q ⊆ P, or equivalently when 
+for any element u, P u ↔ Q u. *)
 
-(* We are ready to give the formal definition of the Kleene's star of l:
-a word w belongs to l* is and only if there exists a list of strings 
-lw such that (conjunct lw l) and  l = flatten lw. *)
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
 
-definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
-notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
-interpretation "star lang" 'star l = (star ? l).
+(* We shall use the infix notation ≐ for the previous notion of equality. *)
 
-(* The derivative of a language A with respect to a character a is the set of
-all strings w such that aw is in A. *)
+(* ≐ is typed as \doteq *)
+notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
+interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
-definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+(* It is important to observe that the eqP is different from Leibniz equality of 
+chpater 3. As we already observed, Leibniz equality is a pretty syntactical (or 
+intensional) notion, that is a notion concerning the "connotation" of an object
+and not its "denotation" (the shape assumed by the object, and not the 
+information it is supposed to convey). Intensionality stands in contrast with 
+"extensionality", referring to principles that judge objects to be equal if they 
+enjoy a given subset of external, observable properties (e.g. the property of 
+having the same elements). For instance given two sets A and B we can prove that
+A ∪ B ≈ B ∪ A, since they have the same elements, but there is no way to prove 
+A ∪ B = B ∪ A.
 
-(* 
-Language equalities
+The main practical consequence is that, while we can always exploit a Leibniz 
+equality between two terms t1 and t2 for rewriting one into the other (in fact, 
+this is the essence of Leibniz equality), we cannot do the same for an 
+extensional equality (we could only rewrite inside propositions ``compatible'' 
+with our external observation of the objects). *)
 
-Equality between languages is just the usual extensional equality between
-sets. The operation of concatenation behaves well with respect to this equality. *)
+lemma eqP_sym: ∀U.∀A,B:U →Prop. 
+  A ≐ B → B ≐ A.
+#U #A #B #eqAB #a @iff_sym @eqAB qed.
+ 
+lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
+  A ≐ B → B ≐ C → A ≐ C.
+#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
 
-lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop. 
-  A =1 C  → A · B =1 C · B.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w1) /6/
+lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
+  A ≐ C  → A ∪ B ≐ C ∪ B.
+#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
+  
+lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
+  B ≐ C  → A ∪ B ≐ A ∪ C.
+#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
+  A ≐ C  → A - B ≐ C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+  
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
+  B ≐ C  → A - B ≐ A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
+(* set equalities *)
+lemma union_empty_r: ∀U.∀A:U→Prop. 
+  A ∪ ∅ ≐ A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
 qed.
 
-lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop. 
-  B =1 C → A · B =1 A · C.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w2) /6/ 
+lemma union_comm : ∀U.∀A,B:U →Prop. 
+  A ∪ B ≐ B ∪ A.
+#U #A #B #a % * /2/ qed. 
+
+lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
+  A ∪ B ∪ C ≐ A ∪ (B ∪ C).
+#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
+qed.  
+
+(*distributivities *)
+
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
 qed.
   
-(* Concatenating a language with the empty language results in the
-empty language. *) 
-lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
-#S #A #w % [|*] * #w1 * #w2 * * #_ *
+lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) - C ≐ (A - C) ∪ (B - C).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
+qed.
+
+(************************ Sets with decidable equality ************************)
+
+(* We say that a property P:A → Prop over a datatype A is decidable when we have 
+an effective way to assess the validity of P a for any a:A. As a consequence of 
+Goedel incompleteness theorem, not every predicate is decidable: for instance, 
+extensional equality on sets is not decidable, in general.  
+
+Decidability can be expressed in several possible ways. A convenient one is to 
+state it in terms of the computability of the characterisitc function of the 
+predicate P, that is in terms of the existence of a function Pb: A → bool such 
+that 
+           P a ⇔ Pb a = true
+           
+Decidability is an important issue, and since equality is an essential 
+predicate, it is always interesting to try to understand when a given notion of 
+equality is decidable or not. 
+
+In particular, Leibniz equality on inductively generated datastructures is often 
+decidable, since we can simply write a decision algorithm by structural 
+induction on the terms. For instance we can define characteristic functions for 
+booleans and natural numbers in the following way: *)
+
+definition beqb ≝ λb1,b2.
+  match b1 with [ true ⇒ b2 | false ⇒ notb b2].
+
+let rec neqb n m ≝ 
+match n with 
+  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
+  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
+  ].
+
+(* It is so important to know if Leibniz equality for a given type is decidable 
+that turns out to be convenient to pack this information into a single algebraic 
+datastructure, called DeqSet: *)
+
+record DeqSet : Type[1] ≝ 
+ { carr :> Type[0];
+   eqb: carr → carr → bool;
+   eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}.
+
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+(* A DeqSet is simply a record composed by a carrier type carr, a boolean 
+function eqb: carr → carr → bool representing the decision algorithm, and a 
+proof eqb_true that the decision algorithm is correct. The :> symbol declares 
+carr as a coercion from a DeqSet to its carrier type. We use the infix notation 
+``=='' for the decidable equality eqb of the carrier.
+
+We can easily prove the following facts: *)
+
+lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
+* * % // normalize #H >H // 
 qed.
 
-(* Concatenating a language l with the singleton language containing the
-empty string, results in the language l; that is {ϵ} is a left and right 
-unit with respect to concatenation. *)
+axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
+(*
+#n elim n 
+  [#m cases m 
+    [% // | #m0 % normalize #H [destruct (H) | @False_ind destruct (H)]] 
+  |#n0 #Hind #m cases m 
+    [% normalize #H destruct (H) |#m0 >(eq_f … S) % #Heq [@eq_f @(Hind m0)//]
+  ]
+qed. *)
+  
+(* Then, we can build the following records: *)
+definition DeqBool : DeqSet ≝ mk_DeqSet bool beqb beqb_true_to_eq.
+definition DeqNat : DeqSet ≝ mk_DeqSet nat neqb neqb_true_to_eq.
+
+(* Note that, since we declare a coercion from the DeqSet to its carrier, the 
+expression 0:DeqNat is well typed, and it is understood by the system as 
+0:carr DeqNat - that is, coercions are automatically insterted by the system, if 
+required. *)
+
+notation "\P H" non associative with precedence 90 
+  for @{(proj1 … (eqb_true ???) $H)}. 
 
-lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
-  A · {ϵ} =1  A. 
-#S #A #w %
-  [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
-  |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
+notation "\b H" non associative with precedence 90 
+  for @{(proj2 … (eqb_true ???) $H)}. 
+  
+lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
+  (eqb ? a b) = false ↔ a ≠ b.
+#S #a #b % #H 
+  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
+  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
   ]
 qed.
+ 
+notation "\Pf H" non associative with precedence 90 
+  for @{(proj1 … (eqb_false ???) $H)}. 
+
+notation "\bf H" non associative with precedence 90 
+  for @{(proj2 … (eqb_false ???) $H)}. 
+
+(****************************** Unification hints *****************************)
+
+(* Suppose now to write an expression of the following kind:
+        b == false
+that, after removing the notation, is equivalent to 
+        eqb ? b false
+The system knows that false is a boolean, so in order to accept the expression, 
+it should "figure out" some DeqSet having bool as carrier. This is not a trivial 
+operation: Matita should either try to synthetize it (that is a complex 
+operation known as narrowing) or look into its database of results for a 
+possible solution. 
+
+In this situations, we may suggest the intended solution to Matita using the 
+mechanism of unification hints \cite{hints}. The concrete syntax of unification 
+hints is a bit involved: we strongly recommend the user to include the file 
+"hints_declaration.ma" that allows you to write thing in a more convenient and 
+readable way. *)
+
+include "hints_declaration.ma".
+
+(* For instance, the following declaration tells Matita that a solution of the 
+equation bool = carr X is X = DeqBool. *)
+
+unification hint 0 ≔ ; 
+    X ≟ DeqBool
+(* ---------------------------------------- *) ⊢ 
+    bool ≡ carr X.
+
+(* Using the previous notation (we suggest the reader to cut and paste it from 
+previous hints) the hint is expressed as an inference rule.
+The conclusion of the rule is the unification problem that we intend to solve, 
+containing one or more variables $X_1,\dots X_b$. The premises of the rule are 
+the solutions we are suggesting to Matita. In general, unification hints should 
+only be used when there exists just one "intended" (canonical) solution for the 
+given equation. 
+When you declare a unification hint, Matita verifies it correctness by 
+instantiating the unification problem with the hinted solution, and checking the 
+convertibility between the two sides of the equation. *)
+ 
+      
+example exhint: ∀b:bool. (b == false) = true → b = false. 
+#b #H @(\P H).
+qed.
 
-lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
-  {ϵ} · A =1  A. 
-#S #A #w %
-  [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
-  |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
+(* In a similar way *)
+
+unification hint  0 ≔ b1,b2:bool; 
+    X ≟ DeqBool
+(* ---------------------------------------- *) ⊢ 
+    beqb b1 b2 ≡ eqb X b1 b2.
+    
+(* pairs *)
+definition eq_pairs ≝
+  λA,B:DeqSet.λp1,p2:A×B.(fst … p1 == fst … p2) ∧ (snd … p1 == snd … p2).
+
+lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
+  eq_pairs A B p1 p2 = true ↔ p1 = p2.
+#A #B * #a1 #b1 * #a2 #b2 %
+  [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
+  |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
   ]
-  qed.
+qed.
+
+definition DeqProd ≝ λA,B:DeqSet.
+  mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+  
+unification hint  0 ≔ C1,C2; 
+    T1 ≟ carr C1,
+    T2 ≟ carr C2,
+    X ≟ DeqProd C1 C2
+(* ---------------------------------------- *) ⊢ 
+    T1×T2 ≡ carr X.
+
+unification hint  0 ≔ T1,T2,p1,p2; 
+    X ≟ DeqProd T1 T2
+(* ---------------------------------------- *) ⊢ 
+    eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+
+example hint2: ∀b1,b2. 
+  〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+#b1 #b2 #H @(\P H)
+qed.
 
-(* Concatenation is distributive w.r.t. union. *)
+(******************************* Prop vs. bool ********************************)
 
-lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
-  (A ∪ B) · C =1  A · C ∪ B · C. 
-#S #A #B #C #w %
-  [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] 
+(* It is probably time to make a discussion about "Prop" and "bool", and their 
+different roles in a the Calculus of Inductive Constructions. 
+
+Inhabitants of the sort "Prop" are logical propositions. In turn, logical
+propositions P:Prop can be inhabitated by their proofs H:P. Since, in general, 
+the validity of a property P is not decidable, the role of the proof is to 
+provide a witness of the correctness of $P$ that the system can automatically 
+check.
+
+On the other hand, bool is just an inductive datatype with two constructors true
+and false: these are terms, not types, and cannot be inhabited.
+Logical connectives on bool are computable functions, defined by their truth 
+tables, using case analysis.
+  
+Prop and bool are, in a sense, complementary: the former is more suited for 
+abstract logical reasoning, while the latter allows, in some situations, for 
+brute-force evaluation. 
+Suppose for instance that we wish to prove that the 4 ≤ 3!. Starting from the 
+definition of the factorial function and properties of the less or equal 
+relation, the previous proof could take several steps. Suppose however we proved
+the decidability of ≤, that is the existence of a boolean function leb 
+reflecting ≤ in the sense that
+    
+                         n ≤ m ⇔ leb n m = true
+             
+Then, we could reduce the verification of 4 ≤ 3! to that of leb 4 3! = true that
+just requires a mere computation! *)
+
+(******************************** Finite Sets *********************************)
+
+(* A finite set is a record consisting of a DeqSet A, a list of elements of type 
+A enumerating all the elements of the set, and the proofs that the enumeration 
+does not contain repetitions and is complete. *)
+
+let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
+  match l with
+  [ nil ⇒ false
+  | cons a tl ⇒ (x == a) ∨ memb S x tl
+  ].
+  
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
 qed.
 
-lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
-  (A ∪ {ϵ}) · C =1  A · C ∪ C. 
-  #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+lemma memb_cons: ∀S,a,b,l. 
+  memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize // 
 qed.
 
-(* The following is a major property of derivatives *)
+lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+  [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
+qed.
 
-lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → deriv S (A·B) a =1 (deriv S A a) · B.
-#S #A #B #a #noteps #w normalize %
-  [* #w1 cases w1 
-    [* #w2 * * #_ #Aeps @False_ind /2/
-    |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
-     #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % //
-    ]
-  |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1))
-   @(ex_intro … w2) % // % normalize //
-  ]
+let rec uniqueb (S:DeqSet) l on l : bool ≝
+  match l with 
+  [ nil ⇒ true
+  | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+  ].
+
+lemma memb_append: ∀S,a,l1,l2. 
+memb S a (l1@l2) = true →
+  memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //] #b #tl #Hind #l2 
+cases (a==b) normalize /2/ 
 qed. 
 
-(* 
-Main Properties of Kleene's star
+lemma memb_append_l1: ∀S,a,l1,l2. 
+ memb S a l1= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize
+  [#le #abs @False_ind /2/ |#b #tl #Hind #l2 cases (a==b) normalize /2/ ]
+qed. 
 
-We conclude this section with some important properties of Kleene's
-star that will be used in the following chapters. *)
+lemma memb_append_l2: ∀S,a,l1,l2. 
+ memb S a l2= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize //#b #tl #Hind #l2 cases (a==b) normalize /2/ 
+qed. 
 
-lemma espilon_in_star: ∀S.∀A:word S → Prop.
-  A^* ϵ.
-#S #A @(ex_intro … [ ]) normalize /2/
+lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → 
+  memb S2 (f a) (map … f l) = true.
+#S1 #S2 #f #a #l elim l normalize [//]
+#x #tl #memba cases (true_or_false (a==x))
+  [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
+  |#eqx >eqx cases (f a==f x) normalize /2/
+  ]
 qed.
 
-lemma cat_to_star:∀S.∀A:word S → Prop.
-  ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
-#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) 
-% normalize /2/
+lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.   
+  memb S1 a1 l1 = true → memb S2 a2 l2 = true →
+  memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
+#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
+  [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map // 
+  |#membtl @memb_append_l2 @Hind //
+  ]
 qed.
 
-lemma fix_star: ∀S.∀A:word S → Prop. 
-  A^* =1 A · A^* ∪ {ϵ}.
-#S #A #w %
-  [* #l generalize in match w; -w cases l [normalize #w * /2/]
-   #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
-   #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
-   % /2/ whd @(ex_intro … tl) /2/
-  |* [2: whd in ⊢ (%→?); #eqw <eqw //]
-   * #w1 * #w2 * * #eqw <eqw @cat_to_star 
+lemma uniqueb_append: ∀A,l1,l2. uniqueb A l1 = true → uniqueb A l2 =true → 
+  (∀a. memb A a l1 =true → ¬ memb A a l2 =true) → uniqueb A (l1@l2) = true.
+#A #l1 elim l1 [normalize //] #a #tl #Hind #l2 #Hatl #Hl2 
+#Hmem normalize cut (memb A a (tl@l2)=false)
+  [2:#Hcut >Hcut normalize @Hind //
+    [@(andb_true_r … Hatl) |#x #Hmemx @Hmem @orb_true_r2 //]
+  |@(noteq_to_eqnot ? true) % #Happend cases (memb_append … Happend)
+    [#H1 @(absurd … H1) @sym_not_eq @eqnot_to_noteq 
+     @sym_eq @(andb_true_l … Hatl)
+    |#H @(absurd … H) @Hmem normalize >(\b (refl ? a)) //
+    ]
   ]
 qed.
 
-lemma star_fix_eps : ∀S.∀A:word S → Prop.
-  A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.  
-#S #A #w %
-  [* #l elim l 
-    [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw // 
-    |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
-       |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1 
-        @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
-         [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
-       ]
+lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,b. 
+  memb ? b (map ?? f l) = true → ∃a. memb ? a l = true ∧ f a = b.
+#A #B #f #l elim l 
+  [#b normalize #H destruct (H) 
+  |#a #tl #Hind #b #H cases (orb_true_l … H) 
+    [#eqb @(ex_intro … a) <(\P eqb) % // 
+    |#memb cases (Hind … memb) #a * #mema #eqb
+     @(ex_intro … a) /3/
     ]
-  |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
-     | whd in ⊢ (%→?); #H <H //
-     ]
   ]
-qed. 
-     
-lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
-  A^* ∪ {ϵ} =1 A^*.
-#S #A #w % /2/ * // 
 qed.
-  
\ No newline at end of file
+
+lemma memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f → 
+  memb ? (f a) (map ?? f l) = true → memb ? a l = true.
+#A #B #f #l #a #injf elim l
+  [normalize //
+  |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
+    [#eqf @orb_true_r1 @(\b ?)  >(injf … (\P eqf)) //
+    |#membtl @orb_true_r2 /2/
+    ]
+  ]
+qed.
+
+lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f → 
+  uniqueb A l = true → uniqueb B (map ?? f l) = true .
+#A #B #f #l #injf elim l 
+  [normalize //
+  |#a #tl #Hind #Htl @true_to_andb_true
+    [@sym_eq @noteq_to_eqnot @sym_not_eq 
+     @(not_to_not ?? (memb_map_inj … injf …) )
+     <(andb_true_l ?? Htl) /2/
+    |@Hind @(andb_true_r ?? Htl)
+    ]
+  ]
+qed.
+
+record FinSet : Type[1] ≝ 
+{ FinSetcarr:> DeqSet;
+  enum: list FinSetcarr;
+  enum_unique: uniqueb FinSetcarr enum = true;
+  enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
+  
+(* The library provides many operations for building new FinSet by composing
+existing ones: for example, if A and B have type FinSet, then also option A, 
+A × B and A + B are finite sets. In all these cases, unification hints are used 
+to suggest the intended finite set structure associated with them, that makes 
+their use quite transparent to the user.*)
+
+definition enum_prod ≝ λA,B:DeqSet.λl1:list A.λl2:list B.
+  compose ??? (pair A B) l1 l2.
+  
+lemma enum_prod_unique: ∀A,B,l1,l2. 
+  uniqueb A l1 = true → uniqueb B l2 = true →
+  uniqueb ? (enum_prod A B l1 l2) = true.
+#A #B #l1 elim l1 //
+  #a #tl #Hind #l2 #H1 #H2 @uniqueb_append 
+  [@unique_map_inj // #b1 #b2 #H3 destruct (H3) //
+  |@Hind // @(andb_true_r … H1)
+  |#p #H3 cases (memb_map_to_exists … H3) #b * 
+   #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
+    [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
+    |elim tl 
+      [normalize //
+      |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
+        [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
+         normalize >(\b (refl ? a)) //
+        |@orb_true_r2 @Hind2 @H4
+        ]
+      ]
+    ]
+  ]
+qed.
+  
+
+lemma enum_prod_complete:∀A,B:DeqSet.∀l1,l2.
+  (∀a. memb A a l1 = true) → (∀b.memb B b l2 = true) →
+    ∀p. memb ? p (enum_prod A B l1 l2) = true.
+#A #B #l1 #l2 #Hl1 #Hl2 * #a #b @memb_compose // 
+qed.
+
+definition FinProd ≝ 
+λA,B:FinSet.mk_FinSet (DeqProd A B)
+  (enum_prod A B (enum A) (enum B)) 
+  (enum_prod_unique A B … (enum_unique A) (enum_unique B)) 
+  (enum_prod_complete A B … (enum_complete A) (enum_complete B)).
+
+unification hint  0 ≔ C1,C2; 
+    T1 ≟ FinSetcarr C1,
+    T2 ≟ FinSetcarr C2,
+    X ≟ FinProd C1 C2
+(* ---------------------------------------- *) ⊢ 
+    T1×T2 ≡ FinSetcarr X.
+
+(* A particularly intersting case is that of the arrow type A → B. We may define 
+the graph of f:A → B, as the set (sigma type) of all pairs 〈a,b〉 such that 
+f a = b. *)
+
+definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (fst … p) = snd … p.
+
+(* In case the equality is decidable, we may effectively enumerate all elements 
+of the graph by simply filtering from pairs in A × B those satisfying the 
+test λp.f (fst … p) == snd … p: *)
+
+definition graph_enum ≝ λA,B:FinSet.λf:A→B. 
+  filter ? (λp.f (fst … p) == snd … p) (enum (FinProd A B)).
+
+(* The proofs that this enumeration does not contain repetitions and
+is complete are straightforward. *)