more porting to machines that can move without writing

diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma
index e00f3a36d5ba6000b3d4bdf0ecabc8900bbe0bf0..0e9ffe09050f189530c2755c29a91e7ad1684506 100644 (file)
--- a/matita/matita/lib/turing/inject.ma
+++ b/matita/matita/lib/turing/inject.ma
@@ -43,15 +43,18 @@ lemma inject_trans_def :∀sig:FinSet.∀n,i:nat.i < S n →
 whd in ⊢ (??%?); >nth_change_vec // >Htrans //
 qed.
 
+lemma inj_ter: ∀A,B,C.∀p:A×B×C. 
+  p = 〈\fst (\fst p), \snd (\fst p), \snd p〉.
+// qed.
 
-axiom inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
+lemma inject_step : ∀sig,n,M,i,q,t,nq,nt,v. i < S n →
   step sig M (mk_config ?? q t) = mk_config ?? nq nt → 
-  cic:/matita/turing/turing/step.def(11) sig n (inject_TM sig M n i) 
+  cic:/matita/turing/turing/step.def(12) sig n (inject_TM sig M n i) 
     (mk_mconfig ?? n q (change_vec ? (S n) v t i)) 
   = mk_mconfig ?? n nq (change_vec ? (S n) v nt i).
-(*#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
+#sig #n #M #i #q #t #nq #nt #v #lein whd in ⊢ (??%?→?);
 whd in match (step ????); >(current_chars_change_vec … lein)
->(eq_pair_fst_snd … (trans sig M ?)) whd in ⊢ (??%?→?); #H
+>(inj_ter … (trans sig M ?)) whd in ⊢ (??%?→?); #H
 >(inject_trans_def sig n i lein M …) 
 [|>(eq_pair_fst_snd ?? (trans sig M 〈q,current sig t〉))
   >(eq_pair_fst_snd ?? (\fst (trans sig M 〈q,current sig t〉))) %
@@ -59,11 +62,11 @@ whd in match (step ????); >(current_chars_change_vec … lein)
 whd in ⊢ (??%?); @eq_f2 [destruct (H) // ]
 @(eq_vec … (niltape ?)) #i0 #lei0n
 cases (decidable_eq_nat … i i0) #Hii0
-[ >Hii0 >nth_change_vec // >pmap_change >nth_change_vec // destruct (H) //
-| >nth_change_vec_neq // >pmap_change >nth_change_vec_neq 
-  >tape_move_null_action //
+[ >Hii0 >nth_change_vec // >tape_move_multi_def >pmap_change >nth_change_vec // destruct (H) //
+| >nth_change_vec_neq // >tape_move_multi_def  >pmap_change >nth_change_vec_neq //
+  <tape_move_multi_def >tape_move_null_action //
 ]
-qed. *)
+qed. 
 
 lemma halt_inject: ∀sig,n,M,i,x.
   cic:/matita/turing/turing/halt.fix(0,2,9) sig n (inject_TM sig M n i) x
@@ -76,7 +79,7 @@ qed.
 
 lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n → 
  loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) → 
- cic:/matita/turing/turing/loopM.def(12) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
+ cic:/matita/turing/turing/loopM.def(13) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
   =Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)).
 #sig #n #M #i #k elim k -k
   [#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct

diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma
index 9309156862befaa1c13832198f86fdfa1f59e49b..688c886387da82c9292a9158def133d06f962bfb 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/compare.ma
+++ b/matita/matita/lib/turing/multi_universal/compare.ma
@@ -119,7 +119,7 @@ cases (nth i ?? (None ?)) in ⊢ (???%→?);
 ]
 qed.
 
-axiom comp_q0_q1 :
+lemma comp_q0_q1 :
   ∀i,j,sig,n,v,a.i ≠ j → i < S n → j < S n → 
   nth i ? (current_chars ?? v) (None ?) = Some ? a →
   nth j ? (current_chars ?? v) (None ?) = Some ? a → 
@@ -129,7 +129,6 @@ axiom comp_q0_q1 :
        (change_vec ?? v
          (tape_move_right ? (nth i ? v (niltape ?))) i)
        (tape_move_right ? (nth j ? v (niltape ?))) j).
-(*
 #i #j #sig #n #v #a #Heq #Hi #Hj #Ha1 #Ha2
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
 [ whd in match (trans ????);
@@ -139,11 +138,12 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
   change with (change_vec ?????) in ⊢ (??(????%)?);
   <(change_vec_same … v j (niltape ?)) in ⊢ (??%?);
   <(change_vec_same … v i (niltape ?)) in ⊢ (??%?);
-  >pmap_change >pmap_change >tape_move_null_action
-  @eq_f2 // @eq_f2 // >nth_change_vec_neq //
+  >tape_move_multi_def 
+  >pmap_change >pmap_change <tape_move_multi_def
+  >tape_move_null_action
+  @eq_f2 // >nth_change_vec_neq //
 ]
 qed.
-*)
 
 lemma sem_comp_step :
   ∀i,j,sig,n.i ≠ j → i < S n → j < S n → 

diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma
index 6e5dad0525594cdb215cae36289afc210e6dd882..ed4142fa327eeda0f8c9f9bce81a5303df955cf0 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/match.ma
+++ b/matita/matita/lib/turing/multi_universal/match.ma
@@ -75,8 +75,42 @@ 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 mmove_states ≝ initN 2.
+
+definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_mmove ≝ 
+ λi,sig,n,D.
+ λp:mmove_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
+ | S _ ⇒ 〈mmove1,null_action sig n〉 ].
+
+definition mmove ≝ 
+  λi,sig,n,D.
+  mk_mTM sig n mmove_states (trans_mmove i sig n D) 
+    mmove0 (λq.q == mmove1).
+    
+definition Rm_multi ≝ 
+  λalpha,n,i,D.λt1,t2:Vector ? (S n).
+  t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
+   
+lemma sem_move_multi :
+  ∀alpha,n,i,D.i ≤ n → 
+  mmove i alpha n D ⊨ Rm_multi alpha n i D.
+#alpha #n #i #D #Hin #int %{2}
+%{(mk_mconfig ? mmove_states n mmove1 ?)} 
+[| %
+ [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f %
+ | whd >tape_move_multi_def
+   <(change_vec_same … (ctapes …) i (niltape ?))
+   >pmap_change <tape_move_multi_def >tape_move_null_action % ] ]
+ qed.
   
-definition rewind ≝ λsrc,dst,sig,n.parmove src dst sig n L · parmove_step src dst sig n R.
+definition rewind ≝ λsrc,dst,sig,n.
+  parmove src dst sig n L · mmove src sig n R · mmove dst sig n R.
 
 definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
   (∀x,x0,xs,rs.
@@ -101,14 +135,14 @@ 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
-check acc_sem_seq_app
-@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst)
-  (accRealize_to_Realize … (sem_parmove_step src dst sig n R Hneq Hsrc Hdst)))
-#ta #tb * #tc * * #HR1 #_ #HR2
+@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) ?)
+[| @(sem_seq_app sig n ????? (sem_move_r_multi …) (sem_move_r_multi …)) //
+ @le_S_S_to_le // ]
+#ta #tb * #tc * * #Htc #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb
 #x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst
->(HR1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in HR2;
+>(Htc ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in Htd;
 [|>Hmidta_dst //
-|>length_append >length_append >Hlen % ] *
+|>length_append >length_append >Hlen % ] * #_
 [ whd in ⊢ (%→?); * #x1 * #x2 * *
   >change_vec_commute in ⊢ (%→?); // >nth_change_vec //
   cases (reverse sig (xs@[x0])@x::rs)

diff --git a/matita/matita/lib/turing/multi_universal/moves.ma b/matita/matita/lib/turing/multi_universal/moves.ma
index ca15620c271806223b7798030162c8098b36e2b1..df620b3520d63f5076a24be061661e7717201fe6 100644 (file)
--- 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 ? (tape_write ? (nth src ? int (niltape ?)) (Some ? x1)) D) src)
-            (tape_move ? (tape_write ? (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).
@@ -120,7 +120,7 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
   whd in ⊢ (??(????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
 qed.
 
-axiom parmove_q0_q1 :
+lemma parmove_q0_q1 :
   ∀src,dst,sig,n,D,is_sep,v.src ≠ dst → src < S n → dst < S n → 
   ∀a1,a2.
   nth src ? (current_chars ?? v) (None ?) = Some ? a1 →
@@ -131,9 +131,8 @@ axiom parmove_q0_q1 :
     mk_mconfig ??? parmove1 
      (change_vec ? (S n) 
        (change_vec ?? v
-         (tape_move ? (tape_write ? (nth src ? v (niltape ?)) (Some ? a1)) D) src)
-       (tape_move ? (tape_write ? (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
@@ -141,13 +140,13 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
   >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
 | whd in match (trans ????);
   >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?);
-  change with (pmap_vec ???????) in ⊢ (??%?);
-  whd in match (vec_map ?????);
-  >pmap_change >pmap_change >tape_move_null_action
+  <(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.
-*)
 
 lemma sem_parmove_step :
   ∀src,dst,sig,n,D,is_sep.src ≠ dst → src < S n → dst < S n → 
@@ -234,15 +233,9 @@ lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) 
       #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) %
+        [ >Hidst >nth_change_vec // 
         | >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)] % 
         ]
       ]
@@ -254,8 +247,7 @@ lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) 
        >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 //]

diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma
index 2455ec582a03ddffef40478de3622313bc5258a6..072d3a15a4b2f3fbd89d58f3a94d163f4a2b296f 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/moves_2.ma
+++ b/matita/matita/lib/turing/multi_universal/moves_2.ma
@@ -100,7 +100,7 @@ whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
   whd in ⊢ (??(????(???%))?); >Hcurdst @tape_move_null_action ]
 qed.
 
-axiom parmove_q0_q1 :
+lemma parmove_q0_q1 :
   ∀src,dst,sig,n,D,v.src ≠ dst → src < S n → dst < S n → 
   ∀a1,a2.
   nth src ? (current_chars ?? v) (None ?) = Some ? a1 →
@@ -112,21 +112,19 @@ axiom parmove_q0_q1 :
        (change_vec ?? v
          (tape_move ? (nth src ? v (niltape ?)) D) src)
        (tape_move ? (nth dst ? v (niltape ?)) D) dst).
-(*
-#src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
-#a1 #a2 #Hcursrc #Hcurdst #Hsep
+#src #dst #sig #n #D #v #Hneq #Hsrc #Hdst
+#a1 #a2 #Hcursrc #Hcurdst
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
 [ whd in match (trans ????);
-  >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
+  >Hcursrc >Hcurdst %
 | whd in match (trans ????);
-  >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); >Hsep whd in ⊢ (??(????(???%))?);
-  change with (pmap_vec ???????) in ⊢ (??%?);
-  whd in match (vec_map ?????);
-  >pmap_change >pmap_change >tape_move_null_action
-  @eq_f2 // @eq_f2 // >nth_change_vec_neq //
+  >Hcursrc >Hcurdst whd in ⊢ (??(????(???%))?); 
+  >tape_move_multi_def <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?);
+  >pmap_change <(change_vec_same ?? v src (niltape ?)) in ⊢(??%?);
+  >pmap_change <tape_move_multi_def >tape_move_null_action
+  @eq_f2 // >nth_change_vec_neq //
 ]
 qed.
