list

List.reverseNil

def reverseNil (A : Type) : reverse (nil : List A) = (nil : List A)

Reversing the empty list gives the empty list.

List.reverseCons

def reverseCons {A : Type} (x : A) (xs : List A) : reverse (cons x xs) = revAcc xs (cons x (nil : List A))

Reversing a cons unfolds to the accumulator-based reversal of the tail with the head as the initial accumulator.

List.myAppendNil

def myAppendNil {A : Type} (xs : List A) : append xs (nil : List A) = xs

Appending the empty list on the right leaves a list unchanged.

List.myAppendAssoc

def myAppendAssoc {A : Type} (xs : List A) (ys : List A) (zs : List A) : append (append xs ys) zs = append xs (append ys zs)

List append is associative.

List.myMapId

def myMapId {A : Type} (xs : List A) : map (fun (x : A) => x) xs = xs

Mapping the identity function over a list leaves it unchanged.

List.myLengthMap

def myLengthMap {A B : Type} (f : A -> B) (xs : List A) : length (map f xs) = length xs

Mapping a function over a list preserves its length.

List.mapFusion

def mapFusion {A B : Type} {C : Type} (f : B -> C) (g : A -> B) (xs : List A) : map f (map g xs) = map (fun (x : A) => f (g x)) xs

Mapping two functions in sequence over a list equals mapping their composition.

List.mapReplicate

def mapReplicate {A B : Type} (f : A -> B) (n : Nat) (x : A) : map f (replicate n x) = replicate n (f x)

Mapping a function over a list of n copies of x gives n copies of f x.

List.zipSigma

def zipSigma {A B : Type} (xs : List A) (ys : List B) : List ((a : A) × B)

Pairs up corresponding elements of two lists as dependent pairs, stopping at the shorter list.

List.unzip

def unzip {A B : Type} (xs : List ((a : A) × B)) : (a : List A) × List B

Splits a list of pairs into the list of first components and the list of second components.

List.takeZero

def takeZero {A : Type} (xs : List A) : take zero xs = (nil : List A)

Taking zero elements gives the empty list.

List.dropZero

def dropZero {A : Type} (xs : List A) : drop zero xs = xs

Dropping zero elements leaves a list unchanged.

List.snocNil

def snocNil {A : Type} (x : A) : snoc (nil : List A) x = cons x (nil : List A)

Appending an element to the end of the empty list gives a singleton list.

List.appendSingle

def appendSingle {A : Type} (xs : List A) (y : A) : append xs (cons y nil) = snoc xs y

Appending a singleton list equals adding that element to the end with snoc.

List.lengthNil

def lengthNil {A : Type} : length (nil : List A) = zero

The empty list has length zero.

List.lengthCons

def lengthCons {A : Type} (x : A) (xs : List A) : length (cons x xs) = succ (length xs)

The length of a cons is one more than the length of its tail.

List.mapDistAppend

def mapDistAppend {A B : Type} (f : A -> B) (xs : List A) (ys : List A) : map f (append xs ys) = append (map f xs) (map f ys)

Mapping over an appended list equals appending the mapped lists.

List.replicateZero

def replicateZero {A : Type} (x : A) : replicate zero x = (nil : List A)

Zero copies of a value form the empty list.

List.replicateOne

def replicateOne {A : Type} (x : A) : replicate (succ zero) x = cons x (nil : List A)

One copy of a value forms a singleton list.

List.zipSigmaNilL

def zipSigmaNilL {A B : Type} (ys : List B) : zipSigma (nil : List A) ys = (nil : List ((a : A) × B))

Zipping the empty list with any list gives the empty list.

List.zipSigmaNilR

def zipSigmaNilR {A B : Type} (xs : List A) : zipSigma xs (nil : List B) = (nil : List ((a : A) × B))

Zipping any list with the empty list gives the empty list.

List.appendNilL

def appendNilL {A : Type} (xs : List A) : append (nil : List A) xs = xs

The empty list is a left identity for append.

List.lengthSnoc

def lengthSnoc {A : Type} (xs : List A) (x : A) : length (snoc xs x) = succ (length xs)

Adding an element to the end of a list increases its length by one.

List.snocCons

def snocCons {A : Type} (x : A) (xs : List A) (y : A) : snoc (cons x xs) y = cons x (snoc xs y)

Adding an element to the end of a cons keeps the head in front.

List.nthOptionZeroCons

def nthOptionZeroCons {A : Type} (x : A) (xs : List A) : nthOption (cons x xs) zero = some x

Indexing a cons at zero gives its head.

List.nthOptionSuccCons

