From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 7 May 2012 15:34:16 +0000 (+0000)
Subject: progress
X-Git-Tag: make_still_working~1768
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c1794aba0652c0b0bce80a9ffc426192327709f;p=helm.git

progress
---

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index a9092336d..5813606a1 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -156,6 +156,18 @@ let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
   ].
   
+lemma loop_S_true : 
+  ∀A,n,f,p,a.  p a = true → 
+  loop A (S n) f p a = Some ? a.
+#A #n #f #p #a #pa normalize >pa //
+qed.
+
+lemma loop_S_false : 
+  ∀A,n,f,p,a.  p a = false → 
+  loop A (S n) f p a = loop A n f p (f a).
+normalize #A #n #f #p #a #Hpa >Hpa %
+qed.  
+  
 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2. 
   loop A k1 f p a1 = Some ? a2 → 
     loop A (k2+k1) f p a1 = Some ? a2.
diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma
index 6bd3cef9b..f970da13e 100644
--- a/matita/matita/lib/turing/universal/move_char_c.ma
+++ b/matita/matita/lib/turing/universal/move_char_c.ma
@@ -107,24 +107,13 @@ definition Rmcc_step_false ≝
     left ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
       current alpha t1 = Some alpha sep ∧ t2 = t1.
     
-lemma loop_S_true : 
-  ∀A,n,f,p,a.  p a = true → 
-  loop A (S n) f p a = Some ? a. /2/
-qed.
-
-lemma loop_S_false : 
-  ∀A,n,f,p,a.  p a = false → 
-  loop A (S n) f p a = loop A n f p (f a).
-normalize #A #n #f #p #a #Hpa >Hpa %
-qed.
-
-lemma trans_init_sep: 
+lemma mcc_trans_init_sep: 
   ∀alpha,sep,x.
   trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
 #alpha #sep #x normalize >(\b ?) //
 qed.
  
-lemma trans_init_not_sep: 
+lemma mcc_trans_init_not_sep: 
   ∀alpha,sep,x,y.y == sep = false → 
   trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉.
 #alpha #sep #x #y #H1 normalize >H1 //
