1
------------------------------------------------------------------------
2
-- A binary representation of natural numbers
3
------------------------------------------------------------------------
7
open import Data.Nat as Nat
8
using (ℕ; zero; z≤n; s≤s) renaming (suc to 1+_)
10
import Data.Nat.Properties as NP
11
open import Data.Digit
12
open import Data.Fin as Fin using (Fin; zero) renaming (suc to 1+_)
13
open import Data.Fin.Props as FP using (_+′_)
14
open import Data.List as List hiding (downFrom)
15
open import Data.Function
16
open import Data.Product
18
open import Relation.Binary
19
open import Relation.Binary.Consequences
20
open import Relation.Binary.PropositionalEquality as PropEq
21
using (_≡_; _≢_; refl; sym)
22
open import Relation.Nullary
24
module BitOrd = StrictTotalOrder (FP.strictTotalOrder 2)
26
------------------------------------------------------------------------
29
-- A representation of binary natural numbers in which there is
30
-- exactly one representative for every number.
32
-- The function toℕ below defines the meaning of Bin.
36
-- bs stands for the binary number 1<reverse bs>, which is positive.
44
-- bs 1# stands for the binary number 1<reverse bs>.
45
_1# : (bs : Bin⁺) → Bin
47
------------------------------------------------------------------------
48
-- Conversion functions
50
-- Converting to a list of bits starting with the _least_ significant
53
toBits : Bin → List Bit
55
toBits (bs 1#) = bs ++ [ 1b ]
57
-- Converting to a natural number.
60
toℕ = fromDigits ∘ toBits
62
-- Converting from a list of bits, starting with the _least_
65
fromBits : List Bit → Bin
67
fromBits (b ∷ bs) with fromBits bs
68
fromBits (b ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
69
fromBits (zero ∷ bs) | 0# = 0#
70
fromBits (1+ zero ∷ bs) | 0# = [] 1#
71
fromBits (1+ 1+ () ∷ bs) | _
73
-- Converting from a natural number.
76
fromℕ n with toDigits 2 n
77
fromℕ .(fromDigits bs) | digits bs = fromBits bs
79
------------------------------------------------------------------------
80
-- (Bin, _≡_, _<_) is a strict total order
84
-- Order relation. Wrapped so that the parameters can be inferred.
86
data _<_ (b₁ b₂ : Bin) : Set where
87
less : (lt : (Nat._<_ on toℕ) b₁ b₂) → b₁ < b₂
90
<-trans : Transitive _<_
91
<-trans (less lt₁) (less lt₂) = less (NP.<-trans lt₁ lt₂)
93
asym : ∀ {b₁ b₂} → b₁ < b₂ → ¬ b₂ < b₁
94
asym {b₁} {b₂} (less lt) (less gt) = tri⟶asym cmp lt gt
95
where cmp = StrictTotalOrder.compare NP.strictTotalOrder
97
irr : ∀ {b₁ b₂} → b₁ < b₂ → b₁ ≢ b₂
98
irr lt eq = asym⟶irr (PropEq.resp₂ _<_) sym asym eq lt
100
irr′ : ∀ {b} → ¬ b < b
101
irr′ lt = irr lt refl
103
∷∙ : ∀ {b₁ b₂ bs₁ bs₂} →
104
bs₁ 1# < bs₂ 1# → (b₁ ∷ bs₁) 1# < (b₂ ∷ bs₂) 1#
105
∷∙ {b₁} {b₂} {bs₁} {bs₂} (less lt) = less (begin
106
1 + (m₁ + n₁ * 2) ≤⟨ ≤-refl {x = 1} +-mono
107
(≤-pred (FP.bounded b₁) +-mono ≤-refl) ⟩
108
1 + (1 + n₁ * 2) ≡⟨ refl ⟩
109
suc n₁ * 2 ≤⟨ lt *-mono ≤-refl ⟩
110
n₂ * 2 ≤⟨ n≤m+n m₂ (n₂ * 2) ⟩
115
open DecTotalOrder decTotalOrder renaming (refl to ≤-refl)
116
m₁ = Fin.toℕ b₁; m₂ = Fin.toℕ b₂
117
n₁ = toℕ (bs₁ 1#); n₂ = toℕ (bs₂ 1#)
120
Fin._<_ b₁ b₂ → (b₁ ∷ bs) 1# < (b₂ ∷ bs) 1#
121
∙∷ {b₁} {b₂} {bs} lt = less (begin
122
1 + (m₁ + n * 2) ≡⟨ sym (+-assoc 1 m₁ (n * 2)) ⟩
123
(1 + m₁) + n * 2 ≤⟨ lt +-mono ≤-refl ⟩
127
open DecTotalOrder decTotalOrder renaming (refl to ≤-refl)
128
open CommutativeSemiring commutativeSemiring using (+-assoc)
129
m₁ = Fin.toℕ b₁; m₂ = Fin.toℕ b₂; n = toℕ (bs 1#)
131
1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1#
132
1<[23] {b} = less (NP.n≤m+n (Fin.toℕ b) 2)
134
1<2+ : ∀ {bs b} → [] 1# < (b ∷ bs) 1#
136
1<2+ {b ∷ bs} = <-trans 1<[23] (∷∙ {b₁ = b} (1<2+ {bs}))
141
0<+ : ∀ {bs} → 0# < bs 1#
143
0<+ {b ∷ bs} = <-trans 0<1 1<2+
145
compare⁺ : Trichotomous (_≡_ on _1#) (_<_ on _1#)
146
compare⁺ [] [] = tri≈ irr′ refl irr′
147
compare⁺ [] (b ∷ bs) = tri< 1<2+ (irr 1<2+) (asym 1<2+)
148
compare⁺ (b ∷ bs) [] = tri> (asym 1<2+) (irr 1<2+ ∘ sym) 1<2+
149
compare⁺ (b₁ ∷ bs₁) (b₂ ∷ bs₂) with compare⁺ bs₁ bs₂
150
... | tri< lt ¬eq ¬gt = tri< (∷∙ lt) (irr (∷∙ lt)) (asym (∷∙ lt))
151
... | tri> ¬lt ¬eq gt = tri> (asym (∷∙ gt)) (irr (∷∙ gt) ∘ sym) (∷∙ gt)
152
compare⁺ (b₁ ∷ bs) (b₂ ∷ .bs) | tri≈ ¬lt refl ¬gt with BitOrd.compare b₁ b₂
153
compare⁺ (b ∷ bs) (.b ∷ .bs) | tri≈ ¬lt refl ¬gt | tri≈ ¬lt′ refl ¬gt′ =
155
... | tri< lt′ ¬eq ¬gt′ = tri< (∙∷ lt′) (irr (∙∷ lt′)) (asym (∙∷ lt′))
156
... | tri> ¬lt′ ¬eq gt′ = tri> (asym (∙∷ gt′)) (irr (∙∷ gt′) ∘ sym) (∙∷ gt′)
158
compare : Trichotomous _≡_ _<_
159
compare 0# 0# = tri≈ irr′ refl irr′
160
compare 0# (bs₂ 1#) = tri< 0<+ (irr 0<+) (asym 0<+)
161
compare (bs₁ 1#) 0# = tri> (asym 0<+) (irr 0<+ ∘ sym) 0<+
162
compare (bs₁ 1#) (bs₂ 1#) = compare⁺ bs₁ bs₂
164
strictTotalOrder : StrictTotalOrder _ _ _
165
strictTotalOrder = record
169
; isStrictTotalOrder = record
170
{ isEquivalence = PropEq.isEquivalence
173
; <-resp-≈ = PropEq.resp₂ _<_
177
------------------------------------------------------------------------
178
-- (Bin, _≡_) is a decidable setoid
180
decSetoid : DecSetoid _ _
181
decSetoid = StrictTotalOrder.decSetoid strictTotalOrder
185
_≟_ : Decidable {A = Bin} _≡_
186
_≟_ = DecSetoid._≟_ decSetoid
188
------------------------------------------------------------------------
191
-- Multiplication by 2.
197
(bs 1#) *2 = (0b ∷ bs) 1#
201
(bs 1#) *2+1 = (1b ∷ bs) 1#
203
-- Division by 2, rounded downwards.
208
⌊ (b ∷ bs) 1# /2⌋ = bs 1#
215
addBits : Carry → Bit → Bit → Carry × Bit
216
addBits c b₁ b₂ with c +′ (b₁ +′ b₂)
217
... | zero = (0b , 0b)
218
... | 1+ zero = (0b , 1b)
219
... | 1+ 1+ zero = (1b , 0b)
220
... | 1+ 1+ 1+ zero = (1b , 1b)
223
addCarryToBitList : Carry → List Bit → List Bit
224
addCarryToBitList zero bs = bs
225
addCarryToBitList (1+ zero) [] = 1b ∷ []
226
addCarryToBitList (1+ zero) (zero ∷ bs) = 1b ∷ bs
227
addCarryToBitList (1+ zero) (1+ zero ∷ bs) = 0b ∷ addCarryToBitList 1b bs
228
addCarryToBitList (1+ 1+ ()) _
229
addCarryToBitList _ ((1+ 1+ ()) ∷ _)
231
addBitLists : Carry → List Bit → List Bit → List Bit
232
addBitLists c [] bs₂ = addCarryToBitList c bs₂
233
addBitLists c bs₁ [] = addCarryToBitList c bs₁
234
addBitLists c (b₁ ∷ bs₁) (b₂ ∷ bs₂) with addBits c b₁ b₂
235
... | (c' , b') = b' ∷ addBitLists c' bs₁ bs₂
239
_+_ : Bin → Bin → Bin
240
m + n = fromBits (addBitLists 0b (toBits m) (toBits n))
246
_*_ : Bin → Bin → Bin
249
-- (b + 2 * bs 1#) * n = b * n + 2 * (bs 1# * n)
250
(b ∷ bs) 1# * n with bs 1# * n
251
(b ∷ bs) 1# * n | 0# = 0#
252
(zero ∷ bs) 1# * n | bs' 1# = (0b ∷ bs') 1#
253
(1+ zero ∷ bs) 1# * n | bs' 1# = n + (0b ∷ bs') 1#
254
((1+ 1+ ()) ∷ _) 1# * _ | _
261
-- Division by 2, rounded upwards.
264
⌈ n /2⌉ = ⌊ suc n /2⌋
270
pred (zero ∷ bs) = pred bs *2+1
271
pred (1+ zero ∷ bs) = (zero ∷ bs) 1#
274
-- downFrom n enumerates all numbers from n - 1 to 0. This function is
275
-- linear in n. Analysis: fromℕ takes linear time, and the preds used
276
-- take amortised constant time (to see this, let the cost of a pred
277
-- be 2, and put 1 debit on every bit which is 1).
279
downFrom : ℕ → List Bin
280
downFrom n = helper n (fromℕ n)
282
helper : ℕ → Bin → List Bin
284
helper (1+ n) (bs 1#) = n′ ∷ helper n n′
287
helper zero (_ 1#) = []
288
helper (1+ _) 0# = []
290
------------------------------------------------------------------------
293
-- The tests below have been commented out since (at least one version
294
-- of) Agda is too slow or memory-hungry to type check them.
297
-- The tests below are run when this module is type checked.
299
-- First some test helpers:
307
nats = List.downFrom testLimit
310
nats⁺ = filter (λ n → decToBool (Nat._≤?_ 1 n)) nats
312
natPairs : List (ℕ × ℕ)
313
natPairs = zip nats (reverse nats)
315
_=[_]_ : (ℕ → ℕ) → List ℕ → (Bin → Bin) → Set
316
f =[ ns ] g = map f ns ≡ map (toℕ ∘ g ∘ fromℕ) ns
318
_=[_]₂_ : (ℕ → ℕ → ℕ) → List (ℕ × ℕ) → (Bin → Bin → Bin) → Set
320
map (uncurry f) ps ≡ map (toℕ ∘ uncurry (g on fromℕ)) ps
322
-- And then the tests:
326
test-*2+1 : (λ n → Nat._+_ (Nat._*_ n 2) 1) =[ nats ] _*2+1
329
test-*2 : (λ n → Nat._*_ n 2) =[ nats ] _*2
332
test-⌊_/2⌋ : Nat.⌊_/2⌋ =[ nats ] ⌊_/2⌋
335
test-+ : Nat._+_ =[ natPairs ]₂ _+_
338
test-* : Nat._*_ =[ natPairs ]₂ _*_
341
test-suc : 1+_ =[ nats ] suc
344
test-⌈_/2⌉ : Nat.⌈_/2⌉ =[ nats ] ⌈_/2⌉
351
test-pred : Nat.pred =[ nats⁺ ] (pred ∘ drop-1#)
354
test-downFrom : map toℕ (downFrom testLimit) ≡
355
List.downFrom testLimit
added
removed
src/Data/Bin.agda