def nthOptionSuccCons {A : Type} (x : A) (xs : List A) (n : Nat) : nthOption (cons x xs) (succ n) = nthOption xs n

Indexing a cons at a successor index indexes into its tail.

List.nthOptionNil

def nthOptionNil {A : Type} (n : Nat) : nthOption (nil : List A) n = (none : Option A)

Indexing the empty list at any position gives nothing.

List.isNil

def isNil {A : Type} (xs : List A) : Bool

Returns true exactly when the list is empty.

List.listSum

def listSum (xs : List Nat) : Nat

Sums a list of natural numbers with a left fold.

List.listProduct

def listProduct (xs : List Nat) : Nat

Multiplies a list of natural numbers with a left fold, giving one for the empty list.

List.filterNil

def filterNil {A : Type} (p : A -> Bool) : filter p (nil : List A) = (nil : List A)

Filtering the empty list gives the empty list.

List.takeNil

def takeNil {A : Type} (n : Nat) : take n (nil : List A) = (nil : List A)

Taking any number of elements from the empty list gives the empty list.

List.dropNil

def dropNil {A : Type} (n : Nat) : drop n (nil : List A) = (nil : List A)

Dropping any number of elements from the empty list gives the empty list.

List.concatNil

def concatNil {A : Type} : concat (nil : List (List A)) = (nil : List A)

Concatenating an empty list of lists gives the empty list.

List.concatCons

def concatCons {A : Type} (xs : List A) (xss : List (List A)) : concat (cons xs xss) = append xs (concat xss)

Concatenating a cons of lists appends the first list to the concatenation of the rest.

List.spanSigmaAcc

def spanSigmaAcc {A : Type} (p : A -> Bool) (xs : List A) (acc : List A) : (a : List A) × List A

Accumulator helper for spanSigma: collects the longest prefix satisfying the predicate and returns it with the remaining suffix.

List.spanSigma

def spanSigma {A : Type} (p : A -> Bool) (xs : List A) : (a : List A) × List A

Splits a list at the first element that fails the predicate, returning the prefix and the suffix as a pair.

List.partitionSigmaAcc

def partitionSigmaAcc {A : Type} (p : A -> Bool) (xs : List A) (yes_acc : List A) (no_acc : List A) : (a : List A) × List A

Accumulator helper for partitionSigma: collects the elements that satisfy and fail the predicate in two accumulators.

List.partitionSigma

def partitionSigma {A : Type} (p : A -> Bool) (xs : List A) : (a : List A) × List A

Splits a list into the elements that satisfy the predicate and those that do not, preserving order.

List.elemNatList

def elemNatList (x : Nat) (xs : List Nat) : Bool

Returns true when the natural number occurs in the list.

List.nubAcc

def nubAcc (xs : List Nat) (seen : List Nat) : List Nat

Accumulator helper for nub: drops elements already present in the list of seen values.

List.nub

def nub (xs : List Nat) : List Nat

Removes duplicate natural numbers from a list, keeping the first occurrence of each.

List.mapConst

def mapConst {A B : Type} (c : B) (xs : List A) : map (fun (_ : A) => c) xs = replicate (length xs) c

Mapping a constant function over a list gives that many copies of the constant.

List.lengthMapNat

def lengthMapNat (f : Nat -> Nat) (xs : List Nat) : length (map f xs) = length xs

Mapping a function over a list of natural numbers preserves its length.

List.isSorted

def isSorted (xs : List Nat) : Bool

Returns true when a list of natural numbers is sorted in ascending order.

List.countNat

def countNat (n : Nat) (xs : List Nat) : Nat

Counts how many times a natural number occurs in a list.

List.sumList

def sumList (xs : List Nat) : Nat

Sums a list of natural numbers by direct recursion.

List.productList

def productList (xs : List Nat) : Nat

Multiplies a list of natural numbers by direct recursion, giving one for the empty list.

List.maxList

def maxList (xs : List Nat) : Nat

Returns the maximum of a list of natural numbers, or zero for the empty list.

List.minList

def minList (xs : List Nat) : Nat

Returns the minimum of a list of natural numbers, or zero for the empty list.

List.sumListSingle

def sumListSingle (n : Nat) : sumList (cons n nil) = n

The sum of a singleton list is its element.

List.scanlNat

def scanlNat (f : Nat -> Nat -> Nat) (z : Nat) (xs : List Nat) : List Nat

Left scan over natural numbers: returns every intermediate accumulator, starting with the initial value.

List.scanrNatGo

def scanrNatGo (f : Nat -> Nat -> Nat) (z : Nat) (xs : List Nat) : (a : Nat) × List Nat

