
   0 | module Data.Refined.Core
   1 | 
   2 | import public Data.DPair
   3 | import public Data.Maybe0
   4 | import public Decidable.HDec
   5 | 
   6 | %default total
   7 | 
   8 | --------------------------------------------------------------------------------
   9 | --          Always and Never
  10 | --------------------------------------------------------------------------------
  11 | 
  12 | ||| The predicate that always holds.
  13 | public export
  14 | data Always : a -> Type where
  15 |   Yes : Always a
  16 | 
  17 | public export %inline
  18 | HDec0 a Always where hdec0 _ = Just0 Yes
  19 | 
  20 | public export %inline
  21 | HDec a Always where hdec _ = Just Yes
  22 | 
  23 | ||| The predicate that never holds.
  24 | public export
  25 | data Never : a -> Type where
  26 | 
  27 | public export %inline
  28 | HDec0 a Never where hdec0 _ = Nothing0
  29 | 
  30 | public export %inline
  31 | HDec a Never where hdec _ = Nothing
  32 | 
  33 | --------------------------------------------------------------------------------
  34 | --          Conjunction and Disjunction
  35 | --------------------------------------------------------------------------------
  36 | 
  37 | ||| Conjunction of two predicates
  38 | public export
  39 | data (&&) : (p : a -> Type) -> (q : a -> Type) -> a -> Type where
  40 |   And : {0 p,q : a -> Type} -> {0 v : a} -> p v -> q v -> (&&) p q v
  41 | 
  42 | public export
  43 | mapFst : {0 p,q,r : _} -> (p x -> r x) -> (p && q) x -> (r && q) x
  44 | mapFst f (And v w) = And (f v) w
  45 | 
  46 | public export
  47 | mapSnd : {0 p,q,r : _} -> (q x -> r x) -> (p && q) x -> (p && r) x
  48 | mapSnd f (And v w) = And v (f w)
  49 | 
  50 | public export
  51 | HDec0 a p => HDec0 a q => HDec0 a (p && q) where
  52 |   hdec0 v = zipWith And (hdec0 v) (hdec0 v)
  53 | 
  54 | public export
  55 | HDec a p => HDec a q => HDec a (p && q) where
  56 |   hdec v = [| And (hdec v) (hdec v) |]
  57 | 
  58 | ||| Disjunction of two predicates
  59 | public export
  60 | data (||) : (p : a -> Type) -> (q : a -> Type) -> a -> Type where
  61 |   L : {0 p,q : a -> Type} -> {0 v : a} -> p v -> (||) p q v
  62 |   R : {0 p,q : a -> Type} -> {0 v : a} -> q v -> (||) p q v
  63 | 
  64 | public export
  65 | mapL : {0 p,q,r : _} -> (p x -> r x) -> (p || q) x -> (r || q) x
  66 | mapL f (L v) = L $ f v
  67 | mapL f (R v) = R v
  68 | 
  69 | public export
  70 | mapR : {0 p,q,r : _} -> (q x -> r x) -> (p || q) x -> (p || r) x
  71 | mapR f (L v) = L v
  72 | mapR f (R v) = R $ f v
  73 | 
  74 | public export
  75 | HDec0 a p => HDec0 a q => HDec0 a (p || q) where
  76 |   hdec0 v = map L (hdec0 v) <|> map R (hdec0 v)
  77 | 
  78 | public export
  79 | HDec a p => HDec a q => HDec a (p || q) where
  80 |   hdec v = map L (hdec v) <|> map R (hdec v)
  81 | 
  82 | export
  83 | deMorgan1 : {0 p,q : a -> Type} -> Not ((p || q) v) -> (Not . p && Not . q) v
  84 | deMorgan1 f = And (f . L) (f . R)
  85 | 
  86 | --------------------------------------------------------------------------------
  87 | --          On
  88 | --------------------------------------------------------------------------------
  89 | 
  90 | public export
  91 | data On : (a -> Type) -> (f : b -> a) -> b -> Type where
  92 |   HoldsOn :
  93 |        {0 p : a -> Type}
  94 |     -> {0 f : b -> a}
  95 |     -> {0 v : b}
  96 |     -> p (f v)
  97 |     -> On p f v
  98 | 
  99 | public export
 100 | {f : b -> a} -> HDec0 a p => HDec0 b (p `On` f) where
 101 |   hdec0 v = map HoldsOn $ hdec0 (f v)
 102 | 
 103 | public export
 104 | {f : b -> a} -> HDec a p => HDec b (p `On` f) where
 105 |   hdec v = map HoldsOn $ hdec (f v)
 106 | 
 107 | public export
 108 | mapOn : {0 p,q : _} -> (p (f x) -> q (f x)) -> On p f x -> On q f x
 109 | mapOn g (HoldsOn y) = HoldsOn $ g y
 110 | 
 111 | --------------------------------------------------------------------------------
 112 | --          Holds
 113 | --------------------------------------------------------------------------------
 114 | 
 115 | ||| Proof that an (explicitly given) boolean predicate holds
 116 | public export
 117 | data Holds : (f : a -> Bool) -> a -> Type where
 118 |   ItHolds :
 119 |        {0 f : a -> Bool}
 120 |     -> {0 v : a}
 121 |     -> (prf : f v === True)
 122 |     -> Holds f v
 123 | 
 124 | public export
 125 | test : (b : Bool) -> Maybe0 (b === True)
 126 | test False = Nothing0
 127 | test True  = Just0 Refl
 128 | 
 129 | public export %inline
 130 | {f : a -> Bool} -> HDec0 a (Holds f) where
 131 |   hdec0 v = map (\v => ItHolds v) $ test (f v)
 132 | 
 133 | public export %inline
 134 | {f : a -> Bool} -> HDec a (Holds f) where
 135 |   hdec v with (f v) proof eq
 136 |     _ | True  = Just (ItHolds eq)
 137 |     _ | False = Nothing
 138 | 
 139 | 0 and : (b === True) -> (c === True) -> (b && c) === True
 140 | and Refl Refl = Refl
 141 | 
 142 | 0 and' : {b,c : Bool} -> (b && c) === True -> (b === True, c === True)
 143 | and' {b = True, c = True}  prf = (Refl, Refl)
 144 | and' {b = True, c = False} prf = absurd prf
 145 | and' {b = False}           prf = absurd prf
 146 | 
 147 | ||| Conversion from type-level `(&&)` to boolean `(&&)`
 148 | export
 149 | 0 holdsAnd :
 150 |      {f,g : a -> Bool}
 151 |   -> (v : a)
 152 |   -> (Holds f && Holds g) v
 153 |   -> Holds (\x => f x && g x) v
 154 | holdsAnd v (And (ItHolds p1) (ItHolds p2)) = ItHolds (and p1 p2)
 155 | 
 156 | ||| Conversion from boolean `(&&)` to type-level `(&&)`
 157 | export
 158 | 0 andHolds :
 159 |      {f,g : a -> Bool}
 160 |   -> (v : a)
 161 |   -> Holds (\x => f x && g x) v
 162 |   -> (Holds f && Holds g) v
 163 | andHolds v (ItHolds prf) =
 164 |   let (x,y) := and' prf
 165 |    in And (ItHolds x) (ItHolds y)
 166 | 
 167 | 0 or1 : (b === True) -> (b || c) === True
 168 | or1 Refl = Refl
 169 | 
 170 | 0 or2 : (c === True) -> (b || c) === True
 171 | or2 {b = True}  Refl = Refl
 172 | or2 {b = False} Refl = Refl
 173 | 
 174 | 0 or' : {b,c : Bool} -> (b || c) === True -> Either (b === True) (c === True)
 175 | or' {b = True}             p = Left Refl
 176 | or' {c = True}             p = Right Refl
 177 | or' {b = False, c = False} p = absurd p
 178 | 
 179 | ||| Conversion from type-level `(||)` to boolean `(||)`
 180 | export
 181 | 0 holdsOr :
 182 |      {f,g : a -> Bool}
 183 |   -> (v : a)
 184 |   -> (Holds f || Holds g) v
 185 |   -> Holds (\x => f x || g x) v
 186 | holdsOr v (L $ ItHolds p) = ItHolds (or1 p)
 187 | holdsOr v (R $ ItHolds p) = ItHolds (or2 p)
 188 | 
 189 | ||| Conversion from boolean `(||)` to type-level `(||)`
 190 | export
 191 | 0 orHolds :
 192 |      {f,g : a -> Bool}
 193 |   -> (v : a)
 194 |   -> Holds (\x => f x || g x) v
 195 |   -> (Holds f || Holds g) v
 196 | orHolds v (ItHolds p) = case or' p of
 197 |   Left  p' => L $ ItHolds p'
 198 |   Right p' => R $ ItHolds p'
 199 | 
 200 | --------------------------------------------------------------------------------
 201 | --          Const
 202 | --------------------------------------------------------------------------------
 203 | 
 204 | ||| The `Const` predicate.
 205 | |||
 206 | ||| This allows us to refine a value based on a refinement on a second
 207 | ||| value.
 208 | public export
 209 | data Const : (p : e -> Type) -> (v : e) -> t -> Type where
 210 |   C : {0 p : e -> Type} -> p v -> Const p v x
 211 | 
 212 | public export
 213 | unConst : Const p v t -> p v
 214 | unConst (C prf) = prf
 215 | 
 216 | public export
 217 | {v : e} -> HDec0 e p => HDec0 t (Const p v) where
 218 |   hdec0 _ = map C $ hdec0 {p} v
 219 | 
 220 | --------------------------------------------------------------------------------
 221 | --          Refine
 222 | --------------------------------------------------------------------------------
 223 | 
 224 | ||| Try to refine a value into a `Subset`.
 225 | public export
 226 | refine0 : HDec0 a p => a -> Maybe (Subset a p)
 227 | refine0 x = case hdec0 {p} x of
 228 |   Just0 prf => Just $ Element x prf
 229 |   Nothing0  => Nothing
 230 | 
 231 | ||| Try to refine a value into a `DPair`.
 232 | public export
 233 | refine : HDec a p => a -> Maybe (DPair a p)
 234 | refine x = case hdec {p} x of
 235 |   Just prf => Just $ (x ** prf)
 236 |   Nothing  => Nothing
 237 |