X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;h=4f1977dd47ec3ea8b7a2d6afaac77acde3f87e35;hb=e47584d3cc500acd8ffb533810daabd3b2ff8300;hp=1d873ee86136796894b1e4d6f3fd5ba1c9561487;hpb=d17dfeccb51f1dd6f94645018c15078ef4d329a4;p=helm.git

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 1d873ee86..4f1977dd4 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -21,8 +21,8 @@ definition write ≝ λalpha,c.
   mk_TM alpha write_states
   (λp.let 〈q,a〉 ≝ p in
     match pi1 … q with 
-    [ O ⇒ 〈wr1,Some ? 〈c,N〉〉
-    | S _ ⇒ 〈wr1,None ?〉 ])
+    [ O ⇒ 〈wr1,Some ? c,N〉
+    | S _ ⇒ 〈wr1,None ?,N〉 ])
   wr0 (λx.x == wr1).
   
 definition R_write ≝ λalpha,c,t1,t2.
@@ -43,29 +43,35 @@ definition move_r ≝
   λalpha:FinSet.mk_TM alpha move_states
   (λp.let 〈q,a〉 ≝ p in
     match a with
-    [ None ⇒ 〈move1,None ?〉
+    [ None ⇒ 〈move1,None ?,N〉
     | Some a' ⇒ match (pi1 … q) with
-      [ O ⇒ 〈move1,Some ? 〈a',R〉〉
-      | S q ⇒ 〈move1,None ?〉 ] ])
+      [ O ⇒ 〈move1,Some ? a',R〉
+      | S q ⇒ 〈move1,None ?,N〉 ] ])
   move0 (λq.q == move1).
   
 definition R_move_r ≝ λalpha,t1,t2.
+  (current ? t1 = None ? → t1 = t2) ∧  
   ∀ls,c,rs.
