0 | module Data.Binary
 1 |
 2 | import Data.Nat.Properties
 3 | import Data.Binary.Digit
 4 | import Syntax.PreorderReasoning
 5 |
 6 | %default total
 7 |
 8 | ||| Bin represents binary numbers right-to-left.
 9 | ||| For instance `4` can be represented as `OOI`.
10 | ||| Note that representations are not unique: one may append arbitrarily
11 | ||| many Os to the right of the representation without changing the meaning.
12 | public export
13 | Bin : Type
14 | Bin = List Digit
15 |
16 | ||| Conversion from lists of bits to natural number.
17 | public export
18 | toNat : Bin -> Nat
19 | toNat = foldr (\ b, acc => toNat b + 2 * acc) 0
20 |
21 | ||| Successor function on binary numbers.
22 | ||| Amortised constant time.
23 | public export
24 | suc : Bin -> Bin
25 | suc [] = [I]
26 | suc (O :: bs) = I :: bs
27 | suc (I :: bs) = O :: (suc bs)
28 |
29 | ||| Correctness proof of `suc` with respect to the semantics in terms of Nat
30 | export
31 | sucCorrect : {bs : Bin} -> toNat (suc bs) === S (toNat bs)
32 | sucCorrect {bs = []} = Refl
33 | sucCorrect {bs = O :: bs} = Refl
34 | sucCorrect {bs = I :: bs} = Calc $
35 |   |~ toNat (suc (I :: bs))
36 |   ~~ toNat (O :: suc bs) ...( Refl )
37 |   ~~ 2 * toNat (suc bs)  ...( Refl )
38 |   ~~ 2 * S (toNat bs)    ...( cong (2 *) sucCorrect )
39 |   ~~ 2 + 2 * toNat bs    ...( unfoldDoubleS )
40 |   ~~ S (toNat (I :: bs)) ...( Refl )
41 |