0 | module Data.Unique.Vect
  1 |
  2 | import Data.Vect
  3 | import Decidable.Equality
  4 | import Misc
  5 |
  6 | %hide Misc.NotElem.NotElem
  7 |
  8 | -- `UniqueVect` and `NotElem` are defined in terms of each other
  9 | mutual
 10 |   ||| A vector that cannot contain duplicates
 11 |   ||| An element can be inserted only if it is not already in the vector
 12 |   ||| Mathematically can be thought of as an ordered set
 13 |   ||| @ a The type of the elements in the list
 14 |   public export
 15 |   data UniqueVect : (0 n : Nat) -> (0 a : Type) -> DecEq a => Type where
 16 |     Nil : {0 a : Type} -> DecEq a => UniqueVect 0 a
 17 |     (::) : {0 a : Type} -> DecEq a =>
 18 |       (x : a) ->
 19 |       (xs : UniqueVect n a) ->
 20 |       {auto prf : NotElem x xs} ->
 21 |       UniqueVect (S n) a
 22 |   
 23 |   ||| A proof that an element `x` is not found in `xs`
 24 |   public export
 25 |   data NotElem : DecEq a => (x : a) -> (xs : UniqueVect n a) -> Type where
 26 |     NotInEmptyVect : DecEq a => (x : a) -> NotElem {a=a} x []
 27 |     NotInNonEmptyVect : (de : DecEq a) =>
 28 |       {x, y : a} ->
 29 |       (xs : UniqueVect n a) ->
 30 |       (ne : NotElem x xs) ->
 31 |       (neq : IsNo (decEq x y)) =>
 32 |       (prf : NotElem y xs) =>
 33 |       NotElem x (y :: xs)
 34 |
 35 | ||| A proof that an element `x` is found in `xs`
 36 | public export
 37 | data Elem : DecEq a => (x : a) -> (xs : UniqueVect n a) -> Type where
 38 |   Here : DecEq a =>
 39 |     {x : a} ->
 40 |     {xs : UniqueVect k a} ->
 41 |     (prf : NotElem x xs) =>
 42 |     Elem x (x :: xs)
 43 |   There : DecEq a =>
 44 |     {x : a} ->
 45 |     {xs : UniqueVect k a} ->
 46 |     (prf : NotElem y xs) =>
 47 |     (later : Elem x xs) ->
 48 |     Elem x (y :: xs)
 49 |
 50 | namespace All
 51 |   ||| A proof that elements of a unique vector satisfy a property
 52 |   public export
 53 |   data All : DecEq a => (0 p : a -> Type) -> UniqueVect rank a -> Type where
 54 |     Nil : DecEq a => {0 p : a -> Type} -> All p []
 55 |     (::) : DecEq a => {0 p : a -> Type} ->
 56 |       {0 x : a} ->
 57 |       {0 xs : UniqueVect k a} ->
 58 |       NotElem x xs =>
 59 |       p x ->
 60 |       All p xs ->
 61 |       All p (x :: xs)
 62 |
 63 |       
 64 | ||| An element cannot be in an empty vector
 65 | public export
 66 | {x : a} -> DecEq a => Uninhabited (Elem x []) where
 67 |   uninhabited Here impossible
 68 |   uninhabited (There later) impossible
 69 |
 70 | ||| A decision procedure for determining whether an element `x` is in `xs`
 71 | public export
 72 | decElemInUniqueVect : DecEq a =>
 73 |   (x : a) -> (xs : UniqueVect n a) -> Dec (Elem x xs)
 74 | decElemInUniqueVect x [] = No absurd
 75 | decElemInUniqueVect x (y :: ys) = case decEq x y of
 76 |   Yes Refl => Yes Here
 77 |   No neq => case decElemInUniqueVect x ys of
 78 |     Yes prf => Yes $ There prf
 79 |     No nprf => No $ \case
 80 |       Here => neq Refl
 81 |       (There later) => nprf later
 82 |
 83 | public export
 84 | notElem : DecEq a =>
 85 |   {x : a} ->
 86 |   {xs : UniqueVect n a} ->
 87 |   Not (Elem x xs) -> NotElem x xs
 88 | notElem {xs = []} f = NotInEmptyVect x
 89 | notElem {xs = (y :: ys)} f with (decEq x y)
 90 |   _ | (Yes Refl) = absurd (f Here)
 91 |   _ | (No neq) = NotInNonEmptyVect
 92 |     {neq=(proofIneqIsNo neq)} ys (notElem (\e => f ?notElem_there))
 93 |
 94 | public export
 95 | toVect : DecEq a => UniqueVect n a -> Vect n a
 96 | toVect [] = []
 97 | toVect (x :: xs) = x :: toVect xs
 98 |
 99 | ||| Converts a vector to a unique vector, removing duplicates if they exist
