Data.List.Equalities

Definitions

snocNonEmpty : Not (xs ++ [x] = [])

  A list constructued using snoc cannot be empty.

Totality: total
Visibility: export

SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (snoc xs x)

  Proof that snoc'ed list is not empty in terms of `NonEmpty`.

Totality: total
Visibility: export

consCong2 : x = y -> xs = ys -> x :: xs = y :: ys

  Two lists are equal, if their heads are equal and their tails are equal.

Totality: total
Visibility: export

snocInjective : snoc xs x = snoc ys y -> (xs = ys, x = y)

  Equal non-empty lists should result in equal components after destructuring 'snoc'.

Totality: total
Visibility: export

appendCong2 : x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2

  Appending pairwise equal lists gives equal lists

Totality: total
Visibility: export

mapDistributesOverAppend : (f : (a -> b)) -> (xs : List a) -> (ys : List a) -> map f (xs ++ ys) = map f xs ++ map f ys

  List.map is distributive over appending.

Totality: total
Visibility: export

lengthDistributesOverAppend : (xs : List a) -> (ys : List a) -> length (xs ++ ys) = length xs + length ys

  List.length is distributive over appending.

Totality: total
Visibility: export

lengthSnoc : (x : a) -> (xs : List a) -> length (snoc xs x) = S (length xs)

  Length of a snoc'd list is the same as Succ of length list.

Totality: total
Visibility: export

appendSameLeftInjective : (xs : List a) -> (ys : List a) -> (zs : List a) -> zs ++ xs = zs ++ ys -> xs = ys

  Appending the same list at left is injective.

Totality: total
Visibility: export

appendSameRightInjective : (xs : List a) -> (ys : List a) -> (zs : List a) -> xs ++ zs = ys ++ zs -> xs = ys

  Appending the same list at right is injective.

Totality: total
Visibility: export

appendNonEmptyLeftNotEq : (zs : List a) -> (xs : List a) -> NonEmpty xs => Not (zs = xs ++ zs)

  List cannot be equal to itself prepended with some non-empty list.

Totality: total
Visibility: export

appendNonEmptyRightNotEq : (zs : List a) -> (xs : List a) -> NonEmpty xs => Not (zs = zs ++ xs)

  List cannot be equal to itself appended with some non-empty list.

Totality: total
Visibility: export

bindConcatPrf : (xs : List a) -> (x : a) -> (f : (a -> List b)) -> (x :: xs) >>= f = f x ++ (xs >>= f)

  Proof of correspondence between list bind and concatenation.

Totality: total
Visibility: export