X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fdatatypes%2Flist.ma;h=2909baf84bc543dc373b11e7f02e078adfd7bbb4;hb=f40d692b9210d044e430efa5f05b0bd38069fb85;hp=0e13377257e180b4a8505741618bd76ed7b86216;hpb=edccb29109d07b54b48230a280f4351ed042dd9f;p=helm.git

diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma
index 0e1337725..2909baf84 100644
--- a/helm/software/matita/nlibrary/datatypes/list.ma
+++ b/helm/software/matita/nlibrary/datatypes/list.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "arithmetics/nat.ma".
+include "logic/pts.ma".
 
 ninductive list (A:Type[0]) : Type[0] ≝ 
   | nil: list A
@@ -33,27 +33,26 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-ntheorem nil_cons:
-  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
-#A;#l;#a;#H;ndestruct;
-nqed.
+nlet rec append A (l1: list A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒ l2
+  | cons hd tl ⇒ hd :: append A tl l2 ].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
 nlet rec id_list A (l: list A) on l ≝ 
   match l with
   [ nil ⇒ []
   | cons hd tl ⇒ hd :: id_list A tl ].
 
-nlet rec append A (l1: list A) l2 on l1 ≝ 
-  match l1 with
-  [ nil ⇒ l2
-  | cons hd tl ⇒ hd :: append A tl l2 ].
 
 ndefinition tail ≝ λA:Type[0].λl:list A.
   match l with
   [ nil ⇒  []
   | cons hd tl ⇒  tl].
 
-interpretation "append" 'append l1 l2 = (append ? l1 l2).
+nlet rec flatten S (l : list (list S)) on l : list S ≝ 
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
 #A;#l;nelim l;//;
@@ -113,12 +112,12 @@ qed.
 
 *)
 
-nlet rec nth A l d n on n ≝
-  match n with
-  [ O ⇒ match l with
-        [ nil ⇒ d
-        | cons (x : A) _ ⇒ x ]
-  | S n' ⇒ nth A (tail ? l) d n'].
+nlet rec nth A l d n on l ≝
+  match l with
+  [ nil ⇒ d
+  | cons (x:A) tl ⇒ match n with
+    [ O ⇒ x
+    | S n' ⇒ nth A tl d n' ] ].
 
 nlet rec map A B f l on l ≝
   match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. 
@@ -201,12 +200,15 @@ naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
   |destruct H4;right;assumption]
 qed.*)
 
-naxiom in_list_tail : \forall l,x,y.
-      in_list nat x (y::l) \to x \neq y \to in_list nat x l.
-(*intros 4;elim (in_list_cons_case ? ? ? ? H)
-  [elim (H2 H1)
-  |assumption]
-qed.*)
+nlemma in_list_tail : \forall A,l,x,y.
+      in_list A x (y::l) \to x \neq y \to in_list A x l.
+#A;#l;#x;#y;#H;#Hneq;
+ninversion H;
+##[#x1;#l1;#Hx;#Hl;ndestruct;nelim Hneq;#Hfalse;
+   nelim (Hfalse ?);@;
+##|#x1;#y1;#l1;#H1;#_;#Hx;#Heq;ndestruct;//;
+##]
+nqed.
 
 naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
 (*intros;elim (in_list_cons_case ? ? ? ? H)
@@ -331,3 +333,175 @@ naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
 qed.*)
 
+nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝ 
+ match l with
+ [ nil ⇒ a
+ | cons b bl ⇒ foldl A B f (f a b) bl ].
+
+nlet rec foldl2 (A,B,C:Type[0]) (f:A → B → C → A) (a:A) (bl:list B) (cl:list C) on bl ≝ 
+ match bl with
+ [ nil ⇒ a
+ | cons b0 bl0 ⇒ match cl with
+   [ nil ⇒ a
+   | cons c0 cl0 ⇒ foldl2 A B C f (f a b0 c0) bl0 cl0 ] ].
+
+nlet rec foldr2 (A,B : Type[0]) (X : Type[0]) (f: A → B → X → X) (x:X)
+                (al : list A) (bl : list B) on al : X ≝
+  match al with
+  [ nil ⇒ x
+  | cons a al1 ⇒ match bl with
+    [ nil ⇒ x
+    | cons b bl1 ⇒ f a b (foldr2 ??? f x al1 bl1) ] ].
+ 
+nlet rec rev (A:Type[0]) (l:list A) on l ≝ 
+ match l with
+ [ nil ⇒ nil A
+ | cons hd tl ⇒ (rev A tl)@[hd] ]. 
+ 
+notation > "hvbox(a break \liff b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+  left associative with precedence 25
+for @{ 'iff $a $b }.
+
+interpretation "logical iff" 'iff x y = (iff x y).
+    
+ndefinition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
+
+notation > "hvbox(a break ≡ b)"
+  non associative with precedence 45
+for @{'equiv $a $b}.
+
+notation < "hvbox(term 46 a break ≡ term 46 b)"
+  non associative with precedence 45
+for @{'equiv $a $b}.
+
+interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
+
+nlemma refl_coincl : ∀A.∀l:list A.l ≡ l.
+#;@;#;//;
+nqed.
+
+nlemma coincl_rev : ∀A.∀l:list A.l ≡ rev ? l.
+#A l x;@;nelim l
+##[##1,3:#H;napply False_ind;ncases (not_in_list_nil ? x);
+   #H1;napply (H1 H);
+##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
+   ##[napply in_list_to_in_list_append_r;nrewrite > H1;@
+   ##|napply in_list_to_in_list_append_l;/2/
+   ##]
+##|#a l0 IH H;ncases (in_list_append_to_or_in_list ???? H);#H1
+   ##[/3/;
+   ##|nrewrite > (in_list_singleton_to_eq ??? H1);@
+   ##]
+##] 
+nqed.    
+
+nlemma not_in_list_nil_r : ∀A.∀l:list A.l = [] → ∀x.x ∉ l.
+#A l;nelim l
+##[#;napply not_in_list_nil
+##|#a l0 IH Hfalse;ndestruct (Hfalse)
+##]
+nqed.
+
+nlemma eq_filter_append : 
+ ∀A,p,l1,l2.filter A (l1@l2) p = filter A l1 p@filter A l2 p.
+#A p l1 l2;nelim l1
+##[@
+##|#a0 l0 IH;nwhd in ⊢ (??%(??%?));ncases (p a0)
+   ##[nwhd in ⊢ (??%%);nrewrite < IH;@
+   ##|nwhd in ⊢ (??%(??%?));nrewrite < IH;@
+   ##]
+##]
+nqed.
+
+nlemma map_ind : 
+ ∀A,B:Type[0].∀f:A→B.∀P:B → Prop.
+  ∀al.(∀a.a ∈ al → P (f a)) → 
+  ∀b. b ∈ map ?? f al → P b.
+#A B f P al;nelim al
+##[#H1 b Hfalse;napply False_ind;
+   ncases (not_in_list_nil ? b);#H2;napply H2;napply Hfalse;
+##|#a1 al1 IH H1 b Hin;nwhd in Hin:(???%);ncases (in_list_cons_case ???? Hin);
+   ##[#e;nrewrite > e;napply H1;@
+   ##|#Hin1;napply IH;
+      ##[#a2 Hin2;napply H1;@2;//;
+      ##|//
+      ##]
+   ##]
+##]
+nqed.
+
+nlemma map_compose : 
+ ∀A,B,C,f,g,l.map B C f (map A B g l) = map A C (λx.f (g x)) l.
+#A B C f g l;nelim l
+##[@
+##|#a0 al0 IH;nchange in ⊢ (??%%) with (cons ???);
+   napply eq_f2; //;
+##]
+nqed.
+
+naxiom incl_incl_to_incl_append : 
+  ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
+  
+naxiom eq_map_append : ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.  
+
+naxiom not_in_list_to_mem_false :
+  ∀A,equ.
+  (∀x,y.equ x y = true → x = y) →
+  ∀x:A.∀l. x ∉ l → mem A equ x l = false.
+
+nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝ 
+ match l with
+ [ nil ⇒ (true:bool)
+ | cons a al ⇒ p a ∧ list_forall A al p ].
+
+nlemma eq_map_f_g :
+ ∀A,B,f,g,xl.(∀x.x ∈ xl → f x = g x) → map A B f xl = map A B g xl.
+#A B f g xl;nelim xl
+##[#;@
+##|#a al IH H1;nwhd in ⊢ (??%%);napply eq_f2
+   ##[napply H1;@;
+   ##|napply IH;#x Hx;napply H1;@2;//
+   ##]
+##]
+nqed.
+
+nlemma x_in_map_to_eq :
+  ∀A,B,f,x,l.x ∈ map A B f l → ∃x'.x = f x' ∧ x' ∈ l.
+#A B f x l;nelim l
+##[#H;ncases (not_in_list_nil ? x);#H1;napply False_ind;napply (H1 H)
+##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
+   ##[nrewrite > H1;@ a;@;@
+   ##|ncases (IH H1);#a0;*;#H2 H3;@a0;@
+      ##[// ##|@2;// ##]
+   ##]
+##]
+nqed.
+
+nlemma list_forall_false :
+ ∀A:Type[0].∀x,xl,p. p x = false → x ∈ xl → list_forall A xl p = false.
+#A x xl p H1;nelim xl
+##[#Hfalse;napply False_ind;ncases (not_in_list_nil ? x);#H2;napply (H2 Hfalse)
+##|#x0 xl0 IH H2;ncases (in_list_cons_case ???? H2);#H3
+   ##[nwhd in ⊢ (??%?);nrewrite < H3;nrewrite > H1;@
+   ##|nwhd in ⊢ (??%?);ncases (p x0)
+      ##[nrewrite > (IH H3);@
+      ##|@
+      ##]
+   ##]
+##]
+nqed.
+
+nlemma list_forall_true :
+ ∀A:Type[0].∀xl,p. (∀x.x ∈ xl → p x = true) → list_forall A xl p = true.
+#A xl p;nelim xl
+##[#;@
+##|#x0 xl0 IH H1;nwhd in ⊢ (??%?);nrewrite > (H1 …)
+   ##[napply IH;#x Hx;napply H1;@2;//
+   ##|@
+   ##]
+##]
+nqed.