Merge branch 'declarative' into matita-lablgtk3

[helm.git] / matita / matita / lib / turing / multi_to_mono / exec_moves.ma

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 496b84c5fa32426c17be632acaec01ee2f1d0edb..ac8cd7ecfc48ba6e47d92c74db28933a8e2546d6 100644 (file)
--- a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
+++ b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma
@@ -2,19 +2,13 @@
 
 include "turing/multi_to_mono/exec_trace_move.ma".
 (* include "turing/turing.ma". *)
-
-let rec exec_moves sig n i on i : TM (multi_sig sig n) ≝
+  
+let rec exec_moves Q sig n i on i : TM (MTA (HC Q n) sig (S n)) ≝
   match i with 
   [ O ⇒ nop ? (* exec_move_i sig n 0 *)
-  | S j ⇒ seq ? (exec_moves sig n j) (exec_move_i sig n j) 
+  | S j ⇒ seq ? (exec_moves Q sig n j) (exec_move_i Q sig n j) 
   ].
-     
-axiom get_moves : ∀sig,n.∀a:multi_sig sig n.∀i.Vector DeqMove i.
 
-axiom get_moves_cons: ∀sig,n,a,j.j < n → 
- get_moves sig n a (S j) = 
- vec_cons ? (get_move ? n a j) j (get_moves sig n a j).
- 
 definition a_moves ≝ 
   λsig,n.λactions: Vector ((option sig) × move) n. 
   vec_map ?? (snd ??) n actions.
@@ -35,6 +29,20 @@ definition tape_writem ≝
   λsig,n,ts,chars.
   pmap_vec ??? (tape_write sig) n ts chars.
 
+(*
+let rec i_moves a i on i : Vector move i ≝
+  match i with 
+  [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
+  | S j ⇒ vec_cons ? (nth j ? a N) j (i_moves a j)
+  ]. *)
+
+definition vec_moves ≝ λQ,sig,n,a,i. 
+  resize_vec … (get_moves Q sig n a) i N.
+
+axiom vec_moves_cons: ∀Q,sig,n,a,j.j < n → 
+ vec_moves Q sig n a (S j) = 
+ vec_cons ? (get_move Q ? n a j) j (vec_moves Q sig n a j).
+
 (*
 axiom actions_commute : ∀sig,n,ts,actions.
   tape_moves sig n (tape_writem ?? ts (a_chars … actions)) (a_moves … actions) = 
@@ -43,25 +51,29 @@ axiom actions_commute : ∀sig,n,ts,actions.
 (* devo rafforzare la semantica, dicendo che i tape non toccati
 dalle moves non cambiano *)
 
-definition R_exec_moves ≝ λsig,n,i,t1,t2.
+
+definition R_exec_moves ≝ λQ,sig,n,i,t1,t2.
 ∀a,ls,rs. 
   t1 = midtape ? ls a rs → 
-  (∀i.regular_trace sig n a ls rs i) → 
-  nth n ? (vec … a) (blank ?) = head ? → 
+  (∀i.regular_trace (TA (HC Q n) sig) (S n) a ls rs i) → 
+  is_head ?? (nth n ? (vec … a) (blank ?)) = true →  
   no_head_in … ls →
   no_head_in … rs →
   ∃ls1,a1,rs1. 
-   t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
-   (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
-   readback sig n ls1 (vec … a1) rs1 i = 
-     tape_moves ?? (readback sig n ls (vec … a) rs i) (get_moves sig n a i) ∧
-   (∀j. i ≤ j → j ≤ n →  
-    rb_trace_i sig n ls1 (vec … a1) rs1 j = 
-      rb_trace_i sig n ls (vec … a) rs j).
+   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) ∧
+   (∀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).
@@ -72,36 +84,33 @@ 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: ∀sig,n,i. i < n → 
-  exec_moves sig n i ⊨ R_exec_moves sig n i.
-#sig #n #i elim i 
+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 … ltj)) -Hind
+   @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind
    #int #outt * #t1 * #H1 #H2
    #a #ls #rs #Hint #H3 #H4 #H5 #H6
    lapply (H1 … Hint H3 H4 H5 H6)
    * #ls1 * #a1 * #rs1 * * * #H7 #H8 #H9 #H10
    lapply (reg_inv … (H8 n) ? H4 H5 H6)
-    [@H10 [@lt_to_le @ltj |@le_n]]
+    [@H10 [@ltj |@le_n]]
    -H3 -H4 -H5 -H6 * * #H3 #H4 #H5
    lapply (H2 … H7 H8 H3 H4 H5)
    * #ls2 * #a2 * #rs2 * * * #Houtt #Hregout #Hrboutt #Hrbid
    %{ls2} %{a2} %{rs2} 
-   cut (∀i. get_move sig n a i = get_move sig n a1 i)
+   cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i)
      [@daemon] #aa1
    %[%[%[@Houtt|@Hregout]
-      |whd in ⊢ (??%?); @Vector_eq >(get_moves_cons … ltj)
-       >tape_moves_def >pmap_vec_cons @eq_f2
-        [<H10 [>aa1 @Hrboutt |@lt_to_le @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) 
@@ -110,16 +119,3 @@ lemma sem_exec_moves: ∀sig,n,i. i < n →
   ]
 qed.
   
-
-
-
-
-
-
-
-
-
-
-
-
-