From aa900a8d853f1040716bb050e38406463de08271 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 24 Oct 2013 10:54:17 +0000
Subject: [PATCH] step (almost) done

---
 .../lib/turing/multi_to_mono/exec_moves.ma    | 93 +++----------------
 .../turing/multi_to_mono/exec_trace_move.ma   | 80 ++++++++++++++--
 .../matita/lib/turing/multi_to_mono/step.ma   | 56 +++++++----
 3 files changed, 126 insertions(+), 103 deletions(-)

diff --git a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
index dae4aa6af..9f6cb718b 100644
--- a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
+++ b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
@@ -2,75 +2,6 @@
 
 include "turing/multi_to_mono/exec_trace_move.ma".
 (* include "turing/turing.ma". *)
-
-(**************************** Vector Operations *******************************)
-
-let rec resize A (l:list A) i d on i ≝
-  match i with 
-  [ O ⇒ [ ]
-  | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
-  ].
-
-lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
-#A #l #i lapply l -l elim i 
-  [#l #d % 
-  |#m #Hind #l cases l 
-    [#d normalize @eq_f @Hind
-    |#a #tl #d normalize @eq_f @Hind
-    ]
-  ]
-qed.
-
-lemma resize_id : ∀A,n,l,d. |l| = n → 
-  resize A l n d = l.
-#A #n elim n 
-  [#l #d #H >(lenght_to_nil … H) //
-  |#m #Hind * #d normalize 
-    [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
-  ]
-qed.
-
-definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
-#A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
-qed.
-
-axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
-  nth i ? (resize_vec A n v j d) d = nth i ? v d.
-  
-lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d. 
-  resize_vec A n v n d = v.
-#A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
-qed.
-
-definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
-  mk_Vector A 1 [a] (refl ??).
-  
-definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
-#A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
->length_append >(len A n v) //
-qed.
-
-lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
-  a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
-// qed.
-
-axiom nth_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. 
-  nth n ? (vec_cons_right A a n v) d = a.
-(*
-#A #a #n elim n 
-  [#v #d >(vector_nil … v) //
-  |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);    
-   whd in match (vec_cons_right ????);  
-*)
-
-lemma get_moves_cons_right: ∀Q,sig,n,q,moves,a.
-  get_moves Q sig (S n)
-    (vec_cons_right ? (Some ? (inl ?? 〈q,moves〉)) (S n) a) = moves.
-#Q #sig #n #q #moves #a whd in ⊢(??%?); >nth_cons_right //
-qed.
-    
-axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. 
-  resize_vec ? (S n) (vec_cons_right A a n v) n d = v.
   
 let rec exec_moves Q sig n i on i : TM (MTA (HC Q n) sig (S n)) ≝
   match i with 
@@ -131,15 +62,18 @@ definition R_exec_moves ≝ λQ,sig,n,i,t1,t2.
   ∃ls1,a1,rs1. 
    t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
    (∀i.regular_trace (TA (HC Q n) sig) (S n) a1 ls1 rs1 i) ∧
-   readback ? (S n) ls1 (vec … a1) rs1 i = 
-     tape_moves ?? (readback ? (S n) ls (vec … a) rs i) (vec_moves Q sig n a i) ∧
-   (∀j. i ≤ j → j ≤ n →  
+   (∀j. j < i → j ≤ n →
+    rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
+     tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs j) (get_move Q sig n a j)) ∧
+    (* tape_moves ?? (readback ? (S n) ls (vec … a) rs i) (vec_moves Q sig n a i) ∧ *)
+   (∀j. i ≤ j → j ≤ n → 
     rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = 
       rb_trace_i ? (S n) ls (vec … a) rs j).
      
 (* alias id "Realize_to_Realize" = 
   "cic:/matita/turing/mono/Realize_to_Realize.def(13)". *)
 
+(*
 lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j →
  nth i ? (readback sig n ls a rs j) (niltape ?) = 
    rb_trace_i sig n ls a rs (j - S i).
@@ -150,14 +84,14 @@ lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j →
     |#m #Hmj >minus_S_S @Hind @le_S_S_to_le //
     ]
   ]
