-- File: sort -- This file contains the example of sorting, as in Section 4.7 Load "nat" Load "list" ----------------------- -- PREDICATE Ordered -- ----------------------- -- Ordered is the smallest predicate with -- * Ordered nil -- * Ordered l -> (@b:Nat. Elem b l -> a<=b) -> Ordered (a;l) -- This is a nice definition, since there are only two clauses, that follow -- the structure of lists. Def Ordered := \l:List Nat. @P:List Nat -> *p. P (nil Nat) -> (@a:Nat.@m:List Nat. P m -> (@b:Nat. Elem b m -> a<=b) -> P (a;m)) -> P l : List Nat -> *p Prove Ordered_nil : Ordered (nil Nat) Prove Ordered_cons : @a:Nat.@m:List Nat. Ordered m -> (@b:Nat. Elem b m -> a<=b) -> Ordered (a;m) Prove Ordered_singleton : @m:Nat. Ordered (singleton m) Prove Ordered_exh : @l:List Nat. Ordered l -> l = nil Nat \/ Ex a:Nat. Ex m:List Nat. l = a;m /\ (@b:Nat. Elem b m -> a<=b) /\ Ordered m Prove Ordered_cons_ : @a:Nat.@m:List Nat. Ordered (a;m) -> (@b:Nat. Elem b m -> a<=b) /\ Ordered m ---------- -- Perm -- ---------- Def Perm := \A:*s. \as,bs: List A. @P : List A -> List A -> *p. (@xs:List A. P xs xs) -> (@xs,ys,zs:List A. P xs ys -> P ys zs -> P xs zs) -> (@xs,ys:List A.@x,y:A. P (xs++(x;y;ys)) (xs++(y;x;ys))) -> P as bs : @A:*s. List A -> List A -> *p Implicit 1 Perm -- An alternative definition of Perm is with clauses -- - @xs:List A. Perm xs xs -- - @xs,ys,zs:List A. Perm xs ys -> Perm ys zs -> Perm xs zs -- - @xs:List A. @x,y:A. Perm (x;y;bs) (y;x;bs) -- - @xs,ys:List A. @x:A. Perm xs ys -> Perm (x;xs) (Perm x;ys) -- Advantage: no concatenation necessary. -- Disadvantage: less intuitive. Prove Perm_refl : @A:*s. @xs:List A. Perm xs xs Prove Perm_trans : @A:*s. @xs,ys,zs:List A. Perm xs ys -> Perm ys zs -> Perm xs zs Prove Perm_swap : @A:*s. @xs,ys:List A.@x,y:A. Perm (xs++(x;y;ys)) (xs++(y;x;ys)) Prove Perm_cons : @A:*s. @a:A. @l,m:List A. Perm l m -> Perm (a;l) (a;m) Prove Perm_sym : @A:*s. @xs,ys:List A. Perm xs ys -> Perm ys xs --------------------- -- FUNCTION insert -- --------------------- Def insert := \n:Nat. primreclist (singleton n) ( \head:Nat. \tail:List Nat. \insert_tail:List Nat. if (leq n head) (n;head;tail) (head;insert_tail)) : Nat -> List Nat -> List Nat Prove insert_nil : @m:Nat. insert m (nil Nat) = singleton m Prove Le__insert : @m,n:Nat.@l:List Nat. m<=n -> insert m (n;l) = m;n;l Prove Gt__insert : @m,n:Nat.@l:List Nat. n<m -> insert m (n;l) = n;(insert m l) Prove Elem_insert_ : @m,n:Nat.@ns:List Nat. Elem m (insert n ns) -> m=n \/ Elem m ns Prove Ordered_insert : @m:Nat. @l:List Nat. Ordered l -> Ordered (insert m l) Prove Perm_insert : @m:Nat. @l:List Nat. Perm (insert m l) (m;l) ---------- -- sort -- ---------- -- sort [] = sort -- sort (x:xs) = insert x (sort xs) Def sort := primreclist (nil Nat) (\head:Nat. \tail:List Nat. \sort_tail:List Nat. insert head sort_tail) : List Nat -> List Nat -- bdRed sort (S O ; O ; nil Nat) -- 255 reductions! Prove sort_nil : sort (nil Nat) = nil Nat Prove sort_cons : @m:Nat.@l:List Nat. sort (m;l) = insert m (sort l) Prove Ordered_sort : @l:List Nat. Ordered (sort l) Prove Perm_sort : @l:List Nat. Perm (sort l) l