From: Andrea Asperti Date: Mon, 5 Dec 2011 07:18:17 +0000 (+0000) Subject: Decidability of equality (draft) X-Git-Tag: make_still_working~2055 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5d5925101dd773efb2f90136adc5d714a530cb9;p=helm.git Decidability of equality (draft) --- diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma new file mode 100644 index 000000000..b5449e4df --- /dev/null +++ b/matita/matita/lib/re/moves.ma @@ -0,0 +1,676 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "re/re.ma". + +let rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ + match E with + [ pz ⇒ 〈 ∅, 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:Alpha.∀x:S.∀i1,i2:pitem S. + move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2). +// qed. + +lemma move_cat: ∀S:Alpha.∀x:S.∀i1,i2:pitem S. + move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2). +// qed. + +lemma move_star: ∀S:Alpha.∀x:S.∀i:pitem S. + move S x i^* = (move ? x i)^⊛. +// qed. + +lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a. +// qed. + +lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b. +// qed. + +definition pmove ≝ λS:Alpha.λx:S.λe:pre S. move ? x (\fst e). + +lemma pmove_def : ∀S:Alpha.∀x:S.∀i:pitem S.∀b. + pmove ? x 〈i,b〉 = move ? x i. +// qed. + +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. + +axiom same_kernel: ∀S:Alpha.∀a:S.∀i:pitem S. + |\fst (move ? a i)| = |i|. +(* #S #a #i elim i // + [#i1 #i2 >move_cat + cases (move S a i1) #i11 #b1 >fst_eq #IH1 + cases (move S a i2) #i21 #b2 >fst_eq #IH2 + normalize *) + +axiom iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C. +axiom iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B. +axiom iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C. + +axiom epsilon_in_star: ∀S.∀A:word S → Prop. A^* [ ]. + +theorem move_ok: + ∀S:Alpha.∀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 + [>(proj1 … (eqb_true …) H) % + [* // #bot @False_ind //| #H1 destruct /2/] + |% [#bot @False_ind // + | #H1 destruct @(absurd ((a==a)=true)) + [>(proj2 … (eqb_true …) (refl …)) // | /2/] + ] + ] + |#i1 #i2 #HI1 #HI2 #w >(sem_cat S i1 i2) >move_cat + @iff_trans[|@sem_odot] >same_kernel >sem_cat_w + @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r % + [* #w1 * #w2 * * #eqw #w1in #w2in @(ex_intro … (a::w1)) + @(ex_intro … w2) % // % normalize // cases (HI1 w1) /2/ + |* #w1 * #w2 * cases w1 + [* #_ #H @False_ind /2/ + |#x #w3 * #eqaw normalize in eqaw; destruct #w3in #w2in + @(ex_intro … w3) @(ex_intro … w2) % // % // cases (HI1 w3) /2/ + ] + ] + |#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 % + [* #w1 * #w2 * * #eqw #w1in #w2in + @(ex_intro … (a::w1)) @(ex_intro … w2) % // % normalize // + cases (HI1 w1 ) /2/ + |* #w1 * #w2 * cases w1 + [* #_ #H @False_ind /2/ + |#x #w3 * #eqaw normalize in eqaw; destruct #w3in #w2in + @(ex_intro … w3) @(ex_intro … w2) % // % // cases (HI1 w3) /2/ + ] + ] + ] +qed. + +notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. +let rec moves (S : Alpha) w e on w : pre S ≝ + match w with + [ nil ⇒ e + | cons x w' ⇒ w' ↦* (move S x (\fst e))]. + +lemma moves_empty: ∀S:Alpha.∀e:pre S. + moves ? [ ] e = e. +// qed. + +lemma moves_cons: ∀S:Alpha.∀a:S.∀w.∀e:pre S. + moves ? (a::w) e = moves ? w (move S a (\fst e)). +// qed. + +lemma not_epsilon_sem: ∀S:Alpha.∀a:S.∀w: word S. ∀e:pre S. + iff ((a::w) ∈ e) ((a::w) ∈ \fst e). +#S #a #w * #i #b >fst_eq cases b normalize + [% /2/ * // #H destruct |% normalize /2/] +qed. + +lemma same_kernel_moves: ∀S:Alpha.∀w.∀e:pre S. + |\fst (moves ? w e)| = |\fst e|. +#S #w elim w // +qed. + +axiom iff_not: ∀A,B. (iff A B) →(iff (¬A) (¬B)). + +axiom iff_sym: ∀A,B. (iff A B) →(iff B A). + +theorem decidable_sem: ∀S:Alpha.∀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. + +lemma not_true_to_false: ∀b.b≠true → b =false. +#b * cases b // #H @False_ind /2/ +qed. + +theorem equiv_sem: ∀S:Alpha.∀e1,e2:pre S. + iff (\sem{e1} =1 \sem{e2}) (∀w.\snd (moves ? w e1) = \snd (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] (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 (b==a) normalize // +qed. + +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 [/2/] #b #tl #Hind +#l2 cases (b==a) normalize /2/ +qed. + +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 + [normalize #le #abs @False_ind /2/ + |#b #tl #Hind #l2 cases (b==a) normalize /2/ + ] +qed. + +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 (b==a) normalize /2/ +qed. + +let rec uniqueb (S:Alpha) l on l : bool ≝ + match l with + [ nil ⇒ true + | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl + ]. + +definition sons ≝ λp:space Bin. + [〈move Bin true (\fst (\fst p)), move Bin true (\fst (\snd p))〉; + 〈move Bin false (\fst (\fst p)), move Bin false (\fst (\snd p))〉 + ]. + +axiom memb_sons: ∀p,q. memb (space Bin) p (sons q) = true → + ∃a.(move ? a (\fst (\fst q)) = \fst p ∧ + move ? a (\fst (\snd q)) = \snd p). + +(* +let rec test_sons (l:list (space Bin)) ≝ + match l with + [ nil ⇒ true + | cons hd tl ⇒ + beqb (\snd (\fst hd)) (\snd (\snd hd)) ∧ test_sons tl + ]. *) + +let rec unique_append (S:Alpha) (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 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. + +let rec bisim (n:nat) (frontier,visited: list (space Bin)) ≝ + 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 m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited))) + (sons hd)) tl) (hd::visited) + else 〈false,visited〉 + ] + ]. + +lemma unfold_bisim: ∀n.∀frontier,visited: list (space Bin). + bisim 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 m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited))) (sons hd)) tl) (hd::visited) + else 〈false,visited〉 + ] + ]. +#n cases n // qed. + +lemma bisim_never: ∀frontier,visited: list (space Bin). + bisim O frontier visited = 〈false,visited〉. +#frontier #visited >unfold_bisim // +qed. + +lemma bisim_end: ∀m.∀visited: list (space Bin). + bisim (S m) [] visited = 〈true,visited〉. +#n #visisted >unfold_bisim // +qed. + +lemma bisim_step_true: ∀m.∀p.∀frontier,visited: list (space Bin). +beqb (\snd (\fst p)) (\snd (\snd p)) = true → + bisim (S m) (p::frontier) visited = + bisim m (unique_append ? (filter ? (λx.notb(memb (space Bin) x (p::visited))) (sons p)) frontier) (p::visited). +#m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // +qed. + +lemma bisim_step_false: ∀m.∀p.∀frontier,visited: list (space Bin). +beqb (\snd (\fst p)) (\snd (\snd p)) = false → + bisim (S m) (p::frontier) visited = 〈false,visited〉. +#m #p #frontier #visited #test >unfold_bisim normalize nodelta >test // +qed. + +definition visited_inv ≝ λe1,e2:pre Bin.λvisited: list (space Bin). +uniqueb ? visited = true ∧ + ∀p. memb ? p visited = true → + (∃w.(moves Bin w e1 = \fst p) ∧ (moves Bin w e2 = \snd p)) ∧ + (beqb (\snd (\fst p)) (\snd (\snd p)) = true). + +definition frontier_inv ≝ λfrontier,visited: list (space Bin). +uniqueb ? frontier = true ∧ +∀p. memb ? p frontier = true → + memb ? p visited = false ∧ + ∃p1.((memb ? p1 visited = true) ∧ + (∃a. move ? a (\fst (\fst p1)) = \fst p ∧ + move ? a (\fst (\snd p1)) = \snd p)). + +definition orb_true_r1: ∀b1,b2:bool. + b1 = true → (b1 ∨ b2) = true. +#b1 #b2 #H >H // qed. + +definition orb_true_r2: ∀b1,b2:bool. + b2 = true → (b1 ∨ b2) = true. +#b1 #b2 #H >H cases b1 // qed. + +definition orb_true_l: ∀b1,b2:bool. + (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true). +* normalize /2/ qed. + +definition andb_true_l1: ∀b1,b2:bool. + (b1 ∧ b2) = true → (b1 = true). +#b1 #b2 cases b1 normalize //. +qed. + +definition andb_true_l2: ∀b1,b2:bool. + (b1 ∧ b2) = true → (b2 = true). +#b1 #b2 cases b1 cases b2 normalize //. +qed. + +definition andb_true_l: ∀b1,b2:bool. + (b1 ∧ b2) = true → (b1 = true) ∧ (b2 = true). +#b1 #b2 cases b1 normalize #H [>H /2/ |@False_ind /2/]. +qed. + +definition andb_true_r: ∀b1,b2:bool. + (b1 = true) ∧ (b2 = true) → (b1 ∧ b2) = true. +#b1 #b2 cases b1 normalize * // +qed. + +lemma notb_eq_true_l: ∀b. notb b = true → b = false. +#b cases b normalize // +qed. + +lemma notb_eq_true_r: ∀b. b = false → notb b = true. +#b cases b normalize // +qed. + +lemma notb_eq_false_l:∀b. notb b = false → b = true. +#b cases b normalize // +qed. + +lemma notb_eq_false_r:∀b. b = true → notb b = false. +#b cases b normalize // +qed. + + +axiom 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 normalize cases (f b) normalize *) + +axiom memb_filter_memb: ∀S,f,a,l. + memb S a (filter S f l) = true → memb S a l = true. + +axiom unique_append_elim: ∀S:Alpha.∀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. + +axiom not_memb_to_not_eq: ∀S,a,b,l. + memb S a l = false → memb S b l = true → a==b = false. + +include "arithmetics/exp.ma". + +let rec pos S (i:re S) on i ≝ + match i with + [ z ⇒ 0 + | e ⇒ 0 + | s y ⇒ 1 + | o i1 i2 ⇒ pos S i1 + pos S i2 + | c i1 i2 ⇒ pos S i1 + pos S i2 + | k i ⇒ pos S i + ]. + +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) + >(proj1 … (eqb_true …) eqba) // + |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl + @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl // + ] +qed. + +lemma length_append: ∀A.∀l1,l2:list A. + |l1@l2| = |l1|+|l2|. +#A #l1 elim l1 // normalize /2/ +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 //] +* #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) + [#eqax @False_ind cases (andb_true_l … unique) + >(proj1 … (eqb_true …) eqax) >membx normalize /2/ + |#membxl4 @memb_append_l2 // + ] + ] +qed. + +axiom memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → +memb S x l = true ∧ (f x = true). + +axiom memb_filter_l: ∀S,f,l,x. memb S x l = true → (f x = true) → +memb S x (filter ? f l) = true. + +axiom sublist_unique_append_l1: + ∀S,l1,l2. sublist S l1 (unique_append S l1 l2). + +axiom sublist_unique_append_l2: + ∀S,l1,l2. sublist S l2 (unique_append S l1 l2). + +definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2. + foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1. + +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) + ]. + +axiom 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. +(* #S #op #a1 #a2 #l1 elim l1 [normalize //] +#x #tl #Hind #l2 elim l2 [#_ normalize #abs @False_ind /2/] +#y #tl2 #Hind2 #membx #memby normalize *) + +axiom pitem_enum_complete: ∀i: pitem Bin. + memb BinItem i (pitem_enum ? (forget ? i)) = true. +(* +#i elim i + [// + |// + |* // + |* // + |#i1 #i2 #Hind1 #Hind2 @memb_compose // + |#i1 #i2 #Hind1 #Hind2 @memb_compose // + | +*) + +definition pre_enum ≝ λS.λi:re S. + compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false]. + +definition space_enum ≝ λS.λi1,i2:re S. + compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i1). + +axiom space_enum_complete : ∀S.∀e1,e2: pre S. + memb (space S) 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true. + +lemma bisim_ok1: ∀e1,e2:pre Bin.\sem{e1}=1\sem{e2} → + ∀n.∀frontier,visited:list (space Bin). + |space_enum Bin (|\fst e1|) (|\fst e2|)| < n + |visited|→ + visited_inv e1 e2 visited → frontier_inv frontier visited → + \fst (bisim n frontier visited) = true. +#e1 #e2 #same #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

