0 | module Data.List.Quantifiers

  2 | import Data.DPair

  3 | import Data.Fin

  4 | import Data.List

  5 | import Data.List.Elem

  7 | %default total

 12 | namespace Any

 14 |   ||| A proof that some element of a list satisfies some property

 17 |   public export

 18 |   data Any : (0 p : a -> Type) -> List a -> Type where

 19 |     ||| A proof that the satisfying element is the first one in the `List`

 20 |     Here  : {0 xs : List a} -> p x -> Any p (x :: xs)

 21 |     ||| A proof that the satisfying element is in the tail of the `List`

 22 |     There : {0 xs : List a} -> Any p xs -> Any p (x :: xs)

 24 | namespace All

 26 |   ||| A proof that all elements of a list satisfy a property. It is a list of

 28 |   public export

 29 |   data All : (0 p : a -> Type) -> List a -> Type where

 30 |     Nil  : All p Nil

 31 |     (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)

 36 | namespace Any

 38 |   export

 39 |   All (Uninhabited . p) xs => Uninhabited (Any p xs) where

 40 |     uninhabited @{s::ss} (Here y)  = uninhabited y

 41 |     uninhabited @{s::ss} (There y) = uninhabited y

 43 |   ||| Modify the property given a pointwise function

 44 |   export

 45 |   mapProperty : (f : {0 x : a} -> p x -> q x) -> Any p l -> Any q l

 46 |   mapProperty f (Here p) = Here (f p)

 47 |   mapProperty f (There p) = There (mapProperty f p)

 49 |   ||| Given a decision procedure for a property, determine if an element of a

 55 |   public export

 56 |   any : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (Any p xs)

 57 |   any _ Nil = No uninhabited

 58 |   any p (x::xs) with (p x)

 59 |     any p (x::xs) | Yes prf = Yes (Here prf)

 60 |     any p (x::xs) | No ctra =

 61 |       case any p xs of

 62 |         Yes prf' => Yes (There prf')

 63 |         No ctra' => No $ \case

 64 |           Here px => ctra px

 65 |           There pxs => ctra' pxs

 67 |   ||| Forget the membership proof

 68 |   public export

 69 |   toDPair : {xs : List a} -> Any p xs -> DPair a p

 70 |   toDPair (Here prf) = (_ ** prf)

 71 |   toDPair (There p)  = toDPair p

 73 |   ||| Forget the membership proof

 74 |   export

 75 |   toExists : Any p xs -> Exists p

 76 |   toExists (Here prf) = Evidence _ prf

 77 |   toExists (There prf) = toExists prf

 79 |   public export

 80 |   anyToFin : Any p xs -> Fin $ length xs

 81 |   anyToFin (Here _)      = FZ

 82 |   anyToFin (There later) = FS (anyToFin later)

 84 |   export

 85 |   anyToFinCorrect : (witness : Any p xs) -> p $ index' xs $ anyToFin witness

 86 |   anyToFinCorrect (Here prf) = prf

 87 |   anyToFinCorrect (There later) = anyToFinCorrect later

 89 |   public export

 90 |   anyToFinV : Any p xs -> (idx : Fin $ length xs ** p $ index' xs idx)

 91 |   anyToFinV $ Here x  = (FZ ** x)

 92 |   anyToFinV $ There x = let (idx ** v) = anyToFinV x in (FS idx ** v)

 94 |   public export

 95 |   pushOut : Functor p => Any (p . q) xs -> p $ Any q xs

 96 |   pushOut @{fp} (Here v)  = map @{fp} Here v

 97 |   pushOut @{fp} (There n) = map @{fp} There $ pushOut n

 99 |   export

100 |   All (Show . p) xs => Show (Any p xs) where

101 |     showPrec d @{s::ss} (Here x)  = showCon d "Here"  $ showArg x

102 |     showPrec d @{s::ss} (There x) = showCon d "There" $ showArg x

104 |   export

105 |   All (Eq . p) xs => Eq (Any p xs) where

106 |     (==) @{s::ss} (Here x)  (Here y)  = x == y

107 |     (==) @{s::ss} (There x) (There y) = x == y

108 |     (==) _ _ = False

110 | namespace All

112 |   Either (Uninhabited $ p x) (Uninhabited $ All p xs) => Uninhabited (All p $ x::xs) where

113 |     uninhabited @{Left  _} (px::pxs) = uninhabited px

114 |     uninhabited @{Right _} (px::pxs) = uninhabited pxs

116 |   ||| Modify the property given a pointwise function

117 |   export

118 |   mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l

119 |   mapProperty f [] = []

120 |   mapProperty f (p::pl) = f p :: mapProperty f pl

122 |   ||| Modify the property given a pointwise interface function

123 |   public export

124 |   imapProperty : {0 a : Type}

125 |               -> {0 p,q : a -> Type}

126 |               -> (0 i : a -> Type)

127 |               -> (f : {0 x : a} -> i x => p x -> q x)

128 |               -> {0 as : List a}

129 |               -> All i as => All p as -> All q as

130 |   imapProperty i f @{[]} [] = []

131 |   imapProperty i f @{ix :: ixs} (x :: xs) = f @{ix} x :: imapProperty i f @{ixs} xs

133 |   ||| Forget property source for a homogeneous collection of properties

134 |   public export

135 |   forget : All (const type) types -> List type

136 |   forget [] = []

137 |   forget (x :: xs) = x :: forget xs

139 |   ||| Given a decision procedure for a property, decide whether all elements of

145 |   public export

146 |   all : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs)