Helper for scanrNat that returns the final right-fold value together with the list of intermediate values.

List.scanrNat

def scanrNat (f : Nat -> Nat -> Nat) (z : Nat) (xs : List Nat) : List Nat

Right scan over natural numbers: returns every intermediate right-fold value, ending with the initial value.

List.intercalateNat

def intercalateNat (sep : List Nat) (xss : List (List Nat)) : List Nat

Joins a list of lists of natural numbers, inserting the separator list between consecutive lists.

List.countNatNil

def countNatNil (n : Nat) : countNat n (nil : List Nat) = zero

Counting occurrences in the empty list gives zero.

List.lastOption

def lastOption {A : Type} (xs : List A) : Option A

Returns the last element of a list, or nothing for the empty list.

List.headNat

def headNat (xs : List Nat) : Nat

Returns the first element of a list of natural numbers, or zero for the empty list.

List.tailList

def tailList {A : Type} (xs : List A) : List A

Returns the list without its first element, or the empty list for the empty list.

List.tailListLength

def tailListLength {A : Type} (xs : List A) : length (tailList xs) = pred (length xs)

Dropping the head of a list decreases its length by one, truncated at zero.

List.insertSorted

def insertSorted (x : Nat) (xs : List Nat) : List Nat

Inserts a natural number into a sorted list, keeping it sorted.

List.insertionSort

def insertionSort (xs : List Nat) : List Nat

Sorts a list of natural numbers by insertion sort.

List.unfoldrNat

def unfoldrNat (fuel : Nat) (f : Nat -> Option ((a : Nat) × Nat)) (seed : Nat) : List Nat

Unfolds a list of natural numbers from a seed for at most fuel steps, stopping early when the step function returns nothing.

List.countdownStep

def countdownStep (n : Nat) : Option ((a : Nat) × Nat)

Step function for countdown: emits n and continues from n - 1, stopping at zero.

List.countdown

def countdown (n : Nat) : List Nat

Generates the list n, n - 1, …, 1.

List.unfoldrNatZeroFuel

def unfoldrNatZeroFuel (f : Nat -> Option ((a : Nat) × Nat)) (s : Nat) : unfoldrNat zero f s = (nil : List Nat)

Unfolding with zero fuel gives the empty list.

List.groupByNatAcc

def groupByNatAcc (xs : List Nat) (cur : Nat) (curGroup : List Nat) : List (List Nat)

Accumulator helper for groupByNat: extends the current group while elements equal the current value.

List.groupByNat

def groupByNat (xs : List Nat) : List (List Nat)

Groups consecutive equal natural numbers into sublists.

List.appendConsL

def appendConsL {A : Type} (x : A) (xs : List A) (ys : List A) : append (cons x xs) ys = cons x (append xs ys)

Appending to a cons keeps the head in front.

List.lengthAppendList

def lengthAppendList (xs : List Nat) (ys : List Nat) : length (append xs ys) = add (length xs) (length ys)

The length of an appended list of natural numbers is the sum of the lengths.

List.appendAssocNat

def appendAssocNat (xs : List Nat) (ys : List Nat) (zs : List Nat) : append (append xs ys) zs = append xs (append ys zs)

Append is associative on lists of natural numbers.

List.appendNilRNat

def appendNilRNat (xs : List Nat) : append xs (nil : List Nat) = xs

Appending the empty list on the right leaves a list of natural numbers unchanged.

List.mapAppendNat

def mapAppendNat (f : Nat -> Nat) (xs : List Nat) (ys : List Nat) : map f (append xs ys) = append (map f xs) (map f ys)

Mapping over an appended list of natural numbers equals appending the mapped lists.

List.mapIdNatList

def mapIdNatList (xs : List Nat) : map (fun (x : Nat) => x) xs = xs

Mapping the identity function over a list of natural numbers leaves it unchanged.

List.mapCompNat

def mapCompNat (f : Nat -> Nat) (g : Nat -> Nat) (xs : List Nat) : map g (map f xs) = map (fun (x : Nat) => g (f x)) xs

Mapping two functions in sequence over a list of natural numbers equals mapping their composition.

List.foldrConsId

def foldrConsId (xs : List Nat) : foldr (fun (y : Nat) => fun (ys : List Nat) => cons y ys) (nil : List Nat) xs = xs

Right-folding cons over a list with the empty list as the base gives back the list.

List.foldrAppendNat

def foldrAppendNat (xss : List (List Nat)) : foldr (fun (a : List Nat) => fun (b : List Nat) => append a b) (nil : List Nat) xss = concat xss

Right-folding append over a list of lists equals concatenating them.

List.sumListAppend

