From 09d38cb67e92bc6cdfe834cb1524a79643cc13e7 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 17 Jan 2013 14:00:11 +0000
Subject: [PATCH] Moved a list comparison function in the list file

---
 matita/matita/lib/arithmetics/primes.ma        |  2 +-
 matita/matita/lib/basics/lists/list.ma         | 18 ++++++++++++++++++
 .../lib/turing/multi_universal/tuples.ma       | 17 -----------------
 3 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 68e511e98..62c0a0081 100644
--- 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 48ee3078a..725f57135 100644
--- 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 76e56068d..0fe4508ed 100644
--- 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.
-- 
2.39.2