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:17229} : DecEq a} -> UniqueVect 0 a

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

data NotElem : {auto {conArg:17264} : 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:17277} : 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:18942} : DecEq a} -> IsNo (decEq x y) -> NotElem y [x]

data Elem : {auto {conArg:17342} : 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:17355} : DecEq a} -> {auto prf : NotElem x xs} -> Elem x (x :: xs)

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

Hint: 

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

data All : {auto {conArg:17427} : 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:17446} : DecEq a} -> All p []

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

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

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

Visibility: public export

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

Visibility: public export

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

Visibility: public export

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

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

Visibility: public export

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

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

Visibility: public export

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

Visibility: public export

drop : {auto {conArg:18257} : 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

Visibility: public export

Test1 : UniqueVect 5 String

Visibility: public export

wher : Elem "c" Test1

Visibility: public export

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

  Remove element from a unique vector at a given index

Visibility: public export

removingElemIsStillNotElem : {auto {conArg:18682} : 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

Visibility: public export

notEqualNotElem : {auto {conArg:18872} : 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

Visibility: public export

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

Visibility: public export

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

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

Visibility: public export

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

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

Visibility: public export

numSymmetricDifference : {auto {conArg:19245} : 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

Visibility: public export

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

  Union

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

expandUnique : {auto {conArg:19438} : 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:19583} : DecEq a} -> (xs : UniqueVect n a) -> (ys : UniqueVect m a) -> UniqueVect (numOverlap xs ys) a

Visibility: public export

notElemIntersect : {auto {conArg:19602} : 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:19742} : 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`

Visibility: public export

allElemIntersectSnd : {auto {conArg:19780} : 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`

Visibility: public export

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

Visibility: public export

l1 : UniqueVect 3 String

Visibility: public export

l2 : UniqueVect 3 String

Visibility: public export

l3 : UniqueVect 5 String

Visibility: public export

l4 : UniqueVect 1 String

Visibility: public export