def sumListAppend (xs : List Nat) (ys : List Nat) : sumList (append xs ys) = add (sumList xs) (sumList ys)

The sum of an appended list is the sum of the two sums.

List.sumListCons

def sumListCons (x : Nat) (xs : List Nat) : sumList (cons x xs) = add x (sumList xs)

The sum of a cons is the head plus the sum of the tail.

List.productListCons

def productListCons (x : Nat) (xs : List Nat) : productList (cons x xs) = mul x (productList xs)

The product of a cons is the head times the product of the tail.

List.sumListReplicate

def sumListReplicate (n : Nat) (x : Nat) : sumList (replicate n x) = mul n x

The sum of n copies of x is n times x.

List.revAccNil

def revAccNil {A : Type} (acc : List A) : revAcc (nil : List A) acc = acc

Accumulator reversal of the empty list returns the accumulator.

List.revAccCons

def revAccCons {A : Type} (x : A) (xs : List A) (acc : List A) : revAcc (cons x xs) acc = revAcc xs (cons x acc)

Accumulator reversal of a cons moves the head onto the accumulator.

List.reverseSingleton

def reverseSingleton {A : Type} (x : A) : reverse (cons x nil) = cons x (nil : List A)

Reversing a singleton list leaves it unchanged.

List.takeSuccCons

def takeSuccCons {A : Type} (n : Nat) (x : A) (xs : List A) : take (succ n) (cons x xs) = cons x (take n xs)

Taking n + 1 elements of a cons keeps the head and takes n from the tail.

List.dropSuccCons

def dropSuccCons {A : Type} (n : Nat) (x : A) (xs : List A) : drop (succ n) (cons x xs) = drop n xs

Dropping n + 1 elements of a cons drops n from the tail.

List.filterTrueNat

def filterTrueNat (xs : List Nat) : filter (fun (_ : Nat) => true) xs = xs

Filtering a list of natural numbers with the always-true predicate leaves it unchanged.

List.filterFalseNat

def filterFalseNat (xs : List Nat) : filter (fun (_ : Nat) => false) xs = (nil : List Nat)

Filtering a list of natural numbers with the always-false predicate gives the empty list.

List.lengthReplicateNat

def lengthReplicateNat (n : Nat) (x : Nat) : length (replicate n x) = n

A list of n copies of a natural number has length n.

List.replicateSucc

def replicateSucc {A : Type} (n : Nat) (x : A) : replicate (succ n) x = cons x (replicate n x)

n + 1 copies of x is x followed by n copies of x.

List.mapReplicateNat

def mapReplicateNat (f : Nat -> Nat) (n : Nat) (x : Nat) : map f (replicate n x) = replicate n (f x)

Mapping a function over n copies of a natural number gives n copies of its image.

List.lengthSnocNat

def lengthSnocNat (xs : List Nat) (x : Nat) : length (snoc xs x) = succ (length xs)

Adding an element to the end of a list of natural numbers increases its length by one.

List.takeWhileNat

def takeWhileNat (p : Nat -> Bool) (xs : List Nat) : List Nat

Returns the longest prefix of a list of natural numbers whose elements all satisfy the predicate.

List.dropWhileNat

def dropWhileNat (p : Nat -> Bool) (xs : List Nat) : List Nat

Drops the longest prefix of a list of natural numbers whose elements all satisfy the predicate.

List.takeWhileTrue

def takeWhileTrue (xs : List Nat) : takeWhileNat (fun (_ : Nat) => true) xs = xs

takeWhileNat with the always-true predicate leaves a list unchanged.

List.dropWhileTrue

def dropWhileTrue (xs : List Nat) : dropWhileNat (fun (_ : Nat) => true) xs = (nil : List Nat)

dropWhileNat with the always-true predicate gives the empty list.

List.takeWhileFalse

def takeWhileFalse (xs : List Nat) : takeWhileNat (fun (_ : Nat) => false) xs = (nil : List Nat)

takeWhileNat with the always-false predicate gives the empty list.

List.findNat

def findNat (p : Nat -> Bool) (xs : List Nat) : Option Nat

Returns the first natural number in the list that satisfies the predicate, or nothing.

List.findIndexNatGo

def findIndexNatGo (p : Nat -> Bool) (xs : List Nat) (idx : Nat) : Option Nat

Helper for findIndexNat that tracks the current index.

List.findIndexNat

def findIndexNat (p : Nat -> Bool) (xs : List Nat) : Option Nat

Returns the index of the first natural number in the list that satisfies the predicate, or nothing.

List.removeNat

def removeNat (x : Nat) (xs : List Nat) : List Nat

Removes the first occurrence of a natural number from a list.

