progress in turing/universal/compare.ma

diff --git a/matita/matita/lib/turing/universal/compare.ma b/matita/matita/lib/turing/universal/compare.ma
index 4b29f4cf48698e4c814083c59d536ce28292397e..b3fa840dcb2fa1ff7a5850d2eeb2a5be2394c1ad 100644 (file)
--- a/matita/matita/lib/turing/universal/compare.ma
+++ b/matita/matita/lib/turing/universal/compare.ma
@@ -103,6 +103,85 @@ lemma sem_atmr_step :
 ]
 qed.
 
+(*
+definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
+  ∀ls,c,rs.
+  t1 = mk_tape alpha ls c rs  → 
+  (c = None ? ∧ t2 = t1) ∨  
+  (∃c'.c = Some ? c' ∧
+    ((test c' = true ∧ t2 = t1) ∨
+     (test c' = false ∧
+       (((∀x.memb ? x rs = true → test x = false) ∧
+         t2 = mk_tape ? (reverse ? rs@c'::ls) (None ?) []) ∨
+        (∃rs1,b,rs2.rs = rs1@b::rs2 ∧
+         test b = true ∧ (∀x.memb ? x rs1 = true → test x = false) ∧
+         t2 = midtape ? (reverse ? rs1@c'::rs) b rs2))))).
+     
+definition adv_to_mark_r ≝ 
+  λalpha,test.whileTM alpha (atmr_step alpha test) 2.
+
+lemma wsem_adv_to_mark_r :
+  ∀alpha,test.
+  WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
+#alpha #test #t #i #outc #Hloop
+lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
+-Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
+[ #tapea * #Htapea *
+  [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
+    #Hfalse destruct (Hfalse)
+  | * #a * #Ha #Htest #ls #c #rs cases c
+    [ #Htapea' % % // >Htapea %
+    | #c' #Htapea' %2 @(ex_intro ?? c') % //
+      cases (true_or_false (test c')) #Htestc
+      [ % % // >Htapea %
+      | %2 % // generalize in match Htapea'; -Htapea'
+        cases rs
+        [ #Htapea' % %
+          [ normalize #x #Hfalse destruct (Hfalse)
+          | <Htapea >Htapea' % 
+    
+    
+   #H2 %
+    >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % // <Htapea //
+  ]
+| #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
+  lapply (IH HRfalse) -IH #IH
+  #ls #c #rs #Htapea
+  cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
+  >Htapea' in Htapea; #Htapea destruct (Htapea) %2 % //
+  generalize in match Htapeb; -Htapeb
+  generalize in match Htapea'; -Htapea'
+  cases rs
+  [ #Htapea #Htapeb % %
+    [ #x0 normalize #Hfalse destruct (Hfalse)
+    | normalize in Htapeb; cases (IH
+  
+  
+   [//]  
+   cases (true_or_false (test c))
+  [ #Htestc %
+  
+  
+  [ #Htapea %2 % [ %2 // ]
+    #rs #Htapea %2
+  
+
+   *
+  [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
+    cases (IH … Htapeb)
+    [ * #_ #Houtc >Houtc >Htapeb %
+    | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
+  | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
+    cases (IH … Htapeb)
+    [ * #Hfalse >(Hmemb …) in Hfalse;
+      [ #Hft destruct (Hft)
+      | @memb_hd ]
+    | * #Htestr1 #H1 >reverse_cons >associative_append
+      @H1 // #x #Hx @Hmemb @memb_cons //
+    ]
+  ]
+qed. *)
+
 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
   ∀ls,c,rs.
   (t1 = midtape alpha ls c rs  → 
@@ -115,7 +194,7 @@ definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 definition adv_to_mark_r ≝ 
   λalpha,test.whileTM alpha (atmr_step alpha test) 2.
 
-lemma sem_adv_to_mark_r :
+lemma wsem_adv_to_mark_r :
   ∀alpha,test.
   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 #alpha #test #t #i #outc #Hloop
@@ -151,43 +230,252 @@ qed.
 
 lemma terminate_adv_to_mark_r :
   ∀alpha,test.
-  ∀t. (* ∀b,a,ls,rs. t = midtape alpha (a::ls) b rs →  
-    (b = sep ∨ memb ? sep rs = true) →  *)
-  Terminate alpha (adv_to_mark_r alpha test) t.
+  ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 #alpha #test #t
 @(terminate_while … (sem_atmr_step alpha test))
   [ %
-  | % #t1 whd in ⊢ (% → ?); * #ls * #c * #rs
-    * * generalize in match c; generalize in match ls;
-    -ls -c elim rs
-    [ #ls #c #Ht #Hc #Ht1
-      % >Ht1 #t2 * #ls0 * #c0 * #rs0 * *
-      normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
-    
-        
-     #Ht #Hc #t1
-    elim t 
-    [ % #a whd in ⊢ (% → ?);
-
- #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcc_step alpha sep))
-  [%
-  |generalize in match Hsep; -Hsep
-   generalize in match Ht; -Ht
-   generalize in match ls; -ls
-   generalize in match a; -a
-   generalize in match b; -b
-   generalize in match t; -t
-   elim rs 
-    [#t #b #a #ls #Ht #Hsep % #tinit 
-     whd in ⊢ (%→?); #H @False_ind
-     cases (H … Ht) #Hb #_ cases Hb #eqb @eqb 
-     cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
-    |#r0 #rs0 #Hind #t #b #a #ls #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 //]
+  | cases t
+    [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse) 
+    |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse) 
+    | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
+      elim rs
+      [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
+       #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1; 
+       % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
+       normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+      | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
+        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
+        >Ht1 @IH
+      ]
+    ]
+  ]
+qed.
+
+lemma sem_adv_to_mark_r :
+  ∀alpha,test.
+  Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
+/2/
+qed.
+
+(* NO OPERATION
+
+  t1 = t2
+  *)
+  
+definition nop_states ≝ initN 1.
+
+definition nop ≝ 
+  λalpha:FinSet.mk_TM alpha nop_states
+  (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
+  O (λ_.true).
+  
+definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
+
+lemma sem_nop :
+  ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
+#alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
+qed.
+
+(*
+   q0 _ → q1, R
+   q1 〈a,false〉 → qF, 〈a,true〉, N
+   q1 〈a,true〉 → qF, _ , N
+   qF _ → None ?
+ *)
+ 
+definition mark_states ≝ initN 3.
+
+definition mark ≝ 
+  λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
+  (λp.let 〈q,a〉 ≝ p in
+    match a with
+    [ None ⇒ 〈2,None ?〉
+    | Some a' ⇒ match q with
+      [ O ⇒ 〈1,Some ? 〈a',R〉〉
+      | S q ⇒ match q with
+        [ O ⇒ let 〈a'',b〉 ≝ a' in
+              〈2,Some ? 〈〈a'',true〉,N〉〉
+        | S _ ⇒ 〈2,None ?〉 ] ] ])
+  O (λq.q == 2).
+  
+definition R_mark ≝ λalpha,t1,t2.
+  ∀ls,c,d,b,rs.
+  t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) → 
+  t2 = midtape ? (c::ls) 〈d,true〉 rs.
+  
+(*lemma mark_q0_q1 : 
+  ∀alpha,ls,c,rs.
+  step alpha (mark alpha)
+    (mk_config ?? 0 (midtape … ls c rs)) =
+  mk_config alpha (states ? (mark alpha)) 1
+    (midtape … (ls a0 rs).*)
+  
+lemma sem_mark :
+  ∀alpha.Realize ? (mark alpha) (R_mark alpha).
+#alpha #intape @(ex_intro ?? 3) cases intape
+[ @ex_intro
+  [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
+|#a #al @ex_intro
+  [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
+|#a #al @ex_intro
+  [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
+| #ls #c *
+  [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
+  | * #d #b #rs @ex_intro
+    [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
+qed.
+
+include "turing/if_machine.ma".
+
+(* TEST CHAR 
+
+   stato finale diverso a seconda che il carattere 
+   corrente soddisfi un test booleano oppure no  
+   
+   q1 = true or no current char
+   q2 = false
+*)
+
+definition tc_states ≝ initN 3.
+
+definition test_char ≝ 
+  λalpha:FinSet.λtest:alpha→bool.
+  mk_TM alpha tc_states
+  (λp.let 〈q,a〉 ≝ p in
+   match a with
+   [ None ⇒ 〈1, None ?〉
+   | Some a' ⇒ 
+     match test a' with
+     [ true ⇒ 〈1,None ?〉
+     | false ⇒ 〈2,None ?〉 ]])
+  O (λx.notb (x == 0)).
+
+definition Rtc_true ≝ 
+  λalpha,test,t1,t2.
+   ∀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.
+     
+lemma tc_q0_q1 :
+  ∀alpha,test,ls,a0,rs. test a0 = true → 
+  step alpha (test_char alpha test)
+    (mk_config ?? 0 (midtape … ls a0 rs)) =
+  mk_config alpha (states ? (test_char alpha test)) 1
+    (midtape … ls a0 rs).
+#alpha #test #ls #a0 #ts #Htest normalize >Htest %
+qed.
+     
+lemma tc_q0_q2 :
+  ∀alpha,test,ls,a0,rs. test a0 = false → 
+  step alpha (test_char alpha test)
+    (mk_config ?? 0 (midtape … ls a0 rs)) =
+  mk_config alpha (states ? (test_char alpha test)) 2
+    (midtape … ls a0 rs).
+#alpha #test #ls #a0 #ts #Htest normalize >Htest %
+qed.
+
+lemma sem_test_char :
+  ∀alpha,test.
+  accRealize alpha (test_char alpha test) 
+    1 (Rtc_true alpha test) (Rtc_false alpha test).
+#alpha #test *
+[ @(ex_intro ?? 2)
+  @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
+  [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
+  % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
+  % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+| #ls #c #rs @(ex_intro ?? 2)
+  cases (true_or_false (test c)) #Htest
+  [ @(ex_intro ?? (mk_config ?? 1 ?))
+    [| % 
+      [ % 
+        [ whd in ⊢ (??%?); >tc_q0_q1 //
+        | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
+      | * #Hfalse @False_ind @Hfalse % ]
+    ]
+  | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
+    % 
+    [ %
+      [ whd in ⊢ (??%?); >tc_q0_q2 //
+      | #Hfalse destruct (Hfalse) ]
+    | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
+    ]
   ]
-qed.
\ No newline at end of file
+]
+qed.
+
+axiom myalpha : FinSet.
+axiom is_bar : FinProd … myalpha FinBool → bool.
+axiom is_grid : FinProd … myalpha FinBool → bool.
+definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
+axiom bar : FinProd … myalpha FinBool.
+axiom grid : FinProd … myalpha FinBool.
+
+definition mark_next_tuple ≝ 
+  seq ? (adv_to_mark_r ? bar_or_grid)
+     (ifTM ? (test_char ? is_bar)
+       (mark ?) (nop ?) 1).
+
+definition R_mark_next_tuple ≝ 
+  λt1,t2.
+    ∀ls,c,rs1,rs2.
+    (* c non può essere un separatore ... speriamo *)
+    t1 = midtape ? ls c (rs1@grid::rs2) → 
+    memb ? grid rs1 = false → bar_or_grid c = false → 
+    (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: 〈d,b〉:: rs4 ∧
+      memb ? bar rs3 = false ∧ 
+      t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (rs4@grid::rs2))
+    ∨
+    (memb ? bar rs1 = false ∧ 
+     t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
+     
+axiom tech_split :
+  ∀A:DeqSet.∀f,l.
+   (∀x.memb A x l = true → f x = false) ∨
+   (∃l1,c,l2.f c = true ∧ l = l1@c::l2).
+(*#A #f #l elim l
+[ % #x normalize #Hfalse *)
+     
+theorem sem_mark_next_tuple :
+  Realize ? mark_next_tuple R_mark_next_tuple.
+#intape 
+lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
+         (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
+[@sem_if //
+| //
+|||#Hif cases (Hif intape) -Hif
+   #j * #outc * #Hloop * #ta * #Hleft #Hright
+   @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
+   -Hloop
+   #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
+   cases (Hleft … Hrs)
+   [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
+   | * #_ #Hta cases (tech_split ? is_bar rs1)
+     [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
+       [ @daemon
+       | @daemon
+       | -Hta #Hta cases Hright
+         [ * #tb * whd in ⊢ (%→?); #Hcurrent
+           @False_ind cases(Hcurrent grid ?)
+           [ #Hfalse (* grid is not a bar *) @daemon
+           | >Hta % ]
+         | * #tb * whd in ⊢ (%→?); #Hcurrent
+           cases (Hcurrent grid ?)
+           [  #_ #Htb whd in ⊢ (%→?); #Houtc
+             %2 %
+             [ (* H1 *) @daemon
+             | >Houtc >Htb >Hta % ]
+           | >Hta % ]
+         ]
+       ]
+    | STOP
+    ]
+  ]
+qed.
+