147 |   all _ Nil = Yes Nil

148 |   all d (x::xs) with (d x)

149 |     all d (x::xs) | No ctra = No $ \(p::_) => ctra p

150 |     all d (x::xs) | Yes prf =

151 |       case all d xs of

152 |         Yes prf' => Yes (prf :: prf')

153 |         No ctra' => No $ \(_::ps) => ctra' ps

155 |   export

156 |   zipPropertyWith : (f : {0 x : a} -> p x -> q x -> r x) ->

157 |                     All p xs -> All q xs -> All r xs

158 |   zipPropertyWith f [] [] = []

159 |   zipPropertyWith f (px :: pxs) (qx :: qxs)

160 |     = f px qx :: zipPropertyWith f pxs qxs

162 |   export

163 |   All (Show . p) xs => Show (All p xs) where

164 |     show pxs = "[" ++ show' "" pxs ++ "]"

165 |       where

166 |         show' : String -> All (Show . p) xs' => All p xs' -> String

167 |         show' acc @{[]} [] = acc

168 |         show' acc @{[_]} [px] = acc ++ show px

169 |         show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs

171 |   export

172 |   All (Eq . p) xs => Eq (All p xs) where

173 |     (==)           [] []             = True

174 |     (==) @{_ :: _} (h1::t1) (h2::t2) = h1 == h2 && t1 == t2

176 |   %hint

177 |   allEq : All (Ord . p) xs => All (Eq . p) xs

178 |   allEq @{[]}     = []

179 |   allEq @{_ :: _} = %search :: allEq

181 |   export

182 |   All (Ord . p) xs => Ord (All p xs) where

183 |     compare            [] []            = EQ

184 |     compare @{_ :: _} (h1::t1) (h2::t2) = case compare h1 h2 of

185 |       EQ => compare t1 t2

186 |       o  => o

188 |   export

189 |   All (Semigroup . p) xs => Semigroup (All p xs) where

190 |     (<+>)           [] [] = []

191 |     (<+>) @{_ :: _} (h1::t1) (h2::t2) = (h1 <+> h2) :: (t1 <+> t2)

193 |   %hint

194 |   allSemigroup : All (Monoid . p) xs => All (Semigroup . p) xs

195 |   allSemigroup @{[]}     = []

196 |   allSemigroup @{_ :: _} = %search :: allSemigroup

198 |   export

199 |   All (Monoid . p) xs => Monoid (All p xs) where

200 |     neutral @{[]}   = []

201 |     neutral @{_::_} = neutral :: neutral

203 |   ||| A heterogeneous list of arbitrary types

204 |   public export

205 |   HList : List Type -> Type

206 |   HList = All id

208 |   ||| Concatenate lists of proofs.

209 |   public export

210 |   (++) : All p xs -> All p ys -> All p (xs ++ ys)

211 |   [] ++ pys = pys

212 |   (px :: pxs) ++ pys = px :: (pxs ++ pys)

214 |   ||| Take the first element.

215 |   public export

216 |   head : All p (x :: xs) -> p x

217 |   head (y :: _) = y

219 |   ||| Take all but the first element.

220 |   public export

221 |   tail : All p (x :: xs) -> All p xs

222 |   tail (_ :: ys) = ys

224 |   export

225 |   splitAt : (xs : List a) -> All p (xs ++ ys) -> (All p xs, All p ys)

226 |   splitAt [] pxs = ([], pxs)

227 |   splitAt (_ :: xs) (px :: pxs) = mapFst (px ::) (splitAt xs pxs)

229 |   export

230 |   take : (xs : List a) -> All p (xs ++ ys) -> All p xs

231 |   take xs pxs = fst (splitAt xs pxs)

233 |   export

234 |   drop : (xs : List a) -> All p (xs ++ ys) -> All p ys

235 |   drop xs pxs = snd (splitAt xs pxs)

237 |   export

238 |   drop' : (l : Nat) -> All p xs -> All p (drop l xs)

239 |   drop' Z     as      = as

240 |   drop' (S k) []      = []

241 |   drop' (S k) (a::as) = drop' k as

243 |   ||| Push in the property from the list level with element level

244 |   public export

245 |   pushIn : (xs : List a) -> (0 _ : All p xs) -> List $ Subset a p

246 |   pushIn []      []      = []

247 |   pushIn (x::xs) (p::ps) = Element x p :: pushIn xs ps