List.replaceNat

def replaceNat (old : Nat) (new : Nat) (xs : List Nat) : List Nat

Replaces the first occurrence of a natural number in a list with a new value.

List.flatMapNat

def flatMapNat (f : Nat -> List Nat) (xs : List Nat) : List Nat

Maps each natural number to a list and concatenates the results.

List.flatMapNatId

def flatMapNatId (xs : List Nat) : flatMapNat (fun (x : Nat) => cons x nil) xs = xs

flatMapNat with the singleton function leaves a list unchanged.

List.crossList

def crossList : List Nat

Example list 3, 1, 4, 1, 5 used to check several properties on the same data.

List.revAccAppendNat

def revAccAppendNat (xs : List Nat) (acc : List Nat) (zs : List Nat) : revAcc xs (append acc zs) = append (revAcc xs acc) zs

Accumulator reversal commutes with appending a suffix to the accumulator, for lists of natural numbers.

List.revAccAppendListNat

def revAccAppendListNat (xs : List Nat) (ys : List Nat) (acc : List Nat) : revAcc (append xs ys) acc = revAcc ys (revAcc xs acc)

Accumulator reversal of an appended list reverses the first part onto the accumulator and then the second.

List.revAppendNat

def revAppendNat (xs : List Nat) (ys : List Nat) : reverse (append xs ys) = append (reverse ys) (reverse xs)

Reversing an appended list of natural numbers appends the reversed second list to the reversed first list.

List.revAccRev

def revAccRev {A : Type} (xs : List A) (acc : List A) : revAcc (revAcc xs acc) nil = revAcc acc xs

Reversing the result of an accumulator reversal gives the accumulator reversed onto the original list.

List.revRev

def revRev {A : Type} (xs : List A) : reverse (reverse xs) = xs

Reversing a list twice gives back the original list.

List.crossList2

def crossList2 : List Nat

Example list 2, 0, 3, 0, 1 used to check several properties on the same data.

List.elemBy

def elemBy {A : Type} (eq : A -> A -> Bool) (a : A) (xs : List A) : Bool

Returns true when the list contains an element equal to a under the given equality test.

List.countBy

def countBy {A : Type} (p : A -> Bool) (xs : List A) : Nat

Counts the elements of a list that satisfy the predicate.

List.nubByAcc

def nubByAcc {A : Type} (eq : A -> A -> Bool) (xs : List A) (acc : List A) : List A

Accumulator helper for nubBy: keeps an element only if it is not equal to one already kept.

List.nubBy

def nubBy {A : Type} (eq : A -> A -> Bool) (xs : List A) : List A

Removes duplicates from a list under the given equality test, keeping the first occurrence of each.

List.scanl

def scanl {A B : Type} (f : B -> A -> B) (z : B) (xs : List A) : List B

Left scan: like foldl but returns every intermediate accumulator, starting with the initial value.

List.scanlLength

def scanlLength {A B : Type} (f : B -> A -> B) (z : B) (xs : List A) : length (scanl f z xs) = succ (length xs)

A left scan has one more element than the input list.

List.lastNat

def lastNat (default : Nat) (xs : List Nat) : Nat

Returns the last element of a list of natural numbers, or the default for the empty list.

List.zipNilL

def zipNilL {A B : Type} (ys : List B) : zip (nil : List A) ys = (nil : List (Pair A B))

Zipping the empty list with any list gives the empty list.

List.zipNilR

def zipNilR {A B : Type} (xs : List A) : zip xs (nil : List B) = (nil : List (Pair A B))

Zipping any list with the empty list gives the empty list.

List.intersperseNil

def intersperseNil {A : Type} (sep : A) : intersperse sep (nil : List A) = (nil : List A)

Interspersing a separator into the empty list gives the empty list.

List.intersperseSingle

def intersperseSingle {A : Type} (sep : A) (x : A) : intersperse sep (cons x nil) = cons x (nil : List A)

Interspersing a separator into a singleton list leaves it unchanged.

List.replicateTwo

def replicateTwo {A : Type} (x : A) : replicate (succ (succ zero)) x = cons x (cons x (nil : List A))

Two copies of x form the list x, x.

List.replicateThree

def replicateThree {A : Type} (x : A) : replicate (succ (succ (succ zero))) x = cons x (cons x (cons x (nil : List A)))

Three copies of x form the list x, x, x.

List.allNil

def allNil {A : Type} (p : A -> Bool) : all p (nil : List A) = true

Every element of the empty list satisfies any predicate.

List.anyNil

def anyNil {A : Type} (p : A -> Bool) : any p (nil : List A) = false

No element of the empty list satisfies any predicate.

