From 64a59f1d6a60237ad78234f2bf90c0e5eb8c89ce Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 17 May 2012 16:33:59 +0000
Subject: [PATCH] Progress

---
 matita/matita/lib/turing/universal/copy.ma | 93 +++++++++++++++++++---
 1 file changed, 81 insertions(+), 12 deletions(-)

diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 467055248..3403d5555 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -130,21 +130,23 @@ definition copy_step ≝
   
 definition R_copy_step_true ≝ 
   λt1,t2.
-    ∀a,l1,x0,a0,l2,c,l3.
-    t1 = midtape STape (l1@〈a0,false〉::〈x0,true〉::l2) 
-         〈c,true〉 (〈a,false〉::l3) → 
-    (∀c.memb ? c l1 = true → is_marked ? c = false) →          
-    (∃x. c = bit x ∧
-    t2 = midtape STape (〈bit x,false〉::l1@〈a0,true〉::〈bit x,false〉::l2) 〈a,true〉 l3) ∨
-    (c = null ∧
-     t2 = midtape ? (〈null,false〉::l1@〈a0,true〉::〈x0,false〉::l2) 〈a,true〉 l3).
+    ∀ls,c,rs. t1 = midtape STape ls 〈c,true〉 rs → 
+    bit_or_null c = true ∧
+    (∀a,l1,x0,a0,l2,l3.
+     ls = (l1@〈a0,false〉::〈x0,true〉::l2) → 
+     rs = (〈a,false〉::l3) → 
+     no_marks l1 →          
+     ((∃x. c = bit x ∧
+      t2 = midtape STape (〈bit x,false〉::l1@〈a0,true〉::〈bit x,false〉::l2) 〈a,true〉 l3) ∨
+      (c = null ∧
+      t2 = midtape ? (〈null,false〉::l1@〈a0,true〉::〈x0,false〉::l2) 〈a,true〉 l3))).
      
 definition R_copy_step_false ≝ 
   λt1,t2.
    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → 
    bit_or_null (\fst c) = false ∧ t2 = t1.
 
-axiom sem_comp_step : 
+axiom sem_copy_step : 
   accRealize ? copy_step (inr … (inl … (inr … 0))) R_copy_step_true R_copy_step_false.
 
 (*
@@ -171,16 +173,83 @@ definition R_copy0 ≝ λt1,t2.
   t1 = midtape STape (l3@l4@〈c0,true〉::ls) 〈c,true〉 (l1@rs) → 
   no_marks l1 → no_marks (l3@l4) → |l1| = |l4| → 
   ∀l1',bv.〈c,false〉::l1 = l1'@[〈comma,bv〉] → only_bits_or_nulls l1' → 
-  ∀l4',bg.l4@[〈c0,true〉] = 〈grid,bg〉::l4' → only_bits_or_nulls l4' → 
+  ∀l4',bg.l4@[〈c0,false〉] = 〈grid,bg〉::l4' → only_bits_or_nulls l4' → 
   (c = comma ∧ t2 = t1) ∨
   (c ≠ comma ∧ 
     t2 = midtape ? (reverse ? l1'@l3@〈grid,true〉::
                   merge_config l4' (reverse ? l1')@ls) 
      〈comma,true〉 rs).
 
