Progress.

[helm.git] / matita / matita / lib / turing / universal / copy.ma

diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma
index 6b77ef9b7ee8704d0429d65f4faf440af9390d43..3ee552d5bb311f05e8a2d45ec8807e297a6ad955 100644 (file)
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -301,11 +301,58 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
           (* by IH, we proceed by cases, whether a = comma 
              (consequently several lists = []) or not *)          
           *
-          [ * #Ha #Houtc1 >Hl1cons in Hl1; >Hla
+          [ * #Ha #Houtc1
+(*           cut (l1 = [〈a,false〉])
+           [ cases l1'' in Hl1cons; // #y #ly #Hly
+             >Hly in Hl1; cases l1' in Hl1bits;
+             [ #_ normalize #Hfalse destruct (Hfalse)
+             | #p #lp #Hl1bits normalize #Heq destruct (Heq)
+               @False_ind lapply (Hl1bits 〈a,false〉 ?)
+               [ cases lp in e0;
+                 [ normalize #Hfalse destruct (Hfalse)
+                 | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
+                   @memb_cons @memb_hd ]
+               | >Ha normalize #Hfalse destruct (Hfalse) ]
+             ]
+           ] #Hl1a
+           cut (l4 = [〈a0,false〉])
+           [ generalize in match Hl4bits; cases l4' in Hl4;
+             [ >Hl4cons #Hfalse #_ 
+               lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
+               cases (reverse ? l4'') normalize
+               [ #Hfalse1 | #p0 #lp0 #Hfalse1 ] destruct (Hfalse1)
+             | #p #lp 
+           
+             cases l4'' in Hl4cons; // #y #ly #Hly
+             >Hly in Hl4; cases l4' in Hl4bits;
+             [ #_ >reverse_cons #Hfalse
+               lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
+               -Hfalse cases ly normalize
+               [ #Hfalse | #p #Hp #Hfalse ] destruct (Hfalse)
+                
+             | #p #lp #Hl1bits normalize #Heq destruct (Heq)
+               @False_ind lapply (Hl1bits 〈a,false〉 ?)
+               [ cases lp in e0;
+                 [ normalize #Hfalse destruct (Hfalse)
+                 | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
+                   @memb_cons @memb_hd ]
+               | >Ha normalize #Hfalse destruct (Hfalse) ]
+             ]
+           ] #Hl1a
+             
+              >Hla normalize #Hl1 destruct (Hl1) lapply (inj_append_ @False_ind
+             
+           cut (l1'' = [] ∧ l4'' = [])
+           [ % [ >Hla in Hl1; normalize #Hl1 destruct (Hl1)
+           
+            cases l1'' in Hl1bits;
+                
+                 [ #_ normalize #H *)
+           cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = [])
+           [ @daemon ] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil
+           >Hl1cons in Hl1; >Hla
            >Houtc1 >Htc #Hl1
            >Hl4cons in Hl4; >Hlb #Hl4
-           cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = []) 
-           [@daemon] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil
            >Hla1 >Hlb1 >Hl1nil >Hl4nil >Hx
            cut (a0 = grid) [ @daemon ] #Ha0 <Ha <Ha0
            normalize in ⊢ (??(??%?%)(??%?%)); >associative_append %
@@ -352,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 (〈c0,true〉::l4) → 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