-qed.
+qed. *)
 
 lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n → 
   exec_moves Q sig n i ⊨ R_exec_moves Q sig n i.
 #Q #sig #n #i elim i 
   [#_ @(Realize_to_Realize … (sem_nop …))
    #t1 #t2 #H #a #ls #rs #Ht1 #Hreg #H1 #H2 #H3 
-   %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| %]|//]
+   %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| #j #ltjO @False_ind /2/]|//]
   |#j #Hind #lttj lapply (lt_to_le … lttj) #ltj
    @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind
    #int #outt * #t1 * #H1 #H2
@@ -173,13 +107,10 @@ lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n →
    cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i)
      [@daemon] #aa1
    %[%[%[@Houtt|@Hregout]
-      |whd in ⊢ (??%?); @Vector_eq >(vec_moves_cons … lttj)
-       >tape_moves_def >pmap_vec_cons @eq_f2
-        [<H10 [>aa1 @Hrboutt |@ltj |@le_n]
-        |<tape_moves_def <H9 (* mitico *) @eq_f 
-         @(eq_vec … (niltape ?)) #i #ltij 
-         >(nth_readback … ltij) >(nth_readback … ltij) @Hrbid 
-          [@(transitive_le … ltj) // |@lt_to_not_eq @lt_plus_to_minus //]
+      |#k #ltk cases (le_to_or_lt_eq … ltk) #Hk #lekn
+        [>(Hrbid … lekn) [2:@lt_to_not_eq @le_S_S_to_le @Hk]
+         @(H9 k ? lekn) @le_S_S_to_le @Hk
+        |destruct (Hk) <H10 // @Hrboutt
         ]
       ]
     |#a #Hja #Han >(Hrbid … Han) 
diff --git a/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma b/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma
index 0fdfa86b8..4c4ee013d 100644
--- a/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma
+++ b/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma
@@ -117,7 +117,71 @@ definition move_R_i ≝ λA,sig,n,i.
 definition Rmove_R_i ≝ λA,sig,n,i. 
   R_guarded_M ? (S n) i (Rmtil A sig n i).
 
+(**************************** Vector Operations *******************************)
 
+let rec resize A (l:list A) i d on i ≝
+  match i with 
+  [ O ⇒ [ ]
+  | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
+  ].
+
+lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
+#A #l #i lapply l -l elim i 
+  [#l #d % 
+  |#m #Hind #l cases l 
+    [#d normalize @eq_f @Hind
+    |#a #tl #d normalize @eq_f @Hind
+    ]
+  ]
+qed.
+
+lemma resize_id : ∀A,n,l,d. |l| = n → 
+  resize A l n d = l.
+#A #n elim n 
+  [#l #d #H >(lenght_to_nil … H) //
+  |#m #Hind * #d normalize 
+    [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
+  ]
+qed.
+
+definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
+#A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
+qed.
+
+axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
+  nth i ? (resize_vec A n v j d) d = nth i ? v d.
+  
+lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d. 
+  resize_vec A n v n d = v.
+#A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
+qed.
+
+definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
+  mk_Vector A 1 [a] (refl ??).
+  
+definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
+#A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
+>length_append >(len A n v) //
+qed.
+
+lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
+  a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
+// qed.
+
+axiom nth_cons_right_n: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. 
+  nth n ? (vec_cons_right A a n v) d = a.
+  
+axiom nth_cons_right_lt: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.∀i. i < n →
+  nth i ? (vec_cons_right A a n v) d = nth i ? v d.
+(*
+#A #a #n elim n 
+  [#v #d >(vector_nil … v) //
+  |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);    
+   whd in match (vec_cons_right ????);  
+*)
+    
+axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. 
+  resize_vec ? (S n) (vec_cons_right A a n v) n d = v.
 (*************************** readback of the tape *****************************)
 
 definition opt_cur ≝ λsig,a. 
@@ -139,12 +203,10 @@ lemma rb_trace_i_def: ∀sig,n,ls,a,rs,i.
     rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs).
 // qed.
 
-let rec readback sig n ls a rs i on i : Vector (tape (sig_ext sig)) i ≝
-  match i with 
-  [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
-  | S j ⇒ vec_cons ? (rb_trace_i sig n ls a rs j) j (readback sig n ls a rs j)
-  ].
-
+(*
+definition readback :∀sig,n,ls,a,rs,i.Vector (tape (sig_ext sig)) i ≝
+vec_map (rb_trace_i *)
+ 
 lemma orb_false_l: ∀b1,b2:bool. 
   (b1 ∨ b2) = false → (b1 = false) ∧ (b2 = false).
 * * normalize /2/ qed.
@@ -316,6 +378,12 @@ definition get_moves ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).
     
 definition get_move ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λi.
   nth i ? (vec … (get_moves Q sig n a)) N.
+  
+lemma get_moves_cons_right: ∀Q,sig,n,q,moves,a.
+  get_moves Q sig (S n)
+    (vec_cons_right ? (Some ? (inl ?? 〈q,moves〉)) (S n) a) = moves.
+#Q #sig #n #q #moves #a whd in ⊢(??%?); >nth_cons_right_n //
+qed.
 
 definition exec_move_i ≝ λQ,sig,n,i.
     (ifTM ? (test_char ? (λa. (get_move Q sig n a i == R)))
diff --git a/matita/matita/lib/turing/multi_to_mono/step.ma b/matita/matita/lib/turing/multi_to_mono/step.ma
index 2defb7c40..fb133e747 100644
--- a/matita/matita/lib/turing/multi_to_mono/step.ma
+++ b/matita/matita/lib/turing/multi_to_mono/step.ma
@@ -113,9 +113,25 @@ definition to_sig_tape ≝ λQ,sig,t.
     | Some x ⇒ midtape ? (to_sig_map Q sig ls) x (to_sig_map Q sig rs) ]
   ].
 
-definition rb_tapes ≝ λQ,sig,n,ls.λa:MTA Q sig (S n).λrs.
-  vec_map ?? (to_sig_tape ??) n (readback ? (S n) ls (vec … a) rs n).
-
+let rec rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs i on i ≝
+  match i with 
+  [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
+  | S j ⇒ vec_cons_right ? (to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs j)) j
+           (rb_tapes Q sig n ls a rs j)].
+ 
+lemma nth_rb_tapes : ∀Q,sig,n,ls.∀a:MTA Q sig (S n).∀rs,j,i. i < j →
+  nth i ? (rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs j) (niltape ?) =
+    to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs i).
+#Q #sig #n #ls #a #rs #j elim j
+  [#i #H @False_ind /2/
+  |#k #Hind #i #lti cases (le_to_or_lt_eq … (le_S_S_to_le … lti))
+    [#Hlt >nth_cons_right_lt [@Hind //|//]
+    |#Heq >Heq @nth_cons_right_n
+    ]
+  ]
+qed.
+  
+ 
 (* q0 is a default value *)
 definition get_state ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λq0.
   match nth n ? (vec … a) (blank ?) with 
