-
Notifications
You must be signed in to change notification settings - Fork 3
/
dk_binary_nat.dk
130 lines (107 loc) · 3.16 KB
/
dk_binary_nat.dk
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
#NAME dk_binary_nat.
def UNat : Type := dk_nat.Nat.
def Bool : Type := dk_bool.Bool.
bNat : cc.uT.
def BNat : Type := cc.eT bNat.
O : BNat.
def S0 : BNat -> BNat.
S1 : BNat -> BNat.
(; twice zero is zero ;)
[] S0 O --> O.
def nat_of_bnat : BNat -> UNat.
[] nat_of_bnat O --> dk_nat.O
[bn]
nat_of_bnat (S0 bn)
-->
dk_nat.mult dk_nat.2 (nat_of_bnat bn)
[bn]
nat_of_bnat (S1 bn)
-->
dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).
def succ : BNat -> BNat.
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
[n] succ (S0 n) --> S1 n
(; 2n + 1 + 1 = 2 (n+1) ;)
[n] succ (S1 n) --> S0 (succ n).
def bnat_of_nat : UNat -> BNat.
[] bnat_of_nat dk_nat.O --> O
[n] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).
(; Order ;)
def lt : BNat -> BNat -> Bool.
def gt : BNat -> BNat -> Bool.
def leq : BNat -> BNat -> Bool.
def geq : BNat -> BNat -> Bool.
[] lt _ O --> dk_bool.false
[] lt O (S1 _) --> dk_bool.true
[n] lt O (S0 n) --> lt O n
[n,m] lt (S0 n) (S0 m) --> lt n m
[n,m] lt (S0 n) (S1 m) --> leq n m
[n,m] lt (S1 n) (S0 m) --> lt n m
[n,m] lt (S1 n) (S1 m) --> lt n m.
[n,m] gt n m --> lt m n.
[] leq O _ --> dk_bool.true
[] leq (S1 _) O --> dk_bool.false
[n] leq (S0 n) O --> leq n O
[n,m] leq (S0 n) (S0 m) --> leq n m
[n,m] leq (S0 n) (S1 m) --> leq n m
[n,m] leq (S1 n) (S0 m) --> lt n m
[n,m] leq (S1 n) (S1 m) --> leq n m.
[n,m] geq n m --> leq m n.
(; Equality ;)
def eq : BNat -> BNat -> Bool.
[n,m] eq n m
--> dk_bool.and (leq n m) (geq n m).
(; Operations ;)
(; Addition ;)
def plus : BNat -> BNat -> BNat.
[m] plus O m --> m
[n] plus n O --> n
[n,m] plus (S0 n) (S0 m) --> S0 (plus n m)
[n,m] plus (S0 n) (S1 m) --> S1 (plus n m)
[n,m] plus (S1 n) (S0 m) --> S1 (plus n m)
[n,m] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).
(; Product ;)
def mult : BNat -> BNat -> BNat.
[] mult O _ --> O
[] mult _ O --> O
[n,m] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[n,m] mult (S0 n) (S1 m) --> S0 (plus (S0 (mult n m)) n)
[n,m] mult (S1 n) (S0 m) --> S0 (plus m (S0 (mult n m)))
[n,m] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).
(; Min and Max ;)
def max : BNat -> BNat -> BNat.
[m,n] max m n --> dk_bool.ite bNat (leq m n) n m.
def min : BNat -> BNat -> BNat.
[m,n] min m n --> dk_bool.ite bNat (leq m n) m n.
(; Euclidian division ;)
(; by a power of 2 ;)
def div2 : BNat -> BNat.
[] div2 O --> O
[n] div2 (S0 n) --> n
[n] div2 (S1 n) --> n.
(; quo2 n k = n / 2^k ;)
def quo2 : BNat -> UNat -> BNat.
[n] quo2 n dk_nat.O --> n
[] quo2 O _ --> O
[n,k] quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[n,k] quo2 (S1 n) (dk_nat.S k) --> quo2 n k.
(; mod2 n k = n % 2^k ;)
def mod2 : BNat -> UNat -> BNat.
[] mod2 _ dk_nat.O --> O
[] mod2 O _ --> O
[n,k] mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[n,k] mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).
(; Casting to machine numbers ;)
def mnat_of_bnat : N : UNat -> bn : BNat -> dk_machine_int.MInt N.
[N] mnat_of_bnat N O --> dk_machine_int.zero N
[ ] mnat_of_bnat dk_nat.O _ --> dk_machine_int.O.
[N,bn]
mnat_of_bnat (dk_nat.S N) (S0 bn)
-->
dk_machine_int.S0 N (mnat_of_bnat N bn)
[N,bn]
mnat_of_bnat (dk_nat.S N) (S1 bn)
-->
dk_machine_int.S1 N (mnat_of_bnat N bn).