]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/lib/basics/list.ma
update in binaries for λδ
[helm.git] / matitaB / matita / lib / basics / list.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_______________________________________________________________ *)
11
12 include "basics/types.ma".
13 include "arithmetics/nat.ma".
14
15 inductive list (A:Type[0]) : Type[0] :=
16   | nil: list A
17   | cons: A -> list A -> list A.
18
19 notation "hvbox(hd break :: tl)"
20   right associative with precedence 47
21   for @{'cons $hd $tl}.
22
23 notation "[ list0 x sep ; ]"
24   non associative with precedence 90
25   for ${fold right @'nil rec acc @{'cons $x $acc}}.
26
27 notation "hvbox(l1 break @ l2)"
28   right associative with precedence 47
29   for @{'append $l1 $l2 }.
30
31 interpretation "nil" 'nil = (nil ?).
32 interpretation "cons" 'cons hd tl = (cons ? hd tl).
33
34 definition not_nil: ∀A:Type[0].list A → Prop ≝
35  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
36
37 theorem nil_cons:
38   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
39   #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
40 qed.
41
42 (*
43 let rec id_list A (l: list A) on l :=
44   match l with
45   [ nil => []
46   | (cons hd tl) => hd :: id_list A tl ]. *)
47
48 let rec append A (l1: list A) l2 on l1 ≝ 
49   match l1 with
50   [ nil ⇒  l2
51   | cons hd tl ⇒  hd :: append A tl l2 ].
52
53 definition hd ≝ λA.λl: list A.λd:A.
54   match l with [ nil ⇒ d | cons a _ ⇒ a].
55
56 definition tail ≝  λA.λl: list A.
57   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
58
59 interpretation "append" 'append l1 l2 = (append ? l1 l2).
60
61 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
62 #A #l (elim l) normalize // qed.
63
64 theorem associative_append: 
65  ∀A.associative (list A) (append A).
66 #A #l1 #l2 #l3 (elim l1) normalize // qed.
67
68 (* deleterio per auto 
69 ntheorem cons_append_commute:
70   ∀A:Type.∀l1,l2:list A.∀a:A.
71     a :: (l1 @ l2) = (a :: l1) @ l2.
72 //; nqed. *)
73
74 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
75 /2/ qed.
76
77 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
78   l1@l2=[] → P (nil A) (nil A) → P l1 l2.
79 #A #l1 #l2 #P (cases l1) normalize //
80 #a #l3 #heq destruct
81 qed.
82
83 theorem nil_to_nil:  ∀A.∀l1,l2:list A.
84   l1@l2 = [] → l1 = [] ∧ l2 = [].
85 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
86 qed.
87
88 (* iterators *)
89
90 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
91  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
92   
93 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
94  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
95  
96 definition filter ≝ 
97   λT.λp:T → bool.
98   foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
99
100 lemma filter_true : ∀A,l,a,p. p a = true → 
101   filter A p (a::l) = a :: filter A p l.
102 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
103
104 lemma filter_false : ∀A,l,a,p. p a = false → 
105   filter A p (a::l) = filter A p l.
106 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
107
108 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
109 #A #B #f #g #l #eqfg (elim l) normalize // qed.
110
111 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
112 match l1 with
113   [ nil ⇒ nil ?
114   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
115   ].
116
117 (**************************** length ******************************)
118
119 let rec length (A:Type[0]) (l:list A) on l ≝ 
120   match l with 
121     [ nil ⇒ 0
122     | cons a tl ⇒ S (length A tl)].
123
124 notation "|M|" non associative with precedence 60 for @{'norm $M}.
125 interpretation "norm" 'norm l = (length ? l).
126
127 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
128   match n with
129     [O ⇒ hd A l d
130     |S m ⇒ nth m A (tail A l) d].
131
132 (**************************** fold *******************************)
133
134 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
135  match l with 
136   [ nil ⇒ b 
137   | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
138       (fold A B op b p f l)].
139       
140 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
141   with precedence 80
142 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
143
144 notation "\fold [ op , nil ]_{ident i ∈ l } f"
145   with precedence 80
146 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
147
148 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
149
150 theorem fold_true: 
151 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
152   \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
153     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
154 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
155
156 theorem fold_false: 
157 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
158 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
159   \fold[op,nil]_{i ∈ l| p i} (f i).
160 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
161
162 theorem fold_filter: 
163 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
164   \fold[op,nil]_{i ∈ l| p i} (f i) = 
165     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
166 #A #B #a #l #p #op #nil #f elim l //  
167 #a #tl #Hind cases(true_or_false (p a)) #pa 
168   [ >filter_true // > fold_true // >fold_true //
169   | >filter_false // >fold_false // ]
170 qed.
171
172 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
173   {op :2> A → A → A; 
174    nill:∀a. op nil a = a; 
175    nilr:∀a. op a nil = a;
176    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
177   }.
178
179 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
180   op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
181     \fold[op,nil]_{i∈(I@J)} (f i).
182 #A #B #I #J #nil #op #f (elim I) normalize 
183   [>nill //|#a #tl #Hind <assoc //]
184 qed.
185