Moved a list comparison function in the list file

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 68e511e982617f293eedfc320aaa6be1ec888447..62c0a0081af5ecadfade0e7b0bbaa1ff4a3b216a 100644 (file)
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -310,7 +310,7 @@ qed.
 
 theorem prime_smallest_factor_n : ∀n. 1 < n → 
   prime (smallest_factor n).
-#n #lt1n (cut (0<n)) [/2/] #posn % /2/ #m #divmmin #lt1m
+#n #lt1n (cut (0<n)) [/2/] #posn % (* bug? *) [/2/] #m #divmmin #lt1m
 @le_to_le_to_eq
   [@divides_to_le // @lt_O_smallest_factor //
   |>smallest_factor_to_min // @true_to_le_min //

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 48ee3078afa691590299a790033311db25ef64d2..725f57135f42428760b67c42cdfa1b9e88d4b531 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -92,6 +92,24 @@ lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
 #A #a1 #a2 #l1 #l2 #Heq destruct //
 qed.
 
+(* comparing lists *)
+
+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.
 (**************************** iterators ******************************)
 
 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝

diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
index 76e56068df9303450f7d7c179b3daf0eb0576827..0fe4508ed63979d2d28011aac21efca38ef9b524 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/tuples.ma
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -39,23 +39,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.