From 278be9d611634dce13657bbe14b5c1bb4f7dd2be Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 23 Dec 2014 20:26:11 +0000 Subject: [PATCH] A compiling version --- matita/matita/lib/tutorial/chapter1.ma | 2 +- matita/matita/lib/tutorial/chapter10.ma | 117 ++++++++++++++++++++++-- matita/matita/lib/tutorial/chapter11.ma | 110 ++++++++++++++-------- matita/matita/lib/tutorial/chapter13.ma | 2 +- matita/matita/lib/tutorial/chapter6.ma | 16 +++- matita/matita/lib/tutorial/chapter8.ma | 4 +- 6 files changed, 201 insertions(+), 50 deletions(-) diff --git a/matita/matita/lib/tutorial/chapter1.ma b/matita/matita/lib/tutorial/chapter1.ma index f2c70a238..bd568a1f4 100644 --- a/matita/matita/lib/tutorial/chapter1.ma +++ b/matita/matita/lib/tutorial/chapter1.ma @@ -206,7 +206,7 @@ them in turn, in a way that will be described at the end of this section. (********************************** Predicates ********************************) -(*I nstead of working with functions, it is sometimes convenient to work with +(* Instead of working with functions, it is sometimes convenient to work with predicates. For instance, instead of defining a function computing the opposite bank, we could declare a predicate stating when two banks are opposite to each other. Only two cases are possible, leading naturally to the following diff --git a/matita/matita/lib/tutorial/chapter10.ma b/matita/matita/lib/tutorial/chapter10.ma index b68736222..38141ae4e 100644 --- a/matita/matita/lib/tutorial/chapter10.ma +++ b/matita/matita/lib/tutorial/chapter10.ma @@ -192,8 +192,107 @@ with the pit state. *) definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. -(* The following function compute the list of characters occurring in a given -item i. *) +(* The following "occur" function compute the list of characters occurring in a +given item i. We first define a special append function that appends two lists +avoiding repetitions, and prove a few properties of it. +*) + +let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons a tl ⇒ + let r ≝ unique_append S tl l2 in + if memb S a r then r else a::r + ]. + +lemma memb_unique_append: ∀S,a,l1,l2. +memb S a (unique_append S 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 (true_or_false … (a==b)) #Hab >Hab normalize /2/ +cases (memb S b (unique_append S tl l2)) normalize + [@Hind | >Hab normalize @Hind] +qed. + +lemma unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. +(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) → +∀x. memb S x (unique_append S l1 l2) = true → P x. +#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) +/2/ +qed. + +lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true → + uniqueb S (unique_append S l1 l2) = true. +#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2 +cases (true_or_false … (memb S a (unique_append S tl l2))) +#H >H normalize [@Hind //] >H normalize @Hind // +qed. + +definition sublist ≝ + λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true. + +lemma memb_exists: ∀S,a,l.memb S a l = true → + ∃l1,l2.l=l1@(a::l2). +#S #a #l elim l [normalize #abs @False_ind /2/] +#b #tl #Hind #H cases (orb_true_l … H) + [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) // + |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl + @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl // + ] +qed. + +lemma sublist_length: ∀S,l1,l2. + uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|. +#S #l1 elim l1 // +#a #tl #Hind #l2 #unique #sub +cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub normalize >(\b (refl … a)) //] +* #l3 * #l4 #eql2 >eql2 >length_append normalize +applyS le_S_S eql2 in sub; #sub #x #membx +cases (memb_append … (sub x (orb_true_r2 … membx))) + [#membxl3 @memb_append_l1 // + |#membxal4 cases (orb_true_l … membxal4) + [#eqxa @False_ind lapply (andb_true_l … unique) + <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 // + ] + ] +qed. + +lemma sublist_unique_append_l1: + ∀S,l1,l2. sublist S l1 (unique_append S l1 l2). +#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/] +#x #tl #Hind #l2 #a +normalize cases (true_or_false … (a==x)) #eqax >eqax +[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2))) + [#H >H normalize // | #H >H normalize >(\b (refl … a)) //] +|cases (memb S x (unique_append S tl l2)) normalize + [/2/ |>eqax normalize /2/] +] +qed. + +lemma sublist_unique_append_l2: + ∀S,l1,l2. sublist S l2 (unique_append S l1 l2). +#S #l1 elim l1 [normalize //] #x #tl #Hind normalize +#l2 #a cases (memb S x (unique_append S tl l2)) normalize +[@Hind | cases (a==x) normalize // @Hind] +qed. + +lemma decidable_sublist:∀S,l1,l2. + (sublist S l1 l2) ∨ ¬(sublist S l1 l2). +#S #l1 #l2 elim l1 + [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/ + |#a #tl * #subtl + [cases (true_or_false (memb S a l2)) #memba + [%1 whd #x #membx cases (orb_true_l … membx) + [#eqax >(\P eqax) // |@subtl] + |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 normalize + >(\b (refl … a)) // + ] + |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 normalize cases (x==a) + normalize // + ] + ] +qed. let rec occur (S: DeqSet) (i: re S) on i ≝ match i with @@ -203,6 +302,8 @@ let rec occur (S: DeqSet) (i: re S) on i ≝ | 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. *) @@ -223,7 +324,7 @@ qed. (* We cannot escape form the pit state. *) -lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i. +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 // @@ -232,17 +333,17 @@ lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i. qed. lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i. -#S #w #i elim w // -qed. +#S #w #i elim w // #a #w1 #H normalize >move_pit @H +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). +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|)))) + |#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 //] diff --git a/matita/matita/lib/tutorial/chapter11.ma b/matita/matita/lib/tutorial/chapter11.ma index 2a5da62ac..2f9e8fd64 100644 --- a/matita/matita/lib/tutorial/chapter11.ma +++ b/matita/matita/lib/tutorial/chapter11.ma @@ -2,20 +2,20 @@ Regular Expressions Equivalence *) -include "tutorial/chapter9.ma". +include "tutorial/chapter10.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). + 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〉. + \sem{e1} ≐ \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)) @@ -31,7 +31,7 @@ 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|)). + 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〉) @@ -48,7 +48,7 @@ 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}. +→ \sem{e1} ≐ \sem{e2}. #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H qed. @@ -61,11 +61,11 @@ 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. + 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). + ∃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] @@ -74,16 +74,27 @@ 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). +(* We define an elimination principle for lists working on the tail, that we +be used in the sequel *) + +lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) → +(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l. +#S #P #Pnil #Pstep #l <(reverse_reverse … l) +generalize in match (reverse S l); #l elim l // +#a #tl #H >reverse_cons @Pstep // +qed. + (* 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}. + is_bisim S l (occ S e1 e2) → memb ?〈e1,e2〉 l = true → \sem{e1} ≐ \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 + |cut (memb S a (occ S e1 e2) = true) + [@Hsub @memb_append_l2 normalize >(\b (refl … a)) //] #occa @(memb_map … occa) ] qed. @@ -120,7 +131,7 @@ let rec bisim S l n (frontier,visited: list ?) on n ≝ match frontier with [ nil ⇒ 〈true,visited〉 | cons hd tl ⇒ - if beqb (\snd (\fst hd)) (\snd (\snd hd)) then + 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〉 @@ -143,7 +154,7 @@ lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?. match frontier with [ nil ⇒ 〈true,visited〉 | cons hd tl ⇒ - if beqb (\snd (\fst hd)) (\snd (\snd hd)) then + 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〉 @@ -162,7 +173,7 @@ lemma bisim_end: ∀Sig,l,m.∀visited: list ?. qed. lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?. -beqb (\snd (\fst p)) (\snd (\snd p)) = true → +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). @@ -170,7 +181,7 @@ beqb (\snd (\fst p)) (\snd (\snd p)) = true → qed. lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?. -beqb (\snd (\fst p)) (\snd (\snd p)) = false → +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. @@ -206,7 +217,7 @@ 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. + memb ? e (pre_enum S (|fst ?? e|)) = true. #S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉)) // cases b normalize // qed. @@ -215,15 +226,16 @@ 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. + memb ? 〈e1,e2〉 ( space_enum S (|fst ?? e1|) (|fst ?? e2|)) = true. +#S #e1 #e2 @(memb_compose ?? (DeqProd (DeqProd ??) (DeqProd ??)) (λi,b.〈i,b〉)) +// qed. -definition all_reachable ≝ λS.λe1,e2: pre S.λl: list ?. +definition all_reachable ≝ λS.λe1,e2:pre S. +λl: list (DeqProd (DeqProd ??) (DeqProd ??)). uniqueb ? l = true ∧ ∀p. memb ? p l = true → - ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p). - + ∃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. @@ -232,25 +244,48 @@ 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} → +(* we first prove a few auxiliary results *) +lemma memb_filter_memb: ∀S,f,a,l. + memb S a (filter S f l) = true → memb S a l = true. +#S #f #a #l elim l [normalize //] #b #tl #Hind normalize (cases (f b)) normalize +cases (a==b) normalize // @Hind +qed. + +lemma filter_true: ∀S,f,a,l. + memb S a (filter S f l) = true → f a = true. +#S #f #a #l elim l [normalize #H @False_ind /2/] #b #tl #Hind +cases (true_or_false (f b)) #H normalize >H normalize [2:@Hind] +cases (true_or_false (a==b)) #eqab [#_ >(\P eqab) // | >eqab normalize @Hind] +qed. + +lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true → +memb S x (filter ? f l) = true. +#S #f #x #l #fx elim l normalize // +#b #tl #Hind cases (true_or_false (x==b)) #eqxb + [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize // + |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind] + ] +qed. + +lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1} ≐ \sem{e2} → ∀l,n.∀frontier,visited:list ((pre S)×(pre S)). - |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→ + |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. + 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|)) + cut ((|fst ?? e11| = |fst ?? e1|) ∧ (|fst ?? e21| = |fst ?? e2|)) [|* #H1 #H2

same_kernel_moves // + cases (H … membp) #w * normalize #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)) + 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) + cut (beqb (snd ?? (fst ?? p)) (snd ?? (snd ?? p)) = true) [cases rp #w * #fstp #sndp (bisim_step_true … ptest) @HI -HI @@ -261,12 +296,13 @@ lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → |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) + [@injective_notb @(filter_true … H) |cut ((q==p) = false) [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //] cases (andb_true … u_frontier) #notp #_ @(\bf ?) @@ -281,7 +317,7 @@ 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). + (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. @@ -299,7 +335,7 @@ lemma bisim_complete: -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)))) + |#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 *) @@ -324,8 +360,8 @@ lemma bisim_complete: 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 //|//] + |(* 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)) @@ -347,15 +383,15 @@ 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 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}. + fst ?? (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \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)〉) + cut (equiv ? re1 re2 = 〈true,snd ?? (equiv ? re1 re2)〉) [(proj2 … (eqb_true S …) (refl S a)) // +qed. + +lemma memb_cons: ∀S,a,b,l. + memb S a l = true → memb S a (b::l) = true. +#S #a #b #l normalize cases (a==b) normalize // +qed. + +lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x. +#S #a #x normalize cases (true_or_false … (a==x)) #H + [#_ >(\P H) // |>H normalize #abs @False_ind /2/] +qed. + let rec uniqueb (S:DeqSet) l on l : bool ≝ match l with [ nil ⇒ true @@ -405,7 +419,7 @@ lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,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)) // + [#eqb @(ex_intro … a) <(\P eqb) % // |#memb cases (Hind … memb) #a * #mema #eqb @(ex_intro … a) /3/ ] diff --git a/matita/matita/lib/tutorial/chapter8.ma b/matita/matita/lib/tutorial/chapter8.ma index ca6b973c9..b9bc64a9c 100644 --- a/matita/matita/lib/tutorial/chapter8.ma +++ b/matita/matita/lib/tutorial/chapter8.ma @@ -297,14 +297,14 @@ lemma true_to_epsilon : ∀S.∀e:pre S. snd … e = true → ϵ ∈ e. #S * #i #b #btrue normalize in btrue; >btrue %2 // qed. -lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}. +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 minus_eps_pre: ∀S.∀e:pre S. \sem{fst ?? e} ≐ \sem{e}-{[ ]}. +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)] -- 2.39.2