@@ -139,7 +155,7 @@ definition readback_config ≝
   λQ,sig,n,q0,ls.λa:MTA (HC Q (S n)) sig (S (S n)).λrs.
   mk_mconfig sig Q n 
     (get_state Q sig (S n) a q0)
-    (rb_tapes (HC Q (S n)) sig (S n) ls a rs).
+    (rb_tapes (HC Q (S n)) sig (S n) ls a rs (S n)).
 
 lemma state_readback : ∀Q,sig,n,q0,ls,a,rs.
   cstate … (readback_config Q sig n q0 ls a rs) =
@@ -148,7 +164,7 @@ lemma state_readback : ∀Q,sig,n,q0,ls,a,rs.
 
 lemma tapes_readback : ∀Q,sig,n,q0,ls,a,rs.
   ctapes … (readback_config Q sig n q0 ls a rs) =
-    rb_tapes (HC Q (S n)) sig (S n) ls a rs.
+    rb_tapes (HC Q (S n)) sig (S n) ls a rs (S n).
 // qed.
     
 definition R_stepM ≝ λsig.λn.λM:mTM sig n.λt1,t2.
@@ -241,7 +257,11 @@ axiom to_sig_write : ∀Q,sig,n,t,c.
   (tape_write ? t (to_sig_conv ??? c))
    = tape_write sig (to_sig_tape ?? t) c.
 
