X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fdatatypes%2Flist.ma;h=836b72ea5bbebe046d2d3825015bc8822361c62f;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hp=5d5ed0e3489faf30fc30e5349a485f147ce39302;hpb=4b940bfbeab1181dd18c56e46761f5e6690d9f9d;p=helm.git

diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma
index 5d5ed0e34..836b72ea5 100644
--- a/helm/software/matita/nlibrary/datatypes/list.ma
+++ b/helm/software/matita/nlibrary/datatypes/list.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "logic/pts.ma".
+include "arithmetics/nat.ma".
 
 ninductive list (A:Type[0]) : Type[0] ≝ 
   | nil: list A
@@ -54,3 +55,491 @@ ndefinition tail ≝ λA:Type[0].λl:list A.
 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;//;
+#a;#l1;#IH;nnormalize;
+nrewrite > IH;//;
+nqed.
+
+ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
+#A;#x;#y;#z;nelim x
+##[//
+##|#a;#x1;#H;nnormalize;//]
+nqed.
+
+ntheorem cons_append_commute:
+  ∀A:Type[0].∀l1,l2:list A.∀a:A.
+    a :: (l1 @ l2) = (a :: l1) @ l2.
+//;
+nqed.
+
+nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
+#A;#a;#l;#l1;nrewrite > (associative_append ????);//;
+nqed.
+
+(*ninductive permutation (A:Type) : list A -> list A -> Prop \def
+  | refl : \forall l:list A. permutation ? l l
+  | swap : \forall l:list A. \forall x,y:A. 
+              permutation ? (x :: y :: l) (y :: x :: l)
+  | trans : \forall l1,l2,l3:list A.
+              permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
+with permut1 : list A -> list A -> Prop \def
+  | step : \forall l1,l2:list A. \forall x,y:A. 
+      permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
+
+(*
+
+definition x1 \def S O.
+definition x2 \def S x1.
+definition x3 \def S x2.
+   
+theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
+  apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
+  apply refl.
+  apply (step ? (x1::[]) [] x2 x3).
+  qed. 
+
+theorem nil_append_nil_both:
+  \forall A:Type.\forall l1,l2:list A.
+    l1 @ l2 = [] \to l1 = [] \land l2 = [].
+
+theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. 
+reflexivity.
+qed.
+
+theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
+simplify.
+reflexivity.
+qed.
+
+*)
+
+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 ]. 
+
+nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ 
+  match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
+   
+ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
+
+ndefinition filter ≝ 
+  λT:Type[0].λl:list T.λp:T → bool.
+  foldr T (list T) 
+    (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
+
+ndefinition iota : nat → nat → list nat ≝
+  λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
+  
+(* ### induction principle for functions visiting 2 lists in parallel *)
+nlemma list_ind2 : 
+  ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
+  length ? l1 = length ? l2 →
+  (P (nil ?) (nil ?)) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
+  P l1 l2.
+#T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
+ngeneralize in match Hl; ngeneralize in match l2;
+nelim l1
+##[#l2;ncases l2;//;
+   nnormalize;#t2;#tl2;#H;ndestruct;
+##|#t1;#tl1;#IH;#l2;ncases l2
+   ##[nnormalize;#H;ndestruct
+   ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
+##]
+nqed.
+
+nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A;#B;#f;#g;#l;#Efg;
+nelim l; nnormalize;//;
+nqed.
+
+nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
+#A;#l;#p;nelim l;nnormalize
+##[//
+##|#a;#tl;#IH;ncases (p a);nnormalize;
+   ##[napply le_S_S;//;
+   ##|@2;//]
+##]
+nqed.
+
+nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
+#A;#l;#m;nelim l;
+##[//
+##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
+nqed.
+
+ninductive in_list (A:Type): A → (list A) → Prop ≝
+| in_list_head : ∀ x,l.(in_list A x (x::l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
+
+ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
+  \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
+  
+notation "hvbox(a break ∉ b)" non associative with precedence 45
+for @{ 'notmem $a $b }. 
+  
+interpretation "list member" 'mem x l = (in_list ? x l).
+interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
+interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
+  
+nlemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
+#A x;@;#H1;ninversion H1;
+##[#a0 al0 H2 H3;ndestruct (H3);
+##|#a0 a1 al0 H2 H3 H4 H5;ndestruct (H5)
+##]
+nqed.
+
+nlemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
+                          x = a \lor in_list A x l.
+#A a0 a1 al0 H1;ninversion H1
+##[#a2 al1 H2 H3;ndestruct (H3);@;@
+##|#a2 a3 al1 H2 H3 H4 H5;ndestruct (H5);@2;//
+##]
+nqed.
+
+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.
+
+nlemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
+#A a0 a1 H1;ncases (in_list_cons_case ???? H1)
+##[//
+##|#H2;napply False_ind;ncases (not_in_list_nil ? a0);#H3;/2/
+##]
+nqed.
+
+nlemma in_list_to_in_list_append_l: \forall A.\forall x:A.
+\forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
+#A a0 al0 al1 H1;nelim H1
+##[#a1 al2;@;
+##|#a1 a2 al2 H2 H3;@2;//
+##]
+nqed.
+
+nlemma in_list_to_in_list_append_r: \forall A.\forall x:A.
+\forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
+#A a0 al0 al1 H1;nelim al0
+##[napply H1
+##|#a1 al2 IH;@2;napply IH
+##]
+nqed.
+
+nlemma in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
+\forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
+#A a0 al0;nelim al0
+##[#al1 H1;@2;napply H1
+##|#a1 al1 IH al2 H1;nnormalize in H1;
+   ncases (in_list_cons_case ???? H1);#H2
+   ##[@;nrewrite > H2;@
+   ##|ncases (IH … H2);#H3
+      ##[@;@2;//
+      ##|@2;//
+      ##]
+   ##]
+##]
+nqed.
+
+nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
+ match l with
+  [ nil ⇒ false
+  | (cons a l') ⇒
+    match eq x a with
+     [ true ⇒ true
+     | false ⇒ mem A eq x l'
+     ]
+  ].
+  
+nlemma mem_true_to_in_list :
+  \forall A,equ.
+  (\forall x,y.equ x y = true \to x = y) \to
+  \forall x,l.mem A equ x l = true \to in_list A x l.
+#A equ H1 a0 al0;nelim al0
+##[nnormalize;#H2;ndestruct (H2)
+##|#a1 al1 IH H2;nwhd in H2:(??%?);
+   nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3
+   ##[nrewrite > (H1 … H3);@
+   ##|@2;napply IH;nrewrite > H3 in H2;nnormalize;//;
+   ##]
+##]
+nqed.
+
+nlemma in_list_to_mem_true :
+  \forall A,equ.
+  (\forall x.equ x x = true) \to
+  \forall x,l.in_list A x l \to mem A equ x l = true.
+#A equ H1 a0 al0;nelim al0
+##[#H2;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H2;nelim H2
+   ##[nnormalize;#a2 al2;nrewrite > (H1 …);@
+   ##|#a2 a3 al2 H3 H4;nnormalize;ncases (equ a2 a3);nnormalize;//;
+   ##]
+##]
+nqed.
+
+nlemma in_list_filter_to_p_true : \forall A,l,x,p.
+in_list A x (filter A l p) \to p x = true.
+#A al0 a0 p;nelim al0
+##[nnormalize;#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H1;nnormalize in H1;nlapply (refl ? (p a1));
+   ngeneralize in match H1;ncases (p a1) in ⊢ (???% -> ???% → %);
+   ##[#H2 H3;ncases (in_list_cons_case ???? H2);#H4
+      ##[nrewrite > H4;//
+      ##|napply (IH H4);
+      ##]
+   ##|#H2 H3;napply (IH H2);
+   ##]
+##]
+nqed.
+
+nlemma in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
+#A al0 p a0;nelim al0
+##[nnormalize;//;
+##|#a1 al1 IH H1;nnormalize in H1;
+   nlapply (refl ? (p a1));ncases (p a1) in ⊢ (???% → %);#H2
+   ##[nrewrite > H2 in H1;#H1;ncases (in_list_cons_case ???? H1);#H3
+      ##[nrewrite > H3;@
+      ##|@2;napply IH;napply H3
+      ##]
+   ##|@2;napply IH;nrewrite > H2 in H1;#H1;napply H1;
+   ##]
+##]
+nqed.
+
+nlemma in_list_filter_r : \forall A,l,p,x.
+              in_list A x l \to p x = true \to in_list A x (filter A l p).
+#A al0 p a0;nelim al0
+##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
+##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3
+   ##[nnormalize;nrewrite < H3;nrewrite > H2;@
+   ##|nnormalize;ncases (p a1);nnormalize;
+      ##[@2;napply IH;//
+      ##|napply IH;//
+      ##]
+   ##]
+##]
+nqed.
+   
+nlemma incl_A_A: ∀T,A.incl T A A.
+#A al0 a0 H1;//;
+nqed.
+
+nlemma incl_append_l : ∀T,A,B.incl T A (A @ B).
+#A al0 al1 a0 H1;/2/;
+nqed.
+
+nlemma incl_append_r : ∀T,A,B.incl T B (A @ B).
+#A al0 al1 a0 H1;/2/;
+nqed.
+
+nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+#A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/;
+#H3;@2;napply H1;//;
+nqed.
+
+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.
+
+nlemma incl_incl_to_incl_append : 
+  ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
+#A al0 al1 al2 al3 H1 H2 a0 H3;
+ncases (in_list_append_to_or_in_list ???? H3);#H4;
+##[napply in_list_to_in_list_append_l;napply H1;//
+##|napply in_list_to_in_list_append_r;napply H2;//
+##]
+nqed.
+  
+nlemma eq_map_append : 
+  ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.
+#A B f al1 al2;nelim al1
+##[@
+##|#a0 al3 IH;nnormalize;nrewrite > IH;@;
+##]
+nqed.
+
+nlemma 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.
+#A equ H1 a0 al0;nelim al0
+##[#_;@
+##|#a1 al1 IH H2;nwhd in ⊢ (??%?);
+   nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3;
+   ##[napply False_ind;ncases H2;#H4;napply H4;
+      nrewrite > (H1 … H3);@
+   ##|napply IH;@;#H4;ncases H2;#H5;napply H5;@2;//
+   ##]
+##]
+nqed.
+
+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.