From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 30 May 2012 14:20:28 +0000 (+0000)
Subject: Progress.
X-Git-Tag: make_still_working~1675
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a386e0eb6b20909ae78c825203d77647b8fde30c;p=helm.git

Progress.
---

diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index d28017acb..dbe481704 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -725,7 +725,7 @@ lemma sem_match_tuple_step:
                 [ >Hrs3 in Heq1; @daemon ] #Hl4
                 @(ex_intro … rs32) @(ex_intro … rs3') % [@Hl4]
                 >Htapeout @eq_f2
-                   [@daemon
+                   [(* by Hoption, H2 *) @daemon
                    |(*>Hrs3 *)>append_cons
                     > (?:l1@〈grid,false〉::l2@〈c1,false〉::l3@〈comma,false〉::rs32@〈bar,false〉::〈d2,true〉::rs3'@〈grid,false〉::rs
                         = (l1@〈grid,false〉::l2@〈c1,false〉::l3@〈comma,false〉::rs32@[〈bar,false〉])@〈d2,true〉::rs3'@〈grid,false〉::rs)
@@ -799,25 +799,6 @@ lemma is_grid_true : ∀c.is_grid c = true → c = grid.
 * normalize [ #b ] #H // destruct (H)
 qed.
 
-definition R_match_tuple ≝ λt1,t2.
-  ∀ls,c,l1,c1,l2,rs,n.
-  is_bit c = true → only_bits l1 → is_bit c1 = true → n = |l1| →
-  table_TM (S n) (〈c1,false〉::l2) → 
-  t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 
-         (l1@〈grid,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → 
-  (* facciamo match *)
-  (∃l3,newc,mv,l4.
-   〈c1,false〉::l2 = l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4 ∧
-   t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉
-        (l3@〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv@l4@〈grid,false〉::rs))
-  ∨
-  (* non facciamo match su nessuna tupla;
-     non specifichiamo condizioni sul nastro di output, perché
-     non eseguiremo altre operazioni, quindi il suo formato non ci interessa *)
-  (current ? t2 = Some ? 〈grid,true〉 ∧
-   ∀l3,newc,mv,l4.
-   〈c1,false〉::l2 ≠ l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv@l4). 
-
 (* possible variante ? 
 definition weakR_match_tuple ≝ λt1,t2.
   (∀ls,cur,rs,b. t1 = midtape STape ls 〈grid,b〉 rs → t2 = t1) ∧
@@ -841,7 +822,7 @@ definition weakR_match_tuple ≝ λt1,t2.
    〈c1,false〉::l3 ≠ l4@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5)).  
 *) 
 
-definition weakR_match_tuple ≝ λt1,t2.
+definition R_match_tuple0 ≝ λt1,t2.
   ∀ls,cur,rs.
   t1 = midtape STape ls cur rs → 
   (is_grid (\fst cur) = true → t2 = t1) ∧
@@ -869,7 +850,7 @@ definition weakR_match_tuple ≝ λt1,t2.
 axiom table_bit_after_bar : 
   ∀n,l1,c,l2.table_TM n (l1@〈bar,false〉::〈c,false〉::l2) → is_bit c = true.
 
-lemma wsem_match_tuple : WRealize ? match_tuple weakR_match_tuple.
+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)
@@ -880,12 +861,17 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
     >Hcur in Hgrid; #Hgrid >(is_grid_true … Hgrid) normalize in ⊢ (%→?);
     #Hc destruct (Hc)
   ]
-| #tb #tc #td whd in ⊢ (%→?); #Htc
+| (* 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
   #Hstar1 #IH whd in ⊢ (%→?); #Hright lapply (IH Hright) -IH whd in ⊢ (%→?); #IH
   #ls #cur #rs #Htb %
-  [ #Hcur cases (Htc … Htb) * #Hfalse @False_ind @Hfalse @(is_grid_true … Hcur)
-  |#c #l1 #c1 #l2 #l3 #ls0 #rs0 #n #Hls #Hcur #Hrs #Hc #Hc1 #Hl1bitnull #Hl1marks 
+  [ (* cur can't be true because we assume at least one iteration *)
+    #Hcur cases (Htc … Htb) * #Hfalse @False_ind @Hfalse @(is_grid_true … Hcur)
+  | (* current and a tuple are marked *)
+   #c #l1 #c1 #l2 #l3 #ls0 #rs0 #n #Hls #Hcur #Hrs #Hc #Hc1 #Hl1bitnull #Hl1marks 
    #Hl1len #Htable cases (Htc … Htb) -Htc -Htb * #_ #Htc
+   (* expose the marked tuple in table *)
    cut (∃la,lb,mv,lc.l3 = la@〈comma,false〉::lb@〈comma,false〉::mv::lc ∧
          S n = |la| ∧ only_bits_or_nulls la)
    [@daemon] * #la * #lb * #mv * #lc * * #Hl3 #Hlalen #Hlabitnull
@@ -900,14 +886,17 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
    |4: whd in ⊢ (??%?); >Hc1 %
    |3: whd in ⊢ (??%?); >Hc %
    |-Htc *
-     [ * #Heq #Htc % %{[]} %{lb} %{mv} %{lc} destruct (Heq) %
+     [ (* case 1: match successful *)
+       * #Heq #Htc % %{[]} %{lb} %{mv} %{lc} destruct (Heq) %
        [%
        | cases (IH … Htc) -IH #Houtc #_ >(Houtc (refl ??)) 
          >Htc @eq_f normalize >associative_append normalize
          >associative_append normalize %
        ]     
-     | * #Hdiff * #c2 * #l5 * #l6 * #Heqlblc #Htc
+     | (* case 2: tuples don't match, we still have other tuples to try *)
+       * #Hdiff * #c2 * #l5 * #l6 * #Heqlblc #Htc
        cases (IH ??? … Htc) -IH #_ #IH 
+       (* by induction hypothesis *)
        lapply (IH ? l1 c2 (l2@〈bar,false〉::〈c1,false〉::la@〈comma,false〉::l5) l6 ? rs0 n (refl ??) (refl ??) ???????)
        [ generalize in match Htable;
          >associative_append normalize 
@@ -922,7 +911,8 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
          >associative_append normalize
          >associative_append %
        |-IH * 
-         [ * #l7 * #newc * #mv0 * #l8 * #Hl7l8 #Houtc %
+         [ (* the while finally matches a tuple *)
+           * #l7 * #newc * #mv0 * #l8 * #Hl7l8 #Houtc %
            >Heqlblc @(ex_intro ?? (〈bar,false〉::〈c1,false〉::la@〈comma,false〉::l5@l7))
            %{newc} %{mv0} %{l8} %
            [ normalize >Hl7l8 >associative_append normalize 
@@ -931,7 +921,8 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
              >associative_append normalize >associative_append 
              normalize >associative_append %
            ]
-         | * #Houtc #Hdiff %2 %
+         | (* the while fails finding a tuple: there are no matches in the whole table *)
+           * #Houtc #Hdiff1 %2 %
            [ @Houtc
            | #l50 #newc #mv0 #l51 >Heqlblc 
              @daemon
@@ -939,20 +930,53 @@ lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop
          ]
        ]
      ]
-   | * * #Hdiff #Hnobars generalize in match (refl ? tc);
+   | (* 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
      cases (IH … Htc) -IH #IH #_ %2 %
      [ destruct (Hcur1) >IH [ >Htc % | % ]
-     | #l4 #newc #mv0 #l5 (* difficile (sempre che sia dimostrabile) 
-          dobbiamo veramente considerare di fare la table in modo più 
-          strutturato
-        *)
+     | #l4 #newc #mv0 #l5
+       (* no_bars except the first one, where the tuple does not match ⇒ 
+          no match *)
         @daemon
      ]
    ]
  ]
 qed.
 
+definition R_match_tuple ≝ λt1,t2.
+  ∀ls,c,l1,c1,l2,rs,n.
+  is_bit c = true → is_bit c1 = true →
+  only_bits_or_nulls l1 → no_marks l1 → S n = |l1| → 
+  table_TM (S n) (〈bar,false〉::〈c1,false〉::l2) → 
+  t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 
+         (l1@〈grid,false〉::〈bar,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → 
+  (* facciamo match *)
+  (∃l3,newc,mv,l4.
+   〈bar,false〉::〈c1,false〉::l2 = l3@〈bar,false〉::〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4 ∧
+   t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉
+        (l3@〈bar,false〉::〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv::l4@〈grid,false〉::rs))
+  ∨
+  (* non facciamo match su nessuna tupla;
+     non specifichiamo condizioni sul nastro di output, perché
+     non eseguiremo altre operazioni, quindi il suo formato non ci interessa *)
+  (current ? t2 = Some ? 〈grid,true〉 ∧
+   ∀l3,newc,mv,l4.
+   〈bar,false〉::〈c1,false〉::l2 ≠ l3@〈bar,false〉::〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4). 
+
+(* we still haven't proved termination *)
+axiom sem_match_tuple0 : Realize ? match_tuple R_match_tuple0.
+
+axiom Realize_to_Realize : 
+  ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
+
+lemma sem_match_tuple : Realize ? match_tuple R_match_tuple.
+generalize in match sem_match_tuple0; @Realize_to_Realize
+#t1 #t2 #HR #ls #c #l1 #c1 #l2 #rs #n #Hc #Hc1 #Hl1bitsnulls #Hl1marks #Hl1len #Htable #Ht1
+cases (HR … Ht1) -HR #_ #HR
+@(HR ??? [] … (refl ??) (refl ??) (refl ??) Hc Hc1 Hl1bitsnulls Hl1marks
+          Hl1len  Htable)
+qed.
\ No newline at end of file
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 5286a3340..b28efc472 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -15,6 +15,7 @@
 *)
 
 include "turing/universal/copy.ma".
+include "turing/universal/move_tape.ma".
 
 (*
 
@@ -58,23 +59,25 @@ definition init_match ≝
   seq ? (mark ?) 
     (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
       (seq ? (move_r ?) 
-        (seq ? (mark ?)
-          (seq ? (move_l ?) 
-            (adv_to_mark_l ? (is_marked ?)))))).
-            
+        (seq ? (move_r ?)
+          (seq ? (mark ?)
+            (seq ? (move_l ?) 
+              (adv_to_mark_l ? (is_marked ?))))))).
+             
 definition R_init_match ≝ λt1,t2.
   ∀ls,l,rs,c,d. no_grids (〈c,false〉::l) → no_marks l → 
-  t1 = midtape STape ls 〈c,false〉 (l@〈grid,false〉::〈d,false〉::rs) →
-  t2 = midtape STape ls 〈c,true〉 (l@〈grid,false〉::〈d,true〉::rs).
+  t1 = midtape STape ls 〈c,false〉 (l@〈grid,false〉::〈bar,false〉::〈d,false〉::rs) →
+  t2 = midtape STape ls 〈c,true〉 (l@〈grid,false〉::〈bar,false〉::〈d,true〉::rs).
   
 lemma sem_init_match : Realize ? init_match R_init_match.
 #intape 
 cases (sem_seq ????? (sem_mark ?)
        (sem_seq ????? (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
         (sem_seq ????? (sem_move_r ?)
-         (sem_seq ????? (sem_mark ?)
-          (sem_seq ????? (sem_move_l ?)
-           (sem_adv_to_mark_l ? (is_marked ?)))))) intape)
+         (sem_seq ????? (sem_move_r ?)
+          (sem_seq ????? (sem_mark ?)
+           (sem_seq ????? (sem_move_l ?)
+            (sem_adv_to_mark_l ? (is_marked ?))))))) intape)
 #k * #outc * #Hloop #HR 
 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 #ls #l #rs #c #d #Hnogrids #Hnomarks #Hintape
@@ -83,15 +86,17 @@ cases HR -HR
 * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb -Hta 
   [* #Hgridc @False_ind @(absurd … Hgridc) @eqnot_to_noteq 
    @(Hnogrids 〈c,false〉) @memb_hd ]
-* #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈d,false〉::rs) (refl …) (refl …) ?) 
+* #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) 
   [#x #membl @Hnogrids @memb_cons @membl] -Htb #Htb
 * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb #Htc
 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc #Htd
 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd #Hte
-whd in ⊢ (%→?); #Htf cases (Htf … Hte) -Htf -Hte 
+* #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+whd in ⊢ (%→?); #Htg cases (Htg … Htf) -Htg -Htf
   [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)]
-* #_ #Htf lapply (Htf (reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) 
-  [#x #membl @Hnomarks @daemon] -Htf #Htf >Htf >reverse_reverse %
+* #_ #Htg lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) 
+  [#x #membl @Hnomarks @daemon] -Htg #Htg >Htg >reverse_cons >reverse_reverse
+   >associative_append %
 qed.
 
 
@@ -234,8 +239,6 @@ cases HR -HR
   ]
 qed. *)
 
-include "turing/universal/move_tape.ma".
-
 definition exec_move ≝ 
   seq ? init_copy
     (seq ? copy
@@ -500,7 +503,7 @@ lemma sem_uni_step :
 [ #intape #outtape 
   #ta whd in ⊢ (%→?); #Hta #HR
   #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv
-  #Htable_len cut (∃t0,table. fulltable =〈t0,false〉::table) [(* 0 < |table| *) @daemon]
+  #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon]
   * #t0 * #table #Hfulltable >Hfulltable -fulltable 
   #Htable #Hmatch #Htape #Hintape #t1' #Ht1'
   >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta 
@@ -516,27 +519,28 @@ lemma sem_uni_step :
     [| * #Hcurrent #Hfalse @False_ind
       (* absurd by Hmatch *) @daemon
     | >Hs0 %
-    | (* da decidere se aggiungere un'assunzione o utilizzare Hmatch *) @daemon
+    | (* Htable (con lemma) *) @daemon
+    | (* Hmatch *) @daemon
     | (* Htable *) @daemon
     | (* Htable, Hmatch → |config| = n 
        necessaria modifica in R_match_tuple, le dimensioni non corrispondono
-      *) @daemon ]
+      *) @daemon
+    ]
     * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc *
     [ * #td * whd in ⊢ (%→?); >Htc -Htc #Htd
       cases (Htd ? (refl ??)) #_ -Htd
       cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc
-      >Hnewc #Htd 
-      cut (∃mv2. mv1 = [〈mv2,false〉])
-      [@daemon] * #mv2 #Hmv1
+      >Hnewc #Htd cut (mv1 = 〈mv,false〉)
+      [@daemon] #Hmv1
       * #te * whd in ⊢ (%→?); #Hte
       cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) 
               〈grid,false〉
-              ((table1@〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
-               newconfig@〈c1,false〉::〈comma,false〉::〈mv2,false〉::table2@〈grid,false〉::rs))
+              ((table1@〈bar,false〉::〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉::
+               newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs))
       [ >Htd @eq_f3 //
         [ >reverse_append >reverse_single %
         | >associative_append >associative_append normalize
-          >associative_append >associative_append >Hmv1 %
+          >associative_append >associative_append >Hmv1 % 
         ]
       ]
       -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte
@@ -555,14 +559,13 @@ lemma sem_uni_step :
       whd in Houttape:(???%); whd in Houttape:(???(??%%%));
       @ex_intro [| @(ex_intro ?? rs1) @ex_intro [| % [ % 
       [ >Houttape @eq_f @eq_f @eq_f @eq_f
-        change with ((〈t0,false〉::table)@?) in ⊢ (???%);
+        change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%);
         >Htableeq >associative_append >associative_append 
         >associative_append normalize >associative_append
         >associative_append normalize >Hnewc <Hmv1
         >associative_append normalize >associative_append
         >Hmv1 % 
-      | >(?: mv = mv2) [| (*Hmatch, Htableeq*) @daemon ]
-        @Hliftte
+      | @Hliftte
       ]
      | //
      ]
@@ -577,5 +580,4 @@ lemma sem_uni_step :
   #b #Hb cases (Ht1 ? Hb) #Hb' #Ht3 >Ht2 % //
   cases b in Hb'; normalize #H1 //
 ]
-qed.
-
+qed.
\ No newline at end of file