Package list-reverse: The list reverse function

Information

namelist-reverse
version1.33
descriptionThe list reverse function
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
list-append
list-def
list-length
list-map
list-set
natural
set
showData.Bool
Data.List
Number.Natural
Set

Files

Defined Constant

Theorems

reverse [] = []

l. reverse (reverse l) = l

l. length (reverse l) = length l

l. toSet (reverse l) = toSet l

l x. member x (reverse l) member x l

f l. reverse (map f l) = map f (reverse l)

l1 l2. reverse (l1 @ l2) = reverse l2 @ reverse l1

h t. reverse (h :: t) = reverse t @ h :: []

Input Type Operators

Input Constants

Assumptions

length [] = 0

toSet [] =

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

m. m + 0 = m

l. [] @ l = l

l. l @ [] = l

f. map f [] = []

() = λp q. p q p

s t. s t = t s

h t. length (h :: t) = suc (length t)

l x. member x l x toSet l

() = λp q. (λf. f p q) = λf. f

h t. toSet (h :: t) = insert h (toSet t)

x s. insert x s = insert x s

m n. m + suc n = suc (m + n)

l1 l2. length (l1 @ l2) = length l1 + length l2

l1 l2. toSet (l1 @ l2) = toSet l1 toSet l2

l h t. (h :: t) @ l = h :: t @ l

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

p. (x. y. p x y) y. x. p x (y x)

f h t. map f (h :: t) = f h :: map f t

f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2

p. p [] (h t. p t p (h :: t)) l. p l

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)