Forgotten in previous commit: move_char machines.

diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma
new file mode 100644 (file)
index 0000000..685f327
--- /dev/null
+++ b/matita/matita/lib/turing/universal/move_char_c.ma
@@ -0,0 +1,231 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+
+(* MOVE_CHAR (variant c) MACHINE
+
+Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
+
+Input:
+(ls,cs,rs can be empty; # is a parameter)
+
+  ls x cs # rs
+       ^
+       H
+
+Output:
+  ls cs x # rs
+        ^
+        H
+
+Initial state = 〈0,#〉
+Final state = 〈4,#〉
+
+*)
+
+include "turing/while_machine.ma".
+
+definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
+
+definition mcc_step ≝ 
+ λalpha:FinSet.λsep:alpha.
+ mk_TM alpha (mcc_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  match a with 
+  [ None ⇒ 〈〈4,sep〉,None ?〉 
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* qinit *)
+    match a' == sep with
+    [ true ⇒ 〈〈4,sep〉,None ?〉
+    | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ]
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *)
+      〈〈2,a'〉,Some ? 〈b,R〉〉
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *)
+        〈〈3,sep〉,Some ? 〈b,R〉〉
+      | S q' ⇒ match q' with
+        [ O ⇒ (* qacc *)
+          〈〈3,sep〉,None ?〉
+        | S q' ⇒ (* qfail *)
+          〈〈4,sep〉,None ?〉 ] ] ] ] ])
+  〈0,sep〉
+  (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
+
+lemma mcc_q0_q1 : 
+  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
+  a0 == sep = false → 
+  step alpha (mcc_step alpha sep)
+    (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
+  mk_config alpha (states ? (mcc_step alpha sep)) 〈1,a0〉
+    (tape_move_left alpha ls a0 rs).
+#alpha #sep #a *
+[ #a0 #rs #Ha0 whd in ⊢ (??%?); 
+  normalize in match (trans ???); >Ha0 %
+| #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
+  normalize in match (trans ???); >Ha0 %
+]
+qed.
+    
+lemma mcc_q1_q2 :
+  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
+  step alpha (mcc_step alpha sep) 
+    (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = 
+  mk_config alpha (states ? (mcc_step alpha sep)) 〈2,a0〉 
+    (tape_move_right alpha ls a rs).
+#alpha #sep #a #ls #a0 * //
+qed.
+
+lemma mcc_q2_q3 :
+  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
+  step alpha (mcc_step alpha sep) 
+    (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = 
+  mk_config alpha (states ? (mcc_step alpha sep)) 〈3,sep〉 
+    (tape_move_right alpha ls a rs).
+#alpha #sep #a #ls #a0 * //
+qed.
+
+definition Rmcc_step_true ≝ 
+  λalpha,sep,t1,t2.
+   ∀a,b,ls,rs.  
+    t1 = midtape alpha (a::ls) b rs → 
+    b ≠ sep ∧
+    t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
+
+definition Rmcc_step_false ≝ 
+  λalpha,sep,t1,t2.
+    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: 
+  ∀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: 
+  ∀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 //
+qed.
+
+lemma sem_mcc_step :
+  ∀alpha,sep.
+  accRealize alpha (mcc_step alpha sep) 
+    〈3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep).
+#alpha #sep *
+[@(ex_intro ?? 2)  
+  @(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〉 (leftof ? l0 lt0)))
+  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
+|#r0 #rt0 @(ex_intro ?? 2)  
+  @(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 % ]
+        |   #Hfalse destruct ]
+      |#_ #H1 #H2 % // normalize >(\P Hc) % ]
+  | @(ex_intro ?? 4) cases lt
+    [ @ex_intro
+      [|% [ %
+            [ >loop_S_false // >mcc_q0_q1 //
+            | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+          | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
+    | #l0 #lt @ex_intro
+      [| % [ %
+             [ >loop_S_false // >mcc_q0_q1 //
+             | #_ #a #b #ls #rs #Hb destruct % 
+               [ @(\Pf Hc)
+               | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ]
+           | normalize in ⊢ (% → ?); * #Hfalse
+             @False_ind /2/ ]
+     ]
+   ]
+ ]
+]
+qed.
+
+(* the move_char (variant c) machine *)
+definition move_char_c ≝ 
+  λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉.
+
+definition R_move_char_c ≝ 
+  λalpha,sep,t1,t2.
+    ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b 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).
+    
+lemma sem_while_move_char :
+  ∀alpha,sep.
+  WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
+#alpha #sep #inc #i #outc #Hloop
+lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
+-Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
+[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
+  %
+  [ #Hb >Htapea in H1; >Hb normalize in ⊢ (%→?); #H1
+   cases (H1 ??)
+   [#_ #H2 >H2 %
+   |*: % #H2 destruct (H2) ]
+  | #rs1 #rs2 #Hrs #Hb #Hrs1 
+    >Htapea in H1; normalize in ⊢ (% → ?); #H1
+    cases (H1 ??)
+    [ #Hfalse @False_ind @(absurd ?? Hb) destruct %
+    |*:% #H2 destruct (H2) ]
+  ]
+| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
+  lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
+  #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
+  #Ha0 #Htapeb %
+  [ #Hfalse @False_ind @(absurd ?? Ha0) //
+  | *
+    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize
+      >Hrs in Htapeb; normalize #Htapeb
+      cases (IH … Htapeb)
+      #Houtc #_ >Houtc //
+    | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
+      cut (r0 ≠ sep ∧ memb … sep rs0 = false)
+      [ %
+         [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
+         | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
+           [ destruct
+           | @Hfalse ]
+         ]
+      ] *
+      #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
+      normalize in ⊢ (%→?); #Htapeb
+      cases (IH … Htapeb) -IH #_ #IH 
+      >reverse_cons >associative_append @IH //
+    ]
+  ]
+qed.
\ No newline at end of file

diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma
new file mode 100644 (file)
index 0000000..8b97dee
--- /dev/null
+++ b/matita/matita/lib/turing/universal/move_char_l.ma
@@ -0,0 +1,224 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+
+(* MOVE_CHAR (left) MACHINE
+
+Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
+
+Input:
+(ls,cs,rs can be empty; # is a parameter)
+
+  ls # cs x rs
+        ^
+        H
+
+Output:
+  ls # x cs rs
+       ^
+       H
+
+Initial state = 〈0,#〉
+Final state = 〈4,#〉
+
+*)
+
+include "turing/while_machine.ma".
+
+definition mcl_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
+
+definition mcl_step ≝ 
+ λalpha:FinSet.λsep:alpha.
+ mk_TM alpha (mcl_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  match a with 
+  [ None ⇒ 〈〈4,sep〉,None ?〉 
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* qinit *)
+    match a' == sep with
+    [ true ⇒ 〈〈4,sep〉,None ?〉
+    | false ⇒ 〈〈1,a'〉,Some ? 〈a',R〉〉 ]
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *)
+      〈〈2,a'〉,Some ? 〈b,L〉〉
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *)
+        〈〈3,sep〉,Some ? 〈b,L〉〉
+      | S q' ⇒ match q' with
+        [ O ⇒ (* qacc *)
+          〈〈3,sep〉,None ?〉
+        | S q' ⇒ (* qfail *)
+          〈〈4,sep〉,None ?〉 ] ] ] ] ])
+  〈0,sep〉
+  (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
+
+lemma mcc_q0_q1 : 
+  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
+  a0 == sep = false → 
+  step alpha (mcl_step alpha sep)
+    (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
+  mk_config alpha (states ? (mcl_step alpha sep)) 〈1,a0〉
+    (tape_move_right alpha ls a0 rs).
+#alpha #sep #a *
+[ #a0 #rs #Ha0 whd in ⊢ (??%?); 
+  normalize in match (trans ???); >Ha0 %
+| #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
+  normalize in match (trans ???); >Ha0 %
+]
+qed.
+    
+lemma mcl_q1_q2 :
+  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
+  step alpha (mcl_step alpha sep) 
+    (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = 
+  mk_config alpha (states ? (mcl_step alpha sep)) 〈2,a0〉 
+    (tape_move_left alpha ls a rs).
+#alpha #sep #a #ls #a0 * //
+qed.
+
+lemma mcc_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)) = 
+  mk_config alpha (states ? (mcl_step alpha sep)) 〈3,sep〉 
+    (tape_move_left alpha ls a rs).
+#alpha #sep #a #ls #a0 * //
+qed.
+
+definition Rmcl_step_true ≝ 
+  λalpha,sep,t1,t2.
+   ∀a,b,ls,rs.  
+    t1 = midtape alpha ls b (a::rs) → 
+    b ≠ sep ∧
+    t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
+
+definition Rmcl_step_false ≝ 
+  λalpha,sep,t1,t2.
+    right ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
+      current alpha t1 = Some alpha sep ∧ t2 = t1.
+    
+lemma mcl_trans_init_sep: 
+  ∀alpha,sep,x.
+  trans ? (mcl_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
+#alpha #sep #x normalize >(\b ?) //
+qed.
+ 
+lemma mcl_trans_init_not_sep: 
+  ∀alpha,sep,x,y.y == sep = false → 
+  trans ? (mcl_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,R〉〉.
+#alpha #sep #x #y #H1 normalize >H1 //
+qed.
+
+(*
+STOP
+
+lemma sem_mcl_step :
+  ∀alpha,sep.
+  accRealize alpha (mcl_step alpha sep) 
+    〈3,sep〉 (Rmcl_step_true alpha sep) (Rmcl_step_false alpha sep).
+#alpha #sep *
+[@(ex_intro ?? 2)  
+  @(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) %]
+|#r0 #rt0 @(ex_intro ?? 2)  
+  @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? 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 % ]
+        |   #Hfalse destruct ]
+      |#_ #H1 #H2 % // normalize >(\P Hc) % ]
+  | @(ex_intro ?? 4) cases lt
+    [ @ex_intro
+      [|% [ %
+            [ >loop_S_false // >mcc_q0_q1 //
+            | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+          | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
+    | #l0 #lt @ex_intro
+      [| % [ %
+             [ >loop_S_false // >mcc_q0_q1 //
+             | #_ #a #b #ls #rs #Hb destruct % 
+               [ @(\Pf Hc)
+               | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ]
+           | normalize in ⊢ (% → ?); * #Hfalse
+             @False_ind /2/ ]
+     ]
+   ]
+ ]
+]
+qed.
+
+(* the move_char (variant c) machine *)
+definition move_char_c ≝ 
+  λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉.
+
+definition R_move_char_c ≝ 
+  λalpha,sep,t1,t2.
+    ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b 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).
+    
+lemma sem_while_move_char :
+  ∀alpha,sep.
+  WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
+#alpha #sep #inc #i #outc #Hloop
+lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
+-Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
+[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
+  %
+  [ #Hb >Htapea in H1; >Hb normalize in ⊢ (%→?); #H1
+   cases (H1 ??)
+   [#_ #H2 >H2 %
+   |*: % #H2 destruct (H2) ]
+  | #rs1 #rs2 #Hrs #Hb #Hrs1 
+    >Htapea in H1; normalize in ⊢ (% → ?); #H1
+    cases (H1 ??)
+    [ #Hfalse @False_ind @(absurd ?? Hb) destruct %
+    |*:% #H2 destruct (H2) ]
+  ]
+| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
+  lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
+  #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
+  #Ha0 #Htapeb %
+  [ #Hfalse @False_ind @(absurd ?? Ha0) //
+  | *
+    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize
+      >Hrs in Htapeb; normalize #Htapeb
+      cases (IH … Htapeb)
+      #Houtc #_ >Houtc //
+    | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
+      cut (r0 ≠ sep ∧ memb … sep rs0 = false)
+      [ %
+         [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
+         | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
+           [ destruct
+           | @Hfalse ]
+         ]
+      ] *
+      #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
+      normalize in ⊢ (%→?); #Htapeb
+      cases (IH … Htapeb) -IH #_ #IH 
+      >reverse_cons >associative_append @IH //
+    ]
+  ]
+qed.
+*)
\ No newline at end of file