From 1695dd8b1861176954666067243c02020e1dcea5 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 21 May 2012 09:12:57 +0000
Subject: [PATCH] New version of init copy

---
 matita/matita/lib/turing/universal/tuples.ma  | 55 +++++++--------
 .../matita/lib/turing/universal/uni_step.ma   | 69 ++++++++++++++++++-
 2 files changed, 90 insertions(+), 34 deletions(-)

diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 2520fed51..f51fdf384 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -225,52 +225,45 @@ lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
 qed.
 
 definition init_current_on_match ≝ 
-  seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-    (seq ? (move_l ?)
-       (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-          (seq ? (move_r ?) (mark ?)))).
+  (seq ? (move_l ?)
+    (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
+      (seq ? (move_r ?) (mark ?)))).
           
 definition R_init_current_on_match ≝ λt1,t2.
-  ∀l1,l2,c,l3,d,rs. no_grids l1 → no_grids l2 → is_grid c = false → is_grid (\fst d) = false → 
-  t1 = midtape STape (l1@〈grid,false〉::l2@〈c,false〉::〈grid,false〉::l3) d rs → 
-  t2 = midtape STape (〈grid,false〉::l3) 〈c,true〉 
-           ((reverse ? (l1@〈grid,false〉::l2)@d::rs)).
+  ∀l1,l2,c,rs. no_grids l1 → is_grid c = false → 
+  t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::l2)  〈grid,false〉 rs → 
+  t2 = midtape STape (〈grid,false〉::l2) 〈c,true〉 ((reverse ? l1)@〈grid,false〉::rs).
 
 lemma sem_init_current_on_match : 
   Realize ? init_current_on_match R_init_current_on_match.
 #intape 
-cases (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-        (sem_seq ????? (sem_move_l ?)
-          (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-             (sem_seq ????? (sem_move_r ?) (sem_mark ?)))) intape)
+cases (sem_seq ????? (sem_move_l ?)
+        (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
+           (sem_seq ????? (sem_move_r ?) (sem_mark ?))) intape)
 #k * #outc * #Hloop #HR 
 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
-#l1 #l2 #c #l3 #d #rs #Hl1 #Hl2 #Hc #Hd #Hintape
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape
-  [ * >Hd #Hfalse normalize in Hfalse; destruct (Hfalse) ]
-* #_ #Hta lapply (Hta l1 〈grid,false〉 ? (refl ??) (refl …) Hl1) -Hta #Hta
-* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta 
-generalize in match Hl2; cases l2
-  [#Hl2 whd in ⊢ ((???(??%%%))→?); #Htb
-   * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htb) -Htb
+#l1 #l2 #c #rs #Hl1 #Hc #Hintape
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape 
+generalize in match Hl1; cases l1
+  [#Hl1 whd in ⊢ ((???(??%%%))→?); #Hta
+   * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Hta
     [* >Hc #Htemp destruct (Htemp) ]
-   * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl2) 
+   * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1) 
    whd in ⊢ ((???(??%%%))→?); -Htc #Htc
    * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd 
    whd in ⊢ ((???(??%%%))→?); #Htd
    whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc
-   >Houtc >reverse_append %
-  |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Htb
-   * #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htb) -Htc
+   >Houtc % 
+  |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Hta
+   * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb
     [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)]    