249 |   ||| Pull the elementwise property out to the list level

250 |   public export

251 |   pullOut : (xs : List $ Subset a p) -> Subset (List a) (All p)

252 |   pullOut [] = Element [] []

253 |   pullOut (Element x p :: xs) = let Element ss ps = pullOut xs in Element (x::ss) (p::ps)

255 |   export

256 |   pushInOutInverse : (xs : List a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf

257 |   pushInOutInverse [] [] = Refl

258 |   pushInOutInverse (x::xs) (p::ps) = rewrite pushInOutInverse xs ps in Refl

260 |   export

261 |   pushOutInInverse : (xs : List $ Subset a p) -> uncurry All.pushIn (pullOut xs) = xs

262 |   pushOutInInverse [] = Refl

263 |   pushOutInInverse (Element x p :: xs) with (pushOutInInverse xs)

264 |     pushOutInInverse (Element x p :: xs) | subprf with (pullOut xs)

265 |       pushOutInInverse (Element x p :: xs) | subprf | Element ss ps = rewrite subprf in Refl

267 |   ||| Given a proof of membership for some element, extract the property proof for it

268 |   public export

269 |   indexAll : Elem x xs -> All p xs -> p x

270 |   indexAll  Here     (p::_  ) = p

271 |   indexAll (There e) ( _::ps) = indexAll e ps

273 |   ||| Given an index of an element, extract the property proof for it

274 |   public export

275 |   index : (idx : Fin $ length xs) -> All p xs -> p (index' xs idx)

276 |   index FZ     (p::ps) = p

277 |   index (FS i) (p::ps) = index i ps

279 |   public export

280 |   pushOut : Applicative p => All (p . q) xs -> p $ All q xs

281 |   pushOut []      = pure []

282 |   pushOut (x::xs) = [| x :: pushOut xs |]

290 | negAnyAll : {xs : List a} -> Not (Any p xs) -> All (Not . p) xs

291 | negAnyAll {xs=Nil}   _ = Nil

292 | negAnyAll {xs=x::xs} f = (f . Here) :: negAnyAll (f . There)

297 | anyNegAll : Any (Not . p) xs -> Not (All p xs)

298 | anyNegAll (Here ctra) (p::_)  = ctra p

299 | anyNegAll (There np)  (_::ps) = anyNegAll np ps

303 | allNegAny : All (Not . p) xs -> Not (Any p xs)

304 | allNegAny [] p = absurd p

305 | allNegAny (np :: npxs) (Here p) = absurd (np p)

306 | allNegAny (np :: npxs) (There p) = allNegAny npxs p

308 | public export

309 | allAnies : All p xs -> List (Any p xs)

310 | allAnies [] = []

311 | allAnies (x::xs) = Here x :: map There (allAnies xs)

314 | altAll : Alternative p => All (p . q) xs -> p $ Any q xs

315 | altAll []      = empty

316 | altAll (a::as) = Here <$> a <|> There <$> altAll as

322 | public export

323 | data Interleaving : (xs, ys, xys : List a) -> Type where

324 |   Nil   : Interleaving [] [] []

325 |   Left  : Interleaving xs ys xys -> Interleaving (x :: xs) ys (x :: xys)

326 |   Right : Interleaving xs ys xys -> Interleaving xs (y :: ys) (y :: xys)

335 | public export

336 | record Split {a : Type} (p : a -> Type) (xys : List a) where

337 |   constructor MkSplit

338 |   {ayes, naws : List a}

339 |   {auto interleaving : Interleaving ayes naws xys}

340 |   ||| A proof that all elements in `ayes` satisfies the property used for the

342 |   prfs    : All p ayes

343 |   ||| A proof that all elements in `naws` do not satisfy the property used for

345 |   contras : All (Not . p) naws

353 | public export

354 | splitOnto :  (dec : (x : a) -> Dec (p x))

355 |           -> (xs : List a)

356 |           -> (a : Split p acc)

357 |           -> Split p (reverseOnto acc xs)

358 | splitOnto dec [] a = a

359 | splitOnto dec (x :: xs) (MkSplit prfs contras) =

360 |   case dec x of

361 |        (Yes prf) => splitOnto dec xs (MkSplit (prf :: prfs) contras)

362 |        (No contra) => splitOnto dec xs (MkSplit prfs (contra :: contras))

371 | public export

372 | split :  (dec : (x : a) -> Dec (p x))

373 |       -> (xs : List a)

374 |       -> Split p (reverse xs)

375 | split dec xs = splitOnto dec xs (MkSplit [] [])

380 | public export

381 | decide : ((x : a) -> Either (p x) (q x)) ->

382 |          (xs : List a) -> Either (All p xs) (Any q xs)

383 | decide dec [] = Left []

384 | decide dec (x :: xs) = case dec x of

385 |   Left px => case decide dec xs of

386 |     Left pxs => Left (px :: pxs)

387 |     Right pxs => Right (There pxs)

388 |   Right px => Right (Here px)