-axiom sem_copy0 : Realize ? copy0 R_copy0.
+lemma wsem_copy0 : WRealize ? copy0 R_copy0.
+#intape #k #outc #Hloop 
+lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
+* #ta * #Hstar @(star_ind_l ??????? Hstar)
+[ #tb whd in ⊢ (%→?); #Hleft
+  #ls #c #c0 #rs #l1 #l3 #l4 #Htb #Hl1nomarks #Hl3l4nomarks #Hlen #l1' #bv
+  #Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits
+  cases (Hleft … Htb) -Hleft #Hc #Houtc % %
+  [ generalize in match Hl1bits; -Hl1bits cases l1' in Hl1;
+    [ normalize #Hl1 #c1 destruct (Hl1) %
+    | * #c' #b' #l0 #Heq normalize in Heq; destruct (Heq)
+      #Hl1bits lapply (Hl1bits 〈c',false〉 ?) [ @memb_hd ] 
+      >Hc #Hfalse destruct ]
+  | @Houtc ]
+| #tb #tc #td whd in ⊢ (%→?→(?→%)→%→?); #Htc #Hstar1 #Hind #Htd
+  lapply (Hind Htd) -Hind #Hind
+  #ls #c #c0 #rs #l1 #l3 #l4 #Htb #Hl1nomarks #Hl3l4nomarks #Hlen #l1' #bv
+  #Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits %2
+  cases (Htc … Htb) -Htc #Hcbitnull #Htc
+  % [ % #Hc' >Hc' in Hcbitnull; normalize #Hfalse destruct (Hfalse) ]
+  cut (|l1| = |reverse ? l4|) [@daemon] #Hlen1
+  @(list_cases_2 … Hlen1)
+  [ #Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize
+    [ #Hl1 destruct normalize in Hcbitnull; destruct (Hcbitnull)
+    | #p0 #l0 normalize #Hfalse destruct (Hfalse) cases l0 in e0;
+      [ normalize #Hfalse1 destruct (Hfalse1)
+      | #p0' #l0' normalize #Hfalse1 destruct (Hfalse1) ] ]
+  | * #a #ba * #a0 #ba0 #l1'' #l4'' #Hl1cons #Hl4cons
+    lapply (eq_f ?? (reverse ?) ?? Hl4cons) >reverse_reverse >reverse_cons -Hl4cons #Hl4cons
+    cut (ba = false) [ @daemon ] #Hba
+    cut (ba0 = false) [ @daemon ] #Hba0
+    >Hba0 in Hl4cons; >Hba in Hl1cons; -Hba0 -Hba #Hl1cons #Hl4cons
+    >Hl4cons in Htc; >Hl1cons #Htc
+    lapply (Htc a (l3@reverse ? l4'') c0 a0 ls (l1''@rs) ? (refl ??) ?)
+    [ #x #Hx @Hl3l4nomarks >Hl4cons <associative_append
+      @memb_append_l1 @Hx
+    | >associative_append >associative_append %
+    | -Htc *
+      [ * #x * #Hx #Htc 
+        lapply (Hind (〈bit x,false〉::ls) a a0 rs l1'' 
+                (〈bit x,false〉::l3) (reverse ? l4'') ????) 
+        [ >Hl1cons in Hlen; >Hl4cons >length_append >commutative_plus 
+          normalize #Hlen destruct (Hlen) //
+        | #x0 #Hx0 cases (orb_true_l … Hx0)
+          [ #Hx0eq >(\P Hx0eq) %
+          | -Hx0 #Hx0 @Hl3l4nomarks >Hl4cons
+            <associative_append @memb_append_l1 // ]
+        | #x0 #Hx0 @Hl1nomarks >Hl1cons @memb_cons //
+        | >Htc >associative_append % 
+        | -Hind 
+          cut (∃la.l1' = 〈c,false〉::la)
+          [ >Hl1cons in Hl1; cases l1'
+            [normalize #Hfalse destruct (Hfalse)
+            | #p #la normalize #Hla destruct (Hla) @(ex_intro ?? la) % ] ]
+          * #la #Hla
+          cut (∃lb.l4' = lb@[〈c0,false〉])
+            [ >Hl4cons in Hl4;
+              @(list_elim_left … l4')
+              (* si usa l'iniettività del "cons destro" 
+              [ normalize 
+              | #p #lb
+             cases l4'
+              [normalize
+              | #p #lb *)
+            
+            @(list_elim_left … l4')
+           <Hl1cons <Hl4cons #Hind lapply (Hind ?? Hl1 ??? Hl4 ?)
 
-definition copy ≝ 
+definition copy
+≝ 
   seq STape (move_l …) (seq ? (adv_to_mark_l … (is_marked ?))
    (seq ? (clear_mark …) (seq ? (adv_to_mark_r … (is_marked ?)) (clear_mark …)))).
 
-- 
2.39.2