X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmoves.ma;h=f725a1940202b8bf641152ce2eeb21d433e5f98d;hb=f5ccde287dec5598a3b88197be03da87ac50ce98;hp=b1dd0ac832cfa73a06376ee3d4ea3b0a00d58cce;hpb=1a054f8c2ca1590cab8d335749a10e2ed13a11eb;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/moves.ma b/matita/matita/lib/turing/multi_universal/moves.ma
index b1dd0ac83..f725a1940 100644
--- a/matita/matita/lib/turing/multi_universal/moves.ma
+++ b/matita/matita/lib/turing/multi_universal/moves.ma
@@ -47,8 +47,8 @@ definition trans_parmove_step ≝
      [ None ⇒ 〈parmove2,null_action ? n〉
      | Some a1 ⇒ 〈parmove1,change_vec ? (S n)
                           (change_vec ?(S n)
-                           (null_action ? n) (Some ? 〈a0,D〉) src)
-                          (Some ? 〈a1,D〉) dst〉 ] ]
+                           (null_action ? n) (〈None sig,D〉) src)
+                          (〈None ?,D〉) dst〉 ] ]
  | S q ⇒ match q with 
    [ O ⇒ (* 1 *) 〈parmove1,null_action ? n〉
    | S _ ⇒ (* 2 *) 〈parmove2,null_action ? n〉 ] ].
@@ -66,8 +66,8 @@ definition R_parmove_step_true ≝
    is_sep x1 = false ∧
    outt = change_vec ?? 
             (change_vec ?? int
-              (tape_move ? (nth src ? int (niltape ?)) (Some ? 〈x1,D〉)) src)
-            (tape_move ? (nth dst ? int (niltape ?)) (Some ? 〈x2,D〉)) dst.
+              (tape_move_mono ? (nth src ? int (niltape ?)) (〈None ?,D〉)) src)
+            (tape_move_mono ? (nth dst ? int (niltape ?)) (〈None ?,D〉)) dst.
 
 definition R_parmove_step_false ≝ 
   λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n).
@@ -88,7 +88,7 @@ lemma parmove_q0_q2_null_src :
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Hcurrent %
-| whd in ⊢ (??(???????(???%))?); >Hcurrent @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
 qed.
 
 lemma parmove_q0_q2_sep :
@@ -101,8 +101,8 @@ lemma parmove_q0_q2_sep :
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
-| whd in ⊢ (??(???????(???%))?); >Hcurrent
-  whd in ⊢ (??(???????(???%))?); >Hsep @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Hcurrent
+  whd in ⊢ (??(????(???%))?); >Hsep @tape_move_null_action ]
 qed.
 
 lemma parmove_q0_q2_null_dst :
@@ -116,8 +116,8 @@ lemma parmove_q0_q2_null_dst :
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Hcursrc whd in ⊢ (??(???%)?); >Hsep >Hcurdst %
-| whd in ⊢ (??(???????(???%))?); >Hcursrc
-  whd in ⊢ (??(???????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Hcursrc
+  whd in ⊢ (??(????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
 qed.
 
 lemma parmove_q0_q1 :
@@ -131,19 +131,19 @@ lemma parmove_q0_q1 :
     mk_mconfig ??? parmove1 
      (change_vec ? (S n) 
        (change_vec ?? v
-         (tape_move ? (nth src ? v (niltape ?)) (Some ? 〈a1,D〉)) src)
-       (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈a2,D〉)) dst).
+         (tape_move_mono ? (nth src ? v (niltape ?)) (〈None ?, D〉)) src)
+       (tape_move_mono ? (nth dst ? v (niltape ?)) (〈None ?, D〉)) dst).
 #src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
 #a1 #a2 #Hcursrc #Hcurdst #Hsep
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
 [ whd in match (trans ????);
   >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
 | whd in match (trans ????);
-  >Hcursrc >Hcurdst whd in ⊢ (??(???????(???%))?); >Hsep
-  change with (change_vec ?????) in ⊢ (??(???????%)?);
-  <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
-  <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
-  >pmap_change >pmap_change >tape_move_null_action
+  >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?);
+  <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?);
+  >tape_move_multi_def >pmap_change
+  <(change_vec_same ?? v src (niltape ?)) in ⊢ (??%?);
+  >pmap_change <tape_move_multi_def >tape_move_null_action
   @eq_f2 // @eq_f2 // >nth_change_vec_neq //
 ]
 qed.
