From 00101d30f0bf914a26ed2ec61a1aa38598b05209 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Sun, 20 Jan 2013 12:31:17 +0000
Subject: [PATCH] semantics of unistep

---
 matita/matita/lib/turing/mono.ma              |  10 ++
 .../lib/turing/multi_universal/normalTM.ma    |  20 ++-
 .../lib/turing/multi_universal/tuples.ma      |  24 ++-
 .../lib/turing/multi_universal/unistep_aux.ma | 154 +++++++++++++++++-
 4 files changed, 197 insertions(+), 11 deletions(-)

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index bab3ab1ba..1508c6c9e 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -134,6 +134,16 @@ definition step ≝ λsig.λM:TM sig.λc:config sig (states sig M).
   let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
   mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
 
+(*
+lemma step_eq : ∀sig,M,c. 
+  let current_char ≝ current ? (ctape ?? c) in
+  let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
+  step sig M c = 
+    mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
+#sig #M #c  
+ whd in match (tape_move_mono sig ??);
+*)
+  
 (******************************** loop ****************************************)
 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
   match n with 
diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma
index 13ef8a66c..8e3af494a 100644
--- a/matita/matita/lib/turing/multi_universal/normalTM.ma
+++ b/matita/matita/lib/turing/multi_universal/normalTM.ma
@@ -80,16 +80,34 @@ record normalTM : Type[0] ≝
   nhalt : initN no_states → bool
 }.
 
+lemma decomp_target : ∀n.∀tg: trans_target n. 
+  ∃qout,cout,m. tg = 〈qout,cout,m〉.
+#n * * #q #c #m %{q} %{c} %{m} //
+qed.
+
 (* A normal machine is just a special case of Turing Machine. *)
 
+definition nstart_state ≝ λM.mk_Sig ?? 0 (pos_no_states M).
+
 definition normalTM_to_TM ≝ λM:normalTM.
   mk_TM FinBool (initN (no_states M)) 
-   (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
+   (ntrans M) (nstart_state M) (nhalt M).
 
 coercion normalTM_to_TM.
 
 definition nconfig ≝ λn. config FinBool (initN n).
 
+(* A normal machine has a non empty graph *)
+
+definition sample_input: ∀M.trans_source (no_states M).
+#M % [@(nstart_state M) | %]
+qed.
+
+lemma nTM_nog: ∀M. graph_enum ?? (ntrans M) ≠ [ ].
+#M % #H lapply(graph_enum_complete ?? (ntrans M) (sample_input M) ? (refl ??))
+>H normalize #Hd destruct
+qed.
+
 (******************************** tuples **************************************)
 
 (* By general results on FinSets we know that every function f between two 
diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
index 0fe4508ed..428d99ccf 100644
--- a/matita/matita/lib/turing/multi_universal/tuples.ma
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -21,8 +21,30 @@ lemma table_TM_cons: ∀n,h,t,o.
   table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h).
 // qed.
 
+lemma initial_bar: ∀n,h,l. l ≠ [ ] →
+  table_TM n l h = bar :: tail ? (table_TM n l h).
+#n #h * 
+  [* #H @False_ind @H // 
+  |#a #tl #_ >table_TM_cons lapply (is_tuple n h a) 
+   * #qin * #cin * #qout * #cout * #mv * #_ #Htup >Htup %
+  ]
+qed. 
+
 (************************** matching in a table *******************************)
-lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
+lemma list_to_table: ∀n,l,h,t. mem ? t l →
+  ∃ll,lr.table_TM n l h = ll@(tuple_encoding n h t)@lr.
+#n #l #h #t elim l 
+  [@False_ind
+  |#hd #tl #Hind *
+    [#Htup %{[]} %{(table_TM n tl h)} >Htup %
+    |#H cases (Hind H) #ll * #lr #H1
+     %{((tuple_encoding n h hd)@ll)} %{lr} 
+     >associative_append <H1 %
+    ]
+  ]
+qed.
+
+lemma list_to_table1: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
   ∃ll,lr.table_TM n l h = ll@tup@lr.
 #n #l #h #tup elim l 
   [@False_ind
diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
index 3c4d28284..9e240013b 100644
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -265,7 +265,11 @@ qed.
 definition char_to_move ≝ λc.match c with
   [ bit b ⇒ if b then R else L
   | _ ⇒ N].
-  
+
+definition char_to_bit_option ≝ λc.match c with
+  [ bit b ⇒ Some ? (bit b)
+  | _ ⇒ None ?]. 
+ 
 definition tape_move_obj : mTM FSUnialpha 2 ≝ 
   ifTM ?? 
    (inject_TM ? (test_char ? (λc:FSUnialpha.c == bit false)) 2 prg)
@@ -303,6 +307,11 @@ definition low_char' ≝ λc.
   | Some b ⇒ if (is_bit b) then b else null
   ].
   
+lemma low_char_option : ∀s.
+  low_char' (option_map FinBool FSUnialpha bit s) = low_char s.
+* //
+qed.
+
 definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
   ∀state,char,table.
   (* cfg *)
@@ -314,12 +323,16 @@ definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
   (* obj *)
   only_bits (list_of_tape ? (nth obj ? t1 (niltape ?))) →
   let conf ≝ (bar::state@[char]) in
-  (∃ll,lr.bar::table = ll@conf@lr) → 
+  (∃ll,lr.bar::table = ll@conf@lr) →
+(*
     ∃nstate,nchar,m,t. tuple_encoding n h t = (conf@nstate@[nchar;m]) ∧ 
-    mem ? t l ∧
+    mem ? t l ∧  *)
+    ∀nstate,nchar,m,t. 
+    tuple_encoding n h t = (conf@nstate@[nchar;m])→ 
+    mem ? t l →
     let new_obj ≝ 
      tape_move_mono ? (nth obj ? t1 (niltape ?)) 
-       〈Some ? nchar,char_to_move m〉 in
+       〈char_to_bit_option nchar,char_to_move m〉 in
     let next_char ≝ low_char' (current ? new_obj) in
     t2 = 
       change_vec ??
@@ -330,17 +343,140 @@ definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
   mk_tape B (map ?? f (left ? t)) 
     (option_map ?? f (current ? t)) 
     (map ?? f (right ? t)).
+    
+lemma map_list_of_tape: ∀A,B,f,t.
+  list_of_tape B (tape_map ?? f t) = map ?? f (list_of_tape A t).
+#A #B #f * // normalize // #ls #c #rs <map_append %
+qed.
+
+lemma low_char_current : ∀t.
+  low_char' (current FSUnialpha (tape_map FinBool FSUnialpha bit t))
+  = low_char (current FinBool t).
+* // qed.
 
 definition low_tapes ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
   [tape_map ?? bit (ctape ?? c);
-   midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
-   midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))
+   midtape ? [ ] bar 
+    ((bits_of_state ? (nhalt M) (cstate ?? c))@[low_char (current ? (ctape ?? c))]);
+   midtape ? [ ] bar (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M)))
   ].
