
  0 | module TyRE.Extra.Reflects
  1 | 
  2 | import TyRE.Extra.Pred
  3 | import Data.List.Elem
  4 | 
  5 | public export
  6 | data Reflects : (p : a -> Type) -> (Maybe a) -> Type where
  7 |   Indeed    : {0 p : a -> Type} -> (prf : p x) -> Reflects p (Just x)
  8 |   Otherwise : {0 p : a -> Type} -> (prf : (x : a) -> Not (p x)) -> Reflects p Nothing
  9 | 
 10 | public export
 11 | record RMaybe {a : Type} p where
 12 |   constructor Because
 13 |   Holds   : Maybe a
 14 |   0 Proof : Reflects p Holds
 15 | 
 16 | public export
 17 | map : {0 p,q : a -> Type} -> p <-> q -> RMaybe p -> RMaybe q
 18 | map iff (Nothing `Because` (Otherwise nprf)) = Nothing `Because` ( Otherwise (\x => \qx => nprf x (iff.If x qx)))
 19 | map iff ((Just x) `Because` (Indeed prf)) = (Just x) `Because` (Indeed (iff.onlyIf x prf))
 20 | 
 21 | public export
 22 | findR : {0 a : Type} -> (pred : a -> Bool) -> (xs : List a) ->
 23 |   RMaybe (\x => (x `Elem` xs, pred x = True))
 24 | 
 25 | findR pred [] = Nothing `Because` Otherwise (\x => \case (_, _) impossible)
 26 | 
 27 | findR pred (x :: xs) with (pred x) proof p
 28 |   findR pred (x :: xs) | True = (Just x) `Because` (Indeed (Here, p))
 29 |   findR pred (x :: xs) | False =
 30 |     let iff: (\y => (y `Elem` (xs), pred y = True)) <-> (\y => (y `Elem` x :: xs,  pred y = True))
 31 |         iff = (\y => (\case
 32 |                      (Here, i) => absurd (trans (sym p) i)
 33 |                      (There e, c) => (e,c)
 34 |                   ))
 35 |               `And`
 36 |               (\_ => (\(e,v) => (There e, v)))
 37 |     in map iff (findR pred xs)
 38 |