- paths and left residuals: first case of the equivalence proved!

[helm.git] / matita / matita / lib / basics / lists / list.ma

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a20a891089cb795ae88cdbe823a18d9a90096ebe..48ee3078afa691590299a790033311db25ef64d2 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -20,7 +20,7 @@ notation "hvbox(hd break :: tl)"
   right associative with precedence 47
   for @{'cons $hd $tl}.
 
-notation "[ list0 x sep ; ]"
+notation "[ list0 term 19 x sep ; ]"
   non associative with precedence 90
   for ${fold right @'nil rec acc @{'cons $x $acc}}.
 
@@ -175,8 +175,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝
     [ nil ⇒ 0
     | cons a tl ⇒ S (length A tl)].
 
-notation "|M|" non associative with precedence 65 for @{'norm $M}.
-interpretation "norm" 'norm l = (length ? l).
+interpretation "list length" 'card l = (length ? l).
 
 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
 #A #l elim l // 
@@ -196,6 +195,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.
@@ -264,6 +268,53 @@ let rec mem A (a:A) (l:list A) on l ≝
   [ nil ⇒ False
   | cons hd tl ⇒ a=hd ∨ mem A a tl
   ]. 
+  
+lemma mem_append: ∀A,a,l1,l2.mem A a (l1@l2) →
+  mem ? a l1 ∨ mem ? a l2.
+#A #a #l1 elim l1 
+  [#l2 #mema %2 @mema
+  |#b #tl #Hind #l2 * 
+    [#eqab %1 %1 @eqab 
+    |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
+    ]
+  ]
+qed.
+
+lemma mem_append_l1: ∀A,a,l1,l2.mem A a l1 → mem A a (l1@l2).
+#A #a #l1 #l2 elim l1
+  [whd in ⊢ (%→?); @False_ind
+  |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
+  ]
+qed.
+
+lemma mem_append_l2: ∀A,a,l1,l2.mem A a l2 → mem A a (l1@l2).
+#A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
+qed.
+
+lemma mem_single: ∀A,a,b. mem A a [b] → a=b.
+#A #a #b * // @False_ind
+qed.
+
+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 ≝ 
@@ -317,6 +368,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
@@ -362,6 +445,33 @@ lemma All_nth : ∀A,P,n,l.
   ]
 ] qed.
 
+lemma All_append: ∀A,P,l1,l2. All A P l1 → All A P l2 → All A P (l1@l2).
+#A #P #l1 elim l1 -l1 //
+#a #l1 #IHl1 #l2 * /3 width=1/
+qed.
+
+lemma All_inv_append: ∀A,P,l1,l2. All A P (l1@l2) → All A P l1 ∧ All A P l2.
+#A #P #l1 elim l1 -l1 /2 width=1/
+#a #l1 #IHl1 #l2 * #Ha #Hl12
+elim (IHl1 … Hl12) -IHl1 -Hl12 /3 width=1/
+qed-.
+
+(**************************** Allr ******************************)
+
+let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
+match l with
+[ nil       ⇒ True
+| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
+].
+
+lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
+#A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
+qed-.
+
+lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l.
+#A #R #a * // #a0 #l * //
+qed-.
+
 (**************************** Exists *******************************)
 
 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