(*
-Regular Expressions Equivalence
+Moves
+We now define the move operation, that corresponds to the advancement of the
+state in response to the processing of an input character a. The intuition is
+clear: we have to look at points inside $e$ preceding the given character a,
+let the point traverse the character, and broadcast it. All other points must
+be removed.
+
+We can give a particularly elegant definition in terms of the
+lifted operators of the previous section:
*)
include "tutorial/chapter9.ma".
-(* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and
-only if b_1 = b_2. *)
-
-definition cofinal ≝ λS.λp:(pre S)×(pre S).
- \snd (\fst p) = \snd (\snd p).
-
-(* As a corollary of decidable_sem, we have that two expressions
-e1 and e2 are equivalent iff for any word w the states reachable
-through w are cofinal. *)
-
-theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
-#S #e1 #e2 %
-[#same_sem #w
- cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
- [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
- #Hcut @Hcut @iff_trans [|@decidable_sem]
- @iff_trans [|@same_sem] @iff_sym @decidable_sem
-|#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
-qed.
+let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+ [ pz ⇒ 〈 pz S, false 〉
+ | pe ⇒ 〈 ϵ, false 〉
+ | ps y ⇒ 〈 `y, false 〉
+ | pp y ⇒ 〈 `y, x == y 〉
+ | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2)
+ | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
+ | pk e ⇒ (move ? x e)^⊛ ].
+
+lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
+// qed.
-(* This does not directly imply decidability: we have no bound over the
-length of w; moreover, so far, we made no assumption over the cardinality
-of S. Instead of requiring S to be finite, we may restrict the analysis
-to characters occurring in the given pres. *)
-
-definition occ ≝ λS.λe1,e2:pre S.
- unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
-
-lemma occ_enough: ∀S.∀e1,e2:pre S.
-(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
- →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
-#S #e1 #e2 #H #w
-cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
- >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
- >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //]
- //
-qed.
+lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
+// qed.
-(* The following is a stronger version of equiv_sem, relative to characters
-occurring the given regular expressions. *)
+lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
+ move S x i^* = (move ? x i)^⊛.
+// qed.
-lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
-(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
-→ \sem{e1}=1\sem{e2}.
-#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
-qed.
+(*
+Example. Let us consider the item
+
+ (•a + ϵ)((•b)*•a + •b)b
-(*
-Bisimulations
+and the two moves w.r.t. the characters a and b.
+For a, we have two possible positions (all other points gets erased); the innermost
+point stops in front of the final b, while the other one broadcast inside (b^*a + b)b,
+so
+
+ move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
+For b, we have two positions too. The innermost point stops in front of the final b too,
+while the other point reaches the end of b* and must go back through b*a:
+
+ move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a + ϵ)((•b)*•a + b)•b, false〉
-We say that a list of pairs of pres is a bisimulation if it is closed
-w.r.t. moves, and all its members are cofinal.
*)
-definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
- map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
+definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
-lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
- ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
- move ? a (\fst (\snd q)) = \snd p).
-#S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
-#a #tl #Hind #p #q #H cases (orb_true_l … H) -H
- [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
-qed.
+lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b.
+ pmove ? x 〈i,b〉 = move ? x i.
+// qed.
-definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
- ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
+lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b.
+ a::l1 = b::l2 → a = b.
+#A #l1 #l2 #a #b #H destruct //
+qed.
-(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
+(* Obviously, a move does not change the carrier of the item, as one can easily
+prove by induction on the item. *)
-lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
- is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
-#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
-#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
-lapply Hsub @(list_elim_left … w) [//]
-#a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
- [#x #Hx @Hsub @memb_append_l1 //
- |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
- @(memb_map … occa)
+lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
+ |\fst (move ? a i)| = |i|.
+#S #a #i elim i //
+ [#i1 #i2 #H1 #H2 >move_cat >erase_odot //
+ |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); //
]
qed.
-(* This is already an interesting result: checking if l is a bisimulation
-is decidable, hence we could generate l with some untrusted piece of code
-and then run a (boolean version of) is_bisim to check that it is actually
-a bisimulation.
-However, in order to prove that equivalence of regular expressions
-is decidable we must prove that we can always effectively build such a list
-(or find a counterexample).
-The idea is that the list we are interested in is just the set of
-all pair of pres reachable from the initial pair via some
-sequence of moves.
-
-The algorithm for computing reachable nodes in graph is a very
-traditional one. We split nodes in two disjoint lists: a list of
-visited nodes and a frontier, composed by all nodes connected
-to a node in visited but not visited already. At each step we select a node
-a from the frontier, compute its sons, add a to the set of
-visited nodes and the (not already visited) sons to the frontier.
-
-Instead of fist computing reachable nodes and then performing the
-bisimilarity test we can directly integrate it in the algorithm:
-the set of visited nodes is closed by construction w.r.t. reachability,
-so we have just to check cofinality for any node we add to visited.
-
-Here is the extremely simple algorithm: *)
-
-let rec bisim S l n (frontier,visited: list ?) on n ≝
- match n with
- [ O ⇒ 〈false,visited〉 (* assert false *)
- | S m ⇒
- match frontier with
- [ nil ⇒ 〈true,visited〉
- | cons hd tl ⇒
- if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
- bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
- (sons S l hd)) tl) (hd::visited)
- else 〈false,visited〉
+(* Here is our first, major result, stating the correctness of the
+move operation. The proof is a simple induction on i. *)
+
+theorem move_ok:
+ ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S.
+ \sem{move ? a i} w ↔ \sem{i} (a::w).
+#S #a #i elim i
+ [normalize /2/
+ |normalize /2/
+ |normalize /2/
+ |normalize #x #w cases (true_or_false (a==x)) #H >H normalize
+ [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
+ |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
]
- ].
-
-(* The integer n is an upper bound to the number of recursive call,
-equal to the dimension of the graph. It returns a pair composed
-by a boolean and a the set of visited nodes; the boolean is true
-if and only if all visited nodes are cofinal.
-
-The following results explicitly state the behaviour of bisim is the general
-case and in some relevant instances *)
-
-lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
- bisim S l n frontier visited =
- match n with
- [ O ⇒ 〈false,visited〉 (* assert false *)
- | S m ⇒
- match frontier with
- [ nil ⇒ 〈true,visited〉
- | cons hd tl ⇒
- if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
- bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
- (sons S l hd)) tl) (hd::visited)
- else 〈false,visited〉
- ]
- ].
-#S #l #n cases n // qed.
+ |#i1 #i2 #HI1 #HI2 #w >move_cat
+ @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
+ @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r
+ @iff_trans[||@iff_sym @deriv_middot //]
+ @cat_ext_l @HI1
+ |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w
+ @iff_trans[|@sem_oplus]
+ @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
+ |#i1 #HI1 #w >move_star
+ @iff_trans[|@sem_ostar] >same_kernel >sem_star_w
+ @iff_trans[||@iff_sym @deriv_middot //]
+ @cat_ext_l @HI1
+ ]
+qed.
+
+(* The move operation is generalized to strings in the obvious way. *)
+
+notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+
+let rec moves (S : DeqSet) w e on w : pre S ≝
+ match w with
+ [ nil ⇒ e
+ | cons x w' ⇒ w' ↦* (move S x (\fst e))].
+
+lemma moves_empty: ∀S:DeqSet.∀e:pre S.
+ moves ? [ ] e = e.
+// qed.
+
+lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
+ moves ? (a::w) e = moves ? w (move S a (\fst e)).
+// qed.
-lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
- bisim S l O frontier visited = 〈false,visited〉.
-#frontier #visited >unfold_bisim //
+lemma moves_left : ∀S,a,w,e.
+ moves S (w@(a::[])) e = move S a (\fst (moves S w e)).
+#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
qed.
-lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
- bisim Sig l (S m) [] visited = 〈true,visited〉.
-#n #visisted >unfold_bisim //
+lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
+ iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+#S #a #w * #i #b cases b normalize
+ [% /2/ * // #H destruct |% normalize /2/]
qed.
-lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
-beqb (\snd (\fst p)) (\snd (\snd p)) = true →
- bisim Sig l (S m) (p::frontier) visited =
- bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
- (sons Sig l p)) frontier) (p::visited).
-#Sig #l #m #p #frontier #visited #test >unfold_bisim whd in ⊢ (??%?); >test //
+lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
+ |\fst (moves ? w e)| = |\fst e|.
+#S #w elim w //
qed.
-lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
-beqb (\snd (\fst p)) (\snd (\snd p)) = false →
- bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
-#Sig #l #m #p #frontier #visited #test >unfold_bisim whd in ⊢ (??%?); >test //
+theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
+ (\snd (moves ? w e) = true) ↔ \sem{e} w.
+#S #w elim w
+ [* #i #b >moves_empty cases b % /2/
+ |#a #w1 #Hind #e >moves_cons
+ @iff_trans [||@iff_sym @not_epsilon_sem]
+ @iff_trans [||@move_ok] @Hind
+ ]
qed.
-(* In order to prove termination of bisim we must be able to effectively
-enumerate all possible pres: *)
-
-(* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
-#b cases b normalize //
-qed. *)
+(* It is now clear that we can build a DFA D_e for e by taking pre as states,
+and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
+final if and only if b is true. The fact that states in D_e are finite is obvious:
+in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
+e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
+whose finite nature only holds after a suitable quotient.
-let rec pitem_enum S (i:re S) on i ≝
- match i with
- [ z ⇒ (pz S)::[]
- | e ⇒ (pe S)::[]
- | s y ⇒ (ps S y)::(pp S y)::[]
- | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
- | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
- | k i ⇒ map ?? (pk S) (pitem_enum S i)
- ].
-
-lemma pitem_enum_complete : ∀S.∀i:pitem S.
- memb (DeqItem S) i (pitem_enum S (|i|)) = true.
-#S #i elim i
- [1,2://
- |3,4:#c normalize >(\b (refl … c)) //
- |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
- |#i #Hind @(memb_map (DeqItem S)) //
- ]
-qed.
+Let us discuss a couple of examples.
-definition pre_enum ≝ λS.λi:re S.
- compose ??? (λi,b.〈i,b〉) ( pitem_enum S i) (true::false::[]).
-
-lemma pre_enum_complete : ∀S.∀e:pre S.
- memb ? e (pre_enum S (|\fst e|)) = true.
-#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
-// cases b normalize //
-qed.
-
-definition space_enum ≝ λS.λi1,i2: re S.
- compose ??? (λe1,e2.〈e1,e2〉) ( pre_enum S i1) (pre_enum S i2).
+Example.
+Below is the DFA associated with the regular expression (ac+bc)*.
-lemma space_enum_complete : ∀S.∀e1,e2: pre S.
- memb ? 〈e1,e2〉 ( space_enum S (|\fst e1|) (|\fst e2|)) = true.
-#S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
-// qed.
+DFA for (ac+bc)
-definition all_reachable ≝ λS.λe1,e2: pre S.λl: list ?.
-uniqueb ? l = true ∧
- ∀p. memb ? p l = true →
- ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
-
-definition disjoint ≝ λS:DeqSet.λl1,l2.
- ∀p:S. memb S p l1 = true → memb S p l2 = false.
-
-(* We are ready to prove that bisim is correct; we use the invariant
-that at each call of bisim the two lists visited and frontier only contain
-nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair
-which is not cofinal. *)
-
-lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
- ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
- |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
- all_reachable S e1 e2 visited →
- all_reachable S e1 e2 frontier →
- disjoint ? frontier visited →
- \fst (bisim S l n frontier visited) = true.
-#Sig #e1 #e2 #same #l #n elim n
- [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
- @le_to_not_lt @sublist_length // * #e11 #e21 #membp
- cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
- [|* #H1 #H2 <H1 <H2 @space_enum_complete]
- cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
- |#m #HI * [#visited #vinv #finv >bisim_end //]
- #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
- #disjoint
- cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
- [@(r_frontier … (memb_hd … ))] #rp
- cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
- [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
- @(proj1 … (equiv_sem … )) @same] #ptest
- >(bisim_step_true … ptest) @HI -HI
- [<plus_n_Sm //
- |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
- |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
- ]
- |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
- @unique_append_elim #q #H
- [cases (memb_sons … (memb_filter_memb … H)) -H
- #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@(a::[])))
- >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
- |@r_frontier @memb_cons //
- ]
- |@unique_append_elim #q #H
- [@injective_notb @(memb_filter_true … H)
- |cut ((q==p) = false)
- [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
- cases (andb_true … u_frontier) #notp #_ @(\bf ?)
- @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
- ]
- ]
- ]
-qed.
-
-(* For completeness, we use the invariant that all the nodes in visited are cofinal,
-and the sons of visited are either in visited or in the frontier; since
-at the end frontier is empty, visited is hence a bisimulation. *)
-
-definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
- (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
-
-definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
-memb ? x l1 = true → sublist ? (sons ? l x) l2.
-
-lemma bisim_complete:
- ∀S,l,n.∀frontier,visited,visited_res:list ?.
- all_true S visited →
- sub_sons S l visited (frontier@visited) →
- bisim S l n frontier visited = 〈true,visited_res〉 →
- is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
-#S #l #n elim n
- [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
- |#m #Hind *
- [(* case empty frontier *)
- -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
- #H1 destruct % #p
- [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
- |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
- [|(* case head of the frontier is non ok (absurd) *)
- #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
- (* frontier = hd:: tl and hd is ok *)
- #H #tl #visited #visited_res #allv >(bisim_step_true … H)
- (* new_visited = hd::visited are all ok *)
- cut (all_true S (hd::visited))
- [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
- (* we now exploit the induction hypothesis *)
- #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
- [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
- [cases (orb_true_l … membp) -membp #membp
- [@memb_append_l2 >(\P membp) @memb_hd
- |@memb_append_l1 @sublist_unique_append_l2 //
- ]
- |@memb_append_l2 @memb_cons //
- ]
- |(* the only thing left to prove is the sub_sons invariant *)
- #x #membx cases (orb_true_l … membx)
- [(* case x = hd *)
- #eqhdx <(\P eqhdx) #xa #membxa
- (* xa is a son of x; we must distinguish the case xa
- was already visited form the case xa is new *)
- cases (true_or_false … (memb ? xa (x::visited)))
- [(* xa visited - trivial *) #membxa @memb_append_l2 //
- |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
- [>membxa //|//]
- ]
- |(* case x in visited *)
- #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
- [#H2 (cases (orb_true_l … H2))
- [#H3 @memb_append_l2 <(\P H3) @memb_hd
- |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
- ]
- |#H2 @memb_append_l2 @memb_cons @H2
- ]
- ]
- ]
- ]
-qed.
+The graphical description of the automaton is the traditional one, with nodes for
+states and labelled arcs for transitions. Unreachable states are not shown.
+Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
+only if b is true, we may just label nodes with the item.
+The automaton is not minimal: it is easy to see that the two states corresponding to
+the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
+that they define the same language!). In fact, an important property of pres e is that
+each state has a clear semantics, given in terms of the specification e and not of the
+behaviour of the automaton. As a consequence, the construction of the automaton is not
+only direct, but also extremely intuitive and locally verifiable.
-(* We can now give the definition of the equivalence algorithm, and
-prove that two expressions are equivalente if and only if they define
-the same language. *)
-
-definition equiv ≝ λSig.λre1,re2:re Sig.
- let e1 ≝ •(blank ? re1) in
- let e2 ≝ •(blank ? re2) in
- let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
- let sig ≝ (occ Sig e1 e2) in
- (bisim ? sig n (〈e1,e2〉::[]) []).
-
-theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
- \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
-#Sig #re1 #re2 %
- [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
- cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
- [<H //] #Hcut
- cases (bisim_complete … Hcut)
- [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
- #Hbisim #Hsub @(bisim_to_sem … Hbisim)
- @Hsub @memb_hd
- |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
- [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
- |//
- |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
- |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
- |#p #_ normalize //
- ]
- ]
-qed.
+Let us consider a more complex case.
-definition eqbnat ≝ λn,m:nat. eqb n m.
+Example.
+Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
+
+DFA for (a+ϵ)(b*a + b)b
+
+Remarkably, this DFA is minimal, testifying the small number of states produced by our
+technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7
+are final, while 8 and 9 are not).
-lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
-#n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
-qed.
-definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
+Move to pit
+.
-definition a ≝ s DeqNat O.
-definition b ≝ s DeqNat (S O).
-definition c ≝ s DeqNat (S (S O)).
+We conclude this chapter with a few properties of the move opertions in relation
+with the pit state. *)
-definition exp1 ≝ ((a·b)^*·a).
-definition exp2 ≝ a·(b·a)^*.
-definition exp4 ≝ (b·a)^*.
+definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
+
+(* The following function compute the list of characters occurring in a given
+item i. *)
+
+let rec occur (S: DeqSet) (i: re S) on i ≝
+ match i with
+ [ z ⇒ [ ]
+ | e ⇒ [ ]
+ | s y ⇒ y::[]
+ | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ | k e ⇒ occur S e].
+
+(* If a symbol a does not occur in i, then move(i,a) gets to the
+pit state. *)
+
+lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
+ move S a i = pit_pre S i.
+#S #a #i elim i //
+ [#x normalize cases (a==x) normalize // #H @False_ind /2/
+ |#i1 #i2 #Hind1 #Hind2 #H >move_cat
+ >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+ >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+ |#i1 #i2 #Hind1 #Hind2 #H >move_plus
+ >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+ >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+ |#i #Hind #H >move_star >Hind //
+ ]
+qed.
-definition exp6 ≝ a·(a ·a ·b^* + b^* ).
-definition exp7 ≝ a · a^* · b^*.
+(* We cannot escape form the pit state. *)
-definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
-definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
+lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+#S #a #i elim i //
+ [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
+ |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
+ |#i #Hind >move_star >Hind //
+ ]
+qed.
-example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
-normalize // qed.
\ No newline at end of file
+lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+#S #w #i elim w //
+qed.
+
+(* If any character in w does not occur in i, then moves(i,w) gets
+to the pit state. *)
+
+lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
+ moves S w e = pit_pre S (\fst e).
+#S #w elim w
+ [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
+ |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
+ [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
+ @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+ [#H2 >(\P H2) // |#H2 @H1 //]
+ |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
+ ]
+ ]
+qed.
\ No newline at end of file
--- /dev/null
+(*
+Regular Expressions Equivalence
+*)
+
+include "tutorial/chapter9.ma".
+
+(* We say that two pres 〈i_1,b_1〉 and 〈i_1,b_1〉 are {\em cofinal} if and
+only if b_1 = b_2. *)
+
+definition cofinal ≝ λS.λp:(pre S)×(pre S).
+ \snd (\fst p) = \snd (\snd p).
+
+(* As a corollary of decidable_sem, we have that two expressions
+e1 and e2 are equivalent iff for any word w the states reachable
+through w are cofinal. *)
+
+theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 %
+[#same_sem #w
+ cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
+ [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
+ #Hcut @Hcut @iff_trans [|@decidable_sem]
+ @iff_trans [|@same_sem] @iff_sym @decidable_sem
+|#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
+qed.
+
+(* This does not directly imply decidability: we have no bound over the
+length of w; moreover, so far, we made no assumption over the cardinality
+of S. Instead of requiring S to be finite, we may restrict the analysis
+to characters occurring in the given pres. *)
+
+definition occ ≝ λS.λe1,e2:pre S.
+ unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
+
+lemma occ_enough: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+ →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 #H #w
+cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //]
+ //
+qed.
+
+(* The following is a stronger version of equiv_sem, relative to characters
+occurring the given regular expressions. *)
+
+lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+→ \sem{e1}=1\sem{e2}.
+#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
+qed.
+
+(*
+Bisimulations
+
+
+We say that a list of pairs of pres is a bisimulation if it is closed
+w.r.t. moves, and all its members are cofinal.
+*)
+
+definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
+ map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
+
+lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
+ ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
+ move ? a (\fst (\snd q)) = \snd p).
+#S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
+#a #tl #Hind #p #q #H cases (orb_true_l … H) -H
+ [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
+qed.
+
+definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
+ ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
+
+(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
+
+lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
+ is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
+#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
+lapply Hsub @(list_elim_left … w) [//]
+#a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
+ [#x #Hx @Hsub @memb_append_l1 //
+ |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
+ @(memb_map … occa)
+ ]
+qed.
+
+(* This is already an interesting result: checking if l is a bisimulation
+is decidable, hence we could generate l with some untrusted piece of code
+and then run a (boolean version of) is_bisim to check that it is actually
+a bisimulation.
+However, in order to prove that equivalence of regular expressions
+is decidable we must prove that we can always effectively build such a list
+(or find a counterexample).
+The idea is that the list we are interested in is just the set of
+all pair of pres reachable from the initial pair via some
+sequence of moves.
+
+The algorithm for computing reachable nodes in graph is a very
+traditional one. We split nodes in two disjoint lists: a list of
+visited nodes and a frontier, composed by all nodes connected
+to a node in visited but not visited already. At each step we select a node
+a from the frontier, compute its sons, add a to the set of
+visited nodes and the (not already visited) sons to the frontier.
+
+Instead of fist computing reachable nodes and then performing the
+bisimilarity test we can directly integrate it in the algorithm:
+the set of visited nodes is closed by construction w.r.t. reachability,
+so we have just to check cofinality for any node we add to visited.
+
+Here is the extremely simple algorithm: *)
+
+let rec bisim S l n (frontier,visited: list ?) on n ≝
+ match n with
+ [ O ⇒ 〈false,visited〉 (* assert false *)
+ | S m ⇒
+ match frontier with
+ [ nil ⇒ 〈true,visited〉
+ | cons hd tl ⇒
+ if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
+ (sons S l hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+
+(* The integer n is an upper bound to the number of recursive call,
+equal to the dimension of the graph. It returns a pair composed
+by a boolean and a the set of visited nodes; the boolean is true
+if and only if all visited nodes are cofinal.
+
+The following results explicitly state the behaviour of bisim is the general
+case and in some relevant instances *)
+
+lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
+ bisim S l n frontier visited =
+ match n with
+ [ O ⇒ 〈false,visited〉 (* assert false *)
+ | S m ⇒
+ match frontier with
+ [ nil ⇒ 〈true,visited〉
+ | cons hd tl ⇒
+ if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
+ (sons S l hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+#S #l #n cases n // qed.
+
+lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
+ bisim S l O frontier visited = 〈false,visited〉.
+#frontier #visited >unfold_bisim //
+qed.
+
+lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
+ bisim Sig l (S m) [] visited = 〈true,visited〉.
+#n #visisted >unfold_bisim //
+qed.
+
+lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
+beqb (\snd (\fst p)) (\snd (\snd p)) = true →
+ bisim Sig l (S m) (p::frontier) visited =
+ bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
+ (sons Sig l p)) frontier) (p::visited).
+#Sig #l #m #p #frontier #visited #test >unfold_bisim whd in ⊢ (??%?); >test //
+qed.
+
+lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
+beqb (\snd (\fst p)) (\snd (\snd p)) = false →
+ bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
+#Sig #l #m #p #frontier #visited #test >unfold_bisim whd in ⊢ (??%?); >test //
+qed.
+
+(* In order to prove termination of bisim we must be able to effectively
+enumerate all possible pres: *)
+
+(* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
+#b cases b normalize //
+qed. *)
+
+let rec pitem_enum S (i:re S) on i ≝
+ match i with
+ [ z ⇒ (pz S)::[]
+ | e ⇒ (pe S)::[]
+ | s y ⇒ (ps S y)::(pp S y)::[]
+ | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
+ | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
+ | k i ⇒ map ?? (pk S) (pitem_enum S i)
+ ].
+
+lemma pitem_enum_complete : ∀S.∀i:pitem S.
+ memb (DeqItem S) i (pitem_enum S (|i|)) = true.
+#S #i elim i
+ [1,2://
+ |3,4:#c normalize >(\b (refl … c)) //
+ |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
+ |#i #Hind @(memb_map (DeqItem S)) //
+ ]
+qed.
+
+definition pre_enum ≝ λS.λi:re S.
+ compose ??? (λi,b.〈i,b〉) ( pitem_enum S i) (true::false::[]).
+
+lemma pre_enum_complete : ∀S.∀e:pre S.
+ memb ? e (pre_enum S (|\fst e|)) = true.
+#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
+// cases b normalize //
+qed.
+
+definition space_enum ≝ λS.λi1,i2: re S.
+ compose ??? (λe1,e2.〈e1,e2〉) ( pre_enum S i1) (pre_enum S i2).
+
+lemma space_enum_complete : ∀S.∀e1,e2: pre S.
+ memb ? 〈e1,e2〉 ( space_enum S (|\fst e1|) (|\fst e2|)) = true.
+#S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
+// qed.
+
+definition all_reachable ≝ λS.λe1,e2: pre S.λl: list ?.
+uniqueb ? l = true ∧
+ ∀p. memb ? p l = true →
+ ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
+
+definition disjoint ≝ λS:DeqSet.λl1,l2.
+ ∀p:S. memb S p l1 = true → memb S p l2 = false.
+
+(* We are ready to prove that bisim is correct; we use the invariant
+that at each call of bisim the two lists visited and frontier only contain
+nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair
+which is not cofinal. *)
+
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
+ ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
+ |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
+ all_reachable S e1 e2 visited →
+ all_reachable S e1 e2 frontier →
+ disjoint ? frontier visited →
+ \fst (bisim S l n frontier visited) = true.
+#Sig #e1 #e2 #same #l #n elim n
+ [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
+ @le_to_not_lt @sublist_length // * #e11 #e21 #membp
+ cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
+ [|* #H1 #H2 <H1 <H2 @space_enum_complete]
+ cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
+ |#m #HI * [#visited #vinv #finv >bisim_end //]
+ #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
+ #disjoint
+ cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
+ [@(r_frontier … (memb_hd … ))] #rp
+ cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
+ [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
+ @(proj1 … (equiv_sem … )) @same] #ptest
+ >(bisim_step_true … ptest) @HI -HI
+ [<plus_n_Sm //
+ |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
+ |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
+ ]
+ |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
+ @unique_append_elim #q #H
+ [cases (memb_sons … (memb_filter_memb … H)) -H
+ #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@(a::[])))
+ >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
+ |@r_frontier @memb_cons //
+ ]
+ |@unique_append_elim #q #H
+ [@injective_notb @(memb_filter_true … H)
+ |cut ((q==p) = false)
+ [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
+ cases (andb_true … u_frontier) #notp #_ @(\bf ?)
+ @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
+ ]
+ ]
+ ]
+qed.
+
+(* For completeness, we use the invariant that all the nodes in visited are cofinal,
+and the sons of visited are either in visited or in the frontier; since
+at the end frontier is empty, visited is hence a bisimulation. *)
+
+definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
+ (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
+
+definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
+memb ? x l1 = true → sublist ? (sons ? l x) l2.
+
+lemma bisim_complete:
+ ∀S,l,n.∀frontier,visited,visited_res:list ?.
+ all_true S visited →
+ sub_sons S l visited (frontier@visited) →
+ bisim S l n frontier visited = 〈true,visited_res〉 →
+ is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
+#S #l #n elim n
+ [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
+ |#m #Hind *
+ [(* case empty frontier *)
+ -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
+ #H1 destruct % #p
+ [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
+ |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
+ [|(* case head of the frontier is non ok (absurd) *)
+ #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
+ (* frontier = hd:: tl and hd is ok *)
+ #H #tl #visited #visited_res #allv >(bisim_step_true … H)
+ (* new_visited = hd::visited are all ok *)
+ cut (all_true S (hd::visited))
+ [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
+ (* we now exploit the induction hypothesis *)
+ #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
+ [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
+ [cases (orb_true_l … membp) -membp #membp
+ [@memb_append_l2 >(\P membp) @memb_hd
+ |@memb_append_l1 @sublist_unique_append_l2 //
+ ]
+ |@memb_append_l2 @memb_cons //
+ ]
+ |(* the only thing left to prove is the sub_sons invariant *)
+ #x #membx cases (orb_true_l … membx)
+ [(* case x = hd *)
+ #eqhdx <(\P eqhdx) #xa #membxa
+ (* xa is a son of x; we must distinguish the case xa
+ was already visited form the case xa is new *)
+ cases (true_or_false … (memb ? xa (x::visited)))
+ [(* xa visited - trivial *) #membxa @memb_append_l2 //
+ |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
+ [>membxa //|//]
+ ]
+ |(* case x in visited *)
+ #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
+ [#H2 (cases (orb_true_l … H2))
+ [#H3 @memb_append_l2 <(\P H3) @memb_hd
+ |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
+ ]
+ |#H2 @memb_append_l2 @memb_cons @H2
+ ]
+ ]
+ ]
+ ]
+qed.
+
+(* We can now give the definition of the equivalence algorithm, and
+prove that two expressions are equivalente if and only if they define
+the same language. *)
+
+definition equiv ≝ λSig.λre1,re2:re Sig.
+ let e1 ≝ •(blank ? re1) in
+ let e2 ≝ •(blank ? re2) in
+ let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
+ let sig ≝ (occ Sig e1 e2) in
+ (bisim ? sig n (〈e1,e2〉::[]) []).
+
+theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
+ \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+#Sig #re1 #re2 %
+ [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
+ cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
+ [<H //] #Hcut
+ cases (bisim_complete … Hcut)
+ [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
+ #Hbisim #Hsub @(bisim_to_sem … Hbisim)
+ @Hsub @memb_hd
+ |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
+ [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
+ |//
+ |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
+ |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
+ |#p #_ normalize //
+ ]
+ ]
+qed.
+
+definition eqbnat ≝ λn,m:nat. eqb n m.
+
+lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
+#n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
+qed.
+
+definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
+
+definition a ≝ s DeqNat O.
+definition b ≝ s DeqNat (S O).
+definition c ≝ s DeqNat (S (S O)).
+
+definition exp1 ≝ ((a·b)^*·a).
+definition exp2 ≝ a·(b·a)^*.
+definition exp4 ≝ (b·a)^*.
+
+definition exp6 ≝ a·(a ·a ·b^* + b^* ).
+definition exp7 ≝ a · a^* · b^*.
+
+definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
+definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
+
+example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
+normalize // qed.
\ No newline at end of file
let rec add n (m:nat) ≝
match n with
[ O ⇒ m
-| S a ⇒ add (S a) m
+| S a ⇒ S (add a m)
].
-check
-
(* Observe that the definition of a recursive function requires the keyword
"let rec" instead of "definition". The specification of formal parameters is
different too. In this case, they come before the body, and do not require a λ.
example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O))))))
= 〈twice (twice (twice (S O))), ff〉.
// qed.
+
+(********************)
+
+inductive Pari : nat → Prop ≝
+ | pariO : Pari O
+ | pari2 : ∀x. Pari x → Pari (S (S x)).
+
+definition natPari ≝ Sub nat Pari.
+
+definition addPari: natPari → natPari → natPari.
+* #a #Ha * #b #Hb check mk_Sub @(mk_Sub … (add a b))
+elim Ha
+ [normalize @Hb
+ |#x #Hx #Hind normalize @pari2 @Hind
+ ]
+qed.
+
(where "rec" is the binder, "acc" is the bound variable and the rest is the
body) over the initial content expression @{$Px}. *)
+lemma distr_and_or_l : ∀A,B,C:Prop. A ∧(B ∨ C) → (A ∧ B) ∨ (A ∧ C).
+#A #B #C * #H *
+ [#H1 %1 % [@H |@H1] |#H1 %2 % //]
+qed.
+
+lemma distr_and_or_r : ∀A,B,C:Prop. (A ∧ B) ∨ (A ∧ C) → A ∧ (B ∨ C).
+#A #B #C * * #H1 #H2
+ [% [// | %1 //] | % [// | %2 //]
+qed.
+
+
+lemma distr_or_and_l : ∀A,B,C:Prop. A ∨(B ∧ C) → (A ∨ B) ∧ (A ∨ C).
+#A #B #C *
+ [#H % [%1 // |%1 //] | * #H1 #H2 % [%2 // | %2 //] ]
+qed.
+
+lemma distr_or_and_r : ∀A,B,C:Prop. (A ∨ B) ∧ (A ∨ C) → A ∨ (B ∧ C).
+#A #B #C
+* * #H * /3/
+qed.
+
+definition neg ≝ λA:Prop. A → False.
+
+lemma neg_neg : ∀A. A → neg (neg A).
+#A #H normalize #H1 @(H1 H)
+qed.
(***************************** Leibniz Equality *******************************)
#n #H
(* After introducing n and the hypothesis H:O = S n we are left with the goal
-False. Now, observe that (not_zero O) reduces to Fals, hence these two terms
-convertible, that is identical. So, it should be possible to replace False with
-(not_zero O) in the conclusion, since they are the same term.
+False. Now, observe that (not_zero O) reduces to False, hence these two terms
+are convertible, that is identical. So, it should be possible to replace False
+with (not_zero O) in the conclusion, since they are the same term.
The tactic that does the job is the "change with" tactic. The invocation of
"change with t" checks that the current goal is convertible with t, and in this
Propositions as Types
*)
-include "tutorial/chapter3.ma".
include "basics/logic.ma".
(* In the previous section, we introduced many interesting logical connectives
inductive DPair (A:Type[0]) (Q:A → Type[0]) : Type[0] ≝
DPair_intro: ∀x:A. Q x → DPair A Q.
+(* We shall use the notation Σx:A.Q x for the sigma type, and the similar
+notation ∑x:A.Q x for dependent pairs. *)
+
+notation "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation "hvbox(\Sigma ident i break . p)"
+ with precedence 20 for @{'sigma (\lambda ${ident i}. $p) }.
+
+interpretation "Sigma" 'sigma x = (Sig ? x).
+
+notation "hvbox(∑ ident i : ty break . p)"
+ left associative with precedence 20
+ for @{'dpair (\lambda ${ident i} : $ty. $p) }.
+
+notation "hvbox(∑ ident i break . p)"
+ with precedence 20 for @{'dpair (\lambda ${ident i}. $p) }.
+
+interpretation "Sum" 'dpair x = (DPair ? x).
+
(* In the first case (traditionally called sigma type), an element of type
(Sig A P) is a pair (Sig_intro ?? a h) where a is an element of type A and h is a
proof that the property (P a) holds.
definition Sig_snd : ∀A,P.∀x:Sig A P.P (Sig_fst A P x) ≝ λA,P,x.
match x return λx.P (Sig_fst A P x) with [Sig_intro a h ⇒ h].
+
+(* Similarly, we have: *)
+definition DPair_fst ≝ λA:Type[0].λP:A→Type[0].λx:DPair A P.
+ match x with [DPair_intro a h ⇒ a].
+
+definition DPair_snd : ∀A,P.∀x:DPair A P.P (DPair_fst A P x) ≝ λA,P,x.
+ match x return λx.P (DPair_fst A P x) with [DPair_intro a h ⇒ h].
+
(* Remark: The careful reader may have possibly remarked that we also did a
systematic abuse of the arrow symbol: the expression A → B was sometimes
interpreted as the "implication" between A and B and sometimes as the "function
Γ,A ⊢ B Γ ⊢ A → B Γ ⊢ A
---------- -------------------
Γ ⊢ A → B Γ ⊢ B
-
+
The first step is to enrich the representation by decorating formulae with
explicit proof terms. In particular, formulae in the context, being assumptions,
will be decorated with free variables (different form each others), while the
cut | reducible expression (redex)
cut free | normal form
cut elimination | normalization
- correctness |type checking
+ correctness | type checking
*)
(******************************* Prop vs. Type ********************************)
-
+
(* In view of the Curry-Howard analogy, the reader could wonder if there is any
actual difference between the two sorts Prop and Type in a system like the
Calculus of Constructions, or if it just a matter of flavour.
match p with
[ or_introl a ⇒ tt
| or_intror b ⇒ ff
- ].
+ ].
If you type the previous definition, Matita will complain with the following
error message: ``TypeChecker failure: Sort elimination not allowed: Prop towards
].
The error message is the same as before: in both cases the sort of the branches
-is Type[0]. The only think we can do is to return other proof, like in the
+is Type[0]. The only thing we can do is to return other proofs, like in the
following example: *)
definition or_elim ≝ λA,B,C:Prop.λp:A∨B.λf:A→C.λg:B→C.
(* Exercise: repeat the previous examples in interactive mode, eliminating the
hypothesis p:A∨B. *)
+(**************************** The axiom of choice *****************************)
+
+(* The axiom of choice says that given a collection of non-empty sets S_i
+indexed over a base set I, it is possible to make a selection of exactly one
+element x_i ∈ S_i.
+In type theory, this can be expressed in the following terms: *)
+
+axiom choice_ax: ∀I:Type[0].∀S:I→Type[0].∀A:(∀i:I.S i → Type[0]).
+ (∀i:I.(∑x:S i.A i x)) → ∑f:∀i:I.S i.∀i:I.A i (f i).
+
+(* The axiom of choice is independent from the traditional basic axioms of set
+theory, like Zermelo–Fraenkel set theory, hence, if required, must be explicitly
+added to the theory. This extension of ZF, known as ZFC, provides the "standard"
+axiomatization of set theory.
+
+The controversial nature of the axiom of choice is related to the effectiveness
+of performing the selection claimed by the axiom of choice; for this reasons the
+axiom of choice is usually rejected by constructive mathematicians.
+
+However, if the proof of the existence on an inhabitant x_i for each type S_i is
+itself constructive, then this proof already provides a method that, when
+applied to an element i∈I returns the witness x_i. In other words, not only the
+above axiom "choice" is perfectly acceptable, but it is actually provable! *)
+
+theorem choice: ∀I:Type[0].∀S:I→Type[0].∀A.
+ (∀i:I.∑x:S i.A i x) → ∑f:∀i:I.S i.∀i:I.A i (f i).
+#I #S #A #H
+(* The goal is
+ ∑f:∀i:I.S i.(∀i:I.A i (f i))
+We need to provide the function f:∀i:I.S i, and the proof that for any i:I,
+A i (f i). The hypothesis H tells us that for any i we can build an object
+(H i): ∑x:S i.A i x. The first projection of (H i) is an element of type (S i),
+and we may define f ≝ λi. DPair_fst … (H i).The second projection of (H i) is
+a witness of A i (DPair_fst … (H i)), that is, according to our defintion
+of f, a witness of A i (f i). Hence, λi.DPair_snd ?? (H i): ∀i:I.A i (f i). *)
+%{(λi.DPair_fst ?? (H i)) (λi.DPair_snd ?? (H i))}
+qed.
+
+(* It is worth to observe that if we try to repeat the same proof with either
+the existential of the sigma type it will not work. For instance, the
+following property is not provable: *)
+
+axiom Pchoice: ∀I:Type[0].∀S:I→Type[0].∀A.
+ (∀i:I.∃x:S i.A i x) → ∃f:∀i:I.S i.∀i:I.A i (f i).
+
+(* The point is that the proof would require to extract from a non-informative
+content, namely the fact that there exists an x such that (A i x), the actual
+witness x, that is an informative notion, and we know that this is forbidden for
+consistency reasons. *)
+
+
+
+
More Data Types
*)
-include "basics/logic.ma".
+include "tutorial/chapter4.ma".
+include "arithmetics/nat.ma".
+
(******************************** Option Type *********************************)
None : option A
| Some : A → option A.
+let rec pred (n:nat) : option nat ≝
+ match n with
+ [ O ⇒ None nat
+ | S a ⇒ Some nat a
+ ].
+
(* The type option A is isomorphic to the disjoint sum between A and unit. The
-two bijections are simply defined as
-follows:
-\begin{lstlisting}[language=grafite]
-definition option_to_sum ≝ λA.λx:option A.
+two bijections are simply defined as follows: *)
+
+definition option_to_sum : ∀A.option A → unit + A ≝ λA.λx:option A.
match x with
[ None ⇒ inl ?? it
| Some a ⇒ inr ?? a ].
-\end{lstlisting}
-\begin{lstlisting}[language=grafite]
-definition sum_to_option ≝ λA.λx:unit+A.
+definition sum_to_option :∀A. unit + A → option A ≝ λA.λx:unit+A.
match x with
[ inl a ⇒ None A
| inr a ⇒ Some A a ].
-\end{lstlisting}
-The fact that going from the option type to the sum and back again we get the
-original element follows from a straightforward case analysis:
-\begin{lstlisting}[language=grafite]
+
+(* The fact that going from the option type to the sum and back again we get the
+original element follows from a straightforward case analysis: *)
+
lemma option_bij1: ∀A,x. sum_to_option A (option_to_sum A x) = x.
-#A * // qed.
-\end{lstlisting}
-The other direction is just slightly more complex, since we need to exploit
-the fact that the unit type contains a single element: we could use lemma ... or
-proceed by cases on the unit element.
-\begin{lstlisting}[language=grafite]
+#A * [normalize // | #a normalize // ] qed.
+
+(* The other direction is just slightly more complex, since we need to exploit
+the fact that the unit type contains a single element: we could use lemma
+eq_unit or proceed by cases on the unit element. *)
+
lemma option_bij2: ∀A,x. option_to_sum A (sum_to_option A x) = x.
-#A * // * // qed.
-\end{lstlisting}
-We shall see more examples of functions involving the otion type in the
-next section.
-
-\subsection{Lists}
-The option type, as well as the cartesian product or the sum are simple
-examples of polymorphic types, that is types that depend in a uniform
-and effective way on other types. This form of polymorphism (sometimes
-called {\em parametric} polymporphism to distinguish it from the
-{\em ad hoc} polymorphism
-typical of object oriented languages) is a major feature of modern
-functional programming languages: in many intersting cases,
-it allows to write {\em generic} functions operating on inputs without
-depending on their type. Typical examples can be found on lists.
-For instance, appending two lists is an operation that is essentially
-independent from the type $A$ of the elements in the list, and we would like
-to write a {\em single} append function working parametrically on $A$.
-
-The first step is to define a type for lists polimorphic over the
-type $A$ of its elements:
-\begin{lstlisting}[language=grafite]
+#A * #x [normalize cases x // | //] qed.
+
+(* We shall see more examples of functions involving the otion type in the
+next section. *)
+
+(********************************** Lists *************************************)
+
+(* The option type, as well as the cartesian product or the sum are simple
+examples of polymorphic types, that is types that depend in a uniform and
+effective way on other types. This form of polymorphism (sometimes called
+"parametric" polymporphism to distinguish it from the "ad hoc" polymorphism
+typical of object oriented languages) is a major feature of modern functional
+programming languages: in many intersting cases, it allows to write generic
+functions operating on inputs without depending on their type. Typical examples
+can be found on lists.
+For instance, appending two lists is an operation that is essentially
+independent from the type A of the elements in the list, and we would like to
+write a single append function working parametrically on A.
+
+The first step is to define a type for lists polimorphic over the type A of its
+elements: *)
+
inductive list (A:Type[0]) : Type[0] :=
| nil: list A
| cons: A -> list A -> list A.
-\end{lstlisting}
-The deinition should be clear: a list is either empty (\verb+nil+) or
-is is obtained by concatenating (\verb+cons+) an element of type $A$
-to a given list. In other word, the type of lists is the smallest inductive
-type generated by the two constructors \verb+nil+ and \verb+cons+.
-
-The first element of a list is called its {\em head}. If the list
-is empty the head is undefined: as discussed in the previous section,
-we should either return a ``default''
-element, or decide to return an option type.
-We have an additional complication in this
-case, since the ``default'' element should have type $A$ (as the head),
-and we know nothing about $A$ (it could even be an empty type!). We
-have no way to guess a canonical element, and the only
-possibility (along this approach) is to take it in input. These
-are the two options:
-\begin{lstlisting}[language=grafite]
+
+(* The definition should be clear: a list is either empty (nil) or it is
+obtained by concatenating (cons) an element of type A to a given list. In other
+words, the type of lists is the smallest inductive type generated by the two
+constructors nil and cons.
+
+The first element of a list is called its "head". If the list is empty the head
+is undefined: as discussed in the previous section, we should either return a
+``default'' element, or decide to return an option type.
+We have an additional complication in this case, since the ``default'' element
+should have type A, and we know nothing about A (it could even be an empty
+type!). We have no way to guess a canonical element, and the only possibility
+(along this approach) is to take it in input. These are the two options: *)
+
definition hd ≝ λA.λl: list A.λd:A.
match l with [ nil ⇒ d | cons a _ ⇒ a].
-definition option_hd ≝
- λA.λl:list A. match l with
- [ nil ⇒ None ?
- | cons a _ ⇒ Some ? a ].
-\end{lstlisting}
-What remains of a list after removing its head is called the {\em tail}
-of the list. Again, the tail of an empty list is undefined, but in
-this case the result must be a list, and we have a canonical inhabitant
-of lists, that is the empty list. So, it is natural to extend the
-definition of tail saying that the tail of nil is nil (that is
-very similar to say that the predecessor of $0$ is $0$):
-\begin{lstlisting}[language=grafite]
+definition option_hd ≝ λA.λl:list A.
+ match l with [ nil ⇒ None ? | cons a _ ⇒ Some ? a ].
+
+(* What remains of a list after removing its head is called the "tail" of the
+list. Again, the tail of an empty list is undefined, but in this case the result
+must be a list, and we have a canonical inhabitant of lists, that is the empty
+list. So, it is natural to extend the definition of tail saying that the tail of
+nil is nil (that is very similar to say that the predecessor of 0 is 0): *)
+
definition tail ≝ λA.λl: list A.
- match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
-\end{lstlisting}
+ match l with [ nil ⇒ nil ? | cons hd tl ⇒ tl].
+
+(* Using destruct, it is easy to prove that cons is injective in both
+arguments. *)
-Using destruct, it is easy to prove that \verb+cons+ is injective
-in both arguments.
-\begin{lstlisting}[language=grafite]
-lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
+lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.
+ cons ?a1 l1 = cons ? a2 l2 → a1 = a2.
#A #a1 #a2 #l1 #l2 #Heq destruct // qed.
-lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
+lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.
+ cons ? a1 l1 = cons ? a2 l2 → l1 = l2.
#A #a1 #a2 #l1 #l2 #Heq destruct // qed.
-\end{lstlisting}
-The append function is defined by recursion over the first list:
-\begin{lstlisting}[language=grafite]
+
+(* The append function is defined by recursion over the first list: *)
let rec append A (l1: list A) l2 on l1 ≝
match l1 with
[ nil ⇒ l2
- | cons hd tl ⇒ hd :: append A tl l2 ].
-\end{lstlisting}
-We leave to the reader to prove that \verb+append+ is associative, and
-that \verb+nil+ is a neutral element for it.
+ | cons hd tl ⇒ cons ? hd (append A tl l2) ].
+
+(******************************* list notation ********************************)
+
+(* Before discussing more operations over lists, it is convenient to introduce a
+bit of notation; in particular, we shall write a::l for (cons ? a l);
+[a1;a2,…, an] for the list composed by the elements a1, a2,…, an and l1@l2 for
+the concatenation of l1 and l2.
+
+This can be obtained by the following declarations: *)
+
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47 for @{'cons $hd $tl}.
+
+notation "[ list0 term 19 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
-\input{list_notation.tex}
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47 for @{'append $l1 $l2}.
-We conclude this section discussing another important operation
-over lists, namely the reverse funtion, retrurning
-a list with the same elements of the original list but in reverse order.
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
-One could define the revert operation as follows:
-\begin{lstlisting}[language=grafite]
-let rec rev S l1 on l1 ≝
+(* Note that [ ] is an alternative notation for the empty list, and [a] is a
+list containing a singleton element a.
+Let us check the notation: *)
+
+example append_ex1: [true;false]@[true] = [true;false;true].
+normalize // qed.
+
+(* As a simple exerices, now that we have a comfortable notation, let to prove
+that append is associative, and that nil is a neutral element for it. *)
+
+lemma associative_append: ∀A.∀l1,l2,l3:list A. l1 @ (l2 @ l3) = (l1 @ l2) @ l3.
+#A #l1 elim l1 [normalize //]
+#a #tl #Hind #l2 #l3 normalize @eq_f @Hind qed.
+
+lemma append_nil: ∀A.∀l:list A. l@[ ] = l.
+#A #l elim l // #a #tl #Hind normalize >Hind // qed.
+
+let rec length (A:Type[0]) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ O
+ | cons a tl ⇒ 1+(length A tl)
+ ].
+
+interpretation "list length" 'card l = (length ? l).
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
+
+lemma length_append: ∀A.∀l1,l2:list A.
+ |l1@l2| = |l1|+|l2|.
+#A #l1 elim l1 // normalize /2/
+qed.
+
+let rec nth (A:Type[0]) (l:list A) n on n ≝
+ match n with
+ [ O ⇒ option_hd ? l
+ | S x ⇒ nth A (tail ? l) x
+ ].
+
+lemma nth_length : ∀A,l,n. n < length A l → nth A l n ≠ None ?.
+#A #l elim l
+ [#n normalize #H @False_ind /2 by absurd/
+ |#a #tl #Hind #n normalize
+ #H lapply (le_S_S_to_le … H) -H cases n
+ [#_ normalize % #H1 destruct (H1)
+ |#m #H normalize @Hind @H
+ ]
+ ]
+qed.
+
+
+(*************************** More list operations *****************************)
+
+(* We conclude this section discussing another important operation over lists,
+namely the reverse funtion, retrurning a list with the same elements of the
+original list but in reverse order.
+
+One could define the revert operation as follows: *)
+
+let rec rev A (l1: list A) on l1 ≝
match l1 with
- [ nil ⇒ nil
+ [ nil ⇒ nil ?
| cons a tl ⇒ rev A tl @ [a]
].
-\end{lstlisting}
-However, this implementation is sligtly inefficient, since it has a
-quadratic complexity.
-A better solution consists in exploiting an accumulator, passing through
-the following auxilary function:
-\begin{lstlisting}[language=grafite]
-let rec rev_append S (l1,l2:list S) on l1 ≝
+
+(* However, this implementation is sligtly inefficient, since it has a quadratic
+complexity. A better solution consists in exploiting an accumulator, passing
+through the following auxilary function: *)
+
+let rec rev_append A (l1,l2:list A) on l1 ≝
match l1 with
[ nil ⇒ l2
- | cons a tl ⇒ rev_append S tl (a::l2)
+ | cons a tl ⇒ rev_append A tl (a::l2)
].
definition reverse ≝λS.λl.rev_append S l [].
-\end{lstlisting}
-{\bf Exercise} Prove the following results:
-\begin{lstlisting}[language=grafite]
-lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+lemma reverse_single : ∀S,a. reverse S [a] = [a].
+// qed.
+
+example example_rev1: reverse ? [true;false] = [false;true].
+normalize // qed.
+
+(* Let us prove the following results, as a simple exercise.
+
+lemma reverse_cons : ∀A,a,l. reverse A (a::l) = (reverse A l)@[a].
+
+If you try a brute force approach (e.g., induction on l); you will get in
+trouble. The point is that reverse is defined as a particular case of
+rev_append, and you should suitably generalize your result taking rev_append in
+mind.
+*)
+
+lemma rev_append_append: ∀A,l1,l2,l3.
+ rev_append A l1 (l2@l3) = rev_append A l1 l2 @l3.
+#A #l1 elim l1 //
+#hd #tl normalize #Hind #l2 #l3 @(Hind (hd::l2)) qed.
+
+(* Now we get reverse_cons as a trivial corollary, since
+ reverse A (a::l) = rev_append A (a::l) [ ] = rev_append l [a] =
+ rev_append l ([ ]@[a]) = (rev_append l [ ])@[a] = reverse A l @ [a]
+*)
+
+lemma reverse_cons : ∀A,a,l. reverse A (a::l) = reverse A l@[a].
+#A #a #l normalize <rev_append_append % qed.
+
+(* More generally, we can prove the following property of rev_append
+specyfing its general behaviour *)
+
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 #l2 normalize <rev_append_append //
+qed.
lemma reverse_append: ∀S,l1,l2.
reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons >Hind >associative_append //
+qed.
lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
-\end{lstlisting}
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
+>reverse_single >Hind // qed.
-\subsection{List iterators}
-In general, an iterator for some data type is an object that enables to
+(***************************** List iterators *********************************)
+
+(* In general, an iterator for some data type is an object that enables to
traverse its structure performing a given computation.
-There is a canonical set of iterators over lists deriving from
-the programming experience. In this section we shall review a few of
-them, proving some of their properties.
-
-A first, famous iterator is the map function, that
-applies a function $f$ to each element of a list $[a_1,\dots , a_n]$,
-building the list $[f\,a_1; \dots ; f\,a_n]$.
-\begin{lstlisting}[language=grafite]
+There is a canonical set of iterators over lists deriving from the programming
+experience. In this section we shall review a few of them, proving some of their
+properties.
+
+A first, famous iterator is the map function, that applies a function f to each
+element of a list [a1,…, an], building the list [f a1; … ; f an]. *)
+
let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
-\end{lstlisting}
-The \verb+map+ function distributes over \verb+append+, as can be simply
-proved by induction over the first list:
-\begin{lstlisting}[language=grafite]
+
+(* The map function distributes over append, as can be simply proved by
+induction over the first list: *)
+
lemma map_append : ∀A,B,f,l1,l2.
(map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
#A #B #f #l1 elim l1
- [ #l2 @refl | #h #t #IH #l2 normalize // ] qed.
-\end{lstlisting}
-The most important itarator is traditionally called {\em fold}; we
-shall only consider the so called fold-right variant,
-that takes in input a function $f:A\to B \to B$, a list $[a_1; \dots; a_n]$
-of elements of type $A$, a base element $b:B$ and returns
-the value $f\,a_1\,(f\,a_2\,(\dots (f\,a_n\,b) \dots))$.
-\begin{lstlisting}[language=grafite]
+ [ #l2 @refl | #h #t #IH #l2 normalize >IH // ] qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+(* The most important iterator is traditionally called "fold"; we shall only
+consider the so called fold-right variant, that takes in input a function
+f:A→B→B, a list [a1; …; an] of elements of type A, a base element b:B and
+returns the value f a1 (f a2 (… (f an b) …)). *)
+
let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
-\end{lstlisting}
-Many other interesting functions can be defined in terms of \verb+foldr+.
-A first interesting example is the filter function, taking in input
-a boolean test \verb+p+ and a list $l$ and returning the sublist of all
-elements of $l$ satisfying the test.
-\begin{lstlisting}[language=grafite]
+
+(* Many other interesting functions can be defined in terms of foldr. A first
+interesting example is the filter function, taking in input a boolean test p and
+a list l and returning the sublist of all elements of l satisfying the test. *)
+
definition filter ≝
λT.λp:T → bool.
foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
-\end{lstlisting}
-As another example, we can generalize the map function to an operation
-taking in input a binary function $f:A\to B \to C$, two lists
-$[a_1;\dots ;a_n]$ and $[b_1;\dots ;b_m]$ and returning the list
-$[f\,a_1\,b_1; \dots ;f\,a_n\,b_1;\dots ;f\,a_1\,b_m; f\,a_n\,b_m]$
-\begin{lstlisting}[language=grafite]
+
+(* As another example, we can generalize the map function to an operation taking
+in input a binary function f:A → B → C, two lists [a1;… ;an] and [b1;… ;bm] and
+returning the list [f a1 b1; ˙… ;f an b1;… ;f a1 b_m; … f an bm]. *)
+
definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
-\end{lstlisting}
-The folded function $\lambda$\verb+i,acc.(map ?? (f i) l2)@acc+
-takes in input an element $i$ and an accumulator,
-and add to the accumulator the values obtained by mapping the
-partial instantiation $f\,i$ on the elements of $l_2$. This function
-is iterated over
-all elements of the first list $l_1$, starting with an empty accumulator.
-
-\subsection{Naive Set Theory}
-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\to \mbox{Prop}$.
-
-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$.
-
-\begin{lstlisting}[language=grafite]
-definition empty_set ≝ λU:Type[0].λu:U.False.
-definition singleton ≝ λU.λx,u:U.x=u.
-\end{lstlisting}
-
-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:
-
-\begin{lstlisting}[language=grafite]
-definition member ≝ λU:Type[0].λu:U.P→Prop:U.P u.
-\end{lstlisting}
-The operations of union, intersection, complementation and substraction
-are defined in a straightforward way, in terms of logical operations:
-
-\begin{lstlisting}[language=grafite]
-definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a.
-
-definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa..P a ∧ Q a.
-
-definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
-
-definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
-\end{lstlisting}
-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$.
-\begin{lstlisting}[language=grafite]
-definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
-\end{lstlisting}
-Then, two sets $P$ and $Q$ are equal when $P \subseteq Q$ and
-$Q \subseteq P$, or equivalently when for any element $u$,
-$P\,u \iff Q\,u$.
-\begin{lstlisting}[language=grafite]
-definition eqP ≝ λA:Type.λP,Q:A → Prop.∀a:A.P a ↔ Q a.
-\end{lstlisting}
-We shall use the infix notation $\approx$ for the previous notion of
-equality.
-It is important to observe that the \verb+eqP+ is
-different from Leibniz equality of section \ref{}. As we already
-observed, Leibniz equality is a pretty syntactical (or intensional)
-notion, that is a notion concerning the {\em connotation} of an object
-and not its {\em denotation} (the shape assumed by the object, and
-not the information it is supposed to convey). Intensionality stands
-in contrast with {\em extensionality}, referring to principles that
-judge objects to be equal if they enjoy {\em 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\cup B \approx B\cup A$, since they have the same elements, but
-there is no way to prove $A\cup B = B\cup A$.
-
-The main practical consequence is that, while we can always exploit
-a Leibniz equality between two terms $t_1$ and $t_2$ for rewriting
-one into the other (in fact, this is the {\em 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).
-
-\subsection{Sets with decidable equality}
-We say that a property $P:A\to Prop$ over a datatype $A$
-is {\em decidable} when we have an
-effective way to assess the validity of $P\,a$ for any
-$a:A$. As a consequence
-of G\"odel 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 \to \mbox{bool}$ such that
- \[P\,a \iff Pb\,a = \mbox{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:
-\begin{lstlisting}[language=grafite]
-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]
- ].
-\end{lstlisting}
-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 \verb+DeqSet+:
-\begin{lstlisting}[language=grafite]
-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).
-\end{lstlisting}
-A \verb+DeqSet+ is simply a record composed by a carrier type \verb+carr+,
-a boolean function \verb+eqb: carr+$\to$\verb+carr+$\to$\verb+carr+ representing
-the decision algorithm, and a {\em proof} \verb+eqb_true+ that the decision algorithm
-is correct. The \verb+:>+ symbol declares \verb+carr+ as a {\em coercion} from a DeqSet to its
-carrier type. We use the infix notation ``=='' for the decidable
-equality \verb+eqb+ of the carrier.
-
-Suppose we proved the following facts (do it as an exercise)
-\begin{lstlisting}[language=grafite]
-lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2.
-lemma neqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
-\end{lstlisting}
-Then, we can build the following records:
-\begin{lstlisting}[language=grafite]
-definition DeqBool ≝ mk_DeqSet bool beqb beqb_true_to_eq.
-definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
-\end{lstlisting}
-Note that, since we declare a coercion from the \verb+DeqSet+ to its
-carrier, the expression \verb+0:DeqNat+ is well typed, and it is understood
-by the system as \verb+0:carr DeqNat+ (that is, coercions are automatically
-insterted by the system, if required).
-
-%It is convenient to have a simple way to {\em reflect} \cite{ssreflect}
-%a proof of
-%$(eqb\;x\;y = true)$ into a proof of $(x = y)$; we use the two operators
-%$\mathit{\\P}$ and $\mathit{\\b}$ to this aim.
-
-\subsection{Unification hints}
-Suppose now to write an expression of the following kind:
-\[b == \mbox{false}\]
-that, after removing the notation, is equivalent to
-\[eqb\;?\;b\;\mbox{false}\]
-The system knows that $\mbox{false}$ is a boolean, so in order to
-accept the expression, he should {\em figure out} some \verb+DeqSet+
-having \verb+bool+
-as carrier. This is not a trivial operation: Matita should either try
-to synthetize it (that is a complex operation known as {\em 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 \verb+hints_declaration.ma+ that allows you
-to write thing in a more convenient and readable way.
-\begin{lstlisting}[language=grafite]
-include ``hints_declaration.ma''.
-\end{lstlisting}
-For instance, the following declaration tells Matita that a solution
-of the equation \verb+bool = carr X+ is $X = DeqBool$.
-\begin{lstlisting}[language=grafite]
-unification hint 0 ≔ ;
- X ≟ DeqBool
-(* ---------------------------------------- *) ⊢
- bool ≡ carr X.
-\end{lstlisting}
-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.
-\begin{lstlisting}[language=grafite]
-example exhint: ∀b:bool. (b == false) = true → b = false.
-#b #H @(\P H).
-qed.
-\end{lstlisting}
-In a similar way,
-
-\begin{lstlisting}[language=grafite]
-unification hint 0 ≔ b1,b2:bool;
- X ≟ mk_DeqSet bool beqb beqb_true
-(* ---------------------------------------- *) ⊢
- beqb b1 b2 ≡ eqb X b1 b2.
-\end{lstlisting}
-
-
-\subsection{Prop vs. bool}
-It is probably time to make a discussion about \verb+Prop+ and \verb+bool+, and
-their different roles in a the Calculus of Inductive Constructions.
-
-Inhabitants of the sort \verb+Prop+ are logical propositions. In turn, logical
-propositions \verb+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 $2 \le 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 $\le$, that is the existence of
-a boolean function $\mbox{leb}$ reflecting $\le$ in the sense that
-\[n \le m \iff \mbox{leb}\,n,m = \mbox{true}\]
-Then, we could reduce the verification of $2 \le 3!$ to that of
-of $\mbox{leb}\,2,3! = \mbox{true}$ that just requires a mere computation!
-
-\subsection{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 (\verb+memb+ is the membership operation on
-lists, defined in the obvious way, and the question mark is an {\em
-implicit parameter} automatically filled in by the system).
-\begin{lstlisting}[language=grafite]
-record FinSet : ≝
-{ FinSetcarr:> DeqSet;
- enum: list FinSetcarr;
- enum_unique: uniqueb FinSetcarr enum = true;
- enum_complete : ∀x:FinSetcarr. memb ? x enum = true}.
-\end{lstlisting}
-The library provides many operations for building new \verb+FinSet+s by
-composing
-existing ones: for example,
-if \verb+A+ and \verb+B+ have type \verb+FinSet+, then
-also \verb+option A+, \verb+A+$\times$\verb+B+,
-\verb+A+$\oplus$\verb+B+ are finite sets. In all these cases, unification
-hints are used to suggest the {\em intended} finite set structure
-associated with them, that makes their use quite transparent to the user.
-
-A particularly intersting case is that of the arrow type \verb+A+$\to$\verb+B+.
-We may define the graph of \verb+f:A+$\to$\verb+B+, as the
-set (sigma type) of all pairs $\langle a,b \rangle$ such that
-$f (a) = b$.
-\begin{lstlisting}[language=grafite]
-definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (\fst p) = \snd p.
-\end{lstlisting}
-In case the equality is decidable, we may effectively
-enumerate all elements of the graph by simply filtering from
-pairs in \verb+A+$\times$\verb+B+ those satisfying the
-test $\lambda$\verb+p.f (\fst p) == \snd p)+:
-
-\begin{lstlisting}[language=grafite]
-definition graph_enum ≝ λA,B:FinSet.λf:A→B.
- filter ? (λp.f (\fst p) == \snd p) (enum (FinProd A B)).
-\end{lstlisting}
-The proofs that this enumeration does not contain repetitions and
-is complete are straightforward.
-
-\subsection{Vectors}
-A vector of length $n$ of elements of type $A$
-is simply defined in Matita as a record composed
-by a list of elements of type $A$, plus a proof that the
-list has the expected length. Vectors are a paradigmatic example
-of {\em dependent} type, that is of a type whose definition depends on
-a term.
-\begin{lstlisting}[language=grafite]
-record Vector (A:Type) (n:nat): Type ≝
+
+(* The folded function
+ λi,acc.(map ?? (f i) l2)@acc
+takes in input an element i and an accumulator, and add to the accumulator the
+values obtained by mapping the partial instantiation (f i) on the elements of
+l2. This function is iterated over all elements of the first list l1, starting
+with an empty accumulator. *)
+
+(************************************ Vectors *********************************)
+
+(* A vector of length n of elements of type A is simply defined in Matita as a
+record composed by a list of elements of type A, plus a proof that the list has
+the expected length. Vectors are a paradigmatic example of dependent type, that
+is of a type whose definition depends on a term. *)
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝
{ vec :> list A;
len: length ? vec = n }.
-\end{lstlisting}
-Given a list $l$ we may trivially turn it into a vector of length $|l|$;
-we just need to prove that $|l|=|l|$ that follows from the reflexivity
-of equality.
-\begin{lstlisting}[language=grafite]
+
+(* Given a list l we may trivially turn it into a vector of length |l|; we just
+need to prove that |l|=|l| that follows from the reflexivity of equality. *)
+
lemma Vector_of_list ≝ λA,l.mk_Vector A (|l|) l (refl ??).
-\end{lstlisting}
-
-Most functions operating on lists can be naturally extended to
-vectors: interesting cases are \verb+vec_append+, concatenating vectors,
-and \verb+vec_map+, mapping a function $f$ on all elements of the input
-vector and returning a vector of the same dimension of the input one.
-
-Since a vector is automatically coerced, if needed, to the list of
-its elements, we may simply use typical functions over lists (such as
-\verb+nth+) to extract/filter specific components.
-
-The function \verb+change_vec A n v a i+ replaces the content of
-the vector $v$ at position $i$ with the value $a$.
-
-The most frequent operation on vectors for the purposes or our work
-is their comparison. In this case, we have essentially two possible
-approaches: we may proceed component-wise, using the following lemma
-\begin{lstlisting}[language=grafite]
-lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d.
- (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
-\end{lstlisting}
-or alternatively we may manipulate vectors exploiting the commutation
-or idempotency of \verb+change_vec+ and its interplay with
-other operations.
+
+(* Then we can prove that any vector of zero lenght has no elements: *)
+
+lemma vector_nil: ∀A.∀v:Vector A 0.
+ v = Vector_of_list A [ ].
+#A * * // #a #tl normalize #H destruct
+qed.
+
+(* It is convenient to re-define on vectors the hd, tail and cons operations
+on lists *)
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+ mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+ mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+definition vec_hd ≝ λA.λn.λv:Vector A (S n). hd A v ?.
+elim v * [normalize #H destruct | #a #H #eq @a]
+qed.
+
+(* Any vector of lenght (S n) can be expanded as a concatenation of a head and a
+tail vector of length n *)
+
+lemma vec_expand: ∀A,n,v.
+ v = vec_cons A (vec_hd A n v) n (vec_tail A (S n) v).
+#A #n * #l cases l [normalize in ⊢ (%→?); #H destruct |//]
+qed.
+
+(* Most functions operating on lists can be naturally extended to vectors:
+interesting cases are vec_append, concatenating vectors, and vec_map, mapping a
+function f on all elements of the input vector and returning a vector of the
+same dimension of the input one. *)
+
+definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
+mk_Vector A (n1+n2) (v1@v2) ?.
+>length_append >(len … v1) >(len … v2) // qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v)
+ (trans_eq … (length_map …) (len A n v)).
+
+(* Since a vector is automatically coerced, if needed, to the list of its
+elements, we may simply use typical functions over lists (such as nth) to
+extract/filter specific components.
+
+The following function (change_vec A n v a i) replaces the content of the vector
+v at position i with the value a. *)
+
+let rec change_vec (A:Type[0]) (n:nat) on n ≝
+match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
+[ O ⇒ λv,a,i.v
+| S m ⇒ λv,a,i.
+ match i with
+ [ O ⇒ vec_cons A a m (vec_tail … v)
+ | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j)
+ ]
+].
+
+(* A frequent operation between vectors is their comparison. The following
+lemma allow us to reduce the comparisons of vectors of a same lenght to the
+comparison of their components. *)
+
+lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.
+ (∀i. i < n → nth A v1 i = nth A v2 i) → v1 = v2.
+#A #n elim n -n
+ [#v1 #v2 #_ >(vector_nil A v1) >(vector_nil A v2) //
+ |#n #Hind #v1 #v2 #H >(vec_expand … v1) >(vec_expand … v2)
+ >(Hind (vec_tail … v1) (vec_tail … v2))
+ [cut (vec_hd A n v1 = vec_hd A n v2) // lapply (H 0 (lt_O_S ?)) -H
+ >(vec_expand … v1) in ⊢ (%→?); >(vec_expand … v2) in ⊢ (%→?);
+ change with (Some ?? = Some ?? → ?) #H destruct (H) @e0
+ |#i #ltin @(H (S i)) @le_S_S //
+ ]
+ ]
+qed.
+
-(*
-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".
-(* 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: *)
-(* 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 union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a.
+interpretation "union" 'union a b = (union ? a b).
-(* Already in the library
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-*)
+definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∧ Q a.
+interpretation "intersection" 'intersects a b = (intersection ? 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. *)
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? 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 ].
+definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
-(* 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. *)
+(* 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). *)
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀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).
+(* 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. *)
-(* 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. *)
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
-definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+(* We shall use the infix notation ≐ for the previous notion of equality. *)
-(*
-Language equalities
+(* ≐ 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).
-Equality between languages is just the usual extensional equality between
-sets. The operation of concatenation behaves well with respect to this equality. *)
+(* 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.
-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/
-qed.
+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). *)
-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/
-qed.
+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 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.
-(* 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 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.
+
+(************************ 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. *)
-
-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/
+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.
+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.
-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/
- ]
- qed.
+(* 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)}.
-(* Concatenation is distributive w.r.t. union. *)
+notation "\b H" non associative with precedence 90
+ for @{(proj2 … (eqb_true ???) $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 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/]
+(* 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.
-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]
+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.
-(* The following is a major property of derivatives *)
+(******************************* Prop vs. bool ********************************)
-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 //
- ]
+(* 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
+ ].
+
+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 destruct /2/ (* destruct added *)
+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/ (* destruct added *)
- |* [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) % // normalize >(\b (refl ? a)) //
+ |#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.
+
+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. *)
-(*
-Regular Expressions
-
-We shall apply all the previous machinery to the study of regular languages
-and the constructions of the associated finite automata. *)
+(*
+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/chapter6.ma".
-(* The type re of regular expressions over an alphabet $S$ is the smallest
-collection of objects generated by the following constructors: *)
-
-inductive re (S: DeqSet) : Type[0] ≝
- z: re S (* empty: ∅ *)
- | e: re S (* epsilon: ϵ *)
- | s: S → re S (* symbol: a *)
- | c: re S → re S → re S (* concatenation: e1 · e2 *)
- | o: re S → re S → re S (* plus: e1 + e2 *)
- | k: re S → re S. (* kleene's star: e* *)
-
-interpretation "re epsilon" 'epsilon = (e ?).
-interpretation "re or" 'plus a b = (o ? a b).
-interpretation "re cat" 'middot a b = (c ? a b).
-interpretation "re star" 'star a = (k ? a).
-
-notation < "a" non associative with precedence 90 for @{ 'ps $a}.
-notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
-interpretation "atom" 'ps a = (s ? a).
+(* A word (or string) over an alphabet S is just a list of elements of S.*)
+definition word ≝ λS:DeqSet.list S.
-notation "`∅" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
+(* For any alphabet there is only one word of length 0, the empty word, which is
+denoted by ϵ .*)
-(* The language sem{e} associated with the regular expression e is inductively
-defined by the following function: *)
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (nil ?).
-let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
-match r with
-[ z ⇒ ∅
-| e ⇒ {ϵ}
-| s x ⇒ { (x::[]) }
-| c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
-| o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
-| k r1 ⇒ (in_l ? r1) ^*].
+(* 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.
+*)
-notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
-interpretation "in_l" 'in_l E = (in_l ? E).
-interpretation "in_l mem" 'mem w l = (in_l ? l w).
+(*
+Operations over languages
-lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
-// qed.
+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. *)
+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).
-(*
-Pointed Regular expressions
-
-We now introduce pointed regular expressions, that are the main tool we shall
-use for the construction of the automaton.
-A pointed regular expression is just a regular expression internally labelled
-with some additional points. Intuitively, points mark the positions inside the
-regular expression which have been reached after reading some prefix of
-the input string, or better the positions where the processing of the remaining
-string has to be started. Each pointed expression for $e$ represents a state of
-the {\em deterministic} automaton associated with $e$; since we obviously have
-only a finite number of possible labellings, the number of states of the automaton
-is finite.
-
-Pointed regular expressions provide the tool for an algebraic revisitation of
-McNaughton and Yamada's algorithm for position automata, making the proof of its
-correctness, that is far from trivial, particularly clear and simple. In particular,
-pointed expressions offer an appealing alternative to Brzozowski's derivatives,
-avoiding their weakest point, namely the fact of being forced to quotient derivatives
-w.r.t. a suitable notion of equivalence in order to get a finite number of states
-(that is not essential for recognizing strings, but is crucial for comparing regular
-expressions).
-
-Our main data structure is the notion of pointed item, that is meant whose purpose
-is to encode a set of positions inside a regular expression.
-The idea of formalizing pointers inside a data type by means of a labelled version
-of the data type itself is probably one of the first, major lessons learned in the
-formalization of the metatheory of programming languages. For our purposes, it is
-enough to mark positions preceding individual characters, so we shall have two kinds
-of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
-
-inductive pitem (S: DeqSet) : Type[0] ≝
- pz: pitem S (* empty *)
- | pe: pitem S (* epsilon *)
- | ps: S → pitem S (* symbol *)
- | pp: S → pitem S (* pointed sysmbol *)
- | pc: pitem S → pitem S → pitem S (* concatenation *)
- | po: pitem S → pitem S → pitem S (* plus *)
- | pk: pitem S → pitem S. (* kleene's star *)
-
-(* A pointed regular expression (pre) is just a pointed item with an additional
-boolean, that must be understood as the possibility to have a trailing point at
-the end of the expression. As we shall see, pointed regular expressions can be
-understood as states of a DFA, and the boolean indicates if
-the state is final or not. *)
-
-definition pre ≝ λS.pitem S × bool.
-
-interpretation "pitem star" 'star a = (pk ? a).
-interpretation "pitem or" 'plus a b = (po ? a b).
-interpretation "pitem cat" 'middot a b = (pc ? a b).
-notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
-notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
-interpretation "pitem pp" 'pp a = (pp ? a).
-interpretation "pitem ps" 'ps a = (ps ? a).
-interpretation "pitem epsilon" 'epsilon = (pe ?).
-interpretation "pitem empty" 'empty = (pz ?).
-
-(* The carrier $|i|$ of an item i is the regular expression obtained from i by
-removing all the points. Similarly, the carrier of a pointed regular expression
-is the carrier of its item. *)
-
-let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
- match l with
- [ pz ⇒ z ? (* `∅ *)
- | pe ⇒ ϵ
- | ps x ⇒ `x
- | pp x ⇒ `x
- | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
- | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
- | pk E ⇒ (forget ? E)^* ].
+(* 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. *)
(* Already in the library
-notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
*)
-interpretation "forget" 'card a = (forget ? a).
-lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
-// qed.
+(* 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. *)
-lemma erase_plus : ∀S.∀i1,i2:pitem S.
- |i1 + i2| = |i1| + |i2|.
-// qed.
+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 ].
-lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
-// qed.
+(* 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. *)
-(*
-Comparing items and pres
-
-Items and pres are very concrete datatypes: they can be effectively compared,
-and enumerated. In particular, we can define a boolean equality beqitem and a proof
-beqitem_true that it refects propositional equality, enriching the set (pitem S)
-to a DeqSet. *)
-
-let rec beqitem S (i1,i2: pitem S) on i1 ≝
- match i1 with
- [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
- | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
- | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
- | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
- | po i11 i12 ⇒ match i2 with
- [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
- | _ ⇒ false]
- | pc i11 i12 ⇒ match i2 with
- [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
- | _ ⇒ false]
- | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
- ].
-
-lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
-#S #i1 elim i1
- [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
- |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
- |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
- [>(\P H) // | @(\b (refl …))]
- |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
- [>(\P H) // | @(\b (refl …))]
- |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
- normalize #H destruct
- [cases (true_or_false (beqitem S i11 i21)) #H1
- [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
- |>H1 in H; normalize #abs @False_ind /2/
- ]
- |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
- ]
- |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
- normalize #H destruct
- [cases (true_or_false (beqitem S i11 i21)) #H1
- [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
- |>H1 in H; normalize #abs @False_ind /2/
- ]
- |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
- ]
- |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
- normalize #H destruct
- [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
- ]
-qed.
+definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
-definition DeqItem ≝ λS.
- mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
+definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
-(* We also add a couple of unification hints to allow the type inference system
-to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
-equality function of a DeqSet. *)
+notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
+interpretation "star lang" 'star l = (star ? l).
-unification hint 0 ≔ S;
- X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
-(* ---------------------------------------- *) ⊢
- pitem S ≡ carr X.
-
-unification hint 0 ≔ S,i1,i2;
- X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
-(* ---------------------------------------- *) ⊢
- beqitem S i1 i2 ≡ eqb X i1 i2.
+(* 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. *)
+
+definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
(*
-Semantics of pointed regular expressions
-
-The intuitive semantic of a point is to mark the position where
-we should start reading the regular expression. The language associated
-to a pre is the union of the languages associated with its points. *)
-
-let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
-match r with
-[ pz ⇒ ∅
-| pe ⇒ ∅
-| ps _ ⇒ ∅
-| pp x ⇒ { (x::[]) }
-| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
-| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
-| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
-
-interpretation "in_pl" 'in_l E = (in_pl ? E).
-interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
-
-definition in_prl ≝ λS : DeqSet.λp:pre S.
- if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
+Language equalities
+
+Equality between languages is just the usual extensional equality between
+sets. The operation of concatenation behaves well with respect to this equality. *)
+
+lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop.
+ A ≐ C → A · B ≐ C · B.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w1) /6/
+qed.
+
+lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
+ B ≐ C → A · B ≐ A · C.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w2) /6/
+qed.
-interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
-interpretation "in_prl" 'in_l E = (in_prl ? E).
-
-(* The following, trivial lemmas are only meant for rewriting purposes. *)
-
-lemma sem_pre_true : ∀S.∀i:pitem S.
- \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
-// qed.
-
-lemma sem_pre_false : ∀S.∀i:pitem S.
- \sem{〈i,false〉} = \sem{i}.
-// qed.
-
-lemma sem_cat: ∀S.∀i1,i2:pitem S.
- \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
-// qed.
-
-lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
-// qed.
-
-lemma sem_plus: ∀S.∀i1,i2:pitem S.
- \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
-// qed.
-
-lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
-// qed.
-
-lemma sem_star : ∀S.∀i:pitem S.
- \sem{i^*} = \sem{i} · \sem{|i|}^*.
-// qed.
-
-lemma sem_star_w : ∀S.∀i:pitem S.∀w.
- \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
-// qed.
-
-(* Below are a few, simple, semantic properties of items. In particular:
-- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
-- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
-The first property is proved by a simple induction on $i$; the other
-results are easy corollaries. We need an auxiliary lemma first. *)
-
-lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
-#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
-
-lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
-#S #e elim e normalize /2/
- [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
- >(append_eq_nil …H…) /2/
- |#r1 #r2 #n1 #n2 % * /2/
- |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
+(* Concatenating a language with the empty language results in the
+empty language. *)
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A ≐ ∅.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+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. *)
+
+lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
+ A · {ϵ} ≐ A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
+ |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
+ ]
+qed.
+
+lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
+ {ϵ} · A ≐ A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
+ |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
]
qed.
-lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
-#S * #i #b cases b // normalize #H @False_ind /2/
+(* Concatenation is distributive w.r.t. union. *)
+
+lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
+ (A ∪ B) · C ≐ A · C ∪ B · C.
+#S #A #B #C #w %
+ [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
qed.
-lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
-#S * #i #b #btrue normalize in btrue; >btrue %2 //
+lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
+ (A ∪ {ϵ}) · C ≐ A · C ∪ C.
+ #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
qed.
-lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-#S #i #w %
- [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
- |* //
+(* The following is a major property of derivatives *)
+
+lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → deriv S (A·B) a ≐ (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 //
+ ]
+qed.
+
+(*
+Main Properties of Kleene's star
+
+We conclude this section with some important properties of Kleene's
+star that will be used in the following chapters. *)
+
+lemma espilon_in_star: ∀S.∀A:word S → Prop.
+ A^* ϵ.
+#S #A @(ex_intro … [ ]) 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 destruct /2/
+qed.
+
+lemma fix_star: ∀S.∀A:word S → Prop.
+ A^* ≐ 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
]
qed.
-lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
-#S * #i *
- [>sem_pre_true normalize in ⊢ (??%?); #w %
- [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
- |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
+lemma star_fix_eps : ∀S.∀A:word S → Prop.
+ A^* ≐ (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 % [@H2 | % #H4 destruct (H4)] ]
+ |whd @(ex_intro … tl) /2/]
+ ]
+ ]
+ |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
+ | whd in ⊢ (%→?); #H <H //
+ ]
]
+qed.
+
+lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
+ A^* ∪ {ϵ} ≐ A^*.
+#S #A #w % /2/ * //
qed.
+
-(*
-Broadcasting points
-
-Intuitively, a regular expression e must be understood as a pointed expression with a single
-point in front of it. Since however we only allow points before symbols, we must broadcast
-this initial point inside e traversing all nullable subexpressions, that essentially corresponds
-to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
-its definition is the expected one: let us start discussing an example.
-
-Example
-Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the
-first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence
-reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in
-parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the
-star, and to traverse it, stopping in front of a; the second point just stops in front of b.
-No point reached that end of b^*a + b hence no further propagation is possible. In conclusion:
- •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
-*)
+(*
+Regular Expressions
+
+We shall apply all the previous machinery to the study of regular languages
+and the constructions of the associated finite automata. *)
include "tutorial/chapter7.ma".
-(* Broadcasting a point inside an item generates a pre, since the point could possibly reach
-the end of the expression.
-Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
-If we define
- 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
-then, we just have •(i1+i2) = •(i1)⊕ •(i2).
-*)
+(* The type re of regular expressions over an alphabet $S$ is the smallest
+collection of objects generated by the following constructors: *)
-definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
+inductive re (S: DeqSet) : Type[0] ≝
+ z: re S (* empty: ∅ *)
+ | e: re S (* epsilon: ϵ *)
+ | s: S → re S (* symbol: a *)
+ | c: re S → re S → re S (* concatenation: e1 · e2 *)
+ | o: re S → re S → re S (* plus: e1 + e2 *)
+ | k: re S → re S. (* kleene's star: e* *)
-lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
-// qed.
+interpretation "re epsilon" 'epsilon = (e ?).
+interpretation "re or" 'plus a b = (o ? a b).
+interpretation "re cat" 'middot a b = (c ? a b).
+interpretation "re star" 'star a = (k ? a).
-(*
-Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2
-we should start broadcasting it inside i1 and then proceed into i2 if and only if a
-point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where
-e ▹ i is a general operation of concatenation between a pre and an item, defined by
-cases on the boolean in e:
-
- 〈i1,true〉 ▹ i2 = i1 ◃ •(i_2)
- 〈i1,false〉 ▹ i2 = i1 · i2
-In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
- i1 ◃ 〈i1,b〉 = 〈i_1 · i2, b〉
-Let us come to the formalized definitions:
-*)
+notation < "a" non associative with precedence 90 for @{ 'ps $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
+interpretation "atom" 'ps a = (s ? a).
-definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
- match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
-
-notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
-interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
+notation "`∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
-lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
- A = B → A =1 B.
-#S #A #B #H >H #x % // qed.
+(* The language sem{e} associated with the regular expression e is inductively
+defined by the following function: *)
-(* The behaviour of ◃ is summarized by the following, easy lemma: *)
+let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
+match r with
+[ z ⇒ ∅
+| e ⇒ {ϵ}
+| s x ⇒ { (x::[]) }
+| c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
+| o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
+| k r1 ⇒ (in_l ? r1) ^*].
-lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
- \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
-#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
->sem_pre_true >sem_cat >sem_pre_true /2/
-qed.
-
-(* The definition of $•(-)$ (eclose) and ▹ (pre_concat_l) are mutually recursive.
-In this situation, a viable alternative that is usually simpler to reason about,
-is to abstract one of the two functions with respect to the other. In particular
-we abstract pre_concat_l with respect to an input bcast function from items to
-pres. *)
-
-definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
- match e1 with
- [ mk_Prod i1 b1 ⇒ match b1 with
- [ true ⇒ (i1 ◃ (bcast ? i2))
- | false ⇒ 〈i1 · i2,false〉
- ]
- ].
-
-notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
-interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
-
-(* We are ready to give the formal definition of the broadcasting operation. *)
-
-notation "•" non associative with precedence 60 for @{eclose ?}.
-let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
- match i with
- [ pz ⇒ 〈 pz ?, false 〉
- | pe ⇒ 〈 ϵ, true 〉
- | ps x ⇒ 〈 `.x, false 〉
- | pp x ⇒ 〈 `.x, false 〉
- | po i1 i2 ⇒ •i1 ⊕ •i2
- | pc i1 i2 ⇒ •i1 ▹ i2
- | pk i ⇒ 〈(\fst (•i))^*,true〉].
-
-notation "• x" non associative with precedence 60 for @{'eclose $x}.
-interpretation "eclose" 'eclose x = (eclose ? x).
-
-(* Here are a few simple properties of ▹ and •(-) *)
+notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
+interpretation "in_l" 'in_l E = (in_l ? E).
+interpretation "in_l mem" 'mem w l = (in_l ? l w).
-lemma pcl_true : ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
+lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
// qed.
-lemma pcl_true_bis : ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
-#S #i1 #i2 normalize cases (•i2) // qed.
-lemma pcl_false: ∀S.∀i1,i2:pitem S.
- 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
-// qed.
+(*
+Pointed Regular expressions
+
+We now introduce pointed regular expressions, that are the main tool we shall
+use for the construction of the automaton.
+A pointed regular expression is just a regular expression internally labelled
+with some additional points. Intuitively, points mark the positions inside the
+regular expression which have been reached after reading some prefix of
+the input string, or better the positions where the processing of the remaining
+string has to be started. Each pointed expression for $e$ represents a state of
+the {\em deterministic} automaton associated with $e$; since we obviously have
+only a finite number of possible labellings, the number of states of the automaton
+is finite.
+
+Pointed regular expressions provide the tool for an algebraic revisitation of
+McNaughton and Yamada's algorithm for position automata, making the proof of its
+correctness, that is far from trivial, particularly clear and simple. In particular,
+pointed expressions offer an appealing alternative to Brzozowski's derivatives,
+avoiding their weakest point, namely the fact of being forced to quotient derivatives
+w.r.t. a suitable notion of equivalence in order to get a finite number of states
+(that is not essential for recognizing strings, but is crucial for comparing regular
+expressions).
+
+Our main data structure is the notion of pointed item, that is meant whose purpose
+is to encode a set of positions inside a regular expression.
+The idea of formalizing pointers inside a data type by means of a labelled version
+of the data type itself is probably one of the first, major lessons learned in the
+formalization of the metatheory of programming languages. For our purposes, it is
+enough to mark positions preceding individual characters, so we shall have two kinds
+of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
+
+inductive pitem (S: DeqSet) : Type[0] ≝
+ pz: pitem S (* empty *)
+ | pe: pitem S (* epsilon *)
+ | ps: S → pitem S (* symbol *)
+ | pp: S → pitem S (* pointed sysmbol *)
+ | pc: pitem S → pitem S → pitem S (* concatenation *)
+ | po: pitem S → pitem S → pitem S (* plus *)
+ | pk: pitem S → pitem S. (* kleene's star *)
+
+(* A pointed regular expression (pre) is just a pointed item with an additional
+boolean, that must be understood as the possibility to have a trailing point at
+the end of the expression. As we shall see, pointed regular expressions can be
+understood as states of a DFA, and the boolean indicates if
+the state is final or not. *)
+
+definition pre ≝ λS.pitem S × bool.
+
+interpretation "pitem star" 'star a = (pk ? a).
+interpretation "pitem or" 'plus a b = (po ? a b).
+interpretation "pitem cat" 'middot a b = (pc ? a b).
+notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "pitem pp" 'pp a = (pp ? a).
+interpretation "pitem ps" 'ps a = (ps ? a).
+interpretation "pitem epsilon" 'epsilon = (pe ?).
+interpretation "pitem empty" 'empty = (pz ?).
+
+(* The carrier $|i|$ of an item i is the regular expression obtained from i by
+removing all the points. Similarly, the carrier of a pointed regular expression
+is the carrier of its item. *)
+
+let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
+ match l with
+ [ pz ⇒ z ? (* `∅ *)
+ | pe ⇒ ϵ
+ | ps x ⇒ `x
+ | pp x ⇒ `x
+ | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
+ | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
+ | pk E ⇒ (forget ? E)^* ].
+
+(* Already in the library
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+*)
+interpretation "forget" 'card a = (forget ? a).
-lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 + i2) = •i1 ⊕ •i2.
+lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
// qed.
-lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 · i2) = •i1 ▹ i2.
+lemma erase_plus : ∀S.∀i1,i2:pitem S.
+ |i1 + i2| = |i1| + |i2|.
// qed.
-lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
- •i^* = 〈(\fst(•i))^*,true〉.
+lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
// qed.
-(* The definition of •(-) (eclose) can then be lifted from items to pres
-in the obvious way. *)
+(*
+Comparing items and pres
+
+Items and pres are very concrete datatypes: they can be effectively compared,
+and enumerated. In particular, we can define a boolean equality beqitem and a proof
+beqitem_true that it refects propositional equality, enriching the set (pitem S)
+to a DeqSet. *)
+
+let rec beqitem S (i1,i2: pitem S) on i1 ≝
+ match i1 with
+ [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
+ | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
+ | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
+ | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
+ | po i11 i12 ⇒ match i2 with
+ [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+ | _ ⇒ false]
+ | pc i11 i12 ⇒ match i2 with
+ [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+ | _ ⇒ false]
+ | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
+ ].
-definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
- match e with
- [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
-
-definition preclose ≝ λS. lift S (eclose S).
-interpretation "preclose" 'eclose x = (preclose ? x).
-
-(* Obviously, broadcasting does not change the carrier of the item,
-as it is easily proved by structural induction. *)
-
-lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
-#S #i elim i //
- [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
- cases (•i1) #i11 #b1 cases b1 // <IH2 >pcl_true_bis //
- | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
- cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
- | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
+lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
+#S #i1 elim i1
+ [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+ |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+ |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+ [>(\P H) // | @(\b (refl …))]
+ |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+ [>(\P H) // | @(\b (refl …))]
+ |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+ normalize #H destruct
+ [cases (true_or_false (beqitem S i11 i21)) #H1
+ [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @False_ind /2/
+ ]
+ |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ ]
+ |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+ normalize #H destruct
+ [cases (true_or_false (beqitem S i11 i21)) #H1
+ [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @False_ind /2/
+ ]
+ |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ ]
+ |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
+ normalize #H destruct
+ [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
]
-qed.
-
-(* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
-
-sem_oplus: \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}
-sem_pcl: \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}
-sem_bullet \sem{•i} =1 \sem{i} ∪ \sem{|i|}
-
-The proof of sem_oplus is straightforward. *)
+qed.
+
+definition DeqItem ≝ λS.
+ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
+
+(* We also add a couple of unification hints to allow the type inference system
+to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
+equality function of a DeqSet. *)
+
+unification hint 0 ≔ S;
+ X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢
+ pitem S ≡ carr X.
+
+unification hint 0 ≔ S,i1,i2;
+ X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢
+ beqitem S i1 i2 ≡ eqb X i1 i2.
+
+(*
+Semantics of pointed regular expressions
+
+The intuitive semantic of a point is to mark the position where
+we should start reading the regular expression. The language associated
+to a pre is the union of the languages associated with its points. *)
+
+let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
+match r with
+[ pz ⇒ ∅
+| pe ⇒ ∅
+| ps _ ⇒ ∅
+| pp x ⇒ { (x::[]) }
+| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
+| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
+| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
+
+interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+definition in_prl ≝ λS : DeqSet.λp:pre S.
+ if (snd ?? p) then \sem{fst ?? p} ∪ {ϵ} else \sem{fst ?? p}.
+
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_l E = (in_prl ? E).
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
-#S * #i1 #b1 * #i2 #b2 #w %
- [cases b1 cases b2 normalize /2/ * /3/ * /3/
- |cases b1 cases b2 normalize /2/ * /3/ * /3/
- ]
-qed.
+(* The following, trivial lemmas are only meant for rewriting purposes. *)
-(* For the others, we proceed as follow: we first prove the following
-auxiliary lemma, that assumes sem_bullet:
+lemma sem_pre_true : ∀S.∀i:pitem S.
+ \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
+// qed.
-sem_pcl_aux:
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+lemma sem_pre_false : ∀S.∀i:pitem S.
+ \sem{〈i,false〉} = \sem{i}.
+// qed.
-Then, using the previous result, we prove sem_bullet by induction
-on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
+lemma sem_cat: ∀S.∀i1,i2:pitem S.
+ \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
+// qed.
-lemma LcatE : ∀S.∀e1,e2:pitem S.
- \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
+lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
+ \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
// qed.
-lemma sem_pcl_aux : ∀S.∀e1:pre S.∀i2:pitem S.
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
-#S * #i1 #b1 #i2 cases b1
- [2:#th >pcl_false >sem_pre_false >sem_pre_false >sem_cat /2/
- |#H >pcl_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
- >erase_bull @eqP_trans [|@(eqP_union_l … H)]
- @eqP_trans [|@eqP_union_l[|@union_comm ]]
- @eqP_trans [|@eqP_sym @union_assoc ] /3/
- ]
-qed.
-
-lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
- \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
-#S #e #i #A #seme
-@eqP_trans [|@minus_eps_pre]
-@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
-@eqP_trans [||@distribute_substract]
-@eqP_substract_r //
-qed.
+lemma sem_plus: ∀S.∀i1,i2:pitem S.
+ \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
+// qed.
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
-#S #e elim e
- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@sem_pcl_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l … IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
- ]
-qed.
+lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
+ \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
+// qed.
-(*
-Blank item
-
+lemma sem_star : ∀S.∀i:pitem S.
+ \sem{i^*} = \sem{i} · \sem{|i|}^*.
+// qed.
-As a corollary of theorem sem_bullet, given a regular expression e, we can easily
-find an item with the same semantics of $e$: it is enough to get an item (blank e)
-having e as carrier and no point, and then broadcast a point in it. The semantics of
-(blank e) is obviously the empty language: from the point of view of the automaton,
-it corresponds with the pit state. *)
-
-let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
- match i with
- [ z ⇒ pz ?
- | e ⇒ ϵ
- | s y ⇒ `y
- | o e1 e2 ⇒ (blank S e1) + (blank S e2)
- | c e1 e2 ⇒ (blank S e1) · (blank S e2)
- | k e ⇒ (blank S e)^* ].
-
-lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
-#S #e elim e normalize //
-qed.
+lemma sem_star_w : ∀S.∀i:pitem S.∀w.
+ \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
+// qed.
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
-#S #e elim e
- [1,2:@eq_to_ex_eq //
- |#s @eq_to_ex_eq //
- |#e1 #e2 #Hind1 #Hind2 >sem_cat
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
- |#e1 #e2 #Hind1 #Hind2 >sem_plus
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
- |#e #Hind >sem_star
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
+(* Below are a few, simple, semantic properties of items. In particular:
+- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
+- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+The first property is proved by a simple induction on $i$; the other
+results are easy corollaries. We need an auxiliary lemma first. *)
+
+lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
+#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
+
+lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
+#S #e elim e normalize
+ [1,2,3:/2/
+ |#x % #H destruct
+ |#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
+ >(append_eq_nil …H…) /2/
+ |#r1 #r2 #n1 #n2 % * /2/
+ |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
]
qed.
-
-theorem re_embedding: ∀S.∀e:re S.
- \sem{•(blank S e)} =1 \sem{e}.
-#S #e @eqP_trans [|@sem_bull] >forget_blank
-@eqP_trans [|@eqP_union_r [|@sem_blank]]
-@eqP_trans [|@union_comm] @union_empty_r.
-qed.
-
-(*
-Lifted Operators
-
-
-Plus and bullet have been already lifted from items to pres. We can now
-do a similar job for concatenation ⊙ and Kleene's star ⊛.*)
-
-definition lifted_cat ≝ λS:DeqSet.λe:pre S.
- lift S (pre_concat_l S eclose e).
-
-notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
-interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
-
-lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
-#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
+lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → snd … e = true.
+#S * #i #b cases b // normalize #H @False_ind /2/
qed.
-lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
-//
-qed.
-
-lemma erase_odot:∀S.∀e1,e2:pre S.
- |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
-#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
+lemma true_to_epsilon : ∀S.∀e:pre S. snd … e = true → ϵ ∈ e.
+#S * #i #b #btrue normalize in btrue; >btrue %2 //
qed.
-(* Let us come to the star operation: *)
-
-definition lk ≝ λS:DeqSet.λe:pre S.
- match e with
- [ mk_Prod i1 b1 ⇒
- match b1 with
- [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
- |false ⇒ 〈i1^*,false〉
- ]
- ].
-
-(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
-interpretation "lk" 'lk a = (lk ? a).
-notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
-
-lemma ostar_true: ∀S.∀i:pitem S.
- 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
-// qed.
-
-lemma ostar_false: ∀S.∀i:pitem S.
- 〈i,false〉^⊛ = 〈i^*, false〉.
-// qed.
-
-lemma erase_ostar: ∀S.∀e:pre S.
- |\fst (e^⊛)| = |\fst e|^*.
-#S * #i * // qed.
-
-lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
- \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
-#S #e1 #i
-cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
-#H >H cases (e1 ▹ i) #i1 #b1 cases b1
- [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l /2/
- |/2/
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+#S #i #w %
+ [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
+ |* //
]
qed.
-lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
- e1 ⊙ 〈i,false〉 = e1 ▹ i.
-#S #e1 #i
-cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
-cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
-qed.
-
-(* We conclude this section with the proof of the main semantic properties
-of ⊙ and ⊛. *)
-
-lemma sem_odot:
- ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
-#S #e1 * #i2 *
- [>sem_pre_true
- @eqP_trans [|@sem_odot_true]
- @eqP_trans [||@union_assoc] @eqP_union_r @sem_pcl_aux //
- |>sem_pre_false >eq_odot_false @sem_pcl_aux //
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{fst ?? e} ≐ \sem{e}-{[ ]}.
+#S * #i *
+ [>sem_pre_true normalize in ⊢ (??%?); #w %
+ [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
+ |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
]
qed.
-
-theorem sem_ostar: ∀S.∀e:pre S.
- \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
-#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
- @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
- |>sem_pre_false >sem_pre_false >sem_star /2/
- ]
-qed.
\ No newline at end of file
projects / helm.git / commitdiff