List.zipWithNilL

def zipWithNilL {A B : Type} {C : Type} (f : A -> B -> C) (ys : List B) : zipWith f (nil : List A) ys = (nil : List C)

zipWith with the empty list on the left gives the empty list.

List.zipWithNilR

def zipWithNilR {A B : Type} {C : Type} (f : A -> B -> C) (xs : List A) : zipWith f xs (nil : List B) = (nil : List C)

zipWith with the empty list on the right gives the empty list.

List.scanlNil

def scanlNil {A B : Type} (f : B -> A -> B) (z : B) : scanl f z (nil : List A) = cons z (nil : List B)

A left scan over the empty list gives the singleton of the initial value.

List.list_return_v140

def list_return_v140 {A : Type} (x : A) : List A

The unit of the list monad: wraps a value in a singleton list.

List.listBind

def listBind {A B : Type} (xs : List A) (f : A -> List B) : List B

The bind of the list monad: applies a list-valued function to each element and concatenates the results.

List.listBindReturn

def listBindReturn {A B : Type} (x : A) (f : A -> List B) : listBind (list_return_v140 x) f = append (f x) (nil : List B)

Binding a singleton list to f gives f x appended with the empty list.

List.listBindReturnNil

def listBindReturnNil {A : Type} : listBind (nil : List A) (fun (x : A) => list_return_v140 x) = (nil : List A)

Binding the empty list to the unit gives the empty list.

List.listBindNil

def listBindNil {A B : Type} (f : A -> List B) : listBind (nil : List A) f = (nil : List B)

Binding the empty list to any function gives the empty list.

List.listBindCons

def listBindCons {A B : Type} (x : A) (xs : List A) (f : A -> List B) : listBind (cons x xs) f = append (f x) (listBind xs f)

Binding a cons appends the image of the head to the bind of the tail.

List.concatMap_v140

def concatMap_v140 {A B : Type} (f : A -> List B) (xs : List A) : List B

Maps each element to a list and concatenates the results.

List.concatMapNil

def concatMapNil {A B : Type} (f : A -> List B) : concatMap_v140 f (nil : List A) = (nil : List B)

concatMap over the empty list gives the empty list.

List.concatMapCons

def concatMapCons {A B : Type} (f : A -> List B) (x : A) (xs : List A) : concatMap_v140 f (cons x xs) = append (f x) (concatMap_v140 f xs)

concatMap over a cons appends the image of the head to the concatMap of the tail.

List.concatMapSingletonNil

def concatMapSingletonNil {A : Type} : concatMap_v140 (fun (x : A) => cons x (nil : List A)) (nil : List A) = (nil : List A)

concatMap of the singleton function over the empty list gives the empty list.

List.iterate_v140

def iterate_v140 {A : Type} (f : A -> A) (n : Nat) (x : A) : List A

Returns the first n iterates x, f x, f (f x), … of a function.

List.iterateZeroV140

def iterateZeroV140 {A : Type} (f : A -> A) (x : A) : iterate_v140 f zero x = (nil : List A)

Zero iterates give the empty list.

List.iterateOneV140

def iterateOneV140 {A : Type} (f : A -> A) (x : A) : iterate_v140 f (succ zero) x = cons x (nil : List A)

One iterate gives the singleton of the starting value.

List.iterateTwo

def iterateTwo {A : Type} (f : A -> A) (x : A) : iterate_v140 f (succ (succ zero)) x = cons x (cons (f x) (nil : List A))

Two iterates give x followed by f x.

List.unfoldr

def unfoldr {A B : Type} (f : B -> (a : A) × B) (n : Nat) (b : B) : List A

Unfolds a list from a seed for exactly n steps, each step producing an element and a new seed.

List.unfoldrZero

def unfoldrZero {A B : Type} (f : B -> (a : A) × B) (b : B) : unfoldr f zero b = (nil : List A)

Unfolding for zero steps gives the empty list.

List.listAppendAssoc

def listAppendAssoc {A : Type} (xs ys zs : List A) : append (append xs ys) zs = append xs (append ys zs)

List append is associative.

List.zipWithNilLeft

def zipWithNilLeft {A B C : Type} (f : A -> B -> C) (ys : List B) : zipWith f (nil : List A) ys = (nil : List C)

zipWith with the empty list on the left gives the empty list.

List.zipWithNilRight

def zipWithNilRight {A B C : Type} (f : A -> B -> C) (x : A) (xs : List A) : zipWith f (cons x xs) (nil : List B) = (nil : List C)

zipWith of a cons with the empty list gives the empty list.

List.zipWithConsCons

