From 9b61b843c4938c57cd5712df0ec8cf6892c0f906 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 18 May 2012 11:24:56 +0000
Subject: [PATCH] init_copy init_match

---
 matita/matita/lib/turing/universal/tuples.ma  | 110 ++++++++++++++++++
 .../matita/lib/turing/universal/uni_step.ma   | 107 ++++++++++++-----
 2 files changed, 185 insertions(+), 32 deletions(-)

diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 3b1e9a393..a7afb0b2b 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -224,6 +224,116 @@ 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 ?)))).
+          
+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)).
+
+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)
+#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
+    [* >Hc #Htemp destruct (Htemp) ]
+   * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl2) 
+   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
+    [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)]    
+   * #Hd >append_cons #Htc lapply (Htc … (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 %
+  ]
+qed.   
+
+(*
+definition init_current_gen ≝ 
+  seq ? (adv_to_mark_l ? (is_marked ?))
+    (seq ? (clear_mark ?)
+       (seq ? (move_l ?)
+         (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
+            (seq ? (move_r ?) (mark ?))))).
+          
+definition R_init_current_gen ≝ λt1,t2.
+  ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 →
+  Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) → 
+  t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs → 
+  t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉
+        ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)).
+
+lemma sem_init_current_gen : Realize ? init_current_gen R_init_current_gen.
+#intape 
+cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
+        (sem_seq ????? (sem_clear_mark ?)
+          (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 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hintape
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape
+  [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
+* #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%] -Hta #Hta
+* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta #Htb 
+* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb 
+generalize in match Hc; generalize in match Hl2; cases l2
+  [#_ whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) 
+   whd in ⊢ ((???(??%%%))→?); #Htc
+   * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
+    [2: * whd in ⊢ (??%?→?); #Htemp destruct (Htemp) ]
+   * #_ #Htd >Htd in Htc; -Htd #Htd
+   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd
+   >reverse_append >reverse_cons 
+   whd in ⊢ ((???(??%%%))→?); #Hte
+   whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc
+   >Houtc %
+  |#d #tl #Htl #Hc0 whd in ⊢ ((???(??%%%))→?); #Htc
+   * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
+    [* >(Htl … (memb_hd …)) whd in ⊢ (??%?→?); #Htemp destruct (Htemp)]    
+   * #Hd #Htd lapply (Htd … (refl ??) (refl ??) ?)
+    [#x #membx @Htl @memb_cons @membx] -Htd #Htd
+   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd
+   >reverse_append >reverse_cons >reverse_cons
+   >reverse_cons in Hc0; >reverse_cons cases (reverse ? tl)
+     [normalize in ⊢ (%→?); #Hc0 destruct (Hc0) #Hte 
+      whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc
+      >Houtc %
+     |* #c2 #b2 #tl2 normalize in ⊢ (%→?); #Hc0 destruct (Hc0)  
+      whd in ⊢ ((???(??%%%))→?); #Hte 
+      whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc
+      >Houtc >associative_append >associative_append >associative_append %
+     ]
+   ]
+qed.
+*)
 definition init_current ≝ 
   seq ? (adv_to_mark_l ? (is_marked ?))
     (seq ? (clear_mark ?)
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 5c48d9272..1cb035a6a 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -94,38 +94,81 @@ whd in ⊢ (%→?); #Htf cases (Htf … Hte) -Htf -Hte
   [#x #membl @Hnomarks @daemon] -Htf #Htf >Htf >reverse_reverse %
 qed.
 
-#Htb lapply (Htb ??? (refl …) (refl …))
+(* init_copy 
 
-lapply (Htb l 〈grid,false〉 (〈d,false〉::rs) (refl … ))
+           adv_mark_r;
+           init_current_on_match; (* no marks in current *)
+           move_r;
+           adv_to_mark_r;
+*)
+     
+definition init_copy ≝ 
+  seq ? (adv_mark_r ?) 
+    (seq ? init_current_on_match
+      (seq ? (move_r ?) 
+        (adv_to_mark_r ? (is_marked ?)))).
+
+definition R_init_copy ≝ λt1,t2.
+  ∀l1,l2,c,l3,d,rs. 
+  no_marks l1 → no_grids l1 → 
+  no_marks l2 → no_grids l2 → is_grid c = false → is_grid d =false →
+  t1 = midtape STape (l1@〈grid,false〉::l2@〈c,false〉::〈grid,false〉::l3) 〈comma,true〉 (〈d,false〉::rs) → 
+  t2 = midtape STape (〈comma,false〉::l1@〈grid,false〉::l2@〈c,true〉::〈grid,false〉::l3) 〈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.
    
- 
-* #tc * whd in ⊢ (%→?); #Htc 
-* #td * whd in ⊢ (%→%→?); #Htd #Houtc
-#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hc0 #Hintape
-cases (Hta … Hintape) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
--Hta * #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%]
--Hta #Hta lapply (Htb … Hta) -Htb #Htb cases (Htc … Htb) [ >Hc -Hc * #Hc destruct (Hc) ] 
--Htc * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@Hl2]
--Htc #Htc lapply (Htd … Htc) -Htd
->reverse_append >reverse_cons 
->reverse_cons in Hc0; cases (reverse … l2)
-[ normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
-  #Htd >(Houtc … Htd) %
-| * #c2 #b2 #tl2 normalize in ⊢ (%→?);
-  #Hc0 #Htd >(Houtc … Htd)
-  whd in ⊢ (???%); destruct (Hc0)
-  >associative_append >associative_append %
-]
+lemma sem_init_copy : Realize ? init_copy R_init_copy.
+#intape 
+cases (sem_seq ????? (sem_adv_mark_r ?)
+       (sem_seq ????? sem_init_current_on_match
+        (sem_seq ????? (sem_move_r ?)
+         (sem_adv_to_mark_r ? (is_marked ?)))) intape)
+#k * #outc * #Hloop #HR 
+@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#l1 #l2 #c #l3 #d #rs #Hl1marks #Hl1grids #Hl2marks #Hl2grids #Hc #Hd #Hintape
+cases HR -HR
+#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta
+* #tb * whd in ⊢ (%→?); 
+>append_cons #Htb lapply (Htb (〈comma,false〉::l1) l2 c … Hta) 
+  [@Hd |@Hc |@Hl2grids 
+   |#x #membx cases (orb_true_l … membx) -membx #membx 
+     [>(\P membx) // | @Hl1grids @membx]
+  ] -Htb #Htb
+* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb
+>reverse_append >reverse_cons cases (list_last ? l2)
+  [#Hl2 >Hl2 >associative_append whd in ⊢ ((???(??%%%))→?); #Htc
+   whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd -Htc
+    [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)]
+   * #_ #Htf lapply (Htf … (refl …) (refl …) ?) 
+    [#x >reverse_cons #membx cases (memb_append … membx) -membx #membx
+      [@Hl1marks @daemon |>(memb_single … membx) //] 
+    -Htf
+    |#Htf >Htf >reverse_reverse >associative_append %
+    ]
+  |* #a * #l21 #Heq >Heq >reverse_append >reverse_single 
+   >associative_append >associative_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc
+   whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd -Htc
+    [* >Hl2marks [#Habs destruct (Habs) |>Heq @memb_append_l2 @memb_hd]]
+   * #_ <associative_append <associative_append #Htf lapply (Htf … (refl …) (refl …) ?) 
+    [#x >reverse_cons #membx cases (memb_append … membx) -membx #membx
+      [cases (memb_append … membx) -membx #membx
+        [@Hl2marks >Heq @memb_append_l1 @daemon
+        |>(memb_single … membx) //]
+      |cases (memb_append … membx) -membx #membx
+        [@Hl1marks @daemon |>(memb_single … membx) //]
+      ]
+    | #Htf >Htf >reverse_append >reverse_reverse
+      >reverse_append >reverse_reverse >associative_append 
+      >reverse_single >associative_append >associative_append 
+      >associative_append % 
+    ]
+  ]
+qed.
+    ]-Htf
 qed.
-
-definition match_tuple_step ≝ 
-  ifTM ? (test_char ? (λc:STape.¬ is_grid (\fst c))) 
-   (single_finalTM ? 
-     (seq ? compare
-      (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
-        (nop ?)
-        (seq ? mark_next_tuple 
-           (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
-             (mark ?) (seq ? (move_l ?) init_current) tc_true)) tc_true)))
-    (nop ?) tc_true.
-          
\ No newline at end of file
-- 
2.39.2