progress in the semantics of binary machines

diff --git a/matita/matita/lib/turing/multi_universal/binaryTM.ma b/matita/matita/lib/turing/multi_universal/binaryTM.ma
index 34c9ae4b8f7e2ec38b95ccb55f2bf9043f3a5937..b430afa4e60bd0c6f217bfd84af1f281bc666acd 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/binaryTM.ma
+++ b/matita/matita/lib/turing/multi_universal/binaryTM.ma
@@ -60,15 +60,14 @@ definition trans_binaryTM : ∀sig,states:FinSet.
   let (H2 : FS_crd sig < S (2*FS_crd sig)) ≝ ? in
   match pi1 … phase with
   [ O ⇒ (*** PHASE 0: read ***)
-      match a with
-      [ Some a0 ⇒ 
-        match pi1 … count with
-        [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
-        | S k ⇒ if (a0 == true) 
-                then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
-                else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉 ]
-      | None ⇒ (* Overflow position! *)
-          〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ]
+      match pi1 … count with
+      [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
+      | S k ⇒ match a with
+        [ Some a0 ⇒ if (a0 == true) 
+                    then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
+                    else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉 
+        | None ⇒ (* Overflow position! *)
+          〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ] ]
   | S phase ⇒ match phase with
   [ O ⇒ (*** PHASE 1: restart ***)
       match pi1 … count with
@@ -131,13 +130,15 @@ definition mk_binaryTM ≝
     (trans_binaryTM sig (states sig M) (trans sig M)) 
     (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).// qed.
 
+definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
+
 definition bin_current ≝ λsig,t.match current ? t with
-[ None ⇒ [ ] | Some c ⇒ unary_of_nat (FS_crd sig) (index_of_FS sig c) ].
+[ None ⇒ [ ] | Some c ⇒ bin_char sig c ].
 
 definition tape_bin_lift ≝ λsig,t.
-let ls' ≝ flatten ? (map ?? (unary_of_nat (FS_crd sig) ∘ (index_of_FS sig)) (left ? t)) in
+let ls' ≝ flatten ? (map ?? (bin_char sig) (left ? t)) in
 let c' ≝ option_hd ? (bin_current sig t) in
-let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (unary_of_nat (FS_crd sig) ∘ (index_of_FS sig)) (right ? t)) in
+let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (bin_char sig) (right ? t)) in
  mk_tape ? ls' c' rs'.
 
 definition R_bin_lift ≝ λsig,R,t1,t2.
@@ -148,6 +149,96 @@ definition state_bin_lift :
   ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M)
  ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉.// qed.
 
+lemma lift_halt_binaryTM : 
+  ∀sig,M,q.halt sig M q = halt ? (mk_binaryTM sig M) (state_bin_lift ? M q).
+// qed.
+
+lemma binaryTM_bin0_bin1 :
+  ∀sig,M,t,q,ch.
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,O〉) t) 
+  = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. //
+qed.
+
+lemma binaryTM_bin0_bin4 :
+  ∀sig,M,t,q,ch,k.
+  current ? t = None ? → S k <S (2*FS_crd sig) → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
+  = mk_config ?? (〈q,bin4,None ?,to_initN 0 ??〉) (tape_move ? t R). [2,3://]
+#sig #M #t #q #ch #k #Hcur #Hk
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+lemma binaryTM_bin0_true :
+  ∀sig,M,t,q,ch,k.
+  current ? t = Some ? true → S k <S (2*FS_crd sig) → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
+  = mk_config ?? (〈q,bin0,FS_nth sig k,to_initN k ??〉) (tape_move ? t R).[2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #Hcur #Hk
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+lemma binaryTM_bin0_false :
+  ∀sig,M,t,q,ch,k.
+  current ? t = Some ? false → S k <S (2*FS_crd sig) → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
+  = mk_config ?? (〈q,bin0,ch,to_initN k ??〉) (tape_move ? t R).[2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #Hcur #Hk
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+(* to be checked *)
+axiom binary_to_bin_char :∀sig,csl,csr,a.
+  csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
+
+lemma binaryTM_phase1_midtape_aux :
+  ∀sig,M,q,ls,a,rs,k.
+  halt sig M q=false → 
+  ∀csr,csl,t,ch.length ? csr < S (2*FS_crd sig) → 
+  t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) → 
+  csl@csr = bin_char sig a → 
+  loopM ? (mk_binaryTM sig M) (S (length ? csr) + k)
+    (mk_config ?? (〈q,bin0,ch,length ? csr〉) t) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉) 
+        (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
+#sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
+[ #csl #t #ch #Hlen #Ht >append_nil #Hcsl >loopM_unfold >loop_S_false [|normalize //]
+  <loopM_unfold @eq_f >binaryTM_bin0_bin1 @eq_f >Ht 
+  whd in match (step ???); whd in match (trans ???); <Hcsl %
+| #c cases c
+  [ #csr0 #IH #csl #t #ch #Hlen #Ht #Heq >loopM_unfold >loop_S_false [|normalize //]
+    <loopM_unfold lapply (binary_to_bin_char … Heq) #Ha >binaryTM_bin0_true 
+    [| >Ht % ]
+    lapply (IH (csl@[true]) (tape_move FinBool t R) ????)
+    [ //
+    | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
+      cases csr0
+      [ cases rs
+        [ normalize >rev_append_def >rev_append_def >reverse_append %
+        | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
+      | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
+    | /2/
+    | @(Some ? a) ]
+    #H whd in match (plus ??); >Ha >H @eq_f @eq_f2 //
+    
+qed.
+
+
+lemma binaryTM_phase1_midtape :
+  ∀sig,M,t,q,ls,a,rs,ch.
+  t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a@rs)) →
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,FS_crd sig〉) t) 
+  = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) 
+      (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs)). [2,3://]
+#sig #M #t #q #ls #a #rs #ch #Ht
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+
 lemma binaryTM_loop :
  ∀sig,M,i,t,q,tf,qf.
  loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
@@ -157,6 +248,17 @@ lemma binaryTM_loop :
 #sig #M #i elim i
 [ #t #q #qf #tf change with (None ?) in ⊢ (??%?→?); #H destruct (H)
 | -i #i #IH #t #q #tf #qf
+  >loopM_unfold 
+  lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t))))
+  cases (halt ?? q) in ⊢ (???%→?); #Hhalt
+  [ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
+    #H destruct (H) %{1} >loopM_unfold >loop_S_true // ]
+  (* interesting case: more than one step *)
+  >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
+  <loopM_unfold >(config_expand ?? (step ???)) #Hloop 
+  lapply (IH … Hloop) -IH * #k0 #IH <config_expand in Hloop; #Hloop
+  %{(S k0)}
+  
 
 
 (*