work in 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 331bf6881fc2103348f42bd4d48536e75a36404c..65bf961b996826ca491dd301e165cdc4b57c74ec 100644 (file)
--- a/matita/matita/lib/turing/universal/copy.ma
+++ b/matita/matita/lib/turing/universal/copy.ma
@@ -10,7 +10,7 @@
       V_____________________________________________________________*)
 
 
-include "turing/universal/tuples.ma".
+include "turing/universal/marks.ma".
 
 definition copy_step_subcase ≝
   λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉))
@@ -47,28 +47,31 @@ cases (sem_if ? (test_char ? (λx. x == 〈c,true〉)) ?????? tc_true (sem_test_
         HelseM intape)
 #k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop
 #a #l1 #x0 #a0 #l2 #x #l3 #Hintape #Hl1marks cases HR -HR
-[ * #ta * whd in ⊢ (%→?); >Hintape #Hta cases (Hta … (refl ??)) -Hta #Hx #Hta
-  * #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Hta -Htb #Htb
-  * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
-  * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
-  [ >Htc * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
-  * #_ #Htd lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ? (refl ??) ?) -Htd
-  [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [@(Hl1marks ? Hx1)|>(memb_single … Hx1) %]
-  | normalize >associative_append % ] #Htd
+[ * #ta * whd in ⊢ (%→?); >Hintape * * #c0 * whd in ⊢ (??%?→?); #Hx #Hc #Hta
+  * #tb * whd in ⊢ (%→?); * #Htb cases (Htb (l1@〈a0,false〉::〈x0,true〉::l2) x) -Htb
+  #Htb lapply (Htb … Hta) -Htb #Htb #_ #_
+  * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+  * #td * whd in ⊢ (%→?); * #_ #Htd cases (Htd … Htc) -Htd #_ #Htd cases (Htd (refl ??))
+  -Htd #Htd lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ???) //
+  [#x1 #Hx1 cases (memb_append … Hx1) [ @Hl1marks | #Hsingle >(memb_single … Hsingle) % ]
+  |whd in ⊢ (??%?); // ]
+  -Htd #Htd #_
   * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd -Htc #Hte
-  * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Hte -Htf >reverse_append #Htf
-  * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf) -Htf -Htg >reverse_single #Htg
-  * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Htg -Hth
+  * #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Hte -Htf >reverse_append #Htf
+  * #tg * whd in ⊢ (%→?); * #Htg #_ lapply (Htg … Htf) -Htf -Htg >reverse_single #Htg
+  * #th * whd in ⊢ (%→?); * #_ #Hth lapply (Hth … Htg) -Htg -Hth
   generalize in match Hl1marks; -Hl1marks @(list_elim_left … l1)
-  [ #Hl1marks #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
+  [ #Hl1marks #Hth whd in ⊢ (%→?); * #_ #Houtc cases (Houtc … Hth) -Houtc
     [ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
-    * #_ #Houtc lapply (Houtc [] ?? (refl ??) (refl ??) Hl1marks) -Houtc
-    #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] @Houtc
+    * * #_ #Houtc #_ lapply (Houtc [] ?? (refl ??) (refl ??) Hl1marks) -Houtc
+    #Houtc % >(\P Hc) in Hx; #Hx destruct (Hx) % // @Houtc
   | -l1 #c1 #l1 #_ #Hl1marks >reverse_append >reverse_single
     #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
     [ * >Hl1marks [ #Hfalse destruct (Hfalse) ] @memb_append_l2 @memb_hd ]
     * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
-    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [ @Hl1marks @memb_append_l1 @daemon | >(memb_single … Hx1) % ]
+    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1   
+      [@Hl1marks @memb_append_l1 <(reverse_reverse … l1) @memb_reverse @Hx1 
+      |>(memb_single … Hx1) % ]
     | normalize >associative_append % ] 
     #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] >Houtc
     >reverse_append >reverse_reverse >associative_append >associative_append % ]
@@ -154,7 +157,9 @@ cases (sem_if ? (test_char ? (λx:STape.x == 〈null,true〉)) ?????? tc_true
     #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
     [ * >Hl1marks [ #Hfalse destruct (Hfalse) ] @memb_append_l2 @memb_hd ]
     * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
-    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [ @Hl1marks @memb_append_l1 @daemon | >(memb_single … Hx1) % ]
+    [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1
+      [@Hl1marks @memb_append_l1 <(reverse_reverse … l1) @memb_reverse @Hx1 
+      |>(memb_single … Hx1) % ]
     | normalize >associative_append % ] 
     #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] >Houtc
     >reverse_append >reverse_reverse >associative_append >associative_append % ]
@@ -272,6 +277,8 @@ lemma inj_append_singleton_l2 :
 >reverse_append >reverse_append normalize #H1 destruct %
 qed.
 
+axiom daemon : ∀P:Prop.P.
+
 lemma wsem_copy0 : WRealize ? copy0 R_copy0.
 #intape #k #outc #Hloop 
 lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
@@ -292,7 +299,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
   #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
+  cut (|l1| = |reverse ? l4|) [>length_reverse @Hlen] #Hlen1
   @(list_cases2 … Hlen1)
   [ (* case l1 = [] is discriminated because l1 contains at least comma *)
     #Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize