0 | module Data.Unique.Vect

  2 | import Data.Vect

  3 | import Decidable.Equality

  4 | import Decidable.Equality.Core

  5 | import Misc

  7 | %hide Misc.NotElem

 11 | namespace UniqueVect

 12 |   mutual

 13 |     ||| A list with unique elements, length tracked statically

 17 |     public export

 18 |     data UniqueVect : (0 n : Nat) -> (0 a : Type) -> DecEq a => Type where

 19 |       Nil : {0 a : Type} -> DecEq a => UniqueVect 0 a

 20 |       (::) : {0 a : Type} -> DecEq a =>

 21 |         (x : a) ->

 22 |         (xs : UniqueVect n a) ->

 23 |         {auto prf : NotElem x xs} ->

 24 |         UniqueVect (S n) a

 25 |   

 26 |     ||| A proof that an element is *not* found in the unique vector

 27 |     public export

 28 |     data NotElem : DecEq a =>

 29 |       (x : a) -> (xs : UniqueVect n a) -> Type where

 30 |       NotInEmptyVect : {0 a : Type} -> DecEq a => (x : a)

 31 |         -> NotElem {a=a} x []

 32 |       NotInNonEmptyVect : {0 a : Type} -> (de : DecEq a) =>

 33 |         {x, y : a} ->

 34 |         (xs : UniqueVect n a) ->

 35 |         (ne : NotElem x xs) ->

 36 |         (neq : IsNo (decEq x y)) =>

 37 |         (prf : NotElem y xs) =>

 38 |         NotElem x (y :: xs)

 40 |   namespace All

 41 |     ||| A proof that elements of a unique vector satisfy a property

 42 |     public export

 43 |     data All : DecEq a => (0 p : a -> Type) -> UniqueVect rank a -> Type where

 44 |       Nil : DecEq a => {0 p : a -> Type} -> All p []

 45 |       (::) : DecEq a => {0 p : a -> Type} ->

 46 |         {0 x : a} ->

 47 |         {0 xs : UniqueVect k a} ->

 48 |         NotElem x xs =>

 49 |         p x ->

 50 |         All p xs ->

 51 |         All p (x :: xs)

 53 |         

 54 |   ||| A proof that an element is found in a vector with unique elements

 55 |   public export

 56 |   data Elem : DecEq a => (x : a) -> (xs : UniqueVect n a) -> Type where

 57 |     Here : DecEq a =>

 58 |       {x : a} ->

 59 |       {xs : UniqueVect k a} ->

 60 |       (prf : NotElem x xs) =>

 61 |       Elem x (x :: xs)

 62 |     There : DecEq a =>

 63 |       {x : a} ->

 64 |       {xs : UniqueVect k a} ->

 65 |       (prf : NotElem y xs) =>

 66 |       (later : Elem x xs) ->

 67 |       Elem x (y :: xs)

 69 |   ||| An element cannot be in an empty vector

 70 |   public export

 71 |   {x : a} -> DecEq a => Uninhabited (Elem x []) where

 72 |     uninhabited Here impossible

 73 |     uninhabited (There later) impossible

 75 |   ||| Decision procedure for unique vector's Elem

 76 |   public export

 77 |   decElemInUniqueVect : DecEq a =>

 78 |     (x : a) -> (xs : UniqueVect n a) -> Dec (Elem x xs)

 79 |   decElemInUniqueVect x [] = No absurd

 80 |   decElemInUniqueVect x (y :: ys) = case decEq x y of

 81 |     Yes Refl => Yes Here

 82 |     No neq => case decElemInUniqueVect x ys of

 83 |       Yes prf => Yes $ There prf

 84 |       No nprf => No $ \case

 85 |         Here => neq Refl

 86 |         (There later) => nprf later

 88 |   public export

 89 |   notElem : DecEq a =>

 90 |     {x : a} ->

 91 |     {xs : UniqueVect n a} ->

 92 |     Not (Elem x xs) -> NotElem x xs

 93 |   notElem {xs = []} f = NotInEmptyVect x

 94 |   notElem {xs = (y :: ys)} f with (decEq x y)

 95 |     _ | (Yes Refl) = absurd (f Here)

 96 |     _ | (No neq) = NotInNonEmptyVect

 97 |       {neq=(proofIneqIsNo neq)} ys (notElem (\e => f ?bb))

 99 |   public export

100 |   toVect : DecEq a => UniqueVect n a -> Vect n a

101 |   toVect [] = []

102 |   toVect (x :: xs) = x :: toVect xs

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

105 |   public export

106 |   fromVect : DecEq a => Vect n a -> (m : Nat ** UniqueVect m a)

107 |   fromVect [] = (0 ** [])

108 |   fromVect (x :: xs) =

109 |     let (k ** t) = fromVect xs

110 |     in case decElemInUniqueVect x t of

111 |       Yes prf => (k ** t)

112 |       No nprf => (S k ** (::) x t {prf=notElem nprf})

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

116 |   public export

117 |   indexOf : DecEq a => {0 n : Nat} -> {0 xs : UniqueVect n a} ->

118 |     Elem x xs -> Fin n

119 |   indexOf Here = FZ

120 |   indexOf (There later) = FS (indexOf later)

122 |   public export

123 |   length : DecEq a => UniqueVect n a -> Nat

124 |   length [] = 0

125 |   length (x :: xs) = 1 + length xs

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

128 |   public export

129 |   drop : DecEq a =>

130 |     (xs : UniqueVect n a) ->

131 |     (elem : Elem x xs) ->

132 |     UniqueVect (n `minus` (finToNat (FS (indexOf elem)))) a

133 |   drop {n=S k} (_ :: xs) Here = rewrite minusZeroRight k in xs

134 |   drop (_ :: xs) (There later) = drop xs later

137 |   public export

138 |   Test1 : UniqueVect 5 String

139 |   Test1 = ["a", "b", "c", "d", "e"]

141 |   public export

142 |   wher : Elem "c" Test1

143 |   wher = There $ There $ Here

145 |   mutual

146 |     ||| Remove element from a unique vector at a given index

147 |     public export

148 |     removeIndex : DecEq a =>

149 |       {n : Nat} ->

150 |       (xs : UniqueVect (S n) a) ->

151 |       Fin (S n) ->

152 |       UniqueVect n a

153 |     removeIndex (x :: xs) FZ = xs

154 |     removeIndex {n = (S k)} (x :: xs) (FS i)

155 |       = (::) x (removeIndex xs i) {prf=removingElemIsStillNotElem}

157 |     ||| Given a vector `xs` and a proof that `x` is not in `xs`, then even if

159 |     public export

160 |     removingElemIsStillNotElem : DecEq a =>

161 |       {n : Nat} ->

162 |       {x : a} ->

163 |       {xs : UniqueVect (S n) a} ->

164 |       {i : Fin (S n)} ->

165 |       (ne : NotElem x xs) =>

166 |       NotElem x (removeIndex xs i)

167 |     removingElemIsStillNotElem {xs = (_ :: _)} {ne = (NotInNonEmptyVect _ ne)} {i = FZ}

168 |       = ne

169 |     removingElemIsStillNotElem {n = (S k)} {xs = (y :: ys)} {ne = (NotInNonEmptyVect ys ne)} {i = (FS j)}

170 |       = NotInNonEmptyVect (removeIndex ys j) removingElemIsStillNotElem {prf=removingElemIsStillNotElem} 

174 |   ||| If `x` is not equal to `y`, then `x` is not in the list `[y]`

178 |   public export

179 |   notEqualNotElem : DecEq a =>

180 |     {x, y : a} ->

181 |     (neq : IsNo (decEq x y)) ->

182 |     NotElem x [y]

183 |   notEqualNotElem _ = NotInNonEmptyVect [] (NotInEmptyVect x)

185 |   %hint

186 |   public export

187 |   notEqualNotElem2 : DecEq a =>

188 |     {x, y : a} ->

189 |     (neq : IsNo (decEq x y)) ->

190 |     NotElem y [x]

191 |   notEqualNotElem2 neq = notEqualNotElem {x=y} {y=x} (isNoSym neq)

193 |   ||| Number of elements found in any of two unique vectors

195 |   public export

196 |   numUnique : {n, m : Nat} -> DecEq a => UniqueVect n a -> UniqueVect m a -> Nat

197 |   numUnique [] _ = m

198 |   numUnique (x :: xs) ys = case decElemInUniqueVect x ys of

199 |     Yes _ => numUnique xs ys -- found in ys, so don't count it again

200 |     No _ => 1 + numUnique xs ys -- not found in ys, so count it

202 |   ||| Number of elements found in both of the two unique vectors

204 |   public export

205 |   numOverlap : {n, m : Nat} -> DecEq a =>

206 |     UniqueVect n a -> UniqueVect m a -> Nat

207 |   numOverlap [] ys = 0

208 |   numOverlap (x :: xs) ys = case decElemInUniqueVect x ys of

209 |     Yes _ => 1 + numOverlap xs ys -- found also in ys, so count it

210 |     No _ => numOverlap xs ys

212 |   ||| Number of elements that are found in one but not both of the two vectors

214 |   public export

215 |   numSymmetricDifference : {n, m : Nat} -> DecEq a =>

216 |     UniqueVect n a -> UniqueVect m a -> Nat

217 |   numSymmetricDifference [] ys = m

