From 0ebe34030d5d1dbac686def6fba0e59d22c7b4b6 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 21 May 2012 16:57:38 +0000
Subject: [PATCH] Progress.

---
 matita/matita/lib/turing/universal/copy.ma    | 50 ++++++++--
 matita/matita/lib/turing/universal/tuples.ma  |  3 +
 .../matita/lib/turing/universal/uni_step.ma   | 97 ++++++++++++++++---
 3 files changed, 126 insertions(+), 24 deletions(-)

diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index de39fb88c..3ee552d5b 100644
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -399,20 +399,54 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
           ]
        ]
 ]]]
-qed.      
+qed.
+
+definition merge_char ≝ λc1,c2.
+  match c2 with
+  [ null ⇒ c1
+  | _ ⇒ c2 ].
+  
+lemma merge_cons : 
+  ∀c1,c2,conf1,conf2.
+  merge_config (〈c1,false〉::conf1) (〈c2,false〉::conf2) = 
+    〈merge_char c1 c2,false〉::merge_config conf1 conf2.
+#c1 #c2 #conf1 #conf2 normalize @eq_f2 //
+cases c2 /2/
+qed.
+
+lemma merge_config_c_nil : 
+  ∀c.merge_config c [] = [].
+#c cases c normalize //
+qed.
+
+axiom reverse_merge_config :
+  ∀c1,c2.|c1| = |c2| → reverse ? (merge_config c1 c2) = 
+    merge_config (reverse ? c1) (reverse ? c2).        
 
 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 …)))).
 
+(*
+   s0, s1 = caratteri di testa dello stato
+   c0 = carattere corrente del nastro oggetto
+   c1 = carattere in scrittura sul nastro oggetto
+   
+   questa dimostrazione sfrutta il fatto che 
+   merge_config (l0@[c0]) (l1@[c1]) = l1@[merge_char c0 c1] 
+   se l0 e l1 non contengono null
+*)
+
 definition R_copy ≝ λt1,t2.
-  ∀ls,c,c0,rs,l1,l3,l4.
-  t1 = midtape STape (l3@〈grid,false〉::l4@〈c0,true〉::ls) 〈c,true〉 (l1@〈comma,false〉::rs) → 
+  ∀ls,s0,s1,c0,c1,rs,l1,l3,l4.
+  t1 = midtape STape (l3@〈grid,false〉::〈c0,false〉::l4@〈s0,true〉::ls) 〈s1,true〉 (l1@〈c1,false〉::〈comma,false〉::rs) → 
   no_marks l1 → no_marks l3 → no_marks l4 → |l1| = |l4| → 
-  only_bits_or_nulls (l4@[〈c0,true〉]) → only_bits_or_nulls (〈c,true〉::l1) → 
-  t2 = midtape STape (reverse ? l1@l3@〈grid,false〉::
-          merge_config (l4@[〈c0,false〉]) (reverse ? (〈c,false〉::l1))@ls) 
-     〈comma,false〉 rs.
-     
+  only_bits (l4@[〈s0,true〉]) → only_bits (〈s1,true〉::l1) → 
+  bit_or_null c0 = true → bit_or_null c1 = true → 
+  t2 = midtape STape (〈c1,false〉::reverse ? l1@〈s1,false〉::l3@〈grid,false〉::
+                      〈merge_char c0 c1,false〉::reverse ? l1@〈s1,false〉::ls)
+       〈comma,false〉 rs.
+
 axiom sem_copy : Realize ? copy R_copy.
+i
\ No newline at end of file
diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index f51fdf384..9826c344e 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -18,6 +18,9 @@ include "turing/universal/marks.ma".
 
 definition STape ≝ FinProd … FSUnialpha FinBool.
 
+definition only_bits ≝ λl.
+  ∀c.memb STape c l = true → is_bit (\fst c) = true.
+
 definition only_bits_or_nulls ≝ λl.
   ∀c.memb STape c l = true → bit_or_null (\fst c) = true.
   
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 34bf17358..1198bb9f1 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -237,26 +237,91 @@ 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 …))))).
+  seq ? init_copy
+    (seq ? copy
+      (seq ? (move_r …) move_tape)).
 
 definition R_exec_move ≝ λt1,t2.
-  ∀n,curconfig,ls,rs,curc,table1,newconfig,mv,table2.
-  table_TM n (table1@〈comma,true〉::newconfig@〈comma,false〉::〈mv,false〉::table2) → 
-  no_marks curconfig → only_bits_or_nulls curconfig → 
+  ∀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 (〈curc,false〉::curconfig@〈grid,false〉::ls) 〈grid,false〉 
-    (table1@〈comma,true〉::newconfig@〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) → 
-  ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → 
-  ∃ls1,rs1,newc.
-  t2 = midtape STape (〈newc,false〉::reverse ? (merge_config (reverse ? curconfig) newconfig)@〈grid,false〉::ls1)
-    〈grid,false〉 (table1@〈comma,true〉::newconfig@〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs1) ∧   
-  lift_tape ls1 〈newc,false〉 rs1 = 
-  tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉).
+  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 
 
+ 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
-- 
2.39.2