-- File: list -- This file introduces lists. -- It consists of two parts. -- 1. Axioms, corresponding to Section 4.5 -- 2. Library, corresponding to Section 4.6 -- naming conventions for lemmas: -- variables for Lists are always ending in s -- e.g. as,xs,ys Load "bool" ----------------------- ----------------------- -- -- -- 1. A X I O M S -- -- -- ----------------------- ----------------------- Var List : *s -> *s Var nil : @A:*s. List A -- Name in lemmas: cons Var (;) : @A:*s. A -> List A -> List A Implicit 1 (;) InfixR 5 (;) Var primreclist : @A,B:*s. B-> (A -> List A -> B -> B) -> List A -> B Implicit 2 primreclist Var primreclist_nil : @A,B:*s. @nv:B. @sv: A -> List A -> B -> B. primreclist nv sv (nil A) = nv Var primreclist_cons : @A,B:*s. @nv:B. @sv: A -> List A -> B -> B. @head:A. @tail:List A. primreclist nv sv (head;tail) = sv head tail (primreclist nv sv tail) Var indlist : @A:*s. @P:List A->*p. P (nil A) -> (@a:A. @as:List A. P as -> P (a;as)) -> (@as:List A. P as) ------------------------- ------------------------- -- -- -- 2. L I B R A R Y -- -- -- ------------------------- ------------------------- -------------- -- iterlist -- -------------- -- iterlist is also known as foldr Def iterlist := \A,B:*s. \nv:B. \sv:A->B->B. primreclist nv (\a:A. \dummy:List A. sv a) : @A,B:*s. B-> (A -> B -> B) -> List A -> B Implicit 2 iterlist Prove iterlist_nil : @A,B:*s. @nv:B. @sv: A -> B -> B. iterlist nv sv (nil A) = nv Prove iterlist_cons : @A,B:*s. @nv:B. @sv: A -> B -> B. @head:A. @tail:List A. iterlist nv sv (head;tail) = sv head (iterlist nv sv tail) ---------- -- tail -- ---------- Def tail := \A:*s. primreclist (nil A) (\hd:A.\tl:List A.\p:List A.tl) Implicit 1 tail Prove tail_nil : @A:*s. tail (nil A) = nil A Prove tail_cons : @A:*s. @a:A. @l:List A. tail (a;l) = l ---------- -- head -- ---------- Def head := \A:*s. \a:A. iterlist a (\a':A. \prev:A.a') : @A:*s. A -> List A -> A Implicit 1 head Prove head_nil : @A:*s. @a:A. head a (nil A) = a Prove head_cons : @A:*s. @a,b:A. @l:List A. head a (b;l) = b ------------------------------------------- -- nil and cons are different injections -- ------------------------------------------- Prove nil_is_cons_ : @A:*s. @l:List A. @a:A. Not (nil A = a;l) Prove cons_is_nil_ : @A:*s. @l:List A. @a:A. Not (a;l = nil A) Prove cons_is_cons_ : @A:*s. @l1,l2:List A. @a1,a2:A. a1;l1 = a2;l2 -> a1 = a2 /\ l1=l2 ------------ -- concat -- ------------ -- Name in lemmas: concat Def (++) := \A:*s. \as,as' : List A. iterlist as' ( \hd:A. \concat_tail : List A. hd;concat_tail) as : @A:*s. List A -> List A -> List A Implicit 1 (++) Prove nil_concat : @A:*s. @as:List A. (nil A)++as = as Prove cons_concat : @A:*s. @a:A. @as,as': List A. (a;as) ++ as' = a ; (as++as') Prove concat_assoc : @A:*s. @bs,cs,as : List A. (as++bs)++cs = as++(bs++cs) Prove concat_nil : @A:*s. @as:List A. as ++ (nil A) = as --------------- -- singleton -- --------------- Def singleton := \A:*s. \a:A. a ; (nil A) : @A:*s. A -> List A Implicit 1 singleton ------------------- -- RELATION Elem -- ------------------- Def Elem := \A:*s.\a:A.\l:List A. @P:List A -> *p. (@m:List A. P (a;m)) -> (@m:List A.@b:A. P m -> P (b;m)) -> P l : @A:*s. A -> List A -> *p Implicit 1 Elem Prove Elem_a_a_cons : @A:*s.@a:A.@l:List A. Elem a (a;l) Prove Elem_a_b_cons : @A:*s.@a,b:A.@l:List A. Elem a l -> Elem a (b;l) Prove Elem_strong_ind : @A:*s.@a:A.@l:List A. Elem a l -> @P:List A -> *p. (@m:List A. P (a;m)) -> (@m:List A. @b:A. Elem a m -> P m -> P (b;m)) -> P l Prove Elem_exh : @A:*s.@a:A.@l:List A. Elem a l -> (Ex m:List A. l = a;m) \/ (Ex m:List A. Ex b:A. l = b;m /\ Elem a m) Prove Elem_nil_ : @A:*s. @a:A. Not (Elem a (nil A)) Prove Elem_cons_ : @A:*s.@a,b:A. @l:List A. Elem a (b;l) -> a=b \/ Elem a l