X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmatch.ma;h=9cd11f61007dce904310557b583ee95ba990e41c;hb=d6b8021e8c83eb19033cad0aeaeebf95b327e78a;hp=40979b2de268e6c78ca3f9de60efd28815858e60;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma
index 40979b2de..9cd11f610 100644
--- a/matita/matita/lib/turing/multi_universal/match.ma
+++ b/matita/matita/lib/turing/multi_universal/match.ma
@@ -12,74 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "turing/simple_machines.ma".
-include "turing/multi_universal/compare.ma".
-include "turing/multi_universal/par_test.ma".
-include "turing/multi_universal/moves_2.ma".
+include "turing/auxiliary_multi_machines.ma".
 
-lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d.
-  nth i ? v2 d = t → 
-  (∀j.i ≠ j → nth j ? v1 d = nth j ? v2 d) → 
-  v2 = change_vec ?? v1 t i.
-#sig #n #v1 #v2 #i #t #d #H1 #H2 @(eq_vec … d)
-#i0 #Hlt cases (decidable_eq_nat i0 i) #Hii0
-[ >Hii0 >nth_change_vec //
-| >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ]
-qed.
-
-lemma right_mk_tape : 
-  ∀sig,ls,c,rs.(c = None ? → ls = [ ] ∨ rs = [ ]) → right ? (mk_tape sig ls c rs) = rs.
-#sig #ls #c #rs cases c // cases ls 
-[ cases rs // 
-| #l0 #ls0 #H normalize cases (H (refl ??)) #H1 [ destruct (H1) | >H1 % ] ]
-qed.
-
-lemma left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
-#sig #ls #c #rs cases c // cases ls // cases rs //
-qed.
-
-lemma current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
-#sig #ls #c #rs cases c // cases ls // cases rs //
-qed.
-
-lemma length_tail : ∀A,l.0 < |l| → |tail A l| < |l|.
-#A * normalize //
-qed.
-
-(*
-[ ]   → [ ], l2, 1
-a::al → 
-      [ ]   → [ ], l1, 2
-      b::bl → match rec(al,bl)
-            x, y, 1 → b::x, y, 1
-            x, y, 2 → a::x, y, 2
-*)
-
-lemma lists_length_split : 
- ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
-#A #l1 elim l1
-[ #l2 %{[ ]} %{l2} % % %
-| #hd1 #tl1 #IH *
-  [ %{[ ]} %{(hd1::tl1)} %2 % %
-  | #hd2 #tl2 cases (IH tl2) #x * #y *
-    [ * #IH1 #IH2 %{(hd2::x)} %{y} % normalize % //
-    | * #IH1 #IH2 %{(hd1::x)} %{y} %2 normalize % // ]
-  ]
-]
-qed.
-
-definition option_cons ≝ λsig.λc:option sig.λl.
-  match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
-
-lemma opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l). 
-#A * //
-qed.
-
-definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n.
-  match (nth src (option sig) v (None ?)) with 
-  [ None ⇒  false 
-  | Some x ⇒  notb (nth dst (DeqOption sig) v (None ?) == None ?) ].
-  
+(* rewind *)
 definition rewind ≝ λsrc,dst,sig,n.
   parmove src dst sig n L · mmove src sig n R · mmove dst sig n R.
 
@@ -117,18 +52,6 @@ definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
    ∀ls0,y,rs0.nth dst ? int (niltape ?) = midtape sig ls0 y rs0 → 
    outt = int).
 
-(*
-theorem accRealize_to_Realize :
-  ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
-  M ⊨ [ acc: Rtrue, Rfalse ] →  M ⊨ Rtrue ∪ Rfalse.
-#sig #n #M #Rtrue #Rfalse #acc #HR #t
-cases (HR t) #k * #outc * * #Hloop
-#Htrue #Hfalse %{k} %{outc} % // 
-cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase
-[ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ]
-qed.
-*)
-
 lemma sem_rewind_strong : ∀src,dst,sig,n.
   src ≠ dst → src < S n → dst < S n → 
   rewind src dst sig n ⊨ R_rewind_strong src dst sig n.
@@ -198,11 +121,18 @@ lemma sem_rewind : ∀src,dst,sig,n.
 #ta #tb * * * #H1 #H2 #H3 #H4 % /2 by /
 qed.
 
+(* match step *) 
+
+definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n.
+  match (nth src (option sig) v (None ?)) with 
+  [ None ⇒  false 
+  | Some x ⇒  notb (nth dst (DeqOption sig) v (None ?) == None ?) ].
+
 definition match_step ≝ λsrc,dst,sig,n.
   compare src dst sig n ·
      (ifTM ?? (partest sig n (match_test src dst sig ?))
       (single_finalTM ??
-        (rewind src dst sig n · (inject_TM ? (move_r ?) n dst)))
+        (rewind src dst sig n · mmove dst ?? R))
       (nop …)
       partest1).
 
