Data.Unique.Vect

Definitions

data UniqueVect : (0 _ : Nat) -> (0 a : Type) -> DecEq a => Type

  A vector that cannot contain duplicates
  An element can be inserted only if it is not already in the vector
  Mathematically can be thought of as an ordered set
  @ a The type of the elements in the list

Totality: total
Visibility: public export
Constructors:

Nil : {auto {conArg:12585} : DecEq a} -> UniqueVect 0 a

(::) : {auto {conArg:12598} : DecEq a} -> (x : a) -> (xs : UniqueVect n a) -> NotElem x xs => UniqueVect (S n) a

data NotElem : {auto {conArg:12620} : DecEq a} -> a -> UniqueVect n a -> Type

  A proof that an element `x` is not found in `xs`

Totality: total
Visibility: public export
Constructors:

NotInEmptyVect : {auto {conArg:12633} : DecEq a} -> (x : a) -> NotElem x []

NotInNonEmptyVect : {auto de : DecEq a} -> (xs : UniqueVect n a) -> NotElem x xs -> IsNo (decEq x y) => {auto prf : NotElem y xs} -> NotElem x (y :: xs)

Hint: 

{auto {conArg:14298} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]

data Elem : {auto {conArg:12698} : DecEq a} -> a -> UniqueVect n a -> Type

  A proof that an element `x` is found in `xs`

Totality: total
Visibility: public export
Constructors:

Here : {auto {conArg:12711} : DecEq a} -> {auto prf : NotElem x xs} -> Elem x (x :: xs)

There : {auto {conArg:12743} : DecEq a} -> {auto prf : NotElem y xs} -> Elem x xs -> Elem x (y :: xs)

Hint: 

{auto {conArg:12879} : DecEq a} -> Uninhabited (Elem x [])

data All : {auto {conArg:12783} : DecEq a} -> (0 _ : (a -> Type)) -> UniqueVect rank a -> Type

  A proof that elements of a unique vector satisfy a property

Totality: total
Visibility: public export
Constructors:

Nil : {auto {conArg:12802} : DecEq a} -> All p []

(::) : {auto {conArg:12823} : DecEq a} -> {auto {conArg:12838} : NotElem x xs} -> p x -> All p xs -> All p (x :: xs)

decElemInUniqueVect : {auto {conArg:12926} : DecEq a} -> (x : a) -> (xs : UniqueVect n a) -> Dec (Elem x xs)

  A decision procedure for determining whether an element `x` is in `xs`

Totality: total
Visibility: public export

notElem : {auto {conArg:13185} : DecEq a} -> Not (Elem x xs) -> NotElem x xs

Totality: total
Visibility: public export

toVect : {auto {conArg:13325} : DecEq a} -> UniqueVect n a -> Vect n a

Totality: total
Visibility: public export

fromVect : {auto {conArg:13365} : DecEq a} -> Vect n a -> (m : Nat ** UniqueVect m a)

  Converts a vector to a unique vector, removing duplicates if they exist

Totality: total
Visibility: public export

indexOf : {auto {conArg:13502} : DecEq a} -> Elem x xs -> Fin n

  Turn the proof that an element `x` is in a vector into the index of `x`

Totality: total
Visibility: public export

length : {auto {conArg:13571} : DecEq a} -> UniqueVect n a -> Nat

Totality: total
Visibility: public export

drop : {auto {conArg:13613} : DecEq a} -> (xs : UniqueVect n a) -> (elem : Elem x xs) -> UniqueVect (minus n (finToNat (FS (indexOf elem)))) a

  Drop all the elements up and until the element `x` from a unique vector

Totality: total
Visibility: public export

Test1 : UniqueVect 5 String

Totality: total
Visibility: public export

wher : Elem "c" Test1

Totality: total
Visibility: public export

removeIndex : {auto {conArg:14021} : DecEq a} -> UniqueVect (S n) a -> Fin (S n) -> UniqueVect n a

  Remove element from a unique vector at a given index

Totality: total
Visibility: public export

removingElemIsStillNotElem : {auto {conArg:14038} : DecEq a} -> NotElem x xs => NotElem x (removeIndex xs i)

  Given a vector `xs` and a proof that `x` is not in `xs`, then even if
  we remove any elemens from `xs`, `x` will still not be in the result

Totality: total
Visibility: public export

notEqualNotElem : {auto {conArg:14228} : DecEq a} -> IsNo (decEq x y) -> NotElem x [y]

  If `x` is not equal to `y`, then `x` is not in the list `[y]`
  It seems that Idris manages to discover this proof automatically, so 
  this is not needed in practice
  Its dual is needed, hence the %hint in for the declaration below

Totality: total
Visibility: public export

notEqualNotElem2 : {auto {conArg:14298} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]

Totality: total
Visibility: public export

numUnique : {auto {conArg:14359} : DecEq a} -> UniqueVect n a -> UniqueVect m a -> Nat

  Number of elements found in any of two unique vectors
  Effectively, union

Totality: total
Visibility: public export

numOverlap : {auto {conArg:14480} : DecEq a} -> UniqueVect n a -> UniqueVect m a -> Nat

  Number of elements found in both of the two unique vectors
  Effectively, intersection

Totality: total
Visibility: public export

numSymmetricDifference : {auto {conArg:14601} : DecEq a} -> UniqueVect n a -> UniqueVect m a -> Nat

  Number of elements that are found in one but not both of the two vectors
  Effectively, symmetric difference

Totality: total
Visibility: public export

(+++) : {auto {conArg:14775} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numUnique xs ys) a

  Union

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5

expandUnique : {auto {conArg:14794} : DecEq a} -> NotElem x xs => NotElem x ys => NotElem x (xs +++ ys)

  If `x` is not in `xs` nor `ys`, then it also won't be in `xs +++ ys`

intersect : {auto {conArg:14939} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numOverlap xs ys) a

Totality: total
Visibility: public export

notElemIntersect : {auto {conArg:14958} : DecEq a} -> NotElem x xs => Elem x ys => NotElem x (intersect xs ys)

  If `x` is not in `xs`, then we can intersect `xs` with any other list,
  and `x` still wont' be in the result (even if `x` was in the other list)

allElemIntersectFst : {auto {conArg:15098} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> All (\x => Elem x xs) (intersect xs ys)

  All elements of the intersection of two vectors `xs` and `ys`
  will be elements of `xs`

Totality: total
Visibility: public export

allElemIntersectSnd : {auto {conArg:15136} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> All (\x => Elem x ys) (intersect xs ys)

  All elements of the intersection of two vectors `xs` and `ys`
  will be elements of `ys`

Totality: total
Visibility: public export

symmetricDifference : {auto {conArg:15174} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numSymmetricDifference xs ys) a

Totality: total
Visibility: public export

l1 : UniqueVect 3 String

Totality: total
Visibility: public export

l2 : UniqueVect 3 String

Totality: total
Visibility: public export

l3 : UniqueVect 5 String

Totality: total
Visibility: public export

l4 : UniqueVect 1 String

Totality: total
Visibility: public export