def zipWithConsCons {A B C : Type} (f : A -> B -> C) (x : A) (xs : List A) (y : B) (ys : List B) : zipWith f (cons x xs) (cons y ys) = cons (f x y) (zipWith f xs ys)

zipWith of two conses combines the heads and zips the tails.

List.zipSigmaConsNil

def zipSigmaConsNil {A B : Type} (x : A) (xs : List A) : zipSigma (cons x xs) (nil : List B) = (nil : List ((a : A) × B))

Zipping a cons with the empty list as dependent pairs gives the empty list.

List.listLen0

def listLen0 {A : Type} : List A

The empty list, as an example of a list of length zero.

List.listLen1

def listLen1 {A : Type} (x : A) : List A

A singleton list, as an example of a list of length one.

List.listLen1Length

def listLen1Length {A : Type} (x : A) : length (listLen1 x) = succ zero

The example singleton list has length one.

List.listLen2

def listLen2 {A : Type} (x y : A) : List A

A two-element list, as an example of a list of length two.

List.listLen2Length

def listLen2Length {A : Type} (x y : A) : length (listLen2 x y) = succ (succ zero)

The example two-element list has length two.

List.reverseLengthPreserve

def reverseLengthPreserve {A : Type} (xs : List A) : length (reverse xs) = length xs

Reversing a list preserves its length.

List.revAccLength

def revAccLength {A : Type} (xs : List A) (acc : List A) : length (revAcc xs acc) = add (length xs) (length acc)

The length of an accumulator reversal is the length of the list plus the length of the accumulator.

List.reverseLength

def reverseLength {A : Type} (xs : List A) : length (reverse xs) = length xs

Reversing a list preserves its length.

List.reverseLengthPreserveV140Helper

def reverseLengthPreserveV140Helper {A : Type} (y : A) (ys : List A) : length (reverse (cons y ys)) = length (cons y ys)

Reversing a cons preserves its length.

List.appendNilNil

def appendNilNil {A : Type} : append (nil : List A) (nil : List A) = (nil : List A)

Appending two empty lists gives the empty list.

List.appendNilCons

def appendNilCons {A : Type} (x : A) (xs : List A) : append (nil : List A) (cons x xs) = cons x xs

Appending a cons to the empty list gives the cons.

List.appendConsNil

def appendConsNil {A : Type} (x : A) : append (cons x (nil : List A)) (nil : List A) = cons x (nil : List A)

Appending the empty list to a singleton list gives the singleton list.

List.appendLengthNil

def appendLengthNil {A : Type} (xs : List A) : length (append xs (nil : List A)) = length xs

Appending the empty list on the right preserves the length.

List.list140c

def list140c : List Nat

Example list 3, 2, 1, 0 used in concrete checks.

List.setNth

def List.setNth {A : Type} (xs : List A) (n : Nat) (x : A) : List A

The list with the element at index n replaced by x; an index past the end leaves the list unchanged.

List.lengthSetNth

def List.lengthSetNth {A : Type} (xs : List A) (n : Nat) (x : A) : length (List.setNth xs n x) = length xs

Replacing an element keeps the length.

List.nthOptionAppendLeft

def List.nthOptionAppendLeft {A : Type} (xs : List A) (ys : List A) (i : Nat) : Nat.blt i (length xs) = true -> List.nthOption (append xs ys) i = List.nthOption xs i

An index inside the first list reads the first list.

List.nthOptionAppendRight

def List.nthOptionAppendRight {A : Type} (xs : List A) (ys : List A) (i : Nat) : Nat.blt i (length xs) = false -> List.nthOption (append xs ys) i = List.nthOption ys (Nat.sub i (length xs))

An index past the first list reads the second, shifted by the first list’s length.

List.setNthAppendLeft

def List.setNthAppendLeft {A : Type} (xs : List A) (ys : List A) (i : Nat) (x : A) : Nat.blt i (length xs) = true -> List.setNth (append xs ys) i x = append (List.setNth xs i x) ys

Replacing inside the first list replaces in the first list.

List.setNthAppendRight

def List.setNthAppendRight {A : Type} (xs : List A) (ys : List A) (i : Nat) (x : A) : Nat.blt i (length xs) = false -> List.setNth (append xs ys) i x = append xs (List.setNth ys (Nat.sub i (length xs)) x)

Replacing past the first list replaces in the second, shifted by the first list’s length.

List.nthOptionSetNthSame

def List.nthOptionSetNthSame {A : Type} (xs : List A) (n : Nat) (x : A) : Nat.blt n (length xs) = true -> List.nthOption (List.setNth xs n x) n = some x

Reading the replaced index gives the new element.

