0 | module Data.Bool.Xor
 1 |
 2 | import Data.Bool
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | xor : Bool -> Bool -> Bool
 8 | xor True True = False
 9 | xor False False = False
10 | xor _ _ = True
11 |
12 | export
13 | xorSameFalse : (b : Bool) -> xor b b = False
14 | xorSameFalse False = Refl
15 | xorSameFalse True = Refl
16 |
17 | export
18 | xorFalseNeutral : (b : Bool) -> xor False b = b
19 | xorFalseNeutral False = Refl
20 | xorFalseNeutral True = Refl
21 |
22 | export
23 | xorTrueNot : (b : Bool) -> xor True b = not b
24 | xorTrueNot False = Refl
25 | xorTrueNot True  = Refl
26 |
27 | export
28 | notXor : (a, b : Bool) -> not (xor a b) = xor (not a) b
29 | notXor True  b = rewrite xorFalseNeutral b in
30 |                  rewrite xorTrueNot b in
31 |                  notInvolutive b
32 | notXor False b = rewrite xorFalseNeutral b in
33 |                  sym $ xorTrueNot b
34 |
35 | export
36 | notXorCancel : (a, b : Bool) -> xor (not a) (not b) = xor a b
37 | notXorCancel True  b = rewrite xorFalseNeutral (not b) in
38 |                        sym $ xorTrueNot b
39 | notXorCancel False b = rewrite xorFalseNeutral b in
40 |                        rewrite xorTrueNot (not b) in
41 |                        notInvolutive b
42 |
43 | export
44 | xorAssociative : (a, b, c : Bool) -> xor a (xor b c) = xor (xor a b) c
45 | xorAssociative False b c =
46 |   rewrite xorFalseNeutral b in
47 |   xorFalseNeutral $ xor b c
48 | xorAssociative True  b c =
49 |   rewrite xorTrueNot b in
50 |   rewrite xorTrueNot (xor b c) in
51 |   notXor b c
52 |
53 | export
54 | xorCommutative : (a, b : Bool) -> xor a b = xor b a
55 | xorCommutative False False = Refl
56 | xorCommutative False True  = Refl
57 | xorCommutative True  False = Refl
58 | xorCommutative True  True  = Refl
59 |
60 | export
61 | xorNotTrue : (a : Bool) -> a `xor` (not a) = True
62 | xorNotTrue False = Refl
63 | xorNotTrue True  = Refl
64 |