cfg_to_obj completed (modulo daemons)

[helm.git] / matita / matita / lib / turing / multi_universal / tuples.ma

diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
index 76e56068df9303450f7d7c179b3daf0eb0576827..428d99ccf0f415ec705d79aeec8de150e3a56ad1 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/tuples.ma
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -21,8 +21,30 @@ lemma table_TM_cons: ∀n,h,t,o.
   table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h).
 // qed.
 
+lemma initial_bar: ∀n,h,l. l ≠ [ ] →
+  table_TM n l h = bar :: tail ? (table_TM n l h).
+#n #h * 
+  [* #H @False_ind @H // 
+  |#a #tl #_ >table_TM_cons lapply (is_tuple n h a) 
+   * #qin * #cin * #qout * #cout * #mv * #_ #Htup >Htup %
+  ]
+qed. 
+
 (************************** matching in a table *******************************)
-lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
+lemma list_to_table: ∀n,l,h,t. mem ? t l →
+  ∃ll,lr.table_TM n l h = ll@(tuple_encoding n h t)@lr.
+#n #l #h #t elim l 
+  [@False_ind
+  |#hd #tl #Hind *
+    [#Htup %{[]} %{(table_TM n tl h)} >Htup %
+    |#H cases (Hind H) #ll * #lr #H1
+     %{((tuple_encoding n h hd)@ll)} %{lr} 
+     >associative_append <H1 %
+    ]
+  ]
+qed.
+
+lemma list_to_table1: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
   ∃ll,lr.table_TM n l h = ll@tup@lr.
 #n #l #h #tup elim l 
   [@False_ind
@@ -39,23 +61,6 @@ definition is_config : nat → list unialpha → Prop ≝
  λn,t.∃qin,cin.
  only_bits qin ∧ cin ≠ bar ∧ |qin| = S n ∧ t = bar::qin@[cin].
 
-lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 → 
-∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
-#A #l1 elim l1
-  [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
-  |#a1 #tl1 #Hind #l2 #l3 cases l3
-    [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq 
-    |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
-      [#l * * #Heq1 #Heq2 %{l}
-        [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
-        |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
-        ]
-      |@(cons_injective_r ????? Heq) 
-      ]
-    ]
-  ]
-qed.
-
 lemma table_to_list: ∀n,l,h,c. is_config n c → 
   (∃ll,lr.table_TM n l h = ll@c@lr) → 
     ∃out,t. tuple_encoding n h t = (c@out) ∧ mem ? t l.