@@ -159,14 +159,12 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
 [ #Hcursrc %{2} %
   [| % [ %
     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
-      <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
     | normalize in ⊢ (%→?); #H destruct (H) ]
     | #_ % // % %2 // ] ]
 | #a #Ha cases (true_or_false (is_sep a)) #Hsep
   [ %{2} %
     [| % [ %
       [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
-        <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
       | normalize in ⊢ (%→?); #H destruct (H) ]
       | #_ % // % % %{a} % // ] ]
   | lapply (refl ? (current ? (nth dst ? int (niltape ?))))
@@ -174,15 +172,11 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
     [ #Hcurdst %{2} %
       [| % [ %
         [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/ 
-          [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-          | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
         | normalize in ⊢ (%→?); #H destruct (H) ]
         | #_ % // %2 // ] ]
     | #b #Hb %{2} %
       [| % [ % 
         [whd in ⊢  (??%?);  >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
-          [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-          | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
         | #_ %{a} %{b} % // % // % // ]
         | * #H @False_ind @H % ]
 ]]]]
@@ -201,76 +195,60 @@ definition R_parmoveL ≝
     outt = change_vec ?? 
            (change_vec ?? int (midtape sig ls sep (reverse ? xs@x::rs)) src)
            (midtape sig ls0 c (reverse ? target@x0::rs0)) dst) ∧
-  (∀s.current ? (nth src ? int (niltape ?)) = Some ? s → is_sep s = true → 
-   outt = int).
+  (((∃s.current ? (nth src ? int (niltape ?)) = Some ? s ∧ is_sep s = true) ∨  
+     current ? (nth src ? int (niltape ?)) = None ? ∨
+     current ? (nth dst ? int (niltape ?)) = None ?) →
+     outt = int).
   
 lemma wsem_parmoveL : ∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n → 
   parmove src dst sig n L is_sep ⊫ R_parmoveL src dst sig n is_sep.
 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) … Hloop) //
 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
-[ #tc whd in ⊢ (%→?); * * [ *
-  [ * #x * #Hx #Hsep #Houtc %
-    [ #ls #x0 #xs #rs #sep #Hsrctc #Hnosep >Hsrctc in Hx; normalize in ⊢ (%→?);
-      #Hx0 destruct (Hx0) lapply (Hnosep ? (memb_hd …)) >Hsep
-      #Hfalse destruct (Hfalse)
-    | #s #Hs #Hseps @Houtc ]
-  | #Hcur #Houtc %
-    [ #ls #x0 #xs #rs #sep #Hsrctc >Hsrctc in Hcur; normalize in ⊢ (%→?); 
-      #Hcur destruct (Hcur) 
-    | >Hcur #s #Hs destruct (Hs) ] ]
-  | #Hcur #Houtc %
-    [ #ls #x0 #xs #rs #sep #Hsrctc #Hnosep #Hsep #ls0 #x1 #target #c #rs0 #Hlen
-      #Hdsttc >Hdsttc in Hcur; normalize in ⊢ (%→?); #Hcur destruct (Hcur)
-    | #s #Hs #Hseps @Houtc ]
-  ]
-| #tc #td #te * #c0 * #c1 * * * #Hc0 #Hc1 #Hc0nosep #Hd #Hstar #IH #He 
+[ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H
+  [ * [ * #x * #Hx #Hsep #ls #x0 #xs #rs #sep #Hsrctc #Hnosep >Hsrctc in Hx; normalize in ⊢ (%→?);
+    #Hx0 destruct (Hx0) lapply (Hnosep ? (memb_hd …)) >Hsep
+    #Hfalse destruct (Hfalse)
+  | #Hcur_src #ls #x0 #xs #rs #sep #Hsrctc >Hsrctc in Hcur_src;
+    normalize in ⊢ (%→?); #H destruct (H)]
+  |#Hcur_dst  #ls #x0 #xs #rs #sep #Hsrctc #Hnosep #Hsep #ls0 #x1 #target 
+   #c #rs0 #Hlen #Hdsttc >Hdsttc in Hcur_dst; normalize in ⊢ (%→?); #H destruct (H)
+  ]  
+| #td #te * #c0 * #c1 * * * #Hc0 #Hc1 #Hc0nosep #Hd #Hstar #IH #He 
   lapply (IH He) -IH * #IH1 #IH2 %
   [ #ls #x #xs #rs #sep #Hsrc_tc #Hnosep #Hsep #ls0 #x0 #target
     #c #rs0 #Hlen #Hdst_tc
-    >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
-(*    <(change_vec_same … tc src (niltape ?)) in Hd:(???(???(???%??)??));
-      <(change_vec_same … tc dst (niltape ?)) in ⊢(???(???(???%??)??)→?); *)
-    >Hdst_tc in Hd; >Hsrc_tc
-(*    >change_vec_change_vec >change_vec_change_vec
-      >(change_vec_commute ?? tc ?? dst src) [|@(sym_not_eq … Hneq)]
-      >change_vec_change_vec *) @(list_cases2 … Hlen)
-    [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >(IH2 … Hsep)
-      [ >Hd -Hd @(eq_vec … (niltape ?))
-        #i #Hi cases (decidable_eq_nat i src) #Hisrc
-        [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
-          >nth_change_vec //
-          >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
-          >nth_change_vec //
-        | cases (decidable_eq_nat i dst) #Hidst
-          [ >Hidst >nth_change_vec // >nth_change_vec //
-            >Hdst_tc in Hc1; >Htargetnil
-            normalize in ⊢ (%→?); #Hc1 destruct (Hc1) %
-          | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
-            >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
-            >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
-            >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % ]
-         ]
-       | >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
-         >nth_change_vec // ]
+   >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
+   >Hdst_tc in Hd; >Hsrc_tc @(list_cases2 … Hlen)
+    [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2 
+      [2: %1 %1 %{sep} % // >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
+      >nth_change_vec //]  
+      >Hd -Hd @(eq_vec … (niltape ?))
+      #i #Hi cases (decidable_eq_nat i src) #Hisrc
+      [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
+        >nth_change_vec //
+      | cases (decidable_eq_nat i dst) #Hidst
+        [ >Hidst >nth_change_vec // 
+        | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % 
+        ]
+      ]
     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
       >(IH1 ls hd1 tl1 (c0::rs) sep ?? Hsep ls0 hd2 tl2 c (x0::rs0))
-      [ >Hd >(change_vec_commute … ?? tc ?? src dst) //
+      [ >Hd >(change_vec_commute … ?? td ?? src dst) //
        >change_vec_change_vec
-       >(change_vec_commute … ?? tc ?? dst src) [|@sym_not_eq //]
+       >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
        >change_vec_change_vec
        >reverse_cons >associative_append
        >reverse_cons >associative_append % 
-     | >Hd >nth_change_vec // >Hdst_tc >Htarget >Hdst_tc in Hc1;
-       normalize in ⊢ (%→?); #H destruct (H) //
+     | >Hd >nth_change_vec //
      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
      | <Hxs #c1 #Hc1 @Hnosep @memb_cons //
      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
        >nth_change_vec // ]
    ]
- | #c #Hc #Hsepc >Hc in Hc0; #Hcc0 destruct (Hcc0) >Hc0nosep in Hsepc;
-   #H destruct (H)
-] ]
+ | >Hc0 >Hc1 * [* [ * #c * #Hc destruct (Hc) >Hc0nosep]] #Habs destruct (Habs)
+ ] ]
 qed.
  
 lemma terminate_parmoveL :  ∀src,dst,sig,n,is_sep,t.
@@ -297,5 +275,6 @@ qed.
 lemma sem_parmoveL : ∀src,dst,sig,n,is_sep.
   src ≠ dst → src < S n → dst < S n → 
   parmove src dst sig n L is_sep ⊨ R_parmoveL src dst sig n is_sep.
-#src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst @WRealize_to_Realize /2/
+#src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst @WRealize_to_Realize 
+[/2/ | @wsem_parmoveL //]
 qed.
\ No newline at end of file