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".
17 ninductive list (A:Type[0]) : Type[0] ≝
19 | cons: A -> list A -> list A.
21 notation "hvbox(hd break :: tl)"
22 right associative with precedence 47
25 notation "[ list0 x sep ; ]"
26 non associative with precedence 90
27 for ${fold right @'nil rec acc @{'cons $x $acc}}.
29 notation "hvbox(l1 break @ l2)"
30 right associative with precedence 47
31 for @{'append $l1 $l2 }.
33 interpretation "nil" 'nil = (nil ?).
34 interpretation "cons" 'cons hd tl = (cons ? hd tl).
37 ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
38 #A;#l;#a; @; #H; ndestruct;
41 nlet rec id_list A (l: list A) on l ≝
44 | cons hd tl ⇒ hd :: id_list A tl ].
46 nlet rec append A (l1: list A) l2 on l1 ≝
49 | cons hd tl ⇒ hd :: append A tl l2 ].
51 ndefinition tail ≝ λA:Type[0].λl:list A.
56 interpretation "append" 'append l1 l2 = (append ? l1 l2).
58 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
60 #a;#l1;#IH;nnormalize;//;
63 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
66 ##|#a;#x1;#H;nnormalize;//]
69 ntheorem cons_append_commute:
70 ∀A:Type[0].∀l1,l2:list A.∀a:A.
71 a :: (l1 @ l2) = (a :: l1) @ l2.
75 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
76 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
79 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
80 | refl : \forall l:list A. permutation ? l l
81 | swap : \forall l:list A. \forall x,y:A.
82 permutation ? (x :: y :: l) (y :: x :: l)
83 | trans : \forall l1,l2,l3:list A.
84 permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
85 with permut1 : list A -> list A -> Prop \def
86 | step : \forall l1,l2:list A. \forall x,y:A.
87 permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
91 definition x1 \def S O.
92 definition x2 \def S x1.
93 definition x3 \def S x2.
95 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
96 apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
98 apply (step ? (x1::[]) [] x2 x3).
101 theorem nil_append_nil_both:
102 \forall A:Type.\forall l1,l2:list A.
103 l1 @ l2 = [] \to l1 = [] \land l2 = [].
105 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
109 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
116 nlet rec nth A l d n on n ≝
120 | cons (x : A) _ ⇒ x ]
121 | S n' ⇒ nth A (tail ? l) d n'].
123 nlet rec map A B f l on l ≝
124 match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
126 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
127 match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
129 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
132 λT:Type[0].λl:list T.λp:T → bool.
134 (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
136 ndefinition iota : nat → nat → list nat ≝
137 λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
139 (* ### induction principle for functions visiting 2 lists in parallel *)
141 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
142 length ? l1 = length ? l2 →
143 (P (nil ?) (nil ?)) →
144 (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
146 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
147 ngeneralize in match Hl; ngeneralize in match l2;
150 nnormalize;#t2;#tl2;#H;ndestruct;
151 ##|#t1;#tl1;#IH;#l2;ncases l2
152 ##[nnormalize;#H;ndestruct
153 ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
157 nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
159 nelim l; nnormalize;//;
162 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
163 #A;#l;#p;nelim l;nnormalize
165 ##|#a;#tl;#IH;ncases (p a);nnormalize;
171 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
174 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
177 ninductive in_list (A:Type): A → (list A) → Prop ≝
178 | in_list_head : ∀ x,l.(in_list A x (x::l))
179 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
181 ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
182 \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
184 notation "hvbox(a break ∉ b)" non associative with precedence 45
185 for @{ 'notmem $a $b }.
187 interpretation "list member" 'mem x l = (in_list ? x l).
188 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
189 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
191 naxiom not_in_list_nil : \forall A,x.\lnot in_list A x [].
192 (*intros.unfold.intro.inversion H
193 [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
197 naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
198 x = a \lor in_list A x l.
199 (*intros;inversion H;intros
200 [destruct H2;left;reflexivity
201 |destruct H4;right;assumption]
204 naxiom in_list_tail : \forall l,x,y.
205 in_list nat x (y::l) \to x \neq y \to in_list nat x l.
206 (*intros 4;elim (in_list_cons_case ? ? ? ? H)
211 naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
212 (*intros;elim (in_list_cons_case ? ? ? ? H)
214 |elim (not_in_list_nil ? ? H1)]
217 naxiom in_list_to_in_list_append_l: \forall A.\forall x:A.
218 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
222 |apply in_list_cons;assumption
226 naxiom in_list_to_in_list_append_r: \forall A.\forall x:A.
227 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
231 |apply in_list_cons;apply H;assumption
235 naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
236 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
240 |simplify in H1.inversion H1;intros; destruct;
241 [left.apply in_list_head
243 [left.apply in_list_cons. assumption
251 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
257 | false ⇒ mem A eq x l'
261 naxiom mem_true_to_in_list :
263 (\forall x,y.equ x y = true \to x = y) \to
264 \forall x,l.mem A equ x l = true \to in_list A x l.
266 [simplify in H1;destruct H1
267 |simplify in H2;apply (bool_elim ? (equ x a))
268 [intro;rewrite > (H ? ? H3);apply in_list_head
269 |intro;rewrite > H3 in H2;simplify in H2;
270 apply in_list_cons;apply H1;assumption]]
273 naxiom in_list_to_mem_true :
275 (\forall x.equ x x = true) \to
276 \forall x,l.in_list A x l \to mem A equ x l = true.
278 [elim (not_in_list_nil ? ? H1)
280 [simplify;rewrite > H;reflexivity
281 |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
284 naxiom in_list_filter_to_p_true : \forall A,l,x,p.
285 in_list A x (filter A l p) \to p x = true.
287 [simplify in H;elim (not_in_list_nil ? ? H)
288 |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
290 [elim (in_list_cons_case ? ? ? ? H1)
291 [rewrite > H3;assumption
296 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
298 [simplify in H;elim (not_in_list_nil ? ? H)
299 |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
301 [elim (in_list_cons_case ? ? ? ? H1)
302 [rewrite > H3;apply in_list_head
303 |apply in_list_cons;apply H;assumption]
304 |apply in_list_cons;apply H;assumption]]
307 naxiom in_list_filter_r : \forall A,l,p,x.
308 in_list A x l \to p x = true \to in_list A x (filter A l p).
310 [elim (not_in_list_nil ? ? H)
311 |elim (in_list_cons_case ? ? ? ? H1)
312 [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
313 |simplify;apply (bool_elim ? (p a));intro;simplify;
314 [apply in_list_cons;apply H;assumption
315 |apply H;assumption]]]
318 naxiom incl_A_A: ∀T,A.incl T A A.
319 (*intros.unfold incl.intros.assumption.
322 naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
323 (*unfold incl; intros;autobatch.
326 naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
327 (*unfold incl; intros;autobatch.
330 naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
331 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.