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 "arithmetics/nat.ma".
16 include "datatypes/list.ma".
19 ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
20 #A;#l;#a; @; #H; ndestruct;
23 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [ ] = l.
25 #a;#l1;#IH;nnormalize;//;
28 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
31 ##|#a;#x1;#H;nnormalize;//]
34 ntheorem cons_append_commute:
35 ∀A:Type[0].∀l1,l2:list A.∀a:A.
36 a :: (l1 @ l2) = (a :: l1) @ l2.
40 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
41 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
44 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
45 | refl : \forall l:list A. permutation ? l l
46 | swap : \forall l:list A. \forall x,y:A.
47 permutation ? (x :: y :: l) (y :: x :: l)
48 | trans : \forall l1,l2,l3:list A.
49 permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
50 with permut1 : list A -> list A -> Prop \def
51 | step : \forall l1,l2:list A. \forall x,y:A.
52 permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
56 definition x1 \def S O.
57 definition x2 \def S x1.
58 definition x3 \def S x2.
60 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
61 apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
63 apply (step ? (x1::[]) [] x2 x3).
66 theorem nil_append_nil_both:
67 \forall A:Type.\forall l1,l2:list A.
68 l1 @ l2 = [] \to l1 = [] \land l2 = [].
70 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
74 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
81 nlet rec nth A l d n on n ≝
85 | cons (x : A) _ ⇒ x ]
86 | S n' ⇒ nth A (tail ? l) d n'].
88 nlet rec map A B f l on l ≝
89 match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
91 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
92 match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
94 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
97 λT:Type[0].λl:list T.λp:T → bool.
99 (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
101 ndefinition iota : nat → nat → list nat ≝
102 λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
104 (* ### induction principle for functions visiting 2 lists in parallel *)
106 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
107 length ? l1 = length ? l2 →
108 (P (nil ?) (nil ?)) →
109 (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
111 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
112 ngeneralize in match Hl; ngeneralize in match l2;
115 nnormalize;#t2;#tl2;#H;ndestruct;
116 ##|#t1;#tl1;#IH;#l2;ncases l2
117 ##[nnormalize;#H;ndestruct
118 ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
122 nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
124 nelim l; nnormalize;//;
127 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
128 #A;#l;#p;nelim l;nnormalize
130 ##|#a;#tl;#IH;ncases (p a);nnormalize;
136 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
139 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
142 ninductive in_list (A:Type): A → (list A) → Prop ≝
143 | in_list_head : ∀ x,l.(in_list A x (x::l))
144 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
146 ndefinition incl : \forall A.(list A) \to (list A) →Prop \def
147 \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
149 notation "hvbox(a break ∉ b)" non associative with precedence 45
150 for @{ 'notmem $a $b }.
152 interpretation "list member" 'mem x l = (in_list ? x l).
153 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
154 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
156 naxiom not_in_list_nil : \forall A,x.\lnot in_list A x [].
157 (*intros.unfold.intro.inversion H
158 [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
162 naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
163 x = a \lor in_list A x l.
164 (*intros;inversion H;intros
165 [destruct H2;left;reflexivity
166 |destruct H4;right;assumption]
169 naxiom in_list_tail : \forall l,x,y.
170 in_list nat x (y::l) \to x \neq y \to in_list nat x l.
171 (*intros 4;elim (in_list_cons_case ? ? ? ? H)
176 naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
177 (*intros;elim (in_list_cons_case ? ? ? ? H)
179 |elim (not_in_list_nil ? ? H1)]
182 naxiom in_list_to_in_list_append_l: \forall A.\forall x:A.
183 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
187 |apply in_list_cons;assumption
191 naxiom in_list_to_in_list_append_r: \forall A.\forall x:A.
192 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
196 |apply in_list_cons;apply H;assumption
200 naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
201 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
205 |simplify in H1.inversion H1;intros; destruct;
206 [left.apply in_list_head
208 [left.apply in_list_cons. assumption
216 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
222 | false ⇒ mem A eq x l'
226 naxiom mem_true_to_in_list :
228 (\forall x,y.equ x y = true \to x = y) \to
229 \forall x,l.mem A equ x l = true \to in_list A x l.
231 [simplify in H1;destruct H1
232 |simplify in H2;apply (bool_elim ? (equ x a))
233 [intro;rewrite > (H ? ? H3);apply in_list_head
234 |intro;rewrite > H3 in H2;simplify in H2;
235 apply in_list_cons;apply H1;assumption]]
238 naxiom in_list_to_mem_true :
240 (\forall x.equ x x = true) \to
241 \forall x,l.in_list A x l \to mem A equ x l = true.
243 [elim (not_in_list_nil ? ? H1)
245 [simplify;rewrite > H;reflexivity
246 |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
249 naxiom in_list_filter_to_p_true : \forall A,l,x,p.
250 in_list A x (filter A l p) \to p x = true.
252 [simplify in H;elim (not_in_list_nil ? ? H)
253 |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
255 [elim (in_list_cons_case ? ? ? ? H1)
256 [rewrite > H3;assumption
261 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
263 [simplify in H;elim (not_in_list_nil ? ? H)
264 |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
266 [elim (in_list_cons_case ? ? ? ? H1)
267 [rewrite > H3;apply in_list_head
268 |apply in_list_cons;apply H;assumption]
269 |apply in_list_cons;apply H;assumption]]
272 naxiom in_list_filter_r : \forall A,l,p,x.
273 in_list A x l \to p x = true \to in_list A x (filter A l p).
275 [elim (not_in_list_nil ? ? H)
276 |elim (in_list_cons_case ? ? ? ? H1)
277 [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
278 |simplify;apply (bool_elim ? (p a));intro;simplify;
279 [apply in_list_cons;apply H;assumption
280 |apply H;assumption]]]
283 naxiom incl_A_A: ∀T,A.incl T A A.
284 (*intros.unfold incl.intros.assumption.
287 naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
288 (*unfold incl; intros;autobatch.
291 naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
292 (*unfold incl; intros;autobatch.
295 naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
296 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.