New notation for congruence

[helm.git] / matita / matita / lib / turing / universal / match_machines.ma

diff --git a/matita/matita/lib/turing/universal/match_machines.ma b/matita/matita/lib/turing/universal/match_machines.ma
index 49f1b69238a630ef6bfc63d655be1977427c8a04..6c7ccc9234a9ae0f52ef9009b797da06c4844c43 100644 (file)
--- a/matita/matita/lib/turing/universal/match_machines.ma
+++ b/matita/matita/lib/turing/universal/match_machines.ma
@@ -287,6 +287,34 @@ definition match_tuple_step ≝
            (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
              (mark ?) (move_l ? · init_current) tc_true)) tc_true)))
     (nop ?) tc_true.
+    
+definition R_match_tuple_step_true_new ≝ λt1,t2.
+  ∃ls,cur,rs.t1 = midtape STape ls cur rs \wedge 
+  \fst cur ≠ grid ∧ 
+  (∀ls0,c,l1,l2,c1,l3,l4,rs0,n.
+   only_bits_or_nulls l1 → no_marks l1 (* → no_grids l2 *) → 
+   bit_or_null c = true → bit_or_null c1 = true →
+   only_bits_or_nulls l3 → S n = |l1| → |l1| = |l3| →
+   table_TM (S n) (l2@〈c1,false〉::l3@〈comma,false〉::l4) → 
+   ls = 〈grid,false〉::ls0 → cur = 〈c,true〉 → 
+   rs = l1@〈grid,false〉::l2@〈c1,true〉::l3@〈comma,false〉::l4@〈grid,false〉::rs0 → 
+   (* facciamo match *)
+   (〈c,false〉::l1 = 〈c1,false〉::l3 ∧
+   t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls0) 〈grid,false〉
+         (l2@〈c1,false〉::l3@〈comma,true〉::l4@〈grid,false〉::rs0))
+   ∨
+   (* non facciamo match e marchiamo la prossima tupla *)
+   (〈c,false〉::l1 ≠ 〈c1,false〉::l3 ∧
+    ∃c2,l5,l6.l4 = l5@〈bar,false〉::〈c2,false〉::l6 ∧
+    (* condizioni su l5 l6 l7 *)
+    t2 = midtape STape (〈grid,false〉::ls0) 〈c,true〉 
+          (l1@〈grid,false〉::l2@〈c1,false〉::l3@〈comma,false〉::
+           l5@〈bar,false〉::〈c2,true〉::l6@〈grid,false〉::rs0))
+   ∨  
+   (* non facciamo match e non c'è una prossima tupla:
+      non specifichiamo condizioni sul nastro di output, perché
+      non eseguiremo altre operazioni, quindi il suo formato non ci interessa *)
+   (〈c,false〉::l1 ≠ 〈c1,false〉::l3 ∧ no_bars l4 ∧ current ? t2 = Some ? 〈grid,true〉)).  
 
 (* universal version 
 definition R_match_tuple_step_true ≝ λt1,t2.
@@ -628,7 +656,7 @@ lemma wsem_match_tuple : WRealize ? match_tuple R_match_tuple0.
 #intape #k #outc #Hloop 
 lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
 * #ta * #Hstar @(star_ind_l ??????? Hstar)
-[ #tb whd in ⊢ (%→?); #Hleft
+[ whd in ⊢ (%→?); #Hleft
   #ls #cur #rs #Htb cases (Hleft … Htb) #Hgrid #Houtc %
   [ #_ @Houtc 
   | #c #l1 #c1 #l2 #l3 #ls0 #rs0 #n #Hls #Hcur #Hrs 
@@ -637,7 +665,7 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
   ]
 | (* in the interesting case, we execute a true iteration, then we restart the
      while cycle, finally we end with a false iteration *)
-  #tb #tc #td whd in ⊢ (%→?); #Htc
+  #tc #td whd in ⊢ (%→?); #Htc
   #Hstar1 #IH whd in ⊢ (%→?); #Hright lapply (IH Hright) -IH whd in ⊢ (%→?); #IH
   #ls #cur #rs #Htb %
   [ (* cur can't be true because we assume at least one iteration *)
@@ -710,16 +738,20 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
    | (* match failed and there is no next tuple: the next while cycle will just exit *)
      * * #Hdiff #Hnobars generalize in match (refl ? tc);
      cases tc in ⊢ (???% → %);
-     [ #_ normalize in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
-     |2,3: #x #xs #_ normalize in ⊢ (??%?→?); #Hfalse destruct (Hfalse) ]
-     #ls1 #cur1 #rs1 #Htc normalize in ⊢ (??%?→?); #Hcur1
+     [ #_ @daemon (* long normalize *) (* 
+          normalize in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
+     *)
+     |2,3: #x #xs #_ @daemon (* long normalize *) (* 
+                     normalize in ⊢ (??%?→?); #Hfalse destruct (Hfalse) *) ]
+     #ls1 #cur1 #rs1 #Htc @daemon (* long normalize *) (* 
+                          normalize in ⊢ (??%?→?); #Hcur1
      cases (IH … Htc) -IH #IH #_ %2 %
      [ destruct (Hcur1) >IH [ >Htc % | % ]
      | #l4 #newc #mv0 #l5
        (* no_bars except the first one, where the tuple does not match ⇒ 
           no match *)
         @daemon
-     ]
+     ] *)
    ]
  ]
 qed.