1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/pts.ma".
16 include "arithmetics/nat.ma".
18 ninductive list (A:Type[0]) : Type[0] ≝
20 | cons: A -> list A -> list A.
22 notation "hvbox(hd break :: tl)"
23 right associative with precedence 47
26 notation "[ list0 x sep ; ]"
27 non associative with precedence 90
28 for ${fold right @'nil rec acc @{'cons $x $acc}}.
30 notation "hvbox(l1 break @ l2)"
31 right associative with precedence 47
32 for @{'append $l1 $l2 }.
34 interpretation "nil" 'nil = (nil ?).
35 interpretation "cons" 'cons hd tl = (cons ? hd tl).
37 nlet rec append A (l1: list A) l2 on l1 ≝
40 | cons hd tl ⇒ hd :: append A tl l2 ].
42 interpretation "append" 'append l1 l2 = (append ? l1 l2).
44 nlet rec id_list A (l: list A) on l ≝
47 | cons hd tl ⇒ hd :: id_list A tl ].
50 ndefinition tail ≝ λA:Type[0].λl:list A.
55 nlet rec flatten S (l : list (list S)) on l : list S ≝
56 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
58 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
60 #a;#l1;#IH;nnormalize;
64 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
67 ##|#a;#x1;#H;nnormalize;//]
70 ntheorem cons_append_commute:
71 ∀A:Type[0].∀l1,l2:list A.∀a:A.
72 a :: (l1 @ l2) = (a :: l1) @ l2.
76 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
77 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
80 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
81 | refl : \forall l:list A. permutation ? l l
82 | swap : \forall l:list A. \forall x,y:A.
83 permutation ? (x :: y :: l) (y :: x :: l)
84 | trans : \forall l1,l2,l3:list A.
85 permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
86 with permut1 : list A -> list A -> Prop \def
87 | step : \forall l1,l2:list A. \forall x,y:A.
88 permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
92 definition x1 \def S O.
93 definition x2 \def S x1.
94 definition x3 \def S x2.
96 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
97 apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
99 apply (step ? (x1::[]) [] x2 x3).
102 theorem nil_append_nil_both:
103 \forall A:Type.\forall l1,l2:list A.
104 l1 @ l2 = [] \to l1 = [] \land l2 = [].
106 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
110 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
117 nlet rec nth A l d n on l ≝
120 | cons (x:A) tl ⇒ match n with
122 | S n' ⇒ nth A tl d n' ] ].
124 nlet rec map A B f l on l ≝
125 match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
127 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
128 match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
130 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
133 λT:Type[0].λl:list T.λp:T → bool.
135 (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
137 ndefinition iota : nat → nat → list nat ≝
138 λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
140 (* ### induction principle for functions visiting 2 lists in parallel *)
142 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
143 length ? l1 = length ? l2 →
144 (P (nil ?) (nil ?)) →
145 (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
147 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
148 ngeneralize in match Hl; ngeneralize in match l2;
151 nnormalize;#t2;#tl2;#H;ndestruct;
152 ##|#t1;#tl1;#IH;#l2;ncases l2
153 ##[nnormalize;#H;ndestruct
154 ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
158 nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
160 nelim l; nnormalize;//;
163 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
164 #A;#l;#p;nelim l;nnormalize
166 ##|#a;#tl;#IH;ncases (p a);nnormalize;
172 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
175 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
178 ninductive in_list (A:Type): A → (list A) → Prop ≝
179 | in_list_head : ∀ x,l.(in_list A x (x::l))
180 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
182 ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
183 \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
185 notation "hvbox(a break ∉ b)" non associative with precedence 45
186 for @{ 'notmem $a $b }.
188 interpretation "list member" 'mem x l = (in_list ? x l).
189 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
190 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
192 nlemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
193 #A x;@;#H1;ninversion H1;
194 ##[#a0 al0 H2 H3;ndestruct (H3);
195 ##|#a0 a1 al0 H2 H3 H4 H5;ndestruct (H5)
199 nlemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
200 x = a \lor in_list A x l.
201 #A a0 a1 al0 H1;ninversion H1
202 ##[#a2 al1 H2 H3;ndestruct (H3);@;@
203 ##|#a2 a3 al1 H2 H3 H4 H5;ndestruct (H5);@2;//
207 nlemma in_list_tail : \forall A,l,x,y.
208 in_list A x (y::l) \to x \neq y \to in_list A x l.
209 #A;#l;#x;#y;#H;#Hneq;
211 ##[#x1;#l1;#Hx;#Hl;ndestruct;nelim Hneq;#Hfalse;
213 ##|#x1;#y1;#l1;#H1;#_;#Hx;#Heq;ndestruct;//;
217 nlemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
218 #A a0 a1 H1;ncases (in_list_cons_case ???? H1)
220 ##|#H2;napply False_ind;ncases (not_in_list_nil ? a0);#H3;/2/
224 nlemma in_list_to_in_list_append_l: \forall A.\forall x:A.
225 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
226 #A a0 al0 al1 H1;nelim H1
228 ##|#a1 a2 al2 H2 H3;@2;//
232 nlemma in_list_to_in_list_append_r: \forall A.\forall x:A.
233 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
234 #A a0 al0 al1 H1;nelim al0
236 ##|#a1 al2 IH;@2;napply IH
240 nlemma in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
241 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
243 ##[#al1 H1;@2;napply H1
244 ##|#a1 al1 IH al2 H1;nnormalize in H1;
245 ncases (in_list_cons_case ???? H1);#H2
247 ##|ncases (IH … H2);#H3
255 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
261 | false ⇒ mem A eq x l'
265 nlemma mem_true_to_in_list :
267 (\forall x,y.equ x y = true \to x = y) \to
268 \forall x,l.mem A equ x l = true \to in_list A x l.
269 #A equ H1 a0 al0;nelim al0
270 ##[nnormalize;#H2;ndestruct (H2)
271 ##|#a1 al1 IH H2;nwhd in H2:(??%?);
272 nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3
273 ##[nrewrite > (H1 … H3);@
274 ##|@2;napply IH;nrewrite > H3 in H2;nnormalize;//;
279 nlemma in_list_to_mem_true :
281 (\forall x.equ x x = true) \to
282 \forall x,l.in_list A x l \to mem A equ x l = true.
283 #A equ H1 a0 al0;nelim al0
284 ##[#H2;napply False_ind;ncases (not_in_list_nil ? a0);/2/
285 ##|#a1 al1 IH H2;nelim H2
286 ##[nnormalize;#a2 al2;nrewrite > (H1 …);@
287 ##|#a2 a3 al2 H3 H4;nnormalize;ncases (equ a2 a3);nnormalize;//;
292 nlemma in_list_filter_to_p_true : \forall A,l,x,p.
293 in_list A x (filter A l p) \to p x = true.
294 #A al0 a0 p;nelim al0
295 ##[nnormalize;#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
296 ##|#a1 al1 IH H1;nnormalize in H1;nlapply (refl ? (p a1));
297 ngeneralize in match H1;ncases (p a1) in ⊢ (???% -> ???% → %);
298 ##[#H2 H3;ncases (in_list_cons_case ???? H2);#H4
302 ##|#H2 H3;napply (IH H2);
307 nlemma in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
308 #A al0 p a0;nelim al0
310 ##|#a1 al1 IH H1;nnormalize in H1;
311 nlapply (refl ? (p a1));ncases (p a1) in ⊢ (???% → %);#H2
312 ##[nrewrite > H2 in H1;#H1;ncases (in_list_cons_case ???? H1);#H3
314 ##|@2;napply IH;napply H3
316 ##|@2;napply IH;nrewrite > H2 in H1;#H1;napply H1;
321 nlemma in_list_filter_r : \forall A,l,p,x.
322 in_list A x l \to p x = true \to in_list A x (filter A l p).
323 #A al0 p a0;nelim al0
324 ##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
325 ##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3
326 ##[nnormalize;nrewrite < H3;nrewrite > H2;@
327 ##|nnormalize;ncases (p a1);nnormalize;
335 nlemma incl_A_A: ∀T,A.incl T A A.
339 nlemma incl_append_l : ∀T,A,B.incl T A (A @ B).
340 #A al0 al1 a0 H1;/2/;
343 nlemma incl_append_r : ∀T,A,B.incl T B (A @ B).
344 #A al0 al1 a0 H1;/2/;
347 nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
348 #A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/;
352 nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝
355 | cons b bl ⇒ foldl A B f (f a b) bl ].
357 nlet rec foldl2 (A,B,C:Type[0]) (f:A → B → C → A) (a:A) (bl:list B) (cl:list C) on bl ≝
360 | cons b0 bl0 ⇒ match cl with
362 | cons c0 cl0 ⇒ foldl2 A B C f (f a b0 c0) bl0 cl0 ] ].
364 nlet rec foldr2 (A,B : Type[0]) (X : Type[0]) (f: A → B → X → X) (x:X)
365 (al : list A) (bl : list B) on al : X ≝
368 | cons a al1 ⇒ match bl with
370 | cons b bl1 ⇒ f a b (foldr2 ??? f x al1 bl1) ] ].
372 nlet rec rev (A:Type[0]) (l:list A) on l ≝
375 | cons hd tl ⇒ (rev A tl)@[hd] ].
377 notation > "hvbox(a break \liff b)"
378 left associative with precedence 25
381 notation "hvbox(a break \leftrightarrow b)"
382 left associative with precedence 25
385 interpretation "logical iff" 'iff x y = (iff x y).
387 ndefinition coincl : ∀A.list A → list A → Prop ≝ λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
389 notation > "hvbox(a break ≡ b)"
390 non associative with precedence 45
393 notation < "hvbox(term 46 a break ≡ term 46 b)"
394 non associative with precedence 45
397 interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
399 nlemma refl_coincl : ∀A.∀l:list A.l ≡ l.
403 nlemma coincl_rev : ∀A.∀l:list A.l ≡ rev ? l.
405 ##[##1,3:#H;napply False_ind;ncases (not_in_list_nil ? x);
407 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
408 ##[napply in_list_to_in_list_append_r;nrewrite > H1;@
409 ##|napply in_list_to_in_list_append_l;/2/
411 ##|#a l0 IH H;ncases (in_list_append_to_or_in_list ???? H);#H1
413 ##|nrewrite > (in_list_singleton_to_eq ??? H1);@
418 nlemma not_in_list_nil_r : ∀A.∀l:list A.l = [] → ∀x.x ∉ l.
420 ##[#;napply not_in_list_nil
421 ##|#a l0 IH Hfalse;ndestruct (Hfalse)
425 nlemma eq_filter_append :
426 ∀A,p,l1,l2.filter A (l1@l2) p = filter A l1 p@filter A l2 p.
429 ##|#a0 l0 IH;nwhd in ⊢ (??%(??%?));ncases (p a0)
430 ##[nwhd in ⊢ (??%%);nrewrite < IH;@
431 ##|nwhd in ⊢ (??%(??%?));nrewrite < IH;@
437 ∀A,B:Type[0].∀f:A→B.∀P:B → Prop.
438 ∀al.(∀a.a ∈ al → P (f a)) →
439 ∀b. b ∈ map ?? f al → P b.
441 ##[#H1 b Hfalse;napply False_ind;
442 ncases (not_in_list_nil ? b);#H2;napply H2;napply Hfalse;
443 ##|#a1 al1 IH H1 b Hin;nwhd in Hin:(???%);ncases (in_list_cons_case ???? Hin);
444 ##[#e;nrewrite > e;napply H1;@
446 ##[#a2 Hin2;napply H1;@2;//;
454 ∀A,B,C,f,g,l.map B C f (map A B g l) = map A C (λx.f (g x)) l.
457 ##|#a0 al0 IH;nchange in ⊢ (??%%) with (cons ???);
462 nlemma incl_incl_to_incl_append :
463 ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
464 #A al0 al1 al2 al3 H1 H2 a0 H3;
465 ncases (in_list_append_to_or_in_list ???? H3);#H4;
466 ##[napply in_list_to_in_list_append_l;napply H1;//
467 ##|napply in_list_to_in_list_append_r;napply H2;//
471 nlemma eq_map_append :
472 ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.
473 #A B f al1 al2;nelim al1
475 ##|#a0 al3 IH;nnormalize;nrewrite > IH;@;
479 nlemma not_in_list_to_mem_false :
481 (∀x,y.equ x y = true → x = y) →
482 ∀x:A.∀l. x ∉ l → mem A equ x l = false.
483 #A equ H1 a0 al0;nelim al0
485 ##|#a1 al1 IH H2;nwhd in ⊢ (??%?);
486 nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3;
487 ##[napply False_ind;ncases H2;#H4;napply H4;
488 nrewrite > (H1 … H3);@
489 ##|napply IH;@;#H4;ncases H2;#H5;napply H5;@2;//
494 nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝
497 | cons a al ⇒ p a ∧ list_forall A al p ].
500 ∀A,B,f,g,xl.(∀x.x ∈ xl → f x = g x) → map A B f xl = map A B g xl.
503 ##|#a al IH H1;nwhd in ⊢ (??%%);napply eq_f2
505 ##|napply IH;#x Hx;napply H1;@2;//
510 nlemma x_in_map_to_eq :
511 ∀A,B,f,x,l.x ∈ map A B f l → ∃x'.x = f x' ∧ x' ∈ l.
513 ##[#H;ncases (not_in_list_nil ? x);#H1;napply False_ind;napply (H1 H)
514 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
515 ##[nrewrite > H1;@ a;@;@
516 ##|ncases (IH H1);#a0;*;#H2 H3;@a0;@
522 nlemma list_forall_false :
523 ∀A:Type[0].∀x,xl,p. p x = false → x ∈ xl → list_forall A xl p = false.
524 #A x xl p H1;nelim xl
525 ##[#Hfalse;napply False_ind;ncases (not_in_list_nil ? x);#H2;napply (H2 Hfalse)
526 ##|#x0 xl0 IH H2;ncases (in_list_cons_case ???? H2);#H3
527 ##[nwhd in ⊢ (??%?);nrewrite < H3;nrewrite > H1;@
528 ##|nwhd in ⊢ (??%?);ncases (p x0)
529 ##[nrewrite > (IH H3);@
536 nlemma list_forall_true :
537 ∀A:Type[0].∀xl,p. (∀x.x ∈ xl → p x = true) → list_forall A xl p = true.
540 ##|#x0 xl0 IH H1;nwhd in ⊢ (??%?);nrewrite > (H1 …)
541 ##[napply IH;#x Hx;napply H1;@2;//