Package list-reverse: Definitions and theorems about the list reverse function

Information

namelist-reverse
version1.11
description Definitions and theorems about the list reverse function
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool
Data.List

Files

Defined Constant

Theorems

l. reverse (reverse l) = l

l. length (reverse l) = length l

l. toSet (reverse l) = toSet l

l m. reverse (l @ m) = reverse m @ reverse l

reverse [] = [] x l. reverse (x :: l) = reverse l @ x :: []

Input Type Operators

Input Constants

Assumptions

T

() = λP. P ((select) P)

t. (x. t) t

() = λp. p = λx. T

x. x = x T

l. l @ [] = l

() = λp q. p q p

s t. Set.∪ s t = Set.∪ t s

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

x s. Set.∪ (Set.insert x Set.∅) s = Set.insert x s

l m. length (l @ m) = Number.Natural.+ (length l) (length m)

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

l m n. l @ m @ n = (l @ m) @ n

length [] = 0 h t. length (h :: t) = Number.Natural.suc (length t)

toSet [] = Set.∅ h t. toSet (h :: t) = Set.insert h (toSet t)

P. P [] (a0 a1. P a1 P (a0 :: a1)) x. P x

NIL' CONS'.
    fn. fn [] = NIL' a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)

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

(n. Number.Natural.+ 0 n = n) (m. Number.Natural.+ m 0 = m)
  (m n.
     Number.Natural.+ (Number.Natural.suc m) n =
     Number.Natural.suc (Number.Natural.+ m n))
  m n.
    Number.Natural.+ m (Number.Natural.suc n) =
    Number.Natural.suc (Number.Natural.+ m n)