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 "basics/eq.ma".
16 include "basics/bool.ma".
18 ninductive list (A:Type) : Type :=
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 ndefinition not_nil: ∀A:Type.list A → Prop ≝
38 λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
41 ∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
42 #A; #l; #a; #Heq; nchange with (not_nil ? (a::l));
47 let rec id_list A (l: list A) on l :=
50 | (cons hd tl) => hd :: id_list A tl ]. *)
52 nlet rec append A (l1: list A) l2 on l1 :=
55 | cons hd tl ⇒ hd :: append A tl l2 ].
57 ndefinition tail := λA:Type.λl: list A.
62 interpretation "append" 'append l1 l2 = (append ? l1 l2).
64 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
65 #A; #l; nelim l; nnormalize;//; nqed.
67 ntheorem associative_append:
68 ∀A:Type.associative (list A) (append A).
69 #A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed.
71 ntheorem cons_append_commute:
72 ∀A:Type.∀l1,l2:list A.∀a:A.
73 a :: (l1 @ l2) = (a :: l1) @ l2.
76 ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
79 nlet rec map (A,B:Type) (f: A → B) (l:list A) on l: list B ≝
80 match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
82 nlet rec foldr (A,B:Type) (f:A → B → B) (b:B) (l:list A) on l :B ≝
83 match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
86 λT:Type.λl:list T.λp:T → bool.
87 foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0).
89 ntheorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
90 #A; #B; #f; #g; #l; #eqfg; nelim l; nnormalize; //; nqed.