-(*
-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).
-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 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 cat : ∀S,l1,l2,w.Prop ≝
- λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
-(*
-notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
-*)
-interpretation "cat lang" 'middot a b = (cat ? a b).
+definition member ≝ λU:Type[0].λu:U.λP:U→Prop.P u.
+
+(* The operations of union, intersection, complementation and substraction are
+defined in a straightforward way, in terms of logical operations: *)
+definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a.
+interpretation "union" 'union a b = (union ? a b).
-(* 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 intersection ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∧ Q a.
+interpretation "intersection" 'intersects a b = (intersection ? a b).
-(* FG: flatten in list.ma gets in the way:
-alias id "flatten" = "cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)".
-does not work, so we use flatten in lists for now
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-*)
+definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
-(* 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. *)
+(* 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). *)
-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 ].
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
-(* 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. *)
+(* 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. *)
+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))
-% destruct // 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))
- % destruct /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. *)
projects / helm.git / blobdiff