100 | public export
101 | fromVect : DecEq a => Vect n a -> (m : Nat ** UniqueVect m a)
102 | fromVect [] = (0 ** [])
103 | fromVect (x :: xs) =
104 |   let (k ** t) = fromVect xs
105 |   in case decElemInUniqueVect x t of
106 |     Yes prf => (k ** t)
107 |     No nprf => (S k ** (::) x t {prf=notElem nprf})
108 |
109 | ||| Turn the proof that an element `x` is in a vector into the index of `x`
110 | public export
111 | indexOf : DecEq a => {0 n : Nat} -> {0 xs : UniqueVect n a} ->
112 |   Elem x xs -> Fin n
113 | indexOf Here = FZ
114 | indexOf (There later) = FS (indexOf later)
115 |
116 | public export
117 | length : DecEq a => UniqueVect n a -> Nat
118 | length [] = 0
119 | length (x :: xs) = 1 + length xs
120 |
121 | ||| Drop all the elements up and until the element `x` from a unique vector
122 | public export
123 | drop : DecEq a =>
124 |   (xs : UniqueVect n a) ->
125 |   (elem : Elem x xs) ->
126 |   UniqueVect (n `minus` (finToNat (FS (indexOf elem)))) a
127 | drop {n=S k} (_ :: xs) Here = rewrite minusZeroRight k in xs
128 | drop (_ :: xs) (There later) = drop xs later
129 |
130 |
131 | public export
132 | Test1 : UniqueVect 5 String
133 | Test1 = ["a", "b", "c", "d", "e"]
134 |
135 | public export
136 | wher : Elem "c" Test1
137 | wher = There $ There $ Here
138 |
139 | mutual
140 |   ||| Remove element from a unique vector at a given index
141 |   public export
142 |   removeIndex : DecEq a =>
143 |     {n : Nat} ->
144 |     (xs : UniqueVect (S n) a) ->
145 |     Fin (S n) ->
146 |     UniqueVect n a
147 |   removeIndex (x :: xs) FZ = xs
148 |   removeIndex {n = (S k)} (x :: xs) (FS i)
149 |     = (::) x (removeIndex xs i) {prf=removingElemIsStillNotElem}
150 |
151 |   ||| Given a vector `xs` and a proof that `x` is not in `xs`, then even if
152 |   ||| we remove any elemens from `xs`, `x` will still not be in the result
153 |   public export
154 |   removingElemIsStillNotElem : DecEq a =>
155 |     {n : Nat} ->
156 |     {x : a} ->
157 |     {xs : UniqueVect (S n) a} ->
158 |     {i : Fin (S n)} ->
159 |     (ne : NotElem x xs) =>
160 |     NotElem x (removeIndex xs i)
161 |   removingElemIsStillNotElem {xs = (_ :: _)} {ne = (NotInNonEmptyVect _ ne)} {i = FZ}
162 |     = ne
163 |   removingElemIsStillNotElem {n = (S k)} {xs = (y :: ys)} {ne = (NotInNonEmptyVect ys ne)} {i = (FS j)}
164 |     = NotInNonEmptyVect (removeIndex ys j) removingElemIsStillNotElem {prf=removingElemIsStillNotElem} 
165 |
166 | ||| If `x` is not equal to `y`, then `x` is not in the list `[y]`
167 | ||| It seems that Idris manages to discover this proof automatically, so 
168 | ||| this is not needed in practice
169 | ||| Its dual is needed, hence the %hint in for the declaration below
170 | public export
171 | notEqualNotElem : DecEq a =>
172 |   {x, y : a} ->
173 |   (neq : IsNo (decEq x y)) ->
174 |   NotElem x [y]
175 | notEqualNotElem _ = NotInNonEmptyVect [] (NotInEmptyVect x)
176 |
177 | %hint
178 | public export
179 | notEqualNotElem2 : DecEq a =>
180 |   {x, y : a} ->
181 |   (neq : IsNo (decEq x y)) ->
182 |   NotElem y [x]
183 | notEqualNotElem2 neq = notEqualNotElem {x=y} {y=x} (isNoSym neq)
184 |
185 | ||| Number of elements found in any of two unique vectors
186 | ||| Effectively, union
187 | public export
188 | numUnique : {n, m : Nat} -> DecEq a => UniqueVect n a -> UniqueVect m a -> Nat
189 | numUnique [] _ = m
190 | numUnique (x :: xs) ys = case decElemInUniqueVect x ys of
191 |   Yes _ => numUnique xs ys -- found in ys, so don't count it again
192 |   No _ => 1 + numUnique xs ys -- not found in ys, so count it
193 |
194 | ||| Number of elements found in both of the two unique vectors
195 | ||| Effectively, intersection
196 | public export
197 | numOverlap : {n, m : Nat} -> DecEq a =>
198 |   UniqueVect n a -> UniqueVect m a -> Nat
199 | numOverlap [] ys = 0
200 | numOverlap (x :: xs) ys = case decElemInUniqueVect x ys of
201 |   Yes _ => 1 + numOverlap xs ys -- found also in ys, so count it
202 |   No _ => numOverlap xs ys
203 |
204 | ||| Number of elements that are found in one but not both of the two vectors
205 | ||| Effectively, symmetric difference
206 | public export
207 | numSymmetricDifference : {n, m : Nat} -> DecEq a =>
208 |   UniqueVect n a -> UniqueVect m a -> Nat
209 | numSymmetricDifference [] ys = m
210 | numSymmetricDifference (x :: xs) ys = case decElemInUniqueVect x ys of
211 |   -- need to pattern match on Elem to propagate length information
212 |   Yes Here => numSymmetricDifference xs (removeIndex ys FZ)
213 |   Yes (There later) => numSymmetricDifference xs (removeIndex ys (FS (indexOf later)))
214 |   No _ => 1 + numSymmetricDifference xs ys
215 |
216 | mutual
217 |   public export infixr 5 +++
218 |
219 |   ||| Union
220 |   public export
221 |   (+++) : DecEq a =>
222 |     (xs : UniqueVect n a) ->
223 |     (ys : UniqueVect m a) ->
224 |     UniqueVect (numUnique xs ys) a
225 |   [] +++ ys = ys
226 |   (x :: xs) +++ ys with (decElemInUniqueVect x ys)
227 |     _ | (Yes prf) = xs +++ ys -- x :: (xs +++ ys)
228 |     _ | (No nprf) = (::) x (xs +++ ys) {prf=expandUnique {prfy=notElem nprf}}
229 |
230 |   ||| If `x` is not in `xs` nor `ys`, then it also won't be in `xs +++ ys`
231 |   public export
232 |   expandUnique : DecEq a =>
233 |     {x : a} ->
234 |     {xs : UniqueVect n a} ->
235 |     {ys : UniqueVect m a} ->
236 |     (prfx : NotElem x xs) =>
237 |     (prfy : NotElem x ys) =>
238 |     NotElem x (xs +++ ys)
239 |   -- todo implement this
240 |
241 | mutual
242 |   public export
243 |   intersect : DecEq a =>
244 |     (xs : UniqueVect n a) ->
245 |     (ys : UniqueVect m a) ->
246 |     UniqueVect (numOverlap xs ys) a
247 |   intersect [] ys = []
248 |   intersect (x :: xs) ys with (decElemInUniqueVect x ys)
249 |     _ | (Yes prf) = (::) x (intersect xs ys) {prf=notElemIntersect}
250 |     _ | (No nprf) = intersect xs ys
251 |
252 |   ||| If `x` is not in `xs`, then we can intersect `xs` with any other list,
253 |   ||| and `x` still wont' be in the result (even if `x` was in the other list)
254 |   public export
255 |   notElemIntersect : DecEq a =>
256 |     {x : a} ->
257 |     {xs : UniqueVect n a} ->
258 |     {ys : UniqueVect m a} ->
259 |     (prfx : NotElem x xs) =>
260 |     (prfy : Elem x ys) =>
261 |     NotElem x (intersect xs ys)
262 |
263 |
264 | ||| All elements of the intersection of two vectors `xs` and `ys`
265 | ||| will be elements of `xs`
266 | public export
267 | allElemIntersectFst : DecEq a => 
268 |   (xs : UniqueVect n a) ->
269 |   (ys : UniqueVect m a) ->
270 |   All (\x => Elem x xs) (intersect xs ys)
271 | allElemIntersectFst = ?allElemIntersect_rhs
272 |
273 | ||| All elements of the intersection of two vectors `xs` and `ys`
274 | ||| will be elements of `ys`
275 | public export
276 | allElemIntersectSnd : DecEq a => 
277 |   (xs : UniqueVect n a) ->
278 |   (ys : UniqueVect m a) ->
279 |   All (\x => Elem x ys) (intersect xs ys)
280 | allElemIntersectSnd = ?allElemIntersect_rhs2
281 |
282 | mutual
283 |   public export
284 |   symmetricDifference : DecEq a => {n, m : Nat} ->
285 |     (xs : UniqueVect n a) ->
286 |     (ys : UniqueVect m a) ->
287 |     UniqueVect (numSymmetricDifference xs ys) a
288 |   symmetricDifference [] ys = ys
289 |   symmetricDifference (x :: xs) ys = ?symmetricDifference_rhs
290 |   
291 |   -- with (decElemInUniqueVect x ys)
292 |     -- _ | Yes p = ?aaa
293 |     -- _ | No neq = ?bbb
294 |
295 |
296 |
297 |
298 |   public export
299 |   l1 : UniqueVect 3 String
300 |   l1 = ["a", "b", "c"]
301 |
302 |   public export
303 |   l2 : UniqueVect 3 String
304 |   l2 = ["c", "d", "e"]
305 |
306 |   public export
307 |   l3 : UniqueVect 5 String
308 |   l3 = l1 +++ l2
309 |
310 |   public export
311 |   l4 : UniqueVect 1 String
312 |   l4 = intersect l1 l2
313 |
314 |     -- expandUnique {xs = []} {ys = (_ :: _)} prf = prf
315 |     -- expandUnique {xs = (x :: xs)} {ys = (y :: ys)} prf = case decElemInUniqueVect x ys of
316 |     --   Yes prf' => expandUnique {prf=prf'} xs ys
317 |
318 |   -- fromVect : DecEq a => Vect n a -> UniqueVect n a
319 |   -- fromVect [] = []
320 |   -- fromVect (x :: xs) = case fromVect xs of
321 |   --   Yes _ => x :: fromVect xs
322 |   --   No _ => fromVect xs