X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fre%2Fmoves.ma;h=c260a6d403dd34c60cc0697a2cf64568a1654b36;hb=927bda3b4b7fe5f521ae73eb008a746e8606a0b4;hp=4967bf0596ddf7ec35fecebd29d8460761247e2e;hpb=5c71d6a1d1461007f941f73d2cc7975c7116fd0d;p=helm.git diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index 4967bf059..c260a6d40 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -64,38 +64,21 @@ theorem move_ok: |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/] - ] + [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/] + |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //] ] |#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/ - ] - ] + @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 % - [* #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/ - ] - ] + @iff_trans[|@sem_ostar] >same_kernel >sem_star_w + @iff_trans[||@iff_sym @deriv_middot //] + @cat_ext_l @HI1 ] qed. @@ -165,18 +148,6 @@ coinductive equiv (S:DeqSet) : pre S â pre S â Prop â equiv S e1 e2. *) -definition beqb â λb1,b2. - match b1 with - [ true â b2 - | false â notb b2 - ]. - -lemma beqb_ok: âb1,b2. iff (beqb b1 b2 = true) (b1 = b2). -#b1 #b2 cases b1 cases b2 normalize /2/ -qed. - -definition Bin â mk_DeqSet bool beqb beqb_ok. - let rec beqitem S (i1,i2: pitem S) on i1 â match i1 with [ pz â match i2 with [ pz â true | _ â false] @@ -192,27 +163,53 @@ let rec beqitem S (i1,i2: pitem S) on i1 â | pk i11 â match i2 with [ pk i21 â beqitem S i11 i21 | _ â false] ]. -axiom beqitem_ok: âS,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2). +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 DeqItem â λS. - mk_DeqSet (pitem S) (beqitem S) (beqitem_ok S). - -definition beqpre â λS:DeqSet.λe1,e2:pre S. - beqitem S (\fst e1) (\fst e2) ⧠beqb (\snd e1) (\snd e2). - -definition beqpairs â λS:DeqSet.λp1,p2:(pre S)Ã(pre S). - beqpre S (\fst p1) (\fst p2) ⧠beqpre S (\snd p1) (\snd p2). + mk_DeqSet (pitem S) (beqitem S) (beqitem_true S). -axiom beqpairs_ok: âS,p1,p2. iff (beqpairs S p1 p2 = true) (p1 = p2). - -definition space â λS.mk_DeqSet ((pre S)Ã(pre S)) (beqpairs S) (beqpairs_ok S). - -(* (sons S l p) computes all sons of p relative to characters in 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. -definition sons â λS:DeqSet.λl:list S.λp:space S. +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. memb (space S) p (sons S l q) = true â +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/] @@ -222,7 +219,7 @@ lemma memb_sons: âS,l,p,q. memb (space S) p (sons S l q) = true â ] qed. -let rec bisim S l n (frontier,visited: list (space S)) on n â +let rec bisim S l n (frontier,visited: list ?) on n â match n with [ O â â©false,visited⪠(* assert false *) | S m â @@ -236,7 +233,7 @@ let rec bisim S l n (frontier,visited: list (space S)) on n â ] ]. -lemma unfold_bisim: âS,l,n.âfrontier,visited: list (space S). +lemma unfold_bisim: âS,l,n.âfrontier,visited: list ?. bisim S l n frontier visited = match n with [ O â â©false,visited⪠(* assert false *) @@ -252,39 +249,39 @@ lemma unfold_bisim: âS,l,n.âfrontier,visited: list (space S). ]. #S #l #n cases n // qed. -lemma bisim_never: âS,l.âfrontier,visited: list (space S). +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 (space Sig). +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 (space Sig). +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 (space Sig) x (p::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 normalize nodelta >test // qed. -lemma bisim_step_false: âSig,l,m.âp.âfrontier,visited: list (space Sig). +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 normalize nodelta >test // qed. -definition visited_inv â λS.λe1,e2:pre S.λvisited: list (space S). +definition visited_inv â λS.λe1,e2:pre S.λvisited: list ?. uniqueb ? visited = true ⧠âp. memb ? p visited = true â (âw.(moves S w e1 = \fst p) ⧠(moves S w e2 = \snd p)) ⧠(beqb (\snd (\fst p)) (\snd (\snd p)) = true). -definition frontier_inv â λS.λfrontier,visited: list (space S). +definition frontier_inv â λS.λfrontier,visited. uniqueb ? frontier = true ⧠-âp. memb ? p frontier = true â +âp:(pre S)Ã(pre S). memb ? p frontier = true â memb ? p visited = false ⧠âp1.((memb ? p1 visited = true) ⧠(âa. move ? a (\fst (\fst p1)) = \fst p ⧠@@ -339,91 +336,98 @@ let rec pitem_enum S (i:re S) on i â | c i1 i2 â compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2) | k i â map ?? (pk S) (pitem_enum S i) ]. - -(* axiom pitem_enum_complete: âS:DeqSet.âi: pitem S. - memb ((pitem S)Ã(pitem S)) i (pitem_enum ? (forget ? i)) = true. *) -(* -#i elim i - [// - |// - |* // - |* // - |#i1 #i2 #Hind1 #Hind2 @memb_compose // - |#i1 #i2 #Hind1 #Hind2 @memb_compose // - | -*) + +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 i1). + compose ??? (λe1,e2.â©e1,e2âª) (pre_enum S i1) (pre_enum S i2). -axiom space_enum_complete : âS.âe1,e2: pre S. - memb (space S) â©e1,e2⪠(space_enum S (|\fst e1|) (|\fst e2|)) = true. +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 visited_inv_1 â λS.λe1,e2:pre S.λvisited: list ?. +uniqueb ? visited = true ⧠+ âp. memb ? p visited = true â + âw.(moves S w e1 = \fst p) ⧠(moves S w e2 = \snd p). lemma bisim_ok1: âS.âe1,e2:pre S.\sem{e1}=1\sem{e2} â - âl,n.âfrontier,visited:list (space S). + âl,n.âfrontier,visited:list (*(space S) *) ((pre S)Ã(pre S)). |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|â - visited_inv S e1 e2 visited â frontier_inv S frontier visited â + visited_inv_1 S e1 e2 visited â frontier_inv S 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