From 5d54a6d3a0f22bb8784387c491de7bb66e67b625 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jun 2012 10:46:29 +0000
Subject: [PATCH] Dropping a coercion and some hints due to conflicts with
 CerCo

---
 matita/matita/lib/basics/deqsets.ma     |  5 ++-
 matita/matita/lib/basics/lists/list.ma  | 58 +++++++++++++++++++++++++
 matita/matita/lib/basics/lists/listb.ma |  9 ++++
 matita/matita/lib/basics/types.ma       |  2 +-
 4 files changed, 71 insertions(+), 3 deletions(-)

diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index fcc89f312..fb6ad5be4 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -207,7 +207,8 @@ qed.
 
 definition DeqSig ≝ λA:DeqSet.λP:A→Prop.
   mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P).
-  
+
+(*
 unification hint  0 ≔ C,P; 
     T ≟ carr C,
     X ≟ DeqSig C P
@@ -218,4 +219,4 @@ unification hint  0 ≔ T,P,p1,p2;
     X ≟ DeqSig T P
 (* ---------------------------------------- *) ⊢ 
     eq_sigma T P p1 p2 ≡ eqb X p1 p2.
-
+*)
diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a20a89108..a330f6224 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -196,6 +196,11 @@ lemma length_reverse: ∀A.∀l:list A.
 #A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
 qed.
 
+lemma lenght_to_nil: ∀A.∀l:list A.
+  |l| = 0 → l = [ ].
+#A * // #a #tl normalize #H destruct
+qed.
+ 
 (****************** traversing two lists in parallel *****************)
 lemma list_ind2 : 
   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
@@ -265,6 +270,27 @@ let rec mem A (a:A) (l:list A) on l ≝
   | cons hd tl ⇒ a=hd ∨ mem A a tl
   ]. 
 
+lemma mem_map: ∀A,B.∀f:A→B.∀l,b. 
+  mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
+#A #B #f #l elim l 
+  [#b normalize @False_ind
+  |#a #tl #Hind #b normalize *
+    [#eqb @(ex_intro … a) /3/
+    |#memb cases (Hind … memb) #a * #mema #eqb
+     @(ex_intro … a) /3/
+    ]
+  ]
+qed.
+
+lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l. 
+  mem A a l → mem B (f a) (map ?? f l).
+ #A #B #f #a #l elim l
+  [normalize @False_ind
+  |#b #tl #Hind * 
+    [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+  ]
+qed.
+
 (***************************** split *******************************)
 let rec split_rev A (l:list A) acc n on n ≝ 
   match n with 
@@ -317,6 +343,38 @@ lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| →
 @(ex_intro … (\snd (split A l n))) % /2/
 qed.
   
+(****************************** flatten ******************************)
+definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
+
+lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
+  (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2  →
+    (∃q.|l1| = n*q)  → mem ? a l.
+#A #n #l elim l
+  [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
+   cut (|a|=0) [@sym_eq @le_n_O_to_eq 
+   @(transitive_le ? (|nil A|)) // >Hnil >length_append >length_append //] /2/
+  |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha 
+   whd in match (flatten ??); #Hflat * #q cases q
+    [<times_n_O #Hl1 
+     cut (a = hd) [>(lenght_to_nil… Hl1) in Hflat; 
+     whd in ⊢ ((???%)→?); #Hflat @sym_eq @(append_l1_injective … Hflat)
+     >Ha >Hlen // %1 //   
+     ] /2/
+    |#q1 #Hl1 lapply (split_exists … n l1 ?) //
+     * #l11 * #l12 * #Heql1 #Hlenl11 %2
+     @(Hind l12 l2 … posn ? Ha) 
+      [#x #memx @Hlen %2 //
+      |@(append_l2_injective ? hd l11) 
+        [>Hlenl11 @Hlen %1 %
+        |>Hflat >Heql1 >associative_append %
+        ]
+      |@(ex_intro …q1) @(injective_plus_r n) 
+       <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
+      ]
+    ]
+  ]
+qed.
+
 (****************************** nth ********************************)
 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
   match n with
diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 438f3b497..a95d8a05a 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -122,6 +122,15 @@ lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true.
     ]
   ]
 qed.
+
+lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l.
+#S #l #a elim l 
+  [normalize #H destruct
+  |#b #tl #Hind #mema cases (orb_true_l … mema) 
+    [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl]
+  ]
+qed.
+
 (**************** unicity test *****************)
 
 let rec uniqueb (S:DeqSet) l on l : bool ≝
diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index b319b5bd0..a5e35c9d2 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -67,7 +67,7 @@ interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
 
 (* sigma *)
 record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
-    pi1:> A
+    pi1: A  (* not a coercion due to problems with Cerco *)
   ; pi2: f pi1
   }.
   
-- 
2.39.2