- 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 a8a01a904bfd98672ea46cce6f5c51cd63fbb122..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}}.
 
@@ -268,6 +268,32 @@ 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.
@@ -419,12 +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 ≝
@@ -599,50 +646,3 @@ match n with
 [ O ⇒ [ ]
 | S m ⇒ a::(make_list A a m)
 ].
-
-(* ******** labelled reflexive and transitive closure ************)
-
-inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
-| lstar_nil : ∀b. lstar A B R ([]) b b
-| lstar_cons: ∀a,b1,b. R a b1 b →
-              ∀l,b2. lstar A B R l b b2 → lstar A B R (a::l) b1 b2
-.
-
-lemma lstar_step: ∀A,B,R,a,b1,b2. R a b1 b2 → lstar A B R ([a]) b1 b2.
-/2 width=3/
-qed.
-
-lemma lstar_inv_nil: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → [] = l → b1 = b2.
-#A #B #R #l #b1 #b2 * -l -b1 -b2 //
-#a #b1 #b #_ #l #b2 #_ #H destruct
-qed-.
-
-lemma lstar_inv_cons: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 →
-                      ∀a0,l0. a0::l0 = l →
-                      ∃∃b. R a0 b1 b & lstar A B R l0 b b2.
-#A #B #R #l #b1 #b2 * -l -b1 -b2
-[ #b #a0 #l0 #H destruct
-| #a #b1 #b #Hb1 #l #b2 #Hb2 #a0 #l0 #H destruct /2 width=3/
-]
-qed-.
-
-lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
-#A #B #R #a #b1 #b2 #H
-elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
-<(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
-qed-.
-
-theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
-                            ∀l. singlevalued … (lstar A B R l).
-#A #B #R #HR #l #b #c1 #H elim H -l -b -c1
-[ /2 width=5 by lstar_inv_nil/
-| #a #b #b1 #Hb1 #l #c1 #_ #IHbc1 #c2 #H
-  elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
-  lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
-]
-qed-.
-
-theorem lstar_trans: ∀A,B,R,l1,b1,b. lstar A B R l1 b1 b →
-                     ∀l2,b2. lstar A B R l2 b b2 → lstar A B R (l1@l2) b1 b2.
-#A #B #R #l1 #b1 #b #H elim H -l1 -b1 -b normalize // /3 width=3/
-qed-.