From d9633eca8fb8556a5eabaffdd1f561d0078d132f Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 23 May 2012 09:52:17 +0000
Subject: [PATCH] Progress

---
 .../matita/lib/turing/universal/move_tape.ma  | 83 +++++++++++++++----
 matita/matita/lib/turing/universal/tuples.ma  |  6 +-
 .../matita/lib/turing/universal/uni_step.ma   | 80 +++++++++++-------
 3 files changed, 121 insertions(+), 48 deletions(-)

diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index d8e4779bc..fc3e3f633 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -357,10 +357,40 @@ definition no_nulls ≝
 definition current_of_alpha ≝ λc:STape.
   match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
 
+(* 
+   no_marks (c::ls@rs) 
+   only_bits (ls@rs)
+   bit_or_null c
+   
+*)
 definition legal_tape ≝ λls,c,rs.
- let t ≝ mk_tape STape ls (current_of_alpha c) rs in
- left ? t = ls ∧ right ? t = rs ∧ current ? t = current_of_alpha c.
+ no_marks (c::ls@rs) ∧ only_bits (ls@rs) ∧ bit_or_null (\fst c) = true ∧
+ (\fst c ≠ null ∨ ls = [] ∨ rs = []).
  
+lemma legal_tape_left :
+  ∀ls,c,rs.legal_tape ls c rs → 
+  left ? (mk_tape STape ls (current_of_alpha c) rs) = ls.
+#ls * #c #bc #rs * * * #_ #_ #_ *
+[ *
+  [ cases c
+    [ #c' #_ %
+    | * #Hfalse @False_ind /2/
+    |*: #_ % ]
+  | #Hls >Hls cases c // cases rs //
+  ]
+| #Hrs >Hrs cases c // cases ls //
+]
+qed.
+
+axiom legal_tape_current :
+  ∀ls,c,rs.legal_tape ls c rs → 
+  current ? (mk_tape STape ls (current_of_alpha c) rs) = current_of_alpha c.
+
+axiom legal_tape_right :
+  ∀ls,c,rs.legal_tape ls c rs → 
+  right ? (mk_tape STape ls (current_of_alpha c) rs) = rs.
+
+(*
 lemma legal_tape_cases : 
   ∀ls,c,rs.legal_tape ls c rs → 
   \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])).
@@ -389,13 +419,13 @@ axiom legal_tape_conditions :
   
   #Hc
 *)
+*)
  
 definition R_move_tape_r_abstract ≝ λt1,t2.
   ∀rs,n,table,curc,curconfig,ls.
-  bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → 
+  is_bit curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → 
   t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 
          〈grid,false〉 rs →
-  no_nulls rs → no_marks rs → 
   legal_tape ls 〈curc,false〉 rs → 
   ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → 
   ∃ls1,rs1,newc.