218 |   numSymmetricDifference (x :: xs) ys = case decElemInUniqueVect x ys of

219 |     -- need to pattern match on Elem to propagate length information

220 |     Yes Here => numSymmetricDifference xs (removeIndex ys FZ)

221 |     Yes (There later) => numSymmetricDifference xs (removeIndex ys (FS (indexOf later)))

222 |     No _ => 1 + numSymmetricDifference xs ys

224 |   

225 |   

226 |   mutual

227 |     public export infixr 5 +++

229 |     ||| Union

230 |     public export

231 |     (+++) : DecEq a =>

232 |       (xs : UniqueVect n a) ->

233 |       (ys : UniqueVect m a) ->

234 |       UniqueVect (numUnique xs ys) a

235 |     [] +++ ys = ys

236 |     (x :: xs) +++ ys with (decElemInUniqueVect x ys)

237 |       _ | (Yes prf) = xs +++ ys -- x :: (xs +++ ys)

238 |       _ | (No nprf) = (::) x (xs +++ ys) {prf=expandUnique {prfy=notElem nprf}}

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

241 |     public export

242 |     expandUnique : DecEq a =>

243 |       {x : a} ->

244 |       {xs : UniqueVect n a} ->

245 |       {ys : UniqueVect m a} ->

246 |       (prfx : NotElem x xs) =>

247 |       (prfy : NotElem x ys) =>

248 |       NotElem x (xs +++ ys)

249 |     -- todo implement this

251 |   mutual

252 |     public export

253 |     intersect : DecEq a =>

254 |       (xs : UniqueVect n a) ->

255 |       (ys : UniqueVect m a) ->

256 |       UniqueVect (numOverlap xs ys) a

257 |     intersect [] ys = []

258 |     intersect (x :: xs) ys with (decElemInUniqueVect x ys)

259 |       _ | (Yes prf) = (::) x (intersect xs ys) {prf=notElemIntersect}

260 |       _ | (No nprf) = intersect xs ys

262 |     ||| If `x` is not in `xs`, then we can intersect `xs` with any other list,

264 |     public export

265 |     notElemIntersect : DecEq a =>

266 |       {x : a} ->

267 |       {xs : UniqueVect n a} ->

268 |       {ys : UniqueVect m a} ->

269 |       (prfx : NotElem x xs) =>

270 |       (prfy : Elem x ys) =>

271 |       NotElem x (intersect xs ys)

274 |   ||| All elements of the intersection of two vectors `xs` and `ys`

276 |   public export

277 |   allElemIntersectFst : DecEq a => 

278 |     (xs : UniqueVect n a) ->

279 |     (ys : UniqueVect m a) ->

280 |     All (\x => Elem x xs) (intersect xs ys)

281 |   allElemIntersectFst = ?allElemIntersect_rhs

283 |   ||| All elements of the intersection of two vectors `xs` and `ys`

285 |   public export

286 |   allElemIntersectSnd : DecEq a => 

287 |     (xs : UniqueVect n a) ->

288 |     (ys : UniqueVect m a) ->

289 |     All (\x => Elem x ys) (intersect xs ys)

290 |   allElemIntersectSnd = ?allElemIntersect_rhs2

292 |   mutual

293 |     public export

294 |     symmetricDifference : DecEq a => {n, m : Nat} ->

295 |       (xs : UniqueVect n a) ->

296 |       (ys : UniqueVect m a) ->

297 |       UniqueVect (numSymmetricDifference xs ys) a

298 |     symmetricDifference [] ys = ys

299 |     symmetricDifference (x :: xs) ys = ?aaa

300 |     

301 |     -- with (decElemInUniqueVect x ys)

302 |       -- _ | Yes p = ?aaa

303 |       -- _ | No neq = ?bbb

308 |   public export

309 |   l1 : UniqueVect 3 String

310 |   l1 = ["a", "b", "c"]

312 |   public export

313 |   l2 : UniqueVect 3 String

314 |   l2 = ["c", "d", "e"]

316 |   public export

317 |   l3 : UniqueVect 5 String

318 |   l3 = l1 +++ l2

320 |   public export

321 |   l4 : UniqueVect 1 String

322 |   l4 = intersect l1 l2

324 |     -- expandUnique {xs = []} {ys = (_ :: _)} prf = prf

325 |     -- expandUnique {xs = (x :: xs)} {ys = (y :: ys)} prf = case decElemInUniqueVect x ys of

326 |     --   Yes prf' => expandUnique {prf=prf'} xs ys

328 |   -- fromVect : DecEq a => Vect n a -> UniqueVect n a

329 |   -- fromVect [] = []

330 |   -- fromVect (x :: xs) = case fromVect xs of

331 |   --   Yes _ => x :: fromVect xs

332 |   --   No _ => fromVect xs