Next: Finite Sets Up: List Previous: Permutation

Sorted Lists

This file sets up the predicate for sorted-ness of a list inductively using list_elim, from the predicate lelist, saying that a given element is less than some other list. The main purpose of the file is to establish a derived induction principle for sorted lists, sorted_list_induction, which was used to give a proof of insert sort in McKinna's (1992) PhD thesis.
``` ** Module lib_list_sorted Imports lib_list_PermII
lengthisahomomorphismcons = ... :
{A|Type}{l|list A}{n|nat}(Eq (suc n) (length l))->
Ex ([a:A]Eq l (cons a (tail l)))
Rlist = ... : {A|Type}{B|Type}(Rel A B)->A->(list B)->Prop
Sorted = ... : {A|Type}(Rel A A)->Pred (list A)
SortSpec = ... : {A|Type}(Rel A A)->Rel (list A) (list A)
sortedlistinduction = ... :
{A|Type}{R:Rel A A}{B|Type}{phi:Rel (list A) B}{n|B}
{c|A->(list A)->B->B}(phi (nil A) n)->
({a|A}{l|list A}{b|B}(Sorted R (cons a l))->(phi l b)->
phi (cons a l) (c a l b))->{l:list A}(Sorted R l)->
phi l (list_rec n ([a:A][l'12:list A][b:B]c a l'12 b) l)
nilSorted = ... : {A|Type}{R:Rel A A}Sorted R (nil A)
nilRlist = ... : {A|Type}{R:Rel A A}{c|A}Rlist R c (nil A)
heredSortedlemma = ... :
{A|Type}{R:Rel A A}{b|A}{n|list A}(Sorted R (cons b n))->Sorted R n
SortedImpliesRlist = ... :
{A|Type}{R:Rel A A}{b|A}{n|list A}(Sorted R (cons b n))->Rlist R b n
heredRlistlemma = ... :
{A|Type}{R:Rel A A}{b,c|A}{n|list A}(Rlist R c (cons b n))->
Rlist R c n
heredRlist1 = ... :
{A|Type}{R:Rel A A}{c|A}{m,n|list A}(Rlist R c (append m n))->
Rlist R c n
heredRlist2 = ... :
{A|Type}{R:Rel A A}{c|A}{m,n|list A}(Rlist R c (append m n))->
Rlist R c m
appclRlist = ... :
{A|Type}{R:Rel A A}{c|A}{m,n|list A}(Rlist R c m)->(Rlist R c n)->
Rlist R c (append m n)
heredSorted = ... :
{A|Type}{R:Rel A A}{m,n|list A}(Sorted R (append m n))->
(Sorted R m /\ Sorted R n)
RlistIsMonotone = ... :
{A|Type}{R:Rel A A}(trans R)->{b,c|A}{m|list A}(R c b)->
(Rlist R b m)->Rlist R c m
PermPreservesRlist = ... :
{A|Type}{R:Rel A A}{c|A}{m,n|list A}(Perm m n)->(Rlist R c m)->
Rlist R c n
{A|Type}{R:Rel A A}(refl R)->{b,c|A}{m,n|list A}
(Sorted R (cons b m))->(Sorted R (cons c n))->
(Perm (cons b m) (cons c n))->R b c