X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=f8c2ac772084c11ba0e0dd273f9676f3ce3d46f5;hb=dd4bd89108bea062338a0f04ea616432edaad13c;hp=a8a01a904bfd98672ea46cce6f5c51cd63fbb122;hpb=cdcfe9f97936f02dab1970ebf3911940bf0a4e29;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a8a01a904..f8c2ac772 100644
--- 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}}.
 
@@ -92,6 +92,34 @@ lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
 #A #a1 #a2 #l1 #l2 #Heq destruct //
 qed.
 
+(* option cons *)
+
+definition option_cons ≝ λsig.λc:option sig.λl.
+  match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
+
+lemma opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l). 
+#A * //
+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 ≝
@@ -181,6 +209,10 @@ lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
 #A #l elim l // 
 qed.
 
+lemma length_tail1 : ∀A,l.0 < |l| → |tail A l| < |l|.
+#A * normalize //
+qed.
+
 lemma length_append: ∀A.∀l1,l2:list A. 
   |l1@l2| = |l1|+|l2|.
 #A #l1 elim l1 // normalize /2/
@@ -200,6 +232,19 @@ lemma lenght_to_nil: ∀A.∀l:list A.
 #A * // #a #tl normalize #H destruct
 qed.
  
+lemma lists_length_split : 
+ ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
+#A #l1 elim l1
+[ #l2 %{[ ]} %{l2} % % %
+| #hd1 #tl1 #IH *
+  [ %{[ ]} %{(hd1::tl1)} %2 % %
+  | #hd2 #tl2 cases (IH tl2) #x * #y *
+    [ * #IH1 #IH2 %{(hd2::x)} %{y} % normalize % //
+    | * #IH1 #IH2 %{(hd1::x)} %{y} %2 normalize % // ]
+  ]
+]
+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.
@@ -268,6 +313,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.
@@ -290,6 +361,109 @@ lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
   ]
 qed.
 
+(****************************** mem filter ***************************)
+lemma mem_filter: ∀S,f,a,l. 
+  mem S a (filter S f l) → mem S a l.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize
+  [* [#eqab %1 @eqab | #H %2 @Hind @H]
+  |#H %2 @Hind @H]
+qed.
+
+lemma mem_filter_true: ∀S,f,a,l. 
+  mem S a (filter S f l)  → f a = true.
+#S #f #a #l elim l [normalize @False_ind ]
+#b #tl #Hind cases (true_or_false (f b)) #H
+normalize >H normalize [2:@Hind]
+* [#eqab // | @Hind]
+qed. 
+
+lemma mem_filter_l: ∀S,f,x,l. (f x = true) → mem S x l →
+mem S x (filter ? f l).
+#S #f #x #l #fx elim l [@False_ind]
+#b #tl #Hind * 
+  [#eqxb <eqxb >(filter_true ???? fx) %1 % 
+  |#Htl cases (true_or_false (f b)) #fb 
+    [>(filter_true ???? fb) %2 @Hind @Htl
+    |>(filter_false ???? fb) @Hind @Htl
+    ]
+  ]
+qed.
+
+lemma filter_case: ∀A,p,l,x. mem ? x l → 
+  mem ? x (filter A p l) ∨ mem ? x (filter A (λx.¬ p x) l).
+#A #p #l elim l 
+  [#x @False_ind 
+  |#a #tl #Hind #x * 
+    [#eqxa >eqxa cases (true_or_false (p a)) #Hcase
+      [%1 >(filter_true A tl a p Hcase) %1 % 
+      |%2 >(filter_true A tl a ??) [%1 % | >Hcase %]
+      ]
+    |#memx cases (Hind … memx) -memx #memx
+      [%1 cases (true_or_false (p a)) #Hpa 
+        [>(filter_true A tl a p Hpa) %2 @memx
+        |>(filter_false A tl a p Hpa) @memx
+        ]
+      |cases (true_or_false (p a)) #Hcase
+        [%2 >(filter_false A tl a) [@memx |>Hcase %]
+        |%2 >(filter_true A tl a) [%2 @memx|>Hcase %]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+lemma filter_length2: ∀A,p,l. |filter A p l|+|filter A (λx.¬ p x) l| = |l|.
+#A #p #l elim l //
+#a #tl #Hind cases (true_or_false (p a)) #Hcase
+  [>(filter_true A tl a p Hcase) >(filter_false A tl a ??) 
+    [@(eq_f ?? S) @Hind | >Hcase %]
+  |>(filter_false A tl a p Hcase) >(filter_true A tl a ??) 
+    [<plus_n_Sm @(eq_f ?? S) @Hind | >Hcase %]
+  ]
+qed.
+
+(***************************** unique *******************************)
+let rec unique A (l:list A) on l ≝ 
+  match l with 
+  [nil ⇒ True
+  |cons a tl ⇒ ¬ mem A a tl ∧ unique A tl].
+
+lemma unique_filter : ∀S,l,f.
+ unique S l → unique S (filter S f l).
+#S #l #f elim l //
+#a #tl #Hind * 
+#memba #uniquetl cases (true_or_false … (f a)) #Hfa
+  [>(filter_true ???? Hfa) % 
+    [@(not_to_not … memba) @mem_filter |/2/ ]
+  |>filter_false /2/
+  ]
+qed.
+
+lemma filter_eqb : ∀m,l. unique ? l → 
+  (mem ? m l ∧ filter ? (eqb m) l = [m])∨(¬mem ? m l ∧ filter ? (eqb m) l = []).
+#m #l elim l
+  [#_ %2 % [% @False_ind | //]
+  |#a #tl #Hind * #Hmema #Hunique
+   cases (Hind Hunique)
+    [* #Hmemm #Hind %1 % [%2 //]
+     >filter_false // @not_eq_to_eqb_false % #eqma @(absurd ? Hmemm) //
+    |* #Hmemm #Hind cases (decidable_eq_nat m a) #eqma 
+      [%1 <eqma % [%1 //] >filter_true [2: @eq_to_eqb_true //] >Hind //
+      |%2 % 
+        [@(not_to_not … Hmemm) * // #H @False_ind  @(absurd … H) //
+        |>filter_false // @not_eq_to_eqb_false @eqma
+        ]
+      ]
+    ]
+  ]
+qed.
+
+lemma length_filter_eqb: ∀m,l. unique ? l → 
+  |filter ? (eqb m) l| ≤ 1.
+#m #l #Huni cases (filter_eqb m l Huni) * #_ #H >H // 
+qed. 
+
 (***************************** split *******************************)
 let rec split_rev A (l:list A) acc n on n ≝ 
   match n with 
@@ -419,12 +593,38 @@ 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-.
+
+lemma Allr_fwd_append_dx: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l2.
+#A #R #l1 elim l1 -l1 // #a1 #l1 #IHl1 #l2 #H
+lapply (Allr_fwd_cons … (l1@l2) H) -H /2 width=1/
+qed-.  
+
 (**************************** Exists *******************************)
 
 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
@@ -599,50 +799,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-.