@@ -411,12 +441,14 @@ lemma lift_tape_not_null :
 [|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 //
 qed.
+
+axiom bit_not_null :  ∀d.is_bit d = true → is_null d = false.
  
 lemma mtr_concrete_to_abstract :
   ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2.
 #t1 #t2 whd in ⊢(%→?); #Hconcrete
-#rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
-#Hrsnonulls #Hrsnomarks #Htape #t1' #Ht1'
+#rs #n #table #curc #curconfig #ls #Hbitcurc #Hcurconfig #Htable #Ht1
+* * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
 cases (Hconcrete … Htable Ht1) //
 [ * #Hrs #Ht2
   @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
@@ -424,9 +456,19 @@ cases (Hconcrete … Htable Ht1) //
   [ %
     [ >Ht2 %
     | >Hrs % ]
-  | % % % ]
+  | % [ % [ %
+    [ >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
+      [ >(\P Hx') % 
+      | @Hnomarks @(memb_append_l1 … Hx') ]
+    | >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
+      [ >(\P Hx') //
+      | @Hbits @(memb_append_l1 … Hx') ]]
+    | % ]
+    | %2 % ]
+  ]
 | * * #r0 #br0 * #rs0 * #Hrs 
-  cut (br0 = false) [@(Hrsnomarks 〈r0,br0〉) >Hrs @memb_hd]
+  cut (br0 = false) 
+  [ @(Hnomarks 〈r0,br0〉) @memb_cons @memb_append_l2 >Hrs @memb_hd]
   #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2
   @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
   @(ex_intro ?? r0) %
@@ -434,12 +476,25 @@ cases (Hconcrete … Htable Ht1) //
     [ >Ht2  //
     | >Hrs >lift_tape_not_null
       [ %
-      | @(Hrsnonulls 〈r0,false〉) >Hrs @memb_hd ] ]
-  | @legal_tape_conditions % % % #Hr0 >Hr0 in Hrs; #Hrs
-    lapply (Hrsnonulls 〈null,false〉 ?)
-    [ >Hrs @memb_hd | normalize #H destruct (H) ]
-  ]
-]
+      | @bit_not_null @(Hbits 〈r0,false〉) >Hrs @memb_append_l2 @memb_hd ] ]
+  | % [ % [ %
+    [ #x #Hx cases (orb_true_l … Hx) #Hx'
+      [ >(\P Hx') % 
+      | cases (memb_append … Hx') #Hx'' @Hnomarks 
+        [ @(memb_append_l1 … Hx'') 
+        | >Hrs @memb_cons @memb_append_l2 @(memb_cons … Hx'') ]
+      ]
+    | whd in ⊢ (?%); #x #Hx cases (orb_true_l … Hx) #Hx'
+      [ >(\P Hx') //
+      | cases (memb_append … Hx') #Hx'' @Hbits
+        [ @(memb_append_l1 … Hx'') | >Hrs @memb_append_l2 @(memb_cons … Hx'') ]
+      ]]
+    | whd in ⊢ (??%?); >(Hbits 〈r0,false〉) //
+      @memb_append_l2 >Hrs @memb_hd ]
+    | % % % #Hr0 lapply (Hbits 〈r0,false〉?) 
+      [ @memb_append_l2 >Hrs @memb_hd
+      | >Hr0 normalize #Hfalse destruct (Hfalse)
+      ] ] ] ]
 qed.
 
 definition R_move_tape_l_abstract ≝ λt1,t2.
diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 9826c344e..b8c0a7ed4 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -654,13 +654,13 @@ definition R_match_tuple ≝ λt1,t2.
          (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 ∧
+   〈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))
+        (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).  
+   〈c1,false〉::l2 ≠ l3@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4).  
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index d4422f2ca..1811d5a19 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -496,40 +496,58 @@ lemma sem_uni_step :
     | (* da decidere se aggiungere un'assunzione o utilizzare Hmatch *) @daemon
     | (* Htable *) @daemon
     | (* Htable, Hmatch → |config| = n *) @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 
-     * #te * whd in ⊢ (%→?); #Hte
-     (* mv1 ha tipo lista ma dovrebbe avere tipo unialpha *)
-     cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) 
+    * #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 (mv1 = 〈\fst mv1,false〉)
+      [ >(eq_pair_fst_snd … mv1) @eq_f (*Htable, Htableeq*) @daemon ] #Hmv1
+      * #te * whd in ⊢ (%→?); #Hte
+      (* mv1 ha tipo lista ma dovrebbe avere tipo unialpha *)
+      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〉::〈\fst mv1,false〉::table2@〈grid,false〉::rs))
-     lapply (Hte … Htd)
-     
-     (* univocità delle tuple in table *)
-     cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc
-   c00 ≝ c0
-   curconfig0 ≝ curconfig
-   s00 ≝ s0
-   ls0 ≝ ls
-   table10 ≝ (table1@〈s0,false〉::curconfig@〈c0,false〉)
-   s10 ≝ s1
-   newconfig0 ≝ newconfig
-   c10 ≝ c1
-   mv0 ≝ mv1
-   table20 ≝ table2
-   rs0 ≝ rs
-               
-     lapply (Hte … Htd)
-   | * #td * whd in ⊢ (%→%→?); >Htc #Htd
-     cases (Htd ? (refl ??)) normalize in ⊢ (%→?);
-     #Hfalse destruct (Hfalse)
-   ]
-    
-  
+      [ >Htd @eq_f3 //
+        [ >reverse_append >reverse_single %
+        | >associative_append >associative_append normalize
+          >associative_append >associative_append <Hmv1 %
+        ]
+      ]
+      -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte
+      [ //
+      |2,3,4,5: (* dovrebbe scomparire (lo metteremo nel legal_tape) *) @daemon
+      | (*|curconfig| = |newconfig|*) @daemon
+      | (* only_bits (〈s1,false〉::newconfig) *) @daemon
+      | (* only_bits (curconfig@[〈s0,false〉]) *) @daemon
+      | (* no_marks (reverse ? curconfig) *) @daemon
+      | <Hmv1 >Hnewc in Htableeq; 
+        >associative_append >associative_append normalize
+        >associative_append >associative_append
+        #Htableeq <Htableeq // ]
+      * #ls1 * #rs1 * #c2 * * #Hte #Hliftte #Hlegalte
+      whd in ⊢ (%→?); #Houttape lapply (Houttape … Hte) -Houttape #Houttape
+      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 ⊢ (???%);
+        >Htableeq >associative_append >associative_append 
+        >associative_append normalize >associative_append
+        >associative_append normalize >Hnewc <Hmv1
+        >associative_append normalize >associative_append % 
+      | >(?: mv = \fst mv1) [| (*Hmatch, Htableeq*) @daemon ]
+        @Hliftte
+      ]
+     | //
+     ]
+    ]
+   ] 
+  | * #td * whd in ⊢ (%→%→?); >Htc #Htd
+    cases (Htd ? (refl ??)) normalize in ⊢ (%→?);
+    #Hfalse destruct (Hfalse)
+  ]
+ ]
 | #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2
   #b #Hb cases (Ht1 ? Hb) #Hb' #Ht3 >Ht2 % //
   cases b in Hb'; normalize #H1 //
-- 
2.39.2