X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmoves_2.ma;h=e56a0f183e434fe96c09a9402e3f982ad631b32b;hb=637ff9311e16f1d58e03d873f84c354e1cf1e716;hp=14f072b4ee966d0ec56602cb7cbac1aaef4e74b3;hpb=64a752136a679bcab14a9cd01823c18b7cc991de;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma
index 14f072b4e..e56a0f183 100644
--- a/matita/matita/lib/turing/multi_universal/moves_2.ma
+++ b/matita/matita/lib/turing/multi_universal/moves_2.ma
@@ -12,6 +12,7 @@
 include "turing/turing.ma".
 include "turing/inject.ma".
 include "turing/while_multi.ma".
+include "turing/while_machine.ma".
 
 definition parmove_states ≝ initN 3.
 
@@ -169,6 +170,13 @@ definition R_parmoveL ≝
     outt = change_vec ?? 
            (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) src)
            (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) dst) ∧
+  (∀x,xs,rs.
+    nth dst ? int (niltape ?) = midtape sig xs x rs → 
+    ∀ls0,x0,target,rs0.|xs| = |target| → 
+    nth src ? int (niltape ?) = midtape sig (target@ls0) x0 rs0 → 
+    outt = change_vec ?? 
+           (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) dst)
+           (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) src) ∧
   ((current ? (nth src ? int (niltape ?)) = None ? ∨
     current ? (nth dst ? int (niltape ?)) = None ?) →
     outt = int).
@@ -178,14 +186,22 @@ lemma wsem_parmoveL : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n 
 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 lapply (sem_while … (sem_parmove_step src dst sig n L Hneq Hsrc Hdst) … Hloop) //
 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