+  
+lemma obj_low_tapes: ∀M,c.
+  nth obj ? (low_tapes M c) (niltape ?) = tape_map ?? bit (ctape ?? c).
+// qed.
+
+lemma cfg_low_tapes: ∀M,c.
+  nth cfg ? (low_tapes M c) (niltape ?) = 
+  midtape ? [ ] bar 
+    ((bits_of_state ? (nhalt M) (cstate ?? c))@[low_char (current ? (ctape ?? c))]).
+// qed.
+
+lemma prg_low_tapes: ∀M,c.
+  nth prg ? (low_tapes M c) (niltape ?) = 
+  midtape ? [ ] bar (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))).
+// qed.
+
+(* commutation lemma for write *)
+lemma map_write: ∀t,cout.
+ tape_write ? (tape_map FinBool ? bit t) (char_to_bit_option (low_char cout))
+  = tape_map ?? bit (tape_write ? t cout).
+#t * // #b whd in match (char_to_bit_option ?);
+whd in ⊢ (??%%); @eq_f3 [elim t // | // | elim t //]
+qed.
+
+(* commutation lemma for moves *)
+lemma map_move: ∀t,m.
+ tape_move ? (tape_map FinBool ? bit t) (char_to_move (low_mv m))
+  = tape_map ?? bit (tape_move ? t m).
+#t * // whd in match (char_to_move ?);
+  [cases t // * // | cases t // #ls #a * //]
+qed.
+  
+(* commutation lemma for actions *)
+lemma map_action: ∀t,cout,m.
+ tape_move ? (tape_write ? (tape_map FinBool ? bit t)
+    (char_to_bit_option (low_char cout))) (char_to_move (low_mv m)) 
+ = tape_map ?? bit (tape_move ? (tape_write ? t cout) m).
+#t #cout #m >map_write >map_move % 
+qed. 
+
+lemma map_move_mono: ∀t,cout,m.
+ tape_move_mono ? (tape_map FinBool ? bit t)
+  〈char_to_bit_option (low_char cout), char_to_move (low_mv m)〉
+ = tape_map ?? bit (tape_move_mono ? t 〈cout,m〉).
+@map_action
+qed. 
 
 definition R_unistep_high ≝ λM:normalTM.λc:nconfig (no_states M).λt1,t2.
   t1 = low_tapes M c → 
   t2 = low_tapes M (step ? M c). 
 
-  
-  
- 
\ No newline at end of file
+lemma R_unistep_equiv : ∀M,c,t1,t2. 
+  R_unistep (no_states M) (graph_enum ?? (ntrans M)) (nhalt M) t1 t2 →
+  R_unistep_high M c t1 t2.
+#M #c #t1 #t2 #H #Ht1
+lapply (initial_bar ? (nhalt M) (graph_enum ?? (ntrans M)) (nTM_nog ?)) #Htable
+(* tup = current tuple *)
+cut (∃t.t = 〈〈cstate … c,current ? (ctape … c)〉, 
+             ntrans M 〈cstate … c,current ? (ctape … c)〉〉) [% //] * #tup #Htup
+(* tup is in the graph *)
+cut (mem ? tup (graph_enum ?? (ntrans M)))
+  [@memb_to_mem >Htup @(graph_enum_complete … (ntrans M)) %] #Hingraph
+(* tupe target = 〈qout,cout,m〉 *)
+lapply (decomp_target ? (ntrans M 〈cstate … c,current ? (ctape … c)〉))
+* #qout * #cout * #m #Htg >Htg in Htup; #Htup
+(* new config *)
+cut (step FinBool M c = mk_config ?? qout (tape_move ? (tape_write ? (ctape … c) cout) m))
+  [>(config_expand … c) whd in ⊢ (??%?); (* >Htg ?? why not?? *)
+   cut (trans ? M 〈cstate  … c, current ? (ctape … c)〉 = 〈qout,cout,m〉) [<Htg %] #Heq1 
+   >Heq1 %] #Hstep
+(* new state *)
+cut (cstate ?? (step FinBool M c) = qout) [>Hstep %] #Hnew_state
+(* new tape *)
+cut (ctape ?? (step FinBool M c) = tape_move ? (tape_write ? (ctape … c) cout) m)
+  [>Hstep %] #Hnew_tape
+lapply(H (bits_of_state ? (nhalt M) (cstate ?? c)) 
+         (low_char (current ? (ctape ?? c)))
+         (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M)))
+         ??????)
+[<Htable
+ lapply(list_to_table … (nhalt M) …Hingraph) * #ll * #lr #Htable1 %{ll} 
+ %{(((bits_of_state ? (nhalt M) qout)@[low_char cout;low_mv m])@lr)} 
+ >Htable1 @eq_f <associative_append @eq_f2 // >Htup
+ whd in ⊢ (??%?); @eq_f >associative_append %
+|>Ht1 >obj_low_tapes >map_list_of_tape elim (list_of_tape ??) 
+  [#b @False_ind | #b #tl #Hind #a * [#Ha >Ha //| @Hind]]
+|@sym_eq @Htable
+|>Ht1 %
+|%{(bits_of_state ? (nhalt M) (cstate ?? c))} %{(low_char (current ? (ctape ?? c)))}
+ % [% [% [// | cases (current ??) normalize [|#b] % #Hd destruct (Hd)]
+      |>length_map whd in match (length ??); @eq_f //]
+   |//]
+|>Ht1 >cfg_low_tapes //] -H #H 
+lapply(H (bits_of_state … (nhalt M) qout) (low_char … cout) 
+         (low_mv … m) tup ? Hingraph)
+  [>Htup whd in ⊢ (??%?); @eq_f >associative_append %] -H
+#Ht2 >Ht2 @(eq_vec ? 3 … (niltape ?)) #i #Hi 
+cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+  [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+    [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+      [@False_ind /2/
+      |>Hi >obj_low_tapes >nth_change_vec //
+       >Ht1 >obj_low_tapes >Hstep @map_action 
+      ]
+    |>Hi >cfg_low_tapes >nth_change_vec_neq 
+      [|% whd in ⊢ (??%?→?);  #H destruct (H)]
+     >nth_change_vec // >Hnew_state @eq_f @eq_f >Hnew_tape 
+     @eq_f2 [|2:%] >Ht1 >obj_low_tapes >map_move_mono >low_char_current %
+    ]
+  |(* program tapes do not change *)
+   >Hi >prg_low_tapes 
+   >nth_change_vec_neq [|% whd in ⊢ (??%?→?);  #H destruct (H)]
+   >nth_change_vec_neq [|% whd in ⊢ (??%?→?);  #H destruct (H)]
+   >Ht1 >prg_low_tapes //
+  ]
+qed. 
+   
+
+    
+         
\ No newline at end of file
-- 
2.39.2