-   * #Hd >append_cons #Htc lapply (Htc … (refl ??) (refl …) ?)
+   * #Hd >append_cons #Htb lapply (Htb … (refl ??) (refl …) ?)
     [#x #membx cases (memb_append … membx) -membx #membx
-      [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]] #Htc
-   * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd 
-   >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htd
-   whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc 
-   >Houtc >reverse_append >reverse_cons >reverse_cons 
-   >associative_append >associative_append >associative_append %
+      [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]]-Htb  #Htb
+   * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc 
+   >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc
+   whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc #Houtc 
+   >Houtc >reverse_cons >associative_append % 
   ]
 qed.   
 
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index c22628d1b..d24dc07ba 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -94,14 +94,77 @@ whd in ⊢ (%→?); #Htf cases (Htf … Hte) -Htf -Hte
   [#x #membl @Hnomarks @daemon] -Htf #Htf >Htf >reverse_reverse %
 qed.
 
+
 (* init_copy 
 
-           adv_mark_r;
            init_current_on_match; (* no marks in current *)
            move_r;
            adv_to_mark_r;
+           adv_mark_r;
+
 *)
-     
+
+definition init_copy ≝ 
+  seq ? init_current_on_match
+    (seq ? (move_r ?) 
+      (seq ? (adv_to_mark_r ? (is_marked ?))
+        (adv_mark_r ?))).
+
+definition R_init_copy ≝ λt1,t2.
+  ∀l1,l2,c,ls,d,rs. 
+  no_marks l1 → no_grids l1 → 
+  no_marks l2 → is_grid c = false → 
+  t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 (l2@〈comma,true〉::〈d,false〉::rs) → 
+  t2 = midtape STape (〈comma,false〉::(reverse ? l2)@〈grid,false〉::l1@〈c,true〉::〈grid,false〉::ls) 〈d,true〉 rs.
+
+lemma list_last: ∀A.∀l:list A.
+  l = [ ] ∨ ∃a,l1. l = l1@[a].
+#A #l <(reverse_reverse ? l) cases (reverse A l)
+  [%1 //
+  |#a #l1 %2 @(ex_intro ?? a) @(ex_intro ?? (reverse ? l1)) //
+  ]
+qed.
+   
+lemma sem_init_copy : Realize ? init_copy R_init_copy.
+#intape 
+cases (sem_seq ????? sem_init_current_on_match
+        (sem_seq ????? (sem_move_r ?)
+          (sem_seq ????? (sem_adv_to_mark_r ? (is_marked ?))
+            (sem_adv_mark_r ?))) intape)
+#k * #outc * #Hloop #HR 
+@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#l1 #l2 #c #ls #d #rs #Hl1marks #Hl1grids #Hl2marks #Hc #Hintape
+cases HR -HR
+#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hl1grids Hc Hintape) -Hta -Hintape #Hta
+* #tb * whd in ⊢ (%→?); #Htb lapply (Htb  … Hta) -Htb -Hta
+generalize in match Hl1marks; -Hl1marks cases (list_last ? l1) 
+  [#eql1 >eql1 #Hl1marks whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); #Htb
+   * #tc * whd in ⊢ (%→?); #Htc lapply (Htc  … Htb) -Htc -Htb *
+    [* whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)]
+   * #_ #Htc lapply (Htc … (refl …) (refl …) ?)
+    [#x #membx @Hl2marks @membx]
+   #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc
+   >Houtc %
+  |* #c1 * #tl #eql1 >eql1 #Hl1marks >reverse_append >reverse_single 
+   whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?);
+   >associative_append whd in ⊢ ((???(????%))→?); #Htb
+   * #tc * whd in ⊢ (%→?); #Htc lapply (Htc  … Htb) -Htc -Htb *
+    [* >Hl1marks [#Htemp destruct (Htemp)] @memb_append_l2 @memb_hd]
+   * #_ >append_cons <associative_append #Htc lapply (Htc … (refl …) (refl …) ?)
+    [#x #membx cases (memb_append … membx) -membx #membx
+      [cases (memb_append … membx) -membx #membx
+        [@Hl1marks @memb_append_l1 @daemon
+        |>(memb_single … membx) %
+        ]
+      |@Hl2marks @membx
+      ]]
+  #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc
+  >Houtc >reverse_append >reverse_append >reverse_single 
+  >reverse_reverse >associative_append >associative_append 
+  >associative_append %
+qed.
+  
+(* OLD 
 definition init_copy ≝ 
   seq ? (adv_mark_r ?) 
     (seq ? init_current_on_match
@@ -169,7 +232,7 @@ cases HR -HR
       >associative_append % 
     ]
   ]
-qed.
+qed. *)
 
 include "turing/universal/move_tape.ma".
 
-- 
2.39.2