X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funi_step.ma;h=1198bb9f1040286a6271dbe2d7da9c46fb93ad5e;hb=0ebe34030d5d1dbac686def6fba0e59d22c7b4b6;hp=701972f3fe1be52c885c55ba91863624a9b45f1c;hpb=06913146ad4e17070d27b6b0a08d48f14fefb188;p=helm.git

diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 701972f3f..1198bb9f1 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,77 +232,96 @@ cases HR -HR
       >associative_append % 
     ]
   ]
-qed.
+qed. *)
 
 include "turing/universal/move_tape.ma".
 
 definition exec_move ≝ 
-  seq ? (adv_to_mark_r … (is_marked ?))
-    (seq ? init_copy
-      (seq ? copy
-        (seq ? (move_r …)
-          (seq ? move_tape (move_r …))))).
-
-definition lift_tape ≝ λls,c,rs.
-  let 〈c0,b〉 ≝ c in
-  let c' ≝ match c0 with
-  [ null ⇒ None ?
-  | _ ⇒ Some ? c ]
-  in
-  mk_tape STape ls c' rs.
-  
-definition sim_current_of_tape ≝ λt.
-  match current STape t with
-  [ None ⇒ 〈null,false〉
-  | Some c0 ⇒ c0 ].
-
-(*
- t1 =  ls # cs c # table # rs  
- 
- let simt ≝ lift_tape ls c rs in
- let simt' ≝ move_left simt' in
- 
- t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
-*)
-          
-(*
-definition R_move
+  seq ? init_copy
+    (seq ? copy
+      (seq ? (move_r …) move_tape)).
 
 definition R_exec_move ≝ λt1,t2.
-  ∀ls,current,table1,newcurrent,table2,rs.
-  t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
-       (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
-        〈grid,false〉::rs) → 
-  table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
-  t2 = midtape
-*)
-
-(*
-
-step :
-
-if is_true(current) (* current state is final *)
-   then nop
-   else 
-   init_match;
-   match_tuple;
-   if is_marked(current) = false (* match ok *)
-      then exec_move; 
-      else sink;
-        
-*)
-
-definition mk_tuple ≝ λc,newc,mv.
-  c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉].
+  ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2.
+  table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → 
+  no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → only_bits (〈s1,false〉::newconfig) → 
+  no_nulls ls → no_nulls rs → 
+  t1 = midtape STape (〈c0,false〉::curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 
+    (table1@〈comma,true〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) → 
+  ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
+  ∃ls1,rs1,c2.
+  t2 = midtape STape ls1 〈grid,false〉 
+    (〈s1,false〉::newconfig@〈c2,false〉::〈grid,false〉::
+     table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs1) ∧   
+  lift_tape ls1 〈c2,false〉 rs1 = 
+  tape_move STape t1' (Some ? 〈〈c2,false〉,move_of_unialpha mv〉).
+  
+lemma sem_exec_move : Realize ? exec_move R_exec_move.
+#intape
+cases (sem_seq … sem_init_copy
+        (sem_seq … sem_copy
+          (sem_seq … (sem_move_r …) sem_move_tape )) intape)
+#k * #outc * #Hloop #HR
+@(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop
+#n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2
+#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hls #Hrs #Hintape #t1' #Ht1'
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta
+lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1
+        (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta
+[ (*Hcurconfig2*) @daemon
+| (*Htable*) @daemon
+| (*FIXME*) @daemon
+| (*FIXME*) @daemon
+| #Hta * #tb * whd in ⊢ (%→?); #Htb
+  lapply (Htb (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Hta ????????) -Htb
+  [9:|*:(* rivedere le precondizioni *) @daemon ]
+  #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc
+  whd in ⊢ (%→?); #Houtc whd in Htc:(???%); whd in Htc:(???(??%%%));
+  lapply (Houtc rs n 
+    (〈comma,false〉::〈s1,false〉::reverse ? newconfig@@〈comma,false〉::reverse ? table1)
+    mv table2 (merge_char curc d1) (merge_config curconfig (reverse ? newconfig1)) ls ????? 
+    Hls Hrs ??)
+  [3: >Htc @(eq_f3 … (midtape ?))
+    [ @eq_f >associative_append >Hnewconfig
+      >reverse_cons >associative_append @eq_f
+      whd in ⊢ (???%); @eq_f whd in ⊢ (???%); @eq_f
+      <Heqcurconfig <reverse_cons >Hnewconfig1 >reverse_append
+      >merge_cons %
+    | %
+    | % ]
+  | %
+  || >reverse_cons >reverse_append >reverse_reverse >reverse_cons
+     >reverse_reverse 
+     >associative_append >associative_append >associative_append
+     normalize @Htable
+  | (* only bits or nulls c1,c2 → only bits or nulls (merge c1 c2) *) @daemon
+  | (* add to hyps? *) @daemon
+  | (* bit_or_null c1,c2 → bit_or_null (merge_char c1 c2) *) @daemon
+  | -Houtc * #ls1 * #rs1 * #newc * #Houtc *
+    [ *
+      [ * #Hmv #Htapemove
+        @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? (\fst newc))
+        %
+        [ >Houtc >reverse_merge_config [| @daemon ]
+          >reverse_reverse @eq_f
+          >reverse_cons >reverse_append >reverse_cons
+          >reverse_reverse >reverse_reverse
+          @daemon
+        | >Hmv >Ht1' whd in Htapemove:(???%); whd in ⊢ (???%);
+          whd in match (lift_tape ???) in ⊢ (???%);
+          >Htapemove
+    
+    
+  
+   >Heqcurconfig
+>append_cons in Hintape; >associative_append
+cases (Hta 
 
-inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝ 
-| mit_hd : 
-   ∀tb.
-   match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb)
-| mit_tl :
-   ∀c0,newc0,mv0,tb.
-   match_in_table c newc mv tb → 
-   match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb).
+ cases (Hta … Hintape) -Hta
+[ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+* #_ #Hta lapply (Hta ? 〈comma,true〉 … (refl ??) (refl ??) ?)
+[ @daemon ] -Hta #Hta
+* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta)
 
 definition move_of_unialpha ≝ 
   λc.match c with
@@ -258,5 +340,7 @@ definition R_uni_step ≝ λt1,t2.
     (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
    lift_tape ls1 〈newc,false〉 rs1 = 
    tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
-  
-  
\ No newline at end of file
+
+definition no_nulls ≝ 
+ λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
+