+definition opt ≝ λA.λoc1: option A.λc2.
+  match oc1 with [None ⇒ c2 | Some c1 ⇒ c1].
+
 axiom rb_write: ∀sig,n,ls,a,rs,i,c1,c2.
+  nth i ? c1 (None ?) = opt ? c2 (nth i ? c1 (None ?)) → 
   rb_trace_i ? n ls c1 rs i =
   tape_write ? (rb_trace_i sig n ls a rs i) c2.
    
@@ -265,7 +285,7 @@ lapply (transf_eq … HaSn (refl ??) (refl ??) (eq_pair_fst_snd …) (refl ??) (
 *)
 lapply (Hmoves … Ht1 ?? H3 H4)
   [>(transf_eq … HaSn (refl ??) (refl ??) (eq_pair_fst_snd …) (refl ??) (refl ??))
-   >nth_cons_right %
+   >nth_cons_right_n %
   | (* regularity is preserved *) @daemon
   |* #ls1 * #a1 * #rs1 * * * #Htout #Hreg #Hrb #HtrSn
    lapply (HtrSn (S n) (le_n ?) (le_n ?)) -HtrSn #HtrSn
@@ -282,26 +302,30 @@ lapply (Hmoves … Ht1 ?? H3 H4)
       [(* state *) >state_readback whd in match (step ????);
        >(cstate_rb … HaSn) >eq_current_chars_resize >get_chars_def
        <Hc1 <Hc2 >Htrans whd in ⊢ (???%);
-       whd in ⊢ (??%?); >Ha1 >HaSn >Htransf >nth_cons_right %
+       whd in ⊢ (??%?); >Ha1 >HaSn >Htransf >nth_cons_right_n %
       |>tapes_readback whd in match (step ????);
        >(cstate_rb … HaSn) >eq_current_chars_resize >get_chars_def
        <Hc1 <Hc2 >Htrans >ctapes_mk_config 
        @(eq_vec … (niltape ?)) #i #lti
-       >nth_vec_map_lt [2:@lti |3:@niltape]
-       >Hrb <nth_pmap_lt [2:@lti|3:@N|4:@niltape]
-       >tapes_readback
-       >Htransf whd in match (vec_moves ?????);
-       >get_moves_cons_right >resize_id [2:@(len ?? moves)]
+       >nth_rb_tapes [2:@lti]
+       >Hrb [2:@lt_to_le @lti|3:@lti]
+       >Htransf whd in match (get_move ?????); (* whd in match (vec_moves ?????); *)
+       >get_moves_cons_right 
        (* lhs *)
        <nth_pmap_lt [2:@lti|3:%[@None|@N]|4:@niltape]
-       >nth_vec_map_lt [2:@lti |3:@niltape]
-       >(eq_pair_fst_snd … (nth i ? actions ?))
+       >ctapes_mk_config >nth_rb_tapes [2:@lti]
+       (* >nth_vec_map_lt [2:@lti |3:@niltape] *)
+       >(eq_pair_fst_snd … (nth i ? actions ?)) 
        >tape_move_mono_def
        cut (snd ?? (nth i ? actions 〈None sig,N〉) = nth i ? moves N)
          [>Hmoves @nth_vec_map] #Hmoves1 >Hmoves1
-       >(nth_readback … lti) >(nth_readback … lti)
        >to_sig_move @eq_f2 [2://]
-       <to_sig_write @eq_f @rb_write (* finto *)
+       <to_sig_write @eq_f @rb_write 
+       >nth_cons_right_lt [2:@lti]
+       >Hnew_chars <nth_pmap_lt [2:@lti|3:@None |4:%[@None|@N]]
+       whd in ⊢ (??%%); 
+       inversion (\fst  (nth i ? actions 〈None sig,N〉))  
+        [#Hcase whd in ⊢ (??%%); >Hcase % |#c #Hcase % ]
       ]
     ]
   ]
-- 
2.39.5