~/bend-docscommunity

list.bend checks

raw source on the hub · import bend-mathlib@0.1.0.1/list.bend as MList

2 imports
import Base
import ./nat.bend as MNat

Laws

law append_nil provedsource · line 5 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {List.append(a, A, xs, []) == xs : List<a, A>}

The empty list is a right identity for append: xs ++ [] = xs.

law nil_append provedsource · line 20 · raw

@-a:Quant -> @-A:Kind(a) -> @-xs:List<a, A> -> {List.append(a, A, [], xs) == xs : List<a, A>}

The empty list is a left identity for append: [] ++ xs = xs.

law append_assoc provedsource · line 30 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-ys:List<a, A> -> @-zs:List<a, A> -> {List.append(a, A, List.append(a, A, xs, ys), zs) == List.append(a, A, xs, List.append(a, A, ys, zs)) : List<a, A>}

Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).

law length_append provedsource · line 47 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-ys:List<a, A> -> {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat}

The length of an append is the sum of the lengths.

law reverse_go_spec provedsource · line 70 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-acc:List<a, A> -> {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List<a, A>}

The reverse accumulator loop appends the reversed list to the accumulator.

law reverse_append provedsource · line 92 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @ys:List<a, A> -> {List.reverse(a, A, List.append(a, A, xs, ys)) == List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) : List<a, A>}

Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.

law reverse_reverse provedsource · line 110 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List<a, A>}

Reversing twice gives the list back.

law length_reverse provedsource · line 129 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat}

Reversing preserves the length.

law foldr_append provedsource · line 139 · raw

@-a:Quant -> @-A:Kind(a) -> @-B:Type -> @-f:(@_:A -> @_:B -> B) -> @xs:List<a, A> -> @-ys:List<a, A> -> @-z:B -> {List.foldr(a, A, B, f, List.append(a, A, xs, ys), z) == List.foldr(a, A, B, f, xs, List.foldr(a, A, B, f, ys, z)) : B}

A right fold over an append folds the first part onto the fold of the second.

law take_append_drop provedsource · line 158 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @n:Nat -> {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List<a, A>}

Taking n elements and appending the rest after dropping n gives the list back.

law length_map provedsource · line 176 · raw

@-A:Type -> @-B:Type -> @-f:(@_:A -> B) -> @xs:List<&1, A> -> {List.length(&1, B, List.map(A, B, f, xs)) == List.length(&1, A, xs) : Nat}

Mapping preserves the length.

law map_append provedsource · line 192 · raw

@-A:Type -> @-B:Type -> @-f:(@_:A -> B) -> @xs:List<&1, A> -> @-ys:List<&1, A> -> {List.map(A, B, f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(A, B, f, xs), List.map(A, B, f, ys)) : List<&1, B>}

Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.

law map_map provedsource · line 209 · raw

@-A:Type -> @-B:Type -> @-C:Type -> @-f:(@_:A -> B) -> @-g:(@_:B -> C) -> @xs:List<&1, A> -> {List.map(B, C, g, List.map(A, B, f, xs)) == List.map(A, C, x => g(f(x)), xs) : List<&1, C>}

Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.

law append_nil_sym provedsource · line 229 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {xs == List.append(a, A, xs, []) : List<a, A>}

The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.

law nil_append_sym provedsource · line 239 · raw

@-a:Quant -> @-A:Kind(a) -> @-xs:List<a, A> -> {xs == List.append(a, A, [], xs) : List<a, A>}

The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.

law append_assoc_sym provedsource · line 249 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-ys:List<a, A> -> @-zs:List<a, A> -> {List.append(a, A, xs, List.append(a, A, ys, zs)) == List.append(a, A, List.append(a, A, xs, ys), zs) : List<a, A>}

Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.

law length_append_sym provedsource · line 261 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-ys:List<a, A> -> {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}

The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.

law reverse_go_spec_sym provedsource · line 272 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-acc:List<a, A> -> {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}

The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.

law reverse_append_sym provedsource · line 283 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @ys:List<a, A> -> {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List<a, A>}

Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.

law reverse_reverse_sym provedsource · line 294 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List<a, A>}

Reversing twice gives the list back, reversed to rewrite toward the simple side.

law length_reverse_sym provedsource · line 304 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat}

Reversing preserves the length, reversed to rewrite toward the simple side.

law foldr_append_sym provedsource · line 314 · raw

@-a:Quant -> @-A:Kind(a) -> @-B:Type -> @-f:(@_:A -> @_:B -> B) -> @xs:List<a, A> -> @-ys:List<a, A> -> @-z:B -> {List.foldr(a, A, B, f, xs, List.foldr(a, A, B, f, ys, z)) == List.foldr(a, A, B, f, List.append(a, A, xs, ys), z) : B}

A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.

law take_append_drop_sym provedsource · line 328 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @n:Nat -> {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}

Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.

law length_map_sym provedsource · line 339 · raw

@-A:Type -> @-B:Type -> @-f:(@_:A -> B) -> @xs:List<&1, A> -> {List.length(&1, A, xs) == List.length(&1, B, List.map(A, B, f, xs)) : Nat}

Mapping preserves the length, reversed to rewrite toward the simple side.

law map_append_sym provedsource · line 350 · raw

@-A:Type -> @-B:Type -> @-f:(@_:A -> B) -> @xs:List<&1, A> -> @-ys:List<&1, A> -> {List.append(&1, B, List.map(A, B, f, xs), List.map(A, B, f, ys)) == List.map(A, B, f, List.append(&1, A, xs, ys)) : List<&1, B>}

Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.

law map_map_sym provedsource · line 362 · raw

@-A:Type -> @-B:Type -> @-C:Type -> @-f:(@_:A -> B) -> @-g:(@_:B -> C) -> @xs:List<&1, A> -> {List.map(A, C, x => g(f(x)), xs) == List.map(B, C, g, List.map(A, B, f, xs)) : List<&1, C>}

Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.

Definitions

def internal_reverse_go_append source · line 62 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-ys:List<a, A> -> @-acc:List<a, A> -> {List.reverse.go(a, A, xs, List.append(a, A, ys, acc)) == List.append(a, A, List.reverse.go(a, A, xs, ys), acc) : List<a, A>}

def internal_reverse_append_go source · line 84 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-ys:List<a, A> -> @-acc:List<a, A> -> {List.reverse.go(a, A, List.append(a, A, xs, ys), acc) == List.reverse.go(a, A, ys, List.reverse.go(a, A, xs, acc)) : List<a, A>}

def internal_reverse_go_go source · line 102 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-acc:List<a, A> -> {List.reverse.go(a, A, List.reverse.go(a, A, xs, acc), []) == List.reverse.go(a, A, acc, xs) : List<a, A>}

def internal_length_reverse_go source · line 119 · raw

@-a:Quant -> @-A:Kind(a) -> @xs:List<a, A> -> @-acc:List<a, A> -> @+n:Nat -> @e:{List.length(a, A, acc) == n : Nat} -> {List.length(a, A, List.reverse.go(a, A, xs, acc)) == Nat.add(n, List.length(a, A, xs)) : Nat}