-  t1 = midtape alpha ls c rs → 
-  t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
+    t1 = midtape alpha ls c rs → 
+    t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
+(*
+  (current ? t1 = None ? ∧ t1 = t2) ∨ 
+  ∃ls,c,rs.
+  t1 = midtape alpha ls c rs ∧ 
+  t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
     
 lemma sem_move_r :
   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
 #alpha #intape @(ex_intro ?? 2) cases intape
 [ @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 | #ls #c #rs
-  @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
-  cases rs0 // ] ] ]
+  @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
+  #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
 qed.
 
 (******************** moves the head one step to the left *********************)
@@ -74,29 +80,30 @@ definition move_l ≝
   λalpha:FinSet.mk_TM alpha move_states
   (λp.let 〈q,a〉 ≝ p in
     match a with
-    [ None ⇒ 〈move1,None ?〉
+    [ None ⇒ 〈move1,None ?,N〉
     | Some a' ⇒ match pi1 … q with
-      [ O ⇒ 〈move1,Some ? 〈a',L〉〉
-      | S q ⇒ 〈move1,None ?〉 ] ])
+      [ O ⇒ 〈move1,Some ? a',L〉
+      | S q ⇒ 〈move1,None ?,N〉 ] ])
   move0 (λq.q == move1).
-  
+
 definition R_move_l ≝ λalpha,t1,t2.
+  (current ? t1 = None ? → t1 = t2) ∧  
   ∀ls,c,rs.
-  t1 = midtape alpha ls c rs → 
-  t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
+    t1 = midtape alpha ls c rs → 
+    t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
     
 lemma sem_move_l :
   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
 #alpha #intape @(ex_intro ?? 2) cases intape
 [ @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 |#a #al @ex_intro
-  [| % [ % | #ls #c #rs #Hfalse destruct ] ]
+  [| % [ % | % // #ls #c #rs #H destruct ] ]
 | #ls #c #rs
-  @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
-  cases ls0 // ] ] ]
+  @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
+  #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 qed.
 
 (********************************* test char **********************************)
@@ -118,20 +125,20 @@ definition test_char ≝
   mk_TM alpha tc_states
   (λp.let 〈q,a〉 ≝ p in
    match a with
-   [ None ⇒ 〈tc_true, None ?〉
+   [ None ⇒ 〈tc_false, None ?,N〉
    | Some a' ⇒ 
      match test a' with
-     [ true ⇒ 〈tc_true,None ?〉
-     | false ⇒ 〈tc_false,None ?〉 ]])
+     [ true ⇒ 〈tc_true,None ?,N〉
+     | false ⇒ 〈tc_false,None ?,N〉 ]])
   tc_start (λx.notb (x == tc_start)).
 
 definition Rtc_true ≝ 
   λalpha,test,t1,t2.
-   ∀c. current alpha t1 = Some ? c → test c = true ∧ t2 = t1.
+   (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
    
 definition Rtc_false ≝ 
   λalpha,test,t1,t2.
-    ∀c. current alpha t1 = Some ? c → test c = false ∧ t2 = t1.
+    (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
      
 lemma tc_q0_q1 :
   ∀alpha,test,ls,a0,rs. test a0 = true → 
@@ -159,19 +166,19 @@ lemma sem_test_char :
     tc_true (Rtc_true alpha test) (Rtc_false alpha test).
 #alpha #test *
 [ @(ex_intro ?? 2)
-  @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) %
-  [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
-| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al)))
-  % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
-| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al)))
-  % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+  @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
+  [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
+  % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
+  % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 | #ls #c #rs @(ex_intro ?? 2)
   cases (true_or_false (test c)) #Htest
   [ @(ex_intro ?? (mk_config ?? tc_true ?))
     [| % 
       [ % 
         [ whd in ⊢ (??%?); >tc_q0_q1 //
-        | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
+        | #_ % // @(ex_intro … c) /2/]
       | * #Hfalse @False_ind @Hfalse % ]
     ]
   | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
@@ -179,12 +186,38 @@ lemma sem_test_char :
     [ %
       [ whd in ⊢ (??%?); >tc_q0_q2 //
       | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
-    | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
+    | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
     ]
   ]
 ]
 qed.
 
+lemma test_char_inv : 
+  ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
+#sig #P #f #t #t0 #HPt * #_ //
+qed.
+
+definition test_null ≝ λalpha.test_char alpha (λ_.true).
+
+definition R_test_null_true ≝ λalpha,t1,t2.
+  current alpha t1 ≠ None ? ∧ t1 = t2.
+  
+definition R_test_null_false ≝ λalpha,t1,t2.
+  current alpha t1 = None ? ∧ t1 = t2.
+  
+lemma sem_test_null : ∀alpha.
+  test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
+#alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
+#Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
+  [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
+| #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
+  [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd 
+    lapply (Habsurd ? (refl ??)) #H destruct (H)
+  | <Houtc % ] ]
+qed.
+
 (************************************* swap ***********************************)
 definition swap_states : FinSet → FinSet ≝ 
   λalpha:FinSet.FinProd (initN 4) alpha.
@@ -194,46 +227,100 @@ definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
 
-definition swap ≝ 
+definition swap_r ≝ 
  λalpha:FinSet.λfoo:alpha.
  mk_TM alpha (swap_states alpha)
  (λp.let 〈q,a〉 ≝ p in
   let 〈q',b〉 ≝ q in
-  let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *)
+  let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
-  [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
+  [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
   | Some a' ⇒ 
   match q' with
-  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',R〉〉  (* save in register and move R *)
+  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉  (* save in register and move R *)
   | S q' ⇒ match q' with
-    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,L〉〉 (* swap with register and move L *)
+    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
     | S q' ⇒ match q' with
-      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
-      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
+      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
       ]
     ]
   ]])
   〈swap0,foo〉
   (λq.\fst q == swap3).
-
-definition Rswap ≝ 
+  
+definition Rswap_r ≝ 
   λalpha,t1,t2.
-   ∀a,b,ls,rs.  
-    t1 = midtape alpha ls b (a::rs) → 
-    t2 = midtape alpha ls a (b::rs).
+    (∀b,ls.
+      t1 = midtape alpha ls b [ ] → 
+      t2 = rightof ? b ls) ∧
+    (∀a,b,ls,rs. 
+      t1 = midtape alpha ls b (a::rs) → 
+      t2 = midtape alpha ls a (b::rs)).
 
-lemma sem_swap : ∀alpha,foo.
-  swap alpha foo ⊨ Rswap alpha. 
+lemma sem_swap_r : ∀alpha,foo.
+  swap_r alpha foo ⊨ Rswap_r alpha. 
 #alpha #foo *
   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
-   % [% |#a #b #ls #rs #H destruct]
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
-   % [% |#a #b #ls #rs #H destruct] 
+   % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
-   % [% |#a #b #ls #rs #H destruct] 
+   % [% |% [#b #ls | #a #b #ls #rs] #H destruct] 
   | #lt #c #rt @(ex_intro ?? 4) cases rt
-    [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
-    |#r0 #rt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
+    [@ex_intro [|% [ % | %
+      [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+    |#r0 #rt0 @ex_intro [| % [ % | %
+      [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
     ]
   ]
 qed.
+
+definition swap_l ≝ 
+ λalpha:FinSet.λfoo:alpha.
+ mk_TM alpha (swap_states alpha)
+ (λp.let 〈q,a〉 ≝ p in
+  let 〈q',b〉 ≝ q in
+  let q' ≝ pi1 nat (λi.i<4) q' in
+  match a with 
+  [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
+  | Some a' ⇒ 
+  match q' with
+  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉  (* save in register and move L *)
+  | S q' ⇒ match q' with
+    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
+    | S q' ⇒ match q' with
+      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
+      ]
+    ]
+  ]])
+  〈swap0,foo〉
+  (λq.\fst q == swap3).
+
+definition Rswap_l ≝ 
+  λalpha,t1,t2.
+   (∀b,rs.  
+     t1 = midtape alpha [ ] b rs → 
+     t2 = leftof ? b rs) ∧
+   (∀a,b,ls,rs.  
+      t1 = midtape alpha (a::ls) b rs → 
+      t2 = midtape alpha (b::ls) a rs).
+
+lemma sem_swap_l : ∀alpha,foo.
+  swap_l alpha foo ⊨ Rswap_l alpha. 
+#alpha #foo *
+  [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
+   % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
+  |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
+   % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
+  |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
+   % [% |% [#b #rs | #a #b #ls #rs] #H destruct] 
+  | #lt #c #rt @(ex_intro ?? 4) cases lt
+    [@ex_intro [|% [ % | %
+      [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
+    |#r0 #rt0 @ex_intro [| % [ % | %
+      [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
+    ]
+  ]
+qed.
\ No newline at end of file