@@ -263,8 +193,8 @@ lemma sem_match_step :
     (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
       (sem_seq … 
         (sem_rewind ???? Hneq Hsrc Hdst) 
-        (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
-      (sem_nop …)))
+        (sem_move_multi … R ?))
+      (sem_nop …))) /2/
 [ #ta #tb #tc * lapply (refl ? (current ? (nth src ? ta (niltape ?))))
   cases (current ? (nth src ? ta (niltape ?))) in ⊢ (???%→%);
   [ #Hcurta_src #Hcomp #_ * #td * >Hcomp [| % %2 %]
@@ -304,15 +234,10 @@ lemma sem_match_step :
           lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
           >change_vec_commute // >change_vec_change_vec
           >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
-          >Hte in Htb; * * #_ >nth_change_vec // #Htb1
-          lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2 %
-          [ @(eq_vec … (niltape ?)) #i #Hi
-            cases (true_or_false ((dst : DeqNat) == i)) #Hdsti
-            [ <(\P Hdsti) >Htb1 >nth_change_vec // >Hmidta_dst
-              >Hrs0 >reverse_reverse cases xs [|#r1 #rs1] %
-            | <Htb2 [|@(\Pf Hdsti)] >nth_change_vec_neq [| @(\Pf Hdsti)]
-              >Hrs0 >reverse_reverse >nth_change_vec_neq in ⊢ (???%); 
-              <Hrs <Hmidta_src [|@(\Pf Hdsti)] >change_vec_same % ]
+          >Hte in Htb; whd in ⊢ (%→?); #Htb >Htb %
+          [ >change_vec_change_vec >nth_change_vec //
+            >reverse_reverse <Hrs <Hmidta_src >change_vec_same <Hrs0 <Hmidta_dst
+            %
           | >Hmidta_dst %{s'} % [%] #_
             >Hrs0 %{xs} %{ci} %{rs''} %{ls0} %{cj} %{rs0'} % // % // 
           ]
@@ -320,14 +245,10 @@ lemma sem_match_step :
       | 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 * * #_ #Hte * * #_ #Htb1 #Htb2
+        #Htd destruct (Htd) * #te * * #_ #Hte whd in ⊢ (%→?); #Htb
         #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] %
-          | <Htb2 [|@(\Pf Hdsti)] >nth_change_vec_neq [| @(\Pf Hdsti)] % ]
+        [ >Htb %
         | >Hs0 %{s0} % // #H destruct (H) @False_ind cases (Hss0) /2/ ]
       ]
     ]
@@ -526,8 +447,8 @@ lemma sem_match_step_termination :
     (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
       (sem_seq … 
         (sem_rewind_strong ???? Hneq Hsrc Hdst) 
-        (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
-      (sem_nop …)))
+        (sem_move_multi … R ?))
+      (sem_nop …))) [/2/]
 [ #ta #tb #tc * lapply (refl ? (current ? (nth src ? ta (niltape ?))))
   cases (current ? (nth src ? ta (niltape ?))) in ⊢ (???%→%);
   [ #Hcurta_src #Hcomp #_ * #td * >Hcomp [| % %2 %]
@@ -572,12 +493,11 @@ lemma sem_match_step_termination :
               lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
               >change_vec_commute [|//] >change_vec_change_vec
               >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
-              >Hte * * #_ >nth_change_vec [|//] >reverse_reverse 
-              #H lapply (H … (refl ??)) -H #Htb1 #Htb2
+              >Hte whd in ⊢ (%→?); >change_vec_change_vec >nth_change_vec [|//] 
+              >reverse_reverse #Htb
               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)
-              [ @(eq_vec_change_vec … (niltape ?))
-                [@Htb1| #j #Hj <Htb2 // >(nth_change_vec_neq ??????? Hj) % ] ]
-              -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+              [ >Htb @eq_f3 // cases (xs@cj::rs0') // ]
+              -Htb #Htb >Htb whd >nth_change_vec [|//]
               >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec [|//]
               >right_mk_tape [|cases xs [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H)]
               normalize in match (left ??);
@@ -593,16 +513,15 @@ 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 #_  whd in ⊢ (%→?); #Htb
               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)
-              [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?)) 
-                [ @Htb1 %
-                | #j #Hj <Htb2 // >change_vec_commute // >change_vec_change_vec
-                  >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec
-                  >nth_change_vec_neq in ⊢ (???%); // ] ]
-              -Htb1 -Htb2 #Htb >Htb whd 
+              [ >Htb >Hte >nth_change_vec // >change_vec_change_vec >change_vec_commute [|//]
+                >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+                >change_vec_change_vec >change_vec_commute [|//]
+                @eq_f3 // cases (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0') // ]
+              -Htb #Htb >Htb whd 
               >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
               >right_mk_tape 
               [| cases (reverse sig (reverse sig xs@s0::reverse sig tla))
@@ -621,14 +540,12 @@ lemma sem_match_step_termination :
               lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
               >change_vec_change_vec >change_vec_commute [|@sym_not_eq //] 
               >change_vec_change_vec #Hte #_
-              >Hte * * #_ >nth_change_vec [|//] >reverse_reverse 
-              #H lapply (H … (refl ??)) -H #Htb1 #Htb2
+              >Hte whd in ⊢ (%→?); >nth_change_vec [|//] >reverse_reverse #Htb 
               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)
-              [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
-                [ @Htb1
-                | #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ] ] 
-              -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+              [ >Htb >change_vec_change_vec >change_vec_commute [|//]
+                @eq_f3 // <Hrs0 cases rs0 // ]
+              -Htb #Htb >Htb whd >nth_change_vec [|//]
               >nth_change_vec_neq [|//] >nth_change_vec [|//]
               >right_mk_tape 
               [| cases xs [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ] 
@@ -645,16 +562,15 @@ 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 #_ whd in ⊢ (%→?); >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb
               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)
-              [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
-                [ @Htb1 % 
-                | #j #Hj <Htb2 [|//] >change_vec_change_vec
-                  >change_vec_commute [|@sym_not_eq //]
-                  >change_vec_change_vec >nth_change_vec_neq in ⊢ (???%); // ] ]
-              -Htb1 -Htb2 #Htb >Htb whd 
+              [ >Htb >change_vec_change_vec >change_vec_commute [|//]
+                >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+                >change_vec_change_vec >change_vec_commute [|//]
+                @eq_f3 // cases (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0') // ]
+              -Htb #Htb >Htb whd 
               >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
               >right_mk_tape
               [| cases (reverse sig (reverse sig xs@s0::reverse sig tlb))
@@ -681,11 +597,11 @@ lemma sem_match_step_termination :
           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
+            lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte)
+            whd in ⊢ (%→?); >Hmidta_dst #Htb
             cut (tb = change_vec ?? ta (mk_tape ? (s0::lsa@lsb) (option_hd ? rs0) (tail ? rs0)) dst)
-            [@(eq_vec_change_vec … (niltape ?)) [@Htb1|@Htb2] ]
-            -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+            [ >Htb cases rs0 // ]
+            -Htb #Htb >Htb whd >nth_change_vec [|//]
             >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
             >right_mk_tape 
             [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H)] ]
@@ -697,14 +613,12 @@ lemma sem_match_step_termination :
             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
+            whd in ⊢ (%→?); >Hte >change_vec_change_vec >nth_change_vec // #Htb
             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)
-            [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
-              [ @Htb1 //
-              | #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ]] 
-            -Htb1 -Htb2 #Htb >Htb whd 
+            [ >Htb >change_vec_commute [|//] @eq_f3 // cases (reverse sig (reverse sig tla)@s0::rs0) // ]
+            -Htb #Htb >Htb whd 
             >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
             >right_mk_tape 
             [| cases (reverse sig (reverse sig tla))
@@ -719,10 +633,10 @@ lemma sem_match_step_termination :
          @(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
+           whd in ⊢ (%→?); #Htb whd >Hmidta_dst
            cut (tb = change_vec (tape sig) (S n) ta (mk_tape ? (s0::ls0) (option_hd ? rs0) (tail ? rs0)) dst)
-           [ @(eq_vec_change_vec … (niltape ?)) // @Htb2 ]
-           -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+           [ >Htb >Hmidta_dst cases rs0 // ]
+           -Htb #Htb >Htb whd >nth_change_vec [|//]
            >nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
            >current_mk_tape >right_mk_tape 
            [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H) ]]
@@ -736,15 +650,13 @@ lemma sem_match_step_termination :
            | >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
+           #Hte whd in ⊢ (%→?); >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb
            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)
-           [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
-             [ @Htb1 %
-             | #j #Hj <Htb2 // >change_vec_commute [|@sym_not_eq //]
-               >nth_change_vec_neq in ⊢ (???%); // ]]
-           -Htb1 -Htb2 #Htb >Htb whd 
+           [ >Htb >change_vec_commute [|//] >change_vec_change_vec
+             @eq_f3 // cases (reverse sig (reverse sig tlb)@s0::rs0) // ]
+           -Htb #Htb >Htb whd 
            >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
            >right_mk_tape
            [| cases (reverse ? (reverse ? tlb)) [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]