-[ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H
-  [ #Hcurtb #x #xs #rs #Hsrctb >Hsrctb in Hcurtb; normalize in ⊢ (%→?);
-    #Hfalse destruct (Hfalse)
-  | #Hcur_dst #x #xs #rs #Hsrctb #ls0 #x0 #target 
-    #rs0 #Hlen #Hdsttb >Hdsttb in Hcur_dst; normalize in ⊢ (%→?); #H destruct (H)
+[ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H #Hcurtb
+  [ % 
+    [ #x #xs #rs #Hsrctb >Hsrctb in Hcurtb; normalize in ⊢ (%→?);
+      #Hfalse destruct (Hfalse)
+    | #x #xs #rs #Hdsttb #ls0 #x0 #target #rs0 #Hlen #Hsrctb >Hsrctb in Hcurtb;
+      normalize in ⊢ (%→?); #H destruct (H)
+    ]
+  | %
+    [ #x #xs #rs #Hsrctb #ls0 #x0 #target 
+      #rs0 #Hlen #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
+    | #x #xs #rs #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?);
+      #Hfalse destruct (Hfalse)
+    ]
   ]  
 | #td #te * #c0 * #c1 * * #Hc0 #Hc1 #Hd #Hstar #IH #He 
-  lapply (IH He) -IH * #IH1 #IH2 %
+  lapply (IH He) -IH * * #IH1a #IH1b #IH2 % [ %
   [ #x #xs #rs #Hsrc_td #ls0 #x0 #target
     #rs0 #Hlen #Hdst_td
     >Hsrc_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
@@ -210,20 +226,55 @@ lapply (sem_while … (sem_parmove_step src dst sig n L Hneq Hsrc Hdst) … Hloo
         ]
       ]
     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
-      >(IH1 hd1 tl1 (c0::rs) ? ls0 hd2 tl2 (x0::rs0))
+      >(IH1a hd1 tl1 (c0::rs) ? ls0 hd2 tl2 (x0::rs0))
       [ >Hd >(change_vec_commute … ?? td ?? src dst) //
-       >change_vec_change_vec
-       >(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 //
-     | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
-     | >Hd >nth_change_vec_neq [|@sym_not_eq //]
-       >nth_change_vec // ]
-   ]
- | >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
- ] ]
+        >change_vec_change_vec
+        >(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 //
+      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
+      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
+        >nth_change_vec // ]
+    ]
+  | #x #xs #rs #Hdst_td #ls0 #x0 #target
+    #rs0 #Hlen #Hsrc_td
+    >Hdst_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
+    >Hsrc_td in Hd; >Hdst_td @(list_cases2 … Hlen)
+    [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2 
+      [2: %2 >Hd >nth_change_vec //]
+      >Hd -Hd @(eq_vec … (niltape ?))
+      #i #Hi cases (decidable_eq_nat i dst) #Hidst
+      [ >Hidst >(nth_change_vec_neq … dst src) //
+        >nth_change_vec // >nth_change_vec //
+      | cases (decidable_eq_nat i src) #Hisrc
+        [ >Hisrc >nth_change_vec // >(nth_change_vec_neq …) [|@sym_not_eq //]
+          >Hsrc_td in Hc1; >Htargetnil
+          normalize in ⊢ (%→?); #Hc1 destruct (Hc1) >nth_change_vec //
+          cases ls0 //
+        | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hidst)] % 
+        ]
+      ]
+    | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
+      >(IH1b hd1 tl1 (x::rs) ? ls0 hd2 tl2 (x0::rs0))
+      [ >Hd >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
+        >change_vec_change_vec
+        >(change_vec_commute … ?? td ?? src dst) //
+        >change_vec_change_vec
+        >reverse_cons >associative_append
+        >reverse_cons >associative_append
+        >change_vec_commute [|@sym_not_eq //] %
+      | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
+      | >Hd >nth_change_vec // ]
+    ]
+  ]
+| >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
+] ]
 qed.
  
 lemma terminate_parmoveL :  ∀src,dst,sig,n,t.
@@ -252,4 +303,125 @@ lemma sem_parmoveL : ∀src,dst,sig,n.
   parmove src dst sig n L ⊨ R_parmoveL src dst sig n.
 #src #dst #sig #n #Hneq #Hsrc #Hdst @WRealize_to_Realize 
 [/2/ | @wsem_parmoveL //]
-qed.
\ No newline at end of file
+qed.
+
+(* while {
+     if current != null 
+        then move_r
+        else nop
+     }
+ *)
+ 
+definition mte_states ≝ initN 3.
+definition mte0 : mte_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
+definition mte1 : mte_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
+definition mte2 : mte_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
+
+definition mte_step ≝ 
+  λalpha:FinSet.λD.mk_TM alpha mte_states
+  (λp.let 〈q,a〉 ≝ p in
+    match a with
+    [ None ⇒ 〈mte1,None ?,N〉
+    | Some a' ⇒ match (pi1 … q) with
+      [ O ⇒ 〈mte2,Some ? a',D〉
+      | S q ⇒ 〈mte2,None ?,N〉 ] ])
+  mte0 (λq.q == mte1 ∨ q == mte2).
+  
+definition R_mte_step_true ≝ λalpha,D,t1,t2.
+  ∃ls,c,rs.
+    t1 = midtape alpha ls c rs ∧ t2 = tape_move ? t1 D.
+
+definition R_mte_step_false ≝ λalpha.λt1,t2:tape alpha.
+  current ? t1 = None ? ∧ t1 = t2.
+
+lemma sem_mte_step :
+  ∀alpha,D.mte_step alpha D ⊨ [ mte2 : R_mte_step_true alpha D, R_mte_step_false alpha ] .
+#alpha #D #intape @(ex_intro ?? 2) cases intape
+[ @ex_intro
+  [| % [ % [ % | normalize #H destruct ] | #_ % // ] ]
+|#a #al @ex_intro
+  [| % [ % [ % | normalize #H destruct ] | #_ % // ] ]
+|#a #al @ex_intro
+  [| % [ % [ % | normalize #H destruct ] | #_ % // ] ]
+| #ls #c #rs
+  @ex_intro [| % [ % [ % | #_ %{ls} %{c} %{rs} % // ]
+                     | normalize in ⊢ (?(??%?)→?); * #H @False_ind /2/ ] ] ]
+qed.
+
+definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) mte2.
+
+definition R_move_to_end_r ≝ 
+  λsig,int,outt.
+  (current ? int = None ? → outt = int) ∧
+  ∀ls,c,rs.int = midtape sig ls c rs → outt = mk_tape ? (reverse ? rs@c::ls) (None ?) [ ].
+  
+lemma wsem_move_to_end_r : ∀sig. move_to_end sig R ⊫ R_move_to_end_r sig.
+#sig #ta #k #outc #Hloop
+lapply (sem_while … (sem_mte_step sig R) … Hloop) //
+-Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
+[ * #Hcurtb #Houtc % /2/ #ls #c #rs #Htb >Htb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
+| #tc #td * #ls * #c * #rs * #Htc >Htc cases rs
+  [ normalize in ⊢ (%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
+    lapply (IH Hfalse) -IH * #Htd1 #_ %
+    [ normalize in ⊢ (%→?); #H destruct (H)
+    | #ls0 #c0 #rs0 #H destruct (H) >Htd1 // ]
+  | #r0 #rs0 whd in ⊢ (???%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
+    lapply (IH Hfalse) -IH * #_ #IH %
+    [ normalize in ⊢ (%→?); #H destruct (H)
+    | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ]
+qed.
+
+lemma terminate_move_to_end_r :  ∀sig,t.move_to_end sig R ↓ t.
+#sig #t @(terminate_while … (sem_mte_step sig R …)) //
+cases t
+[ % #t1 * #ls * #c * #rs * #H destruct
+|2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct
+| #ls #c #rs lapply c -c lapply ls -ls elim rs
+  [ #ls #c % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct %
+    #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct
+  | #r0 #rs0 #IH #ls #c % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH
+  ]
+]
+qed.
+
+lemma sem_move_to_end_r : ∀sig. move_to_end sig R ⊨ R_move_to_end_r sig.
+#sig @WRealize_to_Realize //
+qed.
+
+definition R_move_to_end_l ≝ 
+  λsig,int,outt.
+  (current ? int = None ? → outt = int) ∧
+  ∀ls,c,rs.int = midtape sig ls c rs → outt = mk_tape ? [ ] (None ?) (reverse ? ls@c::rs).
+  
+lemma wsem_move_to_end_l : ∀sig. move_to_end sig L ⊫ R_move_to_end_l sig.
+#sig #ta #k #outc #Hloop
+lapply (sem_while … (sem_mte_step sig L) … Hloop) //
+-Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
+[ * #Hcurtb #Houtc % /2/ #ls #c #rs #Htb >Htb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
+| #tc #td * #ls * #c * #rs * #Htc >Htc cases ls
+  [ normalize in ⊢ (%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
+    lapply (IH Hfalse) -IH * #Htd1 #_ %
+    [ normalize in ⊢ (%→?); #H destruct (H)
+    | #ls0 #c0 #rs0 #H destruct (H) >Htd1 // ]
+  | #l0 #ls0 whd in ⊢ (???%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
+    lapply (IH Hfalse) -IH * #_ #IH %
+    [ normalize in ⊢ (%→?); #H destruct (H)
+    | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ]
+qed.
+
+lemma terminate_move_to_end_l :  ∀sig,t.move_to_end sig L ↓ t.
+#sig #t @(terminate_while … (sem_mte_step sig L …)) //
+cases t
+[ % #t1 * #ls * #c * #rs * #H destruct
+|2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct
+| #ls elim ls
+  [ #c #rs % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct %
+    #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct
+  | #l0 #ls0 #IH #c #rs % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH
+  ]
+]
+qed.
+
+lemma sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
+#sig @WRealize_to_Realize //
+qed.