-*)
 
 lemma sem_parmove_step :
   ∀src,dst,sig,n,D.src ≠ dst → src < S n → dst < S n → 

diff --git a/matita/matita/lib/turing/multi_universal/par_test.ma b/matita/matita/lib/turing/multi_universal/par_test.ma
index 615efdc2e9dd2de576922a0233fc776dd8331a43..1ab0e34a4572e4eb9980db3dfec342cecc52386a 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/par_test.ma
+++ b/matita/matita/lib/turing/multi_universal/par_test.ma
@@ -39,31 +39,29 @@ definition R_partest_false ≝
   λsig,n,test.λint,outt: Vector (tape sig) (S n).
   test (current_chars ?? int) = false ∧ outt = int.
 
-axiom partest_q0_q1:
+lemma partest_q0_q1:
   ∀sig,n,test,v.
   test (current_chars ?? v) = true → 
   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
     = mk_mconfig ??? partest1 v.
-(*#sig #n #test #v #Htest
+#sig #n #test #v #Htest
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Htest %
-| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
-qed.*)
+| whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
+qed.
 
-axiom partest_q0_q2:
+lemma partest_q0_q2:
   ∀sig,n,test,v.
   test (current_chars ?? v) = false → 
   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
     = mk_mconfig ??? partest2 v.
-(*
 #sig #n #test #v #Htest
 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 @eq_f2
 [ whd in ⊢ (??(???%)?); >Htest %
-| whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
+| whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
 qed.
-*)
 
 lemma sem_partest:
   ∀sig,n,test.
@@ -80,5 +78,4 @@ cases (true_or_false (test (current_chars ?? int))) #Htest
       | whd in ⊢ (??%%→?); #H destruct (H)]
   | #_ % //]
 ]
-qed.
-     
\ No newline at end of file
+qed.
\ No newline at end of file

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index 7e9c708d0bda3a345b39122a191446a54a0704f5..4cf3ebaf17a99ed3fe6e0d0333e1db2456794bbe 100644 (file)
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -31,12 +31,14 @@ qed.
 
 definition current_chars ≝ λsig.λn.λtapes.
   vec_map ?? (current sig) (S n) tapes.
-
+  
 definition tape_move_multi ≝ 
   λsig,n,ts,mvs.
-  pmap_vec ??? (tape_move sig) ? 
-    (pmap_vec ??? (tape_write sig) n ts (vec_map ?? (λx.\fst x) ? mvs))
-        (vec_map ?? (λx.\snd x) ? mvs).
+  pmap_vec ??? (tape_move_mono sig) n ts mvs.
+  
+lemma tape_move_multi_def : ∀sig,n,ts,mvs.
+  tape_move_multi sig n ts mvs = pmap_vec ??? (tape_move_mono sig) n ts mvs.
+// qed.
 
 definition step ≝ λsig.λn.λM:mTM sig n.λc:mconfig sig (states ?? M) n.
   let 〈news,mvs〉 ≝ trans sig n M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in