@@ -149,8 +138,8 @@ lemma sem_mcc_step :
     @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
     % [ % 
         [ >(\P Hc) >loop_S_false // >loop_S_true 
-         [ @eq_f whd in ⊢ (??%?); >trans_init_sep %
-         |>(\P Hc) whd in ⊢(??(???(???%))?); >trans_init_sep % ]
+         [ @eq_f whd in ⊢ (??%?); >mcc_trans_init_sep %
+         |>(\P Hc) whd in ⊢(??(???(???%))?); >mcc_trans_init_sep % ]
         |   #Hfalse destruct ]
       |#_ #H1 #H2 % // normalize >(\P Hc) % ]
   | @(ex_intro ?? 4) cases lt
@@ -185,7 +174,7 @@ definition R_move_char_c ≝
      b ≠ sep → memb ? sep rs1 = false → 
      t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
     
-lemma sem_while_move_char :
+lemma sem_move_char_c :
   ∀alpha,sep.
   WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
 #alpha #sep #inc #i #outc #Hloop
diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma
index 8b97dee55..a35d714d8 100644
--- a/matita/matita/lib/turing/universal/move_char_l.ma
+++ b/matita/matita/lib/turing/universal/move_char_l.ma
@@ -86,7 +86,7 @@ lemma mcl_q1_q2 :
 #alpha #sep #a #ls #a0 * //
 qed.
 
-lemma mcc_q2_q3 :
+lemma mcl_q2_q3 :
   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
   step alpha (mcl_step alpha sep) 
     (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = 
@@ -119,9 +119,6 @@ lemma mcl_trans_init_not_sep:
 #alpha #sep #x #y #H1 normalize >H1 //
 qed.
 
-(*
-STOP
-
 lemma sem_mcl_step :
   ∀alpha,sep.
   accRealize alpha (mcl_step alpha sep) 
@@ -131,32 +128,32 @@ lemma sem_mcl_step :
   @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?)))
   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
 |#l0 #lt0 @(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? l0 lt0)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
+  @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0)))
+  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 |#r0 #rt0 @(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? r0 rt0)))
+  @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0)))
   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
   [ @(ex_intro ?? 2) 
     @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
     % [ % 
         [ >(\P Hc) >loop_S_false // >loop_S_true 
-         [ @eq_f whd in ⊢ (??%?); >trans_init_sep %
-         |>(\P Hc) whd in ⊢(??(???(???%))?); >trans_init_sep % ]
+         [ @eq_f whd in ⊢ (??%?); >mcl_trans_init_sep %
+         |>(\P Hc) whd in ⊢(??(???(???%))?); >mcl_trans_init_sep % ]
         |   #Hfalse destruct ]
       |#_ #H1 #H2 % // normalize >(\P Hc) % ]
-  | @(ex_intro ?? 4) cases lt
+  | @(ex_intro ?? 4) cases rt
     [ @ex_intro
       [|% [ %
             [ >loop_S_false // >mcc_q0_q1 //
             | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
           | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
-    | #l0 #lt @ex_intro
+    | #r0 #rt0 @ex_intro
       [| % [ %
              [ >loop_S_false // >mcc_q0_q1 //
-             | #_ #a #b #ls #rs #Hb destruct % 
+             | #_ #a #b #ls #rs #Hb destruct (Hb) % 
                [ @(\Pf Hc)
-               | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ]
+               | >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ]
            | normalize in ⊢ (% → ?); * #Hfalse
              @False_ind /2/ ]
      ]
@@ -166,22 +163,22 @@ lemma sem_mcl_step :
 qed.
 
 (* the move_char (variant c) machine *)
-definition move_char_c ≝ 
-  λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉.
+definition move_char_l ≝ 
+  λalpha,sep.whileTM alpha (mcl_step alpha sep) 〈3,sep〉.
 
-definition R_move_char_c ≝ 
+definition R_move_char_l ≝ 
   λalpha,sep,t1,t2.
-    ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs → 
+    ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) → 
     (b = sep → t2 = t1) ∧
-    (∀rs1,rs2.rs = rs1@sep::rs2 → 
-     b ≠ sep → memb ? sep rs1 = false → 
-     t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
+    (∀ls1,ls2.ls = ls1@sep::ls2 → 
+     b ≠ sep → memb ? sep ls1 = false → 
+     t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
     
-lemma sem_while_move_char :
+lemma sem_move_char_l :
   ∀alpha,sep.
-  WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
+  WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
 #alpha #sep #inc #i #outc #Hloop
-lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
+lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
@@ -201,24 +198,49 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
   #Ha0 #Htapeb %
   [ #Hfalse @False_ind @(absurd ?? Ha0) //
   | *
-    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize
-      >Hrs in Htapeb; normalize #Htapeb
+    [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_ normalize
+      >Hls in Htapeb; normalize #Htapeb
       cases (IH … Htapeb)
       #Houtc #_ >Houtc //
-    | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
-      cut (r0 ≠ sep ∧ memb … sep rs0 = false)
+    | #l0 #ls0 #ls2 #Hls #_ #Hls0
+      cut (l0 ≠ sep ∧ memb … sep ls0 = false)
       [ %
-         [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
-         | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
+         [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
+         | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
            [ destruct
            | @Hfalse ]
          ]
       ] *
-      #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
+      #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
       normalize in ⊢ (%→?); #Htapeb
       cases (IH … Htapeb) -IH #_ #IH 
       >reverse_cons >associative_append @IH //
     ]
   ]
 qed.
-*)
\ No newline at end of file
+
+lemma terminate_move_char_l :
+  ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) → 
+  (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
+#alpha #sep #t #b #a #ls #rs #Ht #Hsep
+@(terminate_while … (sem_mcl_step alpha sep))
+  [%
+  |generalize in match Hsep; -Hsep
+   generalize in match Ht; -Ht
+   generalize in match rs; -rs
+   generalize in match a; -a
+   generalize in match b; -b
+   generalize in match t; -t
+   elim ls 
+    [#t #b #a #rs #Ht #Hsep % #tinit 
+     whd in ⊢ (%→?); #H @False_ind
+     cases (H … Ht) #Hb #_ cases Hb #eqb @eqb 
+     cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
+    |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
+     whd in ⊢ (%→?); #H 
+     cases (H … Ht) #Hbsep #Htinit
+     @(Hind … Htinit) cases Hsep 
+      [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
+        [#eqsep %1 >(\P eqsep) // | #H %2 //]
+  ]
+qed.
\ No newline at end of file