X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmatch.ma;h=0ef1213eaf62ba19f00bac9536db3d62d706c8e9;hb=dae251c38e392d180110a5e3d93522333747296c;hp=fd53d8a90f291e6c1fca909aff518bbbb00dcea8;hpb=26fd200d0b1feff8adaff18d482c30e39eaf01cf;p=helm.git diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index fd53d8a90..0ef1213ea 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -129,6 +129,9 @@ definition R_rewind_strong ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S (midtape sig ls0 y0 (reverse ? target@y::rs0)) src) ∧ (∀x,rs.nth src ? int (niltape ?) = midtape sig [] x rs → ∀ls0,y,rs0.nth dst ? int (niltape ?) = midtape sig ls0 y rs0 → + outt = int) ∧ + (∀x,rs.nth dst ? int (niltape ?) = midtape sig [] x rs → + ∀ls0,y,rs0.nth src ? int (niltape ?) = midtape sig ls0 y rs0 → outt = int). definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). @@ -162,7 +165,7 @@ lemma sem_rewind_strong : ∀src,dst,sig,n. @(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) ?) [| @(sem_seq_app sig n ????? (sem_move_multi … R ?) (sem_move_multi … R ?)) // @le_S_S_to_le // ] -#ta #tb * #tc * * * #Htc1 #Htc2 #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb % [ % +#ta #tb * #tc * * * #Htc1 #Htc2 #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb % [ % [ % [ #x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst >(Htc1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in Htd; [|>Hmidta_dst // @@ -200,14 +203,28 @@ lemma sem_rewind_strong : ∀src,dst,sig,n. >nth_change_vec // >change_vec_change_vec whd in match (tape_move ???);whd in match (tape_move ???); change_vec_same >change_vec_same // -]] + ] ] +| #x #rs #Hmidta_dst #ls0 #y #rs0 #Hmidta_src + lapply (Htc2 … Hmidta_dst … (refl ??) Hmidta_src) -Htc2 #Htc >Htc in Htd; + >change_vec_change_vec >change_vec_commute [|@sym_not_eq //] + >nth_change_vec // lapply (refl ? ls0) cases ls0 in ⊢ (???%→%); + [ #Hls0 destruct (Hls0) #Htd >Htd in Htb; + >nth_change_vec // >change_vec_change_vec + whd in match (tape_move ???);whd in match (tape_move ???); + change_vec_same >change_vec_same // + | #l1 #ls1 #Hls0 destruct (Hls0) #Htd >Htd in Htb; + >nth_change_vec // >change_vec_change_vec + whd in match (tape_move ???); whd in match (tape_move ???); change_vec_same >change_vec_same // + ] +] qed. lemma sem_rewind : ∀src,dst,sig,n. src ≠ dst → src < S n → dst < S n → rewind src dst sig n ⊨ R_rewind src dst sig n. #src #dst #sig #n #Hneq #Hsrc #Hdst @(Realize_to_Realize … (sem_rewind_strong …)) // -#ta #tb * * #H1 #H2 #H3 % /2/ +#ta #tb * * * #H1 #H2 #H3 #H4 % /2/ qed. definition match_step ≝ λsrc,dst,sig,n. @@ -522,18 +539,24 @@ qed. axiom daemon : ∀P:Prop.P. +(* XXX: move to turing (or mono) *) +definition option_cons ≝ λsig.λc:option sig.λl. + match c with [ None ⇒ l | Some c0 ⇒ c0::l ]. + definition R_match_step_true_naive ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). |left ? (nth src ? outt (niltape ?))| + - |right ? (nth dst ? outt (niltape ?))| < + |option_cons ? (current ? (nth dst ? outt (niltape ?))) (right ? (nth dst ? outt (niltape ?)))| < |left ? (nth src ? int (niltape ?))| + - |right ? (nth dst ? int (niltape ?))|. + |option_cons ? (current ? (nth dst ? int (niltape ?))) (right ? (nth dst ? int (niltape ?)))|. axiom right_mk_tape : ∀sig,ls,c,rs.right ? (mk_tape sig ls c rs) = rs. axiom left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls. +axiom current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c. axiom length_tail : ∀A,l.0 < |l| → |tail A l| < |l|. axiom lists_length_split : ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)). +axiom opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l). lemma sem_match_step_termination : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → @@ -580,7 +603,7 @@ lemma sem_match_step_termination : ]] normalize in ⊢ (%→?); #H destruct (H) ] | * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0 - #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * * + #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * * * >Htc >change_vec_commute // >nth_change_vec // >change_vec_commute [|@sym_not_eq //] >nth_change_vec // cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb @@ -588,7 +611,7 @@ lemma sem_match_step_termination : [ #Hte #_ #_ <(reverse_reverse … ls) in Hte; <(reverse_reverse … lsa) cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen' @(list_cases2 … Hlen') - [ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte + [ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte #_ lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte >change_vec_commute // >change_vec_change_vec >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte @@ -598,8 +621,9 @@ lemma sem_match_step_termination : [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // >right_mk_tape normalize in match (left ??); - >Hmidta_src >Hmidta_dst >length_tail >Hrs0 >length_append - normalize in ⊢ (?(?%)(?%?)); >commutative_plus // + >Hmidta_src >Hmidta_dst >current_mk_tape Hrs0 + normalize in ⊢ (?(?%)%); // | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2 >reverse_cons >reverse_cons #Hte lapply (Hte ci hdb (reverse ? xs@s0::reverse ? tlb) rs'' ? @@ -609,7 +633,7 @@ lemma sem_match_step_termination : >H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen' >length_reverse >length_reverse destruct (Hlen') // | /2 by refl, trans_eq/ ] -Hte - #Hte * * #_ >Hte >nth_change_vec // #Htb1 #Htb2 + #Hte #_ * * #_ >Hte >nth_change_vec // #Htb1 #Htb2 cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0'))) dst) (midtape ? [ ] hdb (reverse sig (reverse sig xs@s0::reverse sig tlb)@ci::rs'')) src) @@ -617,7 +641,8 @@ lemma sem_match_step_termination : >nth_change_vec // >nth_change_vec_neq // >nth_change_vec // >right_mk_tape >Hmidta_src >Hmidta_dst whd in match (left ??); whd in match (left ??); whd in match (right ??); - >length_tail >Hrs0 >length_append >length_append >length_reverse + >current_mk_tape Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse >length_append >commutative_plus in match (|reverse ??| + ?); whd in match (|?::?|); >length_reverse >length_reverse <(length_reverse ? ls) H1 normalize // ] @@ -627,19 +652,17 @@ lemma sem_match_step_termination : [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #Hte lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte >change_vec_change_vec >change_vec_commute [|@sym_not_eq //] - >change_vec_change_vec #Hte + >change_vec_change_vec #Hte #_ >Hte * * #_ >nth_change_vec // >reverse_reverse #H lapply (H … (refl ??)) -H #Htb1 #Htb2 - (* cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst) *) cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst) (midtape ? lsb s0 (xs@ci::rs'')) src) [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec // >nth_change_vec_neq // >nth_change_vec // >right_mk_tape normalize in match (left ??); - >Hmidta_src >Hmidta_dst >length_tail >Hrs0 >length_append - >commutative_plus in match (pred ?); normalize - >length_append >(?:|lsa| = O) - [ normalize H1 % ] + >Hmidta_src >Hmidta_dst >current_mk_tape Hrs0 + >length_append normalize >length_append >length_append + <(reverse_reverse ? lsa) >H1 normalize // | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2 >reverse_cons >reverse_cons #Hte lapply (Hte cj hdb (reverse ? xs@s0::reverse ? tlb) rs0' ? @@ -649,7 +672,7 @@ lemma sem_match_step_termination : >H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen' >length_reverse >length_reverse destruct (Hlen') // | /2 by refl, trans_eq/ ] -Hte - #Hte * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2 + #Hte #_ * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2 cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0'))) dst) (midtape ? lsb hda (reverse sig (reverse sig xs@s0::reverse sig tla)@ci::rs'')) src) @@ -657,31 +680,85 @@ lemma sem_match_step_termination : >nth_change_vec // >nth_change_vec_neq // >nth_change_vec // >right_mk_tape >Hmidta_src >Hmidta_dst whd in match (left ??); whd in match (left ??); whd in match (right ??); - >length_tail >Hrs0 >length_append >length_append >length_reverse + >current_mk_tape Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse >length_append >commutative_plus in match (|reverse ??| + ?); - whd in match (|?::?|); >length_reverse >length_reverse >Hlen - <(length_reverse ? ls0) >H2 whd in match (|?::?|); - >length_append normalize // + whd in match (|?::?|); >length_reverse >length_reverse + <(length_reverse ? lsa) >Hlen' >H2 >length_append + normalize // ] ] ] - | FIXME - (* lapply (\Pf Hss0) -Hss0 #Hss0 #Htc cut (tc = ta) + | lapply (\Pf Hss0) -Hss0 #Hss0 #Htc cut (tc = ta) [@Htc % % @(not_to_not ??? Hss0) #H destruct (H) %] -Htc #Htc destruct (Htc) #_ * #td * whd in ⊢ (%→?); * #_ - #Htd destruct (Htd) * #te * * * # #_ >Hmidta_src >Hmidta_dst #Hte - lapply (Hte … (refl ??) … (refl ??)) * * #_ #Htb1 #Htb2 - #s1 #rs1 >Hmidta_src #H destruct (H) - lapply (Hte … Hmidta_src … Hmidta_dst) -Hte #Hte destruct (Hte) % - [ @(eq_vec … (niltape ?)) #i #Hi - cases (true_or_false ((dst : DeqNat) == i)) #Hdsti - [ <(\P Hdsti) >(Htb1 … Hmidta_dst) >nth_change_vec // >Hmidta_dst - cases rs0 [|#r2 #rs2] % - | nth_change_vec_neq [| @(\Pf Hdsti)] % ] - | >Hs0 %{s0} % // #H destruct (H) @False_ind cases (Hss0) /2/ ] *) - ] - ] - ] + #Htd destruct (Htd) * #te * * * * >Hmidta_src >Hmidta_dst + cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb + destruct (Hlsalsb) + [ <(reverse_reverse … ls) <(reverse_reverse … lsa) + cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen' + @(list_cases2 … Hlen') + [ #H1 #H2 >H1 >H2 -H1 -H2 #_ #_ normalize in match (reverse ? [ ]); #Hte #_ + lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte) * * #_ + >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2 + cut (tb = change_vec ?? ta (mk_tape ? (s0::lsa@lsb) (option_hd ? rs0) (tail ? rs0)) dst) + [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec // + >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst + >right_mk_tape normalize in match (left ??); normalize in match (right ??); + >Hmidta_src >Hmidta_dst >current_mk_tape H1 >H2 + >reverse_cons >reverse_cons >associative_append #Hte + lapply (Hte ???? (refl ??) ? s0 ? (reverse ? tla) ?? (refl ??)) + [ >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) // + normalize #H destruct (H) // ] #Hte #_ #_ #_ + * * #_ >Hte >nth_change_vec // #Htb1 #Htb2 + cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta + (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig tla)@s0::rs0)) (tail ? (reverse sig (reverse sig tla)@s0::rs0))) dst) + (midtape ? [ ] hdb (reverse sig (reverse sig tlb)@s::rs)) src) + [@daemon] -Htb1 -Htb2 #Htb >Htb whd + >nth_change_vec // >nth_change_vec_neq // >nth_change_vec // + >right_mk_tape >Hmidta_src >Hmidta_dst + whd in match (left ??); whd in match (left ??); whd in match (right ??); + >current_mk_tape length_append + >length_reverse >length_reverse <(length_reverse ? ls) H1 normalize // ] + | #_ <(reverse_reverse … ls0) <(reverse_reverse … lsa) + cut (|reverse ? lsa| = |reverse ? ls0|) [ // ] #Hlen' + @(list_cases2 … Hlen') + [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #_ #_ #Hte + lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte) + * * #_ >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2 + cut (tb = change_vec (tape sig) (S n) ta (mk_tape ? (s0::ls0) (option_hd ? rs0) (tail ? rs0)) dst) + [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec // + >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst + >current_mk_tape >right_mk_tape normalize in ⊢ (??%); H1 >H2 + >reverse_cons >reverse_cons #Hte #_ #_ + lapply (Hte s0 hdb (reverse ? tlb) rs0 ? + lsb s hda (reverse ? tla) rs ??) + [ /2 by cons_injective_l, nil/ + | >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) // + normalize #H destruct (H) // + | /2 by refl, trans_eq/ ] -Hte + #Hte * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2 + cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta + (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig tlb)@s0::rs0)) (tail ? (reverse sig (reverse sig tlb)@s0::rs0))) dst) + (midtape ? lsb hda (reverse sig (reverse sig tla)@s::rs)) src) + [@daemon] -Htb1 -Htb2 #Htb >Htb whd + >nth_change_vec // >nth_change_vec_neq // >nth_change_vec // + >right_mk_tape >Hmidta_src >Hmidta_dst + whd in match (left ??); whd in match (left ??); whd in match (right ??); + >current_mk_tape length_append + normalize in ⊢ (??%); >length_append >reverse_reverse + <(length_reverse ? lsa) >Hlen' >H2 normalize // + ] + ] + ] + ] + ] | #ta #tb #tc * #Hcomp1 #Hcomp2 * #td * * #Htest #Htd destruct (Htd) whd in ⊢ (%→?); #Htb destruct (Htb) #ls #x #xs #Hta_src lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) @@ -711,21 +788,28 @@ lemma sem_match_step_termination : normalize #H destruct (H) ] ] ] qed. - -definition Pre_match_m ≝ - λsrc,sig,n.λt: Vector (tape sig) (S n). - ∃x,xs. - nth src (tape sig) t (niltape sig) = midtape ? [] x xs. - -lemma terminate_match_m : +axiom terminate_match_m : ∀src,dst,sig,n,t. src ≠ dst → src < S n → dst < S n → - Pre_match_m src sig n t → match_m src dst sig n ↓ t. -#src #dst #sig #n #t #Hneq #Hsrc #Hdst * #start * #xs -#Hmid_src -@(terminate_while … (sem_match_step src dst sig n Hneq Hsrc Hdst)) // +(*#src #dst #sig #n #ta #Hneq #Hsrc #Hdst +@(terminate_while … (sem_match_step_termination src dst sig n Hneq Hsrc Hdst)) // % #tb +letin f ≝ (λt0:Vector (tape sig) (S n).|left ? (nth src (tape ?) t0 (niltape ?))| + +|option_cons ? (current ? (nth dst (tape ?) t0 (niltape ?))) + (right ? (nth dst (tape ?) t0 (niltape ?)))|) +change with (f tb < f ta) in ⊢ (%→?); @(nat_elim1 (f tb)) +#x lapply (refl ? x) cases x in ⊢ (???%→%); +[ #Hx +* +#x #IH #Hx cases + + @IH % #tc change with (f tc < f tb) in ⊢ (%→?); + + )(|left @(nat_elim1 (|left ? (nth ? (tape ?) t (niltape ?))| + +|option_cons sig (current ? (nth dst (tape ?) t (niltape ?))) + (right ? (nth dst (tape ?) t (niltape ?)))|)) <(change_vec_same … t dst (niltape ?)) +<(change_vec_same … t src (niltape ?)) in ⊢ (???(???%??)); lapply (refl ? (nth dst (tape sig) t (niltape ?))) cases (nth dst (tape sig) t (niltape ?)) in ⊢ (???%→?); [ #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //] @@ -757,4 +841,10 @@ cases (nth dst (tape sig) t (niltape ?)) in ⊢ (???%→?); | >Ht1 >nth_change_vec // ] ] ] -qed. \ No newline at end of file +qed. *) + +lemma sem_match_m : ∀src,dst,sig,n. +src ≠ dst → src < S n → dst < S n → + match_m src dst sig n \vDash R_match_m src dst sig n. +#src #dst #sig #n #Hneq #Hsrc #Hdst @WRealize_to_Realize [/2/| @wsem_match_m // ] +qed.