0 | module Data.So
 1 |
 2 | import Data.Bool
 3 |
 4 | %default total
 5 |
 6 | ||| Ensure that some run-time Boolean test has been performed.
 7 | |||
 8 | ||| This lifts a Boolean predicate to the type level. See the function `choose`
 9 | ||| if you need to perform a Boolean test and convince the type checker of this
10 | ||| fact.
11 | |||
12 | ||| If you find yourself using `So` for something other than primitive types,
13 | ||| it may be appropriate to define a type of evidence for the property that you
14 | ||| care about instead.
15 | public export
16 | data So : Bool -> Type where
17 |   Oh : So True
18 |
19 | export
20 | Uninhabited (So False) where
21 |   uninhabited Oh impossible
22 |
23 | ||| Perform a case analysis on a Boolean, providing clients with a `So` proof
24 | export
25 | choose : (b : Bool) -> Either (So b) (So (not b))
26 | choose True  = Left Oh
27 | choose False = Right Oh
28 |
29 | export
30 | decSo : (b : Bool) -> Dec (So b)
31 | decSo True  = Yes Oh
32 | decSo False = No uninhabited
33 |
34 | export
35 | eqToSo : b = True -> So b
36 | eqToSo Refl = Oh
37 |
38 | export
39 | soToEq : So b -> b = True
40 | soToEq Oh = Refl
41 |
42 | ||| If `b` is True, `not b` can't be True
43 | export
44 | soToNotSoNot : So b -> Not (So (not b))
45 | soToNotSoNot Oh = uninhabited
46 |
47 | ||| If `not b` is True, `b` can't be True
48 | export
49 | soNotToNotSo : So (not b) -> Not (So b)
50 | soNotToNotSo = flip soToNotSoNot
51 |
52 | export
53 | soAnd : {a : Bool} -> So (a && b) -> (So a, So b)
54 | soAnd soab with (choose a)
55 |   soAnd {a=True}  soab | Left Oh = (Oh, soab)
56 |   soAnd {a=True}  soab | Right prf = absurd prf
57 |   soAnd {a=False} soab | Right prf = absurd soab
58 |
59 | export
60 | andSo : (So a, So b) -> So (a && b)
61 | andSo (Oh, Oh) = Oh
62 |
63 | export
64 | soOr : {a : Bool} -> So (a || b) -> Either (So a) (So b)
65 | soOr soab with (choose a)
66 |   soOr {a=True}  _    | Left Oh = Left Oh
67 |   soOr {a=False} soab | Right Oh = Right soab
68 |
69 | export
70 | orSo : Either (So a) (So b) -> So (a || b)
71 | orSo (Left Oh)  = Oh
72 | orSo (Right Oh) = rewrite orTrueTrue a in
73 |                   Oh
74 |