fst_eq >snd_eq #we1 #we2 #_ + bisim_end //] + #p #front_tl #visited #Hn * #u_visited #vinv * #u_frontier #finv + cases (finv p (memb_hd …)) #Hp * #p2 * #visited_p2 + * #a * #movea1 #movea2 + cut (∃w.(moves Bin w e1 = \fst p) ∧ (moves Bin w e2 = \snd p)) + [cases (vinv … visited_p2) -vinv * #w1 * #mw1 #mw2 #_ + @(ex_intro … (w1@[a])) /2/] + -movea2 -movea1 -a -visited_p2 -p2 #reachp + cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true) + [cases reachp #w * #move_e1 #move_e2 (bisim_step_true … ptest) @HI -HI + [Hpq @nvq] + cases (andb_true_l … u_frontier) #notp #_ + @(not_memb_to_not_eq … H) @notb_eq_true_l @notp + |cases (proj2 … (finv q ?)) + [#p1 * #Hp1 #reach @(ex_intro … p1) % // @memb_cons // + |@memb_cons // + ] + ] + ] + ] + ] + ] +qed. + +definition all_true ≝ λl.∀p. memb (space Bin) p l = true → + (beqb (\snd (\fst p)) (\snd (\snd p)) = true). + +definition sub_sons ≝ λl1,l2.∀x,a. +memb (space Bin) x l1 = true → + memb (space Bin) 〈move ? a (\fst (\fst x)), move ? a (\fst (\snd x))〉 l2 = true. + +lemma reachable_bisim: + ∀n.∀frontier,visited,visited_res:list (space Bin). + all_true visited → + sub_sons visited (frontier@visited) → + bisim n frontier visited = 〈true,visited_res〉 → + (sub_sons visited_res visited_res ∧ + sublist ? visited visited_res ∧ + all_true visited_res). +#n elim n + [#fron #vis #vis_res #_ #_ >bisim_never #H destruct + |#m #Hind * + [-Hind #vis #vis_res #allv #H normalize in ⊢ (%→?); + #H1 destruct % // % // #p /2/ + |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd)))) + [|#H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct] + #H #tl #visited #visited_res #allv >(bisim_step_true … H) + cut (all_true (hd::visited)) + [#p #H cases (orb_true_l … H) + [#eqp <(proj1 … (eqb_true …) eqp) // |@allv]] + #allh #subH #bisim cases (Hind … allh … bisim) -Hind + [* #H1 #H2 #H3 % // % // #p #H4 @H2 @memb_cons //] + #x #a #membx + cases (orb_true_l … membx) + [#eqhdx >(proj1 … (eqb_true …) eqhdx) + letin xa ≝ 〈move Bin a (\fst (\fst x)), move Bin a (\fst (\snd x))〉 + cases (true_or_false … (memb (space Bin) xa (x::visited))) + [#membxa @memb_append_l2 // + |#membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l + [whd in ⊢ (??(??%%)?); cases a [@memb_hd |@memb_cons @memb_hd] + |>membxa // + ] + ] + |#H1 letin xa ≝ 〈move Bin a (\fst (\fst x)), move Bin a (\fst (\snd x))〉 + cases (memb_append … (subH x a H1)) + [#H2 (cases (orb_true_l … H2)) + [#H3 @memb_append_l2 >(proj1 … (eqb_true …) H3) @memb_hd + |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3 + ] + |#H2 @memb_append_l2 @memb_cons @H2 + ] + ] + ] + ] +qed. + +axiom bisim_char: ∀e1,e2:pre Bin. +(∀w.(beqb (\snd (moves ? w e1)) (\snd (moves ? w e2))) = true) → +\sem{e1}=1\sem{e2}. + +lemma bisim_ok2: ∀e1,e2:pre Bin. + (beqb (\snd e1) (\snd e2) = true) → + ∀n.∀frontier:list (space Bin). + sub_sons [〈e1,e2〉] (frontier@[〈e1,e2〉]) → + \fst (bisim n frontier [〈e1,e2〉]) = true → \sem{e1}=1\sem{e2}. +#e1 #e2 #Hnil #n #frontier #init #bisim_true +letin visited_res ≝ (\snd (bisim n frontier [〈e1,e2〉])) +cut (bisim n frontier [〈e1,e2〉] = 〈true,visited_res〉) + [fst_eq >snd_eq >moves_cons >moves_cons + @(Hind 〈?,?〉) @(H1 〈?,?〉) //] #all_reach +@bisim_char #w @(H3 〈?,?〉) @(all_reach w 〈?,?〉) @H2 // +qed. + +definition tt ≝ ps Bin true. +definition ff ≝ ps Bin false. +definition eps ≝ pe Bin. +definition exp1 ≝ (ff + tt · ff). +definition exp2 ≝ ff · (eps + tt). + +definition exp3 ≝ move Bin true (\fst (•exp1)). +definition exp4 ≝ move Bin true (\fst (•exp2)). +definition exp5 ≝ move Bin false (\fst (•exp1)). +definition exp6 ≝ move Bin false (\fst (•exp2)). + +example comp1 : bequiv 15 (•exp1) (•exp2) [ ] = false . +normalize // +qed. + + diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma index dadd3db3e..388c27e70 100644 --- a/matita/matita/lib/re/re.ma +++ b/matita/matita/lib/re/re.ma @@ -1,5 +1,3 @@ - - (**************************************************************************) (* ___ *) (* ||M|| *) @@ -97,6 +95,9 @@ 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 rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*. +// qed. + notation "a || b" left associative with precedence 30 for @{'orb $a $b}. interpretation "orb" 'orb a b = (orb a b). @@ -122,9 +123,11 @@ interpretation "pcat" 'pc 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 "ppatom" 'pp a = (pp ? a). + (* to get rid of \middot ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?. *) + interpretation "patom" 'ps a = (ps ? a). interpretation "pepsilon" 'epsilon = (pe ?). interpretation "pempty" 'empty = (pz ?). @@ -142,7 +145,6 @@ let rec forget (S: Alpha) (l : pitem S) on l: re S ≝ (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*) interpretation "forget" 'norm a = (forget ? a). - let rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ match r with [ pz ⇒ {} @@ -180,14 +182,26 @@ 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. + lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ]. #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed. @@ -206,7 +220,7 @@ lemma epsilon_to_true : ∀S.∀e:pre S. [ ] ∈ e → \snd e = true. qed. lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → [ ] ∈ e. -#S * #i #b #btrue normalize in btrue >btrue %2 // +#S * #i #b #btrue normalize in btrue; >btrue %2 // qed. definition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉. @@ -219,8 +233,8 @@ lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2 definition pre_concat_r ≝ λS:Alpha.λi:pitem S.λe:pre S. match e with [ pair i1 b ⇒ 〈i · i1, b〉]. -notation "i ▸ e" left associative with precedence 60 for @{'trir $i $e}. -interpretation "pre_concat_r" 'trir i e = (pre_concat_r ? i e). +notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}. +interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e). definition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w. notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}. @@ -241,7 +255,7 @@ lemma union_assoc: ∀S.∀A,B,C:word S → Prop. qed. lemma sem_pre_concat_r : ∀S,i.∀e:pre S. - \sem{i ▸ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. + \sem{i ◂ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}. #S #i * #i1 #b1 cases b1 /2/ >sem_pre_true >sem_cat >sem_pre_true /2/ qed. @@ -249,33 +263,49 @@ qed. definition lc ≝ λS:Alpha.λbcast:∀S:Alpha.pitem S → pre S.λe1:pre S.λi2:pitem S. match e1 with [ pair i1 b1 ⇒ match b1 with - [ true ⇒ (i1 ▸ (bcast ? i2)) + [ true ⇒ (i1 ◂ (bcast ? i2)) | false ⇒ 〈i1 · i2,false〉 ] ]. -definition lift ≝ λf:∀S.pitem S →pre S.λS.λe:pre S. +definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. match e with - [ pair i b ⇒ 〈\fst (f S i), \snd (f S i) || b〉]. + [ pair i b ⇒ 〈\fst (f i), \snd (f i) || b〉]. -notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. +notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}. interpretation "lc" 'lc op a b = (lc ? op a b). -notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}. definition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λe:pre S. match e with [ pair i1 b1 ⇒ match b1 with [true ⇒ 〈(\fst (bcast ? i1))^*, true〉 - |false ⇒ 〈i1^*,true〉 + |false ⇒ 〈i1^*,false〉 ] - ]. + ]. + +(* +lemma oplus_tt : ∀S: Alpha.∀i1,i2:pitem S. + 〈i1,true〉 ⊕ 〈i2,true〉 = 〈i1 + i2,true〉. +// qed. + +lemma oplus_tf : ∀S: Alpha.∀i1,i2:pitem S. + 〈i1,true〉 ⊕ 〈i2,false〉 = 〈i1 + i2,true〉. +// qed. + +lemma oplus_ft : ∀S: Alpha.∀i1,i2:pitem S. + 〈i1,false〉 ⊕ 〈i2,true〉 = 〈i1 + i2,true〉. +// qed. + +lemma oplus_ff : ∀S: Alpha.∀i1,i2:pitem S. + 〈i1,false〉 ⊕ 〈i2,false〉 = 〈i1 + i2,false〉. +// qed. *) (* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.*) interpretation "lk" 'lk op a = (lk ? op a). -notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. +notation "a^⊛" non associative with precedence 90 for @{'lk eclose $a}. -notation > "•" non associative with precedence 60 for @{eclose ?}. +notation "•" non associative with precedence 60 for @{eclose ?}. let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝ match i with @@ -284,9 +314,8 @@ let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝ | ps x ⇒ 〈 `.x, false〉 | pp x ⇒ 〈 `.x, false 〉 | po i1 i2 ⇒ •i1 ⊕ •i2 - | pc i1 i2 ⇒ •i1 ⊙ i2 - | pk i ⇒ 〈(\fst(•i))^*,true〉]. - + | 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). @@ -296,14 +325,14 @@ lemma eclose_plus: ∀S:Alpha.∀i1,i2:pitem S. // qed. lemma eclose_dot: ∀S:Alpha.∀i1,i2:pitem S. - •(i1 · i2) = •i1 ⊙ i2. + •(i1 · i2) = •i1 ▸ i2. // qed. lemma eclose_star: ∀S:Alpha.∀i:pitem S. •i^* = 〈(\fst(•i))^*,true〉. // qed. -definition reclose ≝ lift eclose. +definition reclose ≝ λS. lift S (eclose S). interpretation "reclose" 'eclose x = (reclose ? x). lemma epsilon_or : ∀S:Alpha.∀b1,b2. epsilon S (b1 || b2) =1 ϵ b1 ∪ ϵ b2. @@ -318,27 +347,27 @@ nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a. #S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.*) (* theorem 16: 2 *) -(* -lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S. - \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. -#S * #i1 #b1 * #i2 #b2 #w % -[normalize * [* /3/ | cases b1 cases b2 normalize /3/ ] -|normalize * * /3/ cases b1 cases b2 normalize /3/ *] -qed. *) +lemma sem_oplus: ∀S:Alpha.∀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. lemma odot_true : ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ⊙ i2 = i1 ▸ (•i2). + 〈i1,true〉 ▸ i2 = i1 ◂ (•i2). // qed. lemma odot_true_bis : ∀S.∀i1,i2:pitem S. - 〈i1,true〉 ⊙ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. + 〈i1,true〉 ▸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉. #S #i1 #i2 normalize cases (•i2) // qed. lemma odot_false: ∀S.∀i1,i2:pitem S. - 〈i1,false〉 ⊙ i2 = 〈i1 · i2, false〉. + 〈i1,false〉 ▸ i2 = 〈i1 · i2, false〉. // qed. lemma LcatE : ∀S.∀e1,e2:pitem S. @@ -365,11 +394,10 @@ lemma erase_plus : ∀S.∀i1,i2:pitem S. lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. // qed. -(* definition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w. interpretation "substract" 'minus a b = (substract ? a b). -nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}. +(* nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}. #S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed. nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a. @@ -402,6 +430,15 @@ axiom union_ext_r: ∀S.∀A,B,C:word S →Prop. axiom union_comm : ∀S.∀A,B:word S →Prop. A ∪ B =1 B ∪ A. + +axiom union_idemp: ∀S.∀A:word S →Prop. + A ∪ A =1 A. + +axiom cat_ext_l: ∀S.∀A,B,C:word S →Prop. + A =1 C → A · B =1 C · B. + +axiom cat_ext_r: ∀S.∀A,B,C:word S →Prop. + B =1 C → A · B =1 A · C. lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop. (A ∪ B) · C =1 A · C ∪ B · C. @@ -409,6 +446,26 @@ lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop. [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/] qed. +axiom fix_star: ∀S.∀A:word S → Prop. + A^* =1 A · A^* ∪ { [ ] }. + +axiom star_epsilon: ∀S:Alpha.∀A:word S → Prop. + A^* ∪ { [ ] } =1 A^*. + +lemma sem_eclose_star: ∀S:Alpha.∀i:pitem S. + \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ { [ ] }. +/2/ qed. + +(* +lemma sem_eclose_star: ∀S:Alpha.∀i:pitem S. + \sem{〈i^*,true〉} =1 \sem{〈i,true〉}·\sem{|i|}^* ∪ { [ ] }. +/2/ qed. + +#S #i #b cases b + [>sem_pre_true >sem_star + |/2/ + ] *) + (* this kind of results are pretty bad for automation; better not index them *) lemma epsilon_cat_r: ∀S.∀A:word S →Prop. @@ -451,99 +508,90 @@ napply Hw2; nqed.*) (* theorem 16: 1 → 3 *) lemma odot_dot_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}. + \sem{e1 ▸ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}. #S * #i1 #b1 #i2 cases b1 [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/ |#H >odot_true >sem_pre_true @(ext_eq_trans … (sem_pre_concat_r …)) - >erase_bull - @ext_eq_trans - [|@(union_ext_r … H) - |@ext_eq_trans - [|@union_ext_r [|@union_comm ] - |@ext_eq_trans (* /3 by eq_ext_sym, union_ext_l/; *) - [|@eq_ext_sym @union_assoc - |/3/ - (* - by eq_ext_sym, union_ext_l; @union_ext_l /3 - /3/ ext_eq_trans /2/ - /3 width=5 by eq_ext_sym, union_ext_r/ *) - ] - ] - ] - ] + >erase_bull @ext_eq_trans [|@(union_ext_r … H)] + @ext_eq_trans [|@union_ext_r [|@union_comm ]] + @ext_eq_trans [|@eq_ext_sym @union_assoc ] /3/ + ] qed. -(* nlemma sub_dot_star : - ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*. -#S X b; napply extP; #w; @; -##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //] - *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj; - @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //; - @; //; napply (subW … sube); -##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //] - #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *; - ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2; - @; ncases b in H1; #H1; - ##[##2: nrewrite > (sub0…); @w'; @(w1@w2); - nrewrite > (associative_append ? w' w1 w2); - nrewrite > defwl'; @; ##[@;//] @(wl'); @; //; - ##| ncases w' in Pw'; - ##[ #ne; @w1; @w2; nrewrite > defwl'; @; //; @; //; - ##| #x xs Px; @(x::xs); @(w1@w2); - nrewrite > (defwl'); @; ##[@; //; @; //; @; nnormalize; #; ndestruct] - @wl'; @; //; ##] ##] - ##| #wlnil; nchange in match (flatten ? (w'::wl')) with (w' @ flatten ? wl'); - nrewrite < (wlnil); nrewrite > (append_nil…); ncases b; - ##[ ncases w' in Pw'; /2/; #x xs Pxs; @; @(x::xs); @([]); - nrewrite > (append_nil…); @; ##[ @; //;@; //; nnormalize; @; #; ndestruct] - @[]; @; //; - ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //] - @; //; @; //; @; *;##]##]##] -nqed. *) +axiom star_fix : + ∀S.∀X:word S → Prop.(X - {[ ]}) · X^* ∪ {[ ]} =1 X^*. + +axiom sem_fst: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}. + +axiom sem_fst_aux: ∀S.∀e:pre S.∀i:pitem S.∀A. + \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}). (* theorem 16: 1 *) -alias symbol "pc" (instance 13) = "cat lang". -alias symbol "in_pl" (instance 23) = "in_pl". -alias symbol "in_pl" (instance 5) = "in_pl". -alias symbol "eclose" (instance 21) = "eclose". -ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|. -#S e; nelim e; //; - ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror; - ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *; - ##| #e1 e2 IH1 IH2; - nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉); - nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2); - nrewrite > (IH1 …); nrewrite > (cup_dotD …); - nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …); - nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …); - nrewrite < (erase_dot …); nrewrite < (cupA …); //; - ##| #e1 e2 IH1 IH2; - nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …); - nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …); - nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…); - nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …); - nrewrite < (erase_plus …); //. - ##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH; - nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉); - nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]}); - nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* ); - nrewrite > (erase_bull…e); - nrewrite > (erase_star …); - nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[##2: - nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH; - ##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH; - nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//; - ##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##] - nrewrite > (cup_dotD…); nrewrite > (cupA…); - nrewrite > (?: ((?·?)∪{[]} = 𝐋 |e^*|)); //; - nchange in match (𝐋 |e^*|) with ((𝐋 |e|)^* ); napply sub_dot_star;##] - nqed. +theorem sem_bull: ∀S:Alpha. ∀e:pitem S. \sem{•e} =1 \sem{e} ∪ \sem{|e|}. +#S #e elim e + [#w normalize % [/2/ | * //] + |/2/ + |#x normalize #w % [ /2/ | * [@False_ind | //]] + |#x normalize #w % [ /2/ | * // ] + |#i1 #i2 #IH1 #IH2 >eclose_dot + @ext_eq_trans [|@odot_dot_aux //] >sem_cat + @ext_eq_trans + [|@union_ext_l + [|@ext_eq_trans [|@(cat_ext_l … IH1)] @distr_cat_r]] + @ext_eq_trans [|@union_assoc] + @ext_eq_trans [||@eq_ext_sym @union_assoc] + @union_ext_r // + |#i1 #i2 #IH1 #IH2 >eclose_plus + @ext_eq_trans [|@sem_oplus] >sem_plus >erase_plus + @ext_eq_trans [|@(union_ext_r … IH2)] + @ext_eq_trans [|@eq_ext_sym @union_assoc] + @ext_eq_trans [||@union_assoc] @union_ext_l + @ext_eq_trans [||@eq_ext_sym @union_assoc] + @ext_eq_trans [||@union_ext_r [|@union_comm]] + @ext_eq_trans [||@union_assoc] /3/ + |#i #H >sem_pre_true >sem_star >erase_bull >sem_star + @ext_eq_trans [|@union_ext_l [|@cat_ext_l [|@sem_fst_aux //]]] + @ext_eq_trans [|@union_ext_l [|@distr_cat_r]] + @ext_eq_trans [|@union_assoc] @union_ext_r >erase_star @star_fix + ] +qed. + +definition lifted_cat ≝ λS:Alpha.λe:pre S. + lift S (lc S eclose e). -(* theorem 16: 3 *) -nlemma odot_dot: - ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2. -#S e1 e2; napply odot_dot_aux; napply (bull_cup S (\fst e2)); nqed. +notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}. +interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2). + +lemma sem_odot_true: ∀S:Alpha.∀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 @ext_eq_trans [||@eq_ext_sym @union_assoc] + @union_ext_r /2/ + |/2/ + ] +qed. + +lemma eq_odot_false: ∀S:Alpha.∀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. + +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 + @ext_eq_trans [|@sem_odot_true] + @ext_eq_trans [||@union_assoc] @union_ext_l @odot_dot_aux // + |>sem_pre_false >eq_odot_false @odot_dot_aux // + ] +qed. + +(* nlemma dot_star_epsilon : ∀S.∀e:re S.𝐋 e · 𝐋 e^* ∪ {[]} = 𝐋 e^*. #S e; napply extP; #w; nnormalize; @; ##[ *; ##[##2: #H; nrewrite < H; @[]; /3/] *; #w1; *; #w2; @@ -568,30 +616,23 @@ nlemma rcanc_sing : ∀S.∀A,C:word S → Prop.∀b:word S . #S A C b nbA defC; nrewrite < defC; napply extP; #w; @; ##[ #Aw; /3/| *; *; //; #H nH; ncases nH; #abs; nlapply (abs H); *] nqed. +*) (* theorem 16: 4 *) -nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 |\fst e|)^*. -#S p; ncases p; #e b; ncases b; -##[ nchange in match (〈e,true〉^⊛) with 〈?,?〉; - nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); - nchange in ⊢ (??%?) with (?∪?); - nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* ); - nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b' )); ##[##2: - nlapply (bull_cup ? e); #bc; - nchange in match (𝐋\p (•e)) in bc with (?∪?); - nchange in match b' in bc with b'; - ncases b' in bc; ##[##2: nrewrite > (cup0…); nrewrite > (sub0…); //] - nrewrite > (cup_sub…); ##[napply rcanc_sing] //;##] - nrewrite > (cup_dotD…); nrewrite > (cupA…);nrewrite > (erase_bull…); - nrewrite > (sub_dot_star…); - nchange in match (𝐋\p 〈?,?〉) with (?∪?); - nrewrite > (cup_dotD…); nrewrite > (epsilon_dot…); //; -##| nwhd in match (〈e,false〉^⊛); nchange in match (𝐋\p 〈?,?〉) with (?∪?); - nrewrite > (cup0…); - nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* ); - nrewrite < (cup0 ? (𝐋\p e)); //;##] -nqed. - +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 + @ext_eq_trans [|@union_ext_l [|@cat_ext_l [|@sem_fst_aux //]]] + @ext_eq_trans [|@union_ext_l [|@distr_cat_r]] + @ext_eq_trans [||@eq_ext_sym @distr_cat_r] + @ext_eq_trans [|@union_assoc] @union_ext_r + @ext_eq_trans [||@eq_ext_sym @epsilon_cat_l] @star_fix + |>sem_pre_false >sem_pre_false >sem_star /2/ + ] +qed. + +(* nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝ match e with [ z ⇒ pz ? @@ -643,238 +684,6 @@ ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ | nrewrite > defsnde; #H; nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //; -STOP - -notation > "\move term 90 x term 90 E" -non associative with precedence 60 for @{move ? $x $E}. -nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝ - match E with - [ pz ⇒ 〈 ∅, 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)^⊛ ]. -notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}. -notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}. -interpretation "move" 'move x E = (move ? x E). - -ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e). -interpretation "rmove" 'move x E = (rmove ? x E). - -nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → False. -#S w abs; ninversion abs; #; ndestruct; -nqed. - - -nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False. -#S w abs; ninversion abs; #; ndestruct; -nqed. - -nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False. -#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe; -nqed. - - -naxiom in_move_cat: - ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) → - (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2. -#S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2); -ncases e1 in H; ncases e2; -##[##1: *; ##[*; nnormalize; #; ndestruct] - #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] - nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; -##|##2: *; ##[*; nnormalize; #; ndestruct] - #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] - nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze; -##| #r; *; ##[ *; nnormalize; #; ndestruct] - #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct] - ##[##2: nnormalize; #; ndestruct; @2; @2; //.##] - nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz; -##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##] - #H; ninversion H; nnormalize; #; ndestruct; - ##[ncases (?:False); /2/ by XXz] /3/ by or_intror; -##| #r1 r2; *; ##[ *; #defw] - ... -nqed. - -ntheorem move_ok: - ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E. -#S E; ncases E; #r b; nelim r; -##[##1,2: #a w; @; - ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##] - #H; ninversion H; #; ndestruct; - ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##] - #H; ninversion H; #; ndestruct;##] -##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##] - *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct; -##|#a c w; @; nnormalize; - ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2; nrewrite > (eqb_t … ca); @; ##] - #H; ninversion H; #; ndestruct; - ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct] - #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##] -##|#r1 r2 H1 H2 a w; @; - ##[ #H; ncases (in_move_cat … H); - ##[ *; #w1; *; #w2; *; *; #defw w1m w2m; - ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good; - nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //. - ##| - ... -##| -##| -##] -nqed. - - -notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}. -nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝ - match w with - [ nil ⇒ E - | cons x w' ⇒ w' ↦* (x ↦ \snd E)]. - -ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E). - -ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝ - mk_equiv: - ∀E1,E2: bool × (pre S). - \fst E1 = \fst E2 → - (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) → - equiv S E1 E2. - -ndefinition NAT: decidable. - @ nat eqb; /2/. -nqed. - -include "hints_declaration.ma". - -alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". -unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat. - -ninductive unit: Type[0] ≝ I: unit. - -nlet corec foo_nop (b: bool): - equiv ? - 〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉 - 〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?. - @; //; #x; ncases x - [ nnormalize in ⊢ (??%%); napply (foo_nop false) - | #y; ncases y - [ nnormalize in ⊢ (??%%); napply (foo_nop false) - | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##] -nqed. - -(* -nlet corec foo (a: unit): - equiv NAT - (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))))) - (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))) -≝ ?. - @; - ##[ nnormalize; // - ##| #x; ncases x - [ nnormalize in ⊢ (??%%); - nnormalize in foo: (? → ??%%); - @; //; #y; ncases y - [ nnormalize in ⊢ (??%%); napply foo_nop - | #y; ncases y - [ nnormalize in ⊢ (??%%); - - ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##] - ##| #y; nnormalize in ⊢ (??%%); napply foo_nop - ##] -nqed. *) -ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0. -ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩. -ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*. - -nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true. - nnormalize in match test3; - nnormalize; -//; -nqed. - -(**********************************************************) - -ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝ - der_z: der S a (z S) (z S) - | der_e: der S a (e S) (z S) - | der_s1: der S a (s S a) (e ?) - | der_s2: ∀b. a ≠ b → der S a (s S b) (z S) - | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' → - der S a (c ? e1 e2) (o ? (c ? e1' e2) e2') - | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' → - der S a (c ? e1 e2) (c ? e1' e2) - | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' → - der S a (o ? e1 e2) (o ? e1' e2'). - -nlemma eq_rect_CProp0_r: - ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p. - #A; #a; #x; #p; ncases p; #P; #H; nassumption. -nqed. - -nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed. - -naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2). -(* #S; #r1; #r2; #w; nelim r1 - [ #K; ninversion K - | #H1; #H2; napply (in_c ? []); // - | (* tutti casi assurdi *) *) - -ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝ - in_l_empty1: ∀E.in_l S [] E → in_l' S [] E - | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e. - -ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝ - mk_eq_re: ∀E1,E2. - (in_l S [] E1 → in_l S [] E2) → - (in_l S [] E2 → in_l S [] E1) → - (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') → - eq_re S E1 E2. - -(* serve il lemma dopo? *) -ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2. - #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ % - [ #r; #K (* ok *) - | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4; - -(* IL VICEVERSA NON VALE *) -naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E. -(* #S; #w; #E; #H; nelim H - [ // - | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *) - ] -nqed. *) - -ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e. - #S; #a; #E; #E'; #w; #H; nelim H - [##1,2: #H1; ninversion H1 - [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/ - |##2,9: #X; #Y; #K; ncases (?:False); /2/ - |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ - |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ - |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ - |##6,13: #x; #y; #K; ncases (?:False); /2/ - |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/] -##| #H1; ninversion H1 - [ // - | #X; #Y; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ - | #x; #y; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] -##| #H1; #H2; #H3; ninversion H3 - [ #_; #K; ncases (?:False); /2/ - | #X; #Y; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/ - | #x; #y; #K; ncases (?:False); /2/ - | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ] -##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6; - -lemma \ No newline at end of file