List.nthOptionSetNthOther

def List.nthOptionSetNthOther {A : Type} (xs : List A) (n : Nat) (m : Nat) (x : A) : Nat.beq n m = false -> List.nthOption (List.setNth xs n x) m = List.nthOption xs m

Reading another index is unaffected by the replacement.

List.setNthOutside

def List.setNthOutside {A : Type} (xs : List A) (n : Nat) (x : A) : Nat.blt n (length xs) = false -> List.setNth xs n x = xs

Replacing past the end leaves the list unchanged.

List.allSome

def List.allSome {A : Type} (xs : List (Option A)) : Bool

Whether every cell holds a value.

List.somes

def List.somes {A : Type} (xs : List (Option A)) : List A

The values of the cells, skipping empty ones.

List.nthOptionOutside

def List.nthOptionOutside {A : Type} (xs : List A) (i : Nat) : Nat.blt i (length xs) = false -> List.nthOption xs i = none

Reading past the end gives none.

List.nthOptionTake

def List.nthOptionTake {A : Type} (n : Nat) (xs : List A) (i : Nat) : Nat.blt i n = true -> List.nthOption (List.take n xs) i = List.nthOption xs i

Reading inside a prefix reads the list.

List.lengthTake

def List.lengthTake {A : Type} (n : Nat) (xs : List A) : Nat.ble n (length xs) = true -> length (List.take n xs) = n

A prefix no longer than the list has the asked length.

List.takeSetNth

def List.takeSetNth {A : Type} (n : Nat) (xs : List A) (i : Nat) (x : A) : List.take n (List.setNth xs i x) = List.setNth (List.take n xs) i x

Replacing inside a prefix commutes with taking the prefix.

List.lengthSomes

def List.lengthSomes {A : Type} (xs : List (Option A)) : List.allSome xs = true -> length (List.somes xs) = length xs

When every cell holds a value, the values are as many as the cells.

List.nthOptionSomes

def List.nthOptionSomes {A : Type} (xs : List (Option A)) (i : Nat) : List.allSome xs = true -> List.nthOption (List.somes xs) i = Option.bind (List.nthOption xs i) (fun (c : Option A) => c)

When every cell holds a value, reading the values reads the cell’s value.

List.allSomeSetNth

def List.allSomeSetNth {A : Type} (xs : List (Option A)) (i : Nat) (x : A) : List.allSome xs = true -> List.allSome (List.setNth xs i (some x)) = true

Writing a value keeps every cell holding a value.

List.somesSetNth

def List.somesSetNth {A : Type} (xs : List (Option A)) (i : Nat) (x : A) : List.allSome xs = true -> List.somes (List.setNth xs i (some x)) = List.setNth (List.somes xs) i x

Writing a value into full cells writes the value into the values.

List.takeSuccSetNth

def List.takeSuccSetNth {A : Type} (n : Nat) (xs : List A) (x : A) : Nat.blt n (length xs) = true -> List.take (succ n) (List.setNth xs n x) = List.snoc (List.take n xs) x

Taking one past a replaced index ends with the new element.

List.takeAppendLeft

def List.takeAppendLeft {A : Type} (n : Nat) (xs : List A) (ys : List A) : Nat.ble n (length xs) = true -> List.take n (append xs ys) = List.take n xs

A prefix of the first list is a prefix of the concatenation.

List.allSomeSnoc

def List.allSomeSnoc {A : Type} (xs : List (Option A)) (x : A) : List.allSome xs = true -> List.allSome (List.snoc xs (some x)) = true

Appending a value keeps every cell holding a value.

List.somesSnoc

def List.somesSnoc {A : Type} (xs : List (Option A)) (x : A) : List.somes (List.snoc xs (some x)) = List.snoc (List.somes xs) x

The values of cells ending with a value end with that value.

List.takeTakeSucc

def List.takeTakeSucc {A : Type} (m : Nat) (xs : List A) : List.take m (List.take (succ m) xs) = List.take m xs

Within a longer prefix, the shorter prefix is the same.

List.allSomeTake

def List.allSomeTake {A : Type} (m : Nat) (xs : List (Option A)) : List.allSome xs = true -> List.allSome (List.take m xs) = true

A prefix of full cells is full.

List.somesTake

def List.somesTake {A : Type} (m : Nat) (xs : List (Option A)) : List.allSome xs = true -> List.somes (List.take m xs) = List.take m (List.somes xs)

When every cell holds a value, the values of a prefix are the prefix of the values.

List.nilOfLengthZero

def List.nilOfLengthZero {A : Type} (xs : List A) : length xs = zero -> xs = nil

A list of length zero is empty.