0 | module Data.Bool
  1 |
  2 | %default total
  3 |
  4 | export
  5 | notInvolutive : (x : Bool) -> not (not x) = x
  6 | notInvolutive True  = Refl
  7 | notInvolutive False = Refl
  8 |
  9 | -- AND
 10 |
 11 | export
 12 | andSameNeutral : (x : Bool) -> x && x = x
 13 | andSameNeutral False = Refl
 14 | andSameNeutral True = Refl
 15 |
 16 | export
 17 | andFalseFalse : (x : Bool) -> x && False = False
 18 | andFalseFalse False = Refl
 19 | andFalseFalse True = Refl
 20 |
 21 | export
 22 | andTrueNeutral : (x : Bool) -> x && True = x
 23 | andTrueNeutral False = Refl
 24 | andTrueNeutral True = Refl
 25 |
 26 | export
 27 | andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
 28 | andAssociative True  _ _ = Refl
 29 | andAssociative False _ _ = Refl
 30 |
 31 | export
 32 | andCommutative : (x, y : Bool) -> x && y = y && x
 33 | andCommutative x True  = andTrueNeutral x
 34 | andCommutative x False = andFalseFalse x
 35 |
 36 | export
 37 | andNotFalse : (x : Bool) -> x && not x = False
 38 | andNotFalse False = Refl
 39 | andNotFalse True = Refl
 40 |
 41 | -- OR
 42 |
 43 | export
 44 | orSameNeutral : (x : Bool) -> x || x = x
 45 | orSameNeutral False = Refl
 46 | orSameNeutral True = Refl
 47 |
 48 | export
 49 | orFalseNeutral : (x : Bool) -> x || False = x
 50 | orFalseNeutral False = Refl
 51 | orFalseNeutral True = Refl
 52 |
 53 | export
 54 | orTrueTrue : (x : Bool) -> x || True = True
 55 | orTrueTrue False = Refl
 56 | orTrueTrue True = Refl
 57 |
 58 | export
 59 | orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
 60 | orAssociative True  _ _ = Refl
 61 | orAssociative False _ _ = Refl
 62 |
 63 | export
 64 | orCommutative : (x, y : Bool) -> x || y = y || x
 65 | orCommutative x True  = orTrueTrue x
 66 | orCommutative x False = orFalseNeutral x
 67 |
 68 | export
 69 | orNotTrue : (x : Bool) -> x || not x = True
 70 | orNotTrue False = Refl
 71 | orNotTrue True = Refl
 72 |
 73 | export
 74 | orBothFalse : {0 x, y : Bool} -> (0 prf : x || y = False) -> (x = False, y = False)
 75 | orBothFalse prf = unerase $ orBothFalse' prf
 76 |   where
 77 |     unerase : (0 prf : (x = False, y = False)) -> (x = False, y = False)
 78 |     unerase (p, q) = (irrelevantEq p, irrelevantEq q)
 79 |
 80 |     orBothFalse' : {x, y : Bool} -> x || y = False -> (x = False, y = False)
 81 |     orBothFalse' {x = False} yFalse = (Refl, yFalse)
 82 |     orBothFalse' {x = True} trueFalse = absurd trueFalse
 83 |
 84 | -- interaction & De Morgan's laws
 85 |
 86 | export
 87 | orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
 88 | orSameAndRightNeutral False _ = Refl
 89 | orSameAndRightNeutral True  _ = Refl
 90 |
 91 | export
 92 | andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
 93 | andDistribOrR False _ _ = Refl
 94 | andDistribOrR True  _ _ = Refl
 95 |
 96 | export
 97 | orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
 98 | orDistribAndR False _ _ = Refl
 99 | orDistribAndR True  _ _ = Refl
100 |
101 | export
102 | notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
103 | notAndIsOr False _ = Refl
104 | notAndIsOr True  _ = Refl
105 |
106 | export
107 | notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
108 | notOrIsAnd False _ = Refl
109 | notOrIsAnd True  _ = Refl
110 |
111 | -- Interaction with typelevel `Not`
112 |
113 | export
114 | notTrueIsFalse : {1 x : Bool} -> Not (x = True) -> x = False
115 | notTrueIsFalse {x=False} _ = Refl
116 | notTrueIsFalse {x=True}  f = absurd $ f Refl
117 |
118 | export
119 | notFalseIsTrue : {1 x : Bool} -> Not (x = False) -> x = True
120 | notFalseIsTrue {x=True} _  = Refl
121 | notFalseIsTrue {x=False} f = absurd $ f Refl
122 |
123 | --------------------------------------------------------------------------------
124 | -- Decidability specialized on bool
125 | --------------------------------------------------------------------------------
126 |
127 | ||| You can reverse decidability when bool is involved.
128 | -- Given a contra on bool equality Not (a = b), produce a proof of the opposite (that (not a) = b)
129 | public export
130 | invertContraBool : (a, b : Bool) -> Not (a = b) -> (not a = b)
131 | invertContraBool False False contra = absurd $ contra Refl
132 | invertContraBool False True contra = Refl
133 | invertContraBool True False contra = Refl
134 | invertContraBool True True contra = absurd $ contra Refl
135 |