dk_binary_nat.dk 3.38 KB
Newer Older
1
#NAME dk_binary_nat
2

3
4
UNat : Type := dk_nat.Nat.
Bool : Type := dk_bool.Bool.
5

6
7
bNat : cc.uT.
BNat : Type := cc.eT bNat.
8

9
10
11
O : BNat.
S0 : BNat -> BNat.
S1 : BNat -> BNat.
12
13
14
(; twice zero is zero ;)
[] S0 O --> O.

15
nat_of_bnat : BNat -> UNat.
16
[] nat_of_bnat O --> dk_nat.O
17
18
19
20
21
22
23
24
25
26
[ bn : BNat ]
    nat_of_bnat (S0 bn)
      -->
    dk_nat.mult dk_nat.2 (nat_of_bnat bn)
[ bn : BNat ]
    nat_of_bnat (S1 bn)
      -->
    dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).

succ : BNat -> BNat.
27
28
29
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
30
[ n : BNat ] succ (S0 n) --> S1 n
31
(; 2n + 1 + 1 = 2 (n+1) ;)
32
[ n : BNat ] succ (S1 n) --> S0 (succ n).
33

34
bnat_of_nat : UNat -> BNat.
35
36
37
38
[] bnat_of_nat dk_nat.O --> O
[ n : UNat ] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).

(; Order ;)
39
40
41
42
lt : BNat -> BNat -> Bool.
gt : BNat -> BNat -> Bool.
leq : BNat -> BNat -> Bool.
geq : BNat -> BNat -> Bool.
43

44
45
46
47
48
49
[ n : BNat ] lt n O --> dk_bool.false
[ m : BNat ] lt O m --> dk_bool.true
[ n : BNat, m : BNat ] lt (S0 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] lt (S0 n) (S1 m) --> leq n m
[ n : BNat, m : BNat ] lt (S1 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] lt (S1 n) (S1 m) --> lt n m.
50

51
[ n : BNat, m : BNat ] gt n m --> lt m n.
52

53
54
55
56
57
58
[ m : BNat ] leq O m --> dk_bool.true
[ n : BNat ] leq n O --> dk_bool.false
[ n : BNat, m : BNat ] leq (S0 n) (S0 m) --> leq n m
[ n : BNat, m : BNat ] leq (S0 n) (S1 m) --> leq n m
[ n : BNat, m : BNat ] leq (S1 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] leq (S1 n) (S1 m) --> leq n m.
59

60
[ n : BNat, m : BNat ] geq n m --> leq m n.
61
62

(; Equality ;)
63
64
eq : BNat -> BNat -> Bool.
[ n : BNat, m : BNat ] eq n m
65
      --> dk_bool.and (leq n m) (geq n m).
66
67
68
69

(; Operations ;)

(; Addition ;)
70
71
72
73
74
75
76
plus : BNat -> BNat -> BNat.
[ m : BNat ] plus O m --> m
[ n : BNat ] plus n O --> n
[ n : BNat, m : BNat ] plus (S0 n) (S0 m) --> S0 (plus n m)
[ n : BNat, m : BNat ] plus (S0 n) (S1 m) --> S1 (plus n m)
[ n : BNat, m : BNat ] plus (S1 n) (S0 m) --> S1 (plus n m)
[ n : BNat, m : BNat ] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).
77
78

(; Product ;)
79
80
81
82
83
84
85
mult : BNat -> BNat -> BNat.
[ m : BNat ] mult O m --> O
[ n : BNat ] mult n O --> O
[ n : BNat, m : BNat ] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[ n : BNat, m : BNat ] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[ n : BNat, m : BNat ] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[ n : BNat, m : BNat ] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).
86
87

(; Min and Max ;)
88
89
90
max : BNat -> BNat -> BNat.
[ m : BNat, n : BNat ]
    max m n --> dk_bool.ite bNat (leq m n) n m.
91

92
93
94
min : BNat -> BNat -> BNat.
[ m : BNat, n : BNat ]
    min m n --> dk_bool.ite bNat (leq m n) m n.
95
96
97

(; Euclidian division ;)
(; by a power of 2 ;)
98
div2 : BNat -> BNat.
99
[] div2 O --> O
100
101
[ n : BNat ] div2 (S0 n) --> n
[ n : BNat ] div2 (S1 n) --> n.
102

103
length : BNat -> UNat.
104
[] length O --> dk_nat.O
105
106
[ n : BNat ] length (S0 n) --> dk_nat.S (length n)
[ n : BNat ] length (S1 n) --> dk_nat.S (length n).
107
108

(; quo2 n k = n / 2^k ;)
109
110
quo2 : BNat -> UNat -> BNat.
[ n : BNat ] quo2 n dk_nat.O --> n
111
[ k : UNat ] quo2 O k --> O
112
[ n : BNat, k : UNat ]
113
    quo2 (S0 n) (dk_nat.S k) --> quo2 n k
114
[ n : BNat, k : UNat ]
115
    quo2 (S1 n) (dk_nat.S k) --> quo2 n k.
116
117

(; mod2 n k = n % 2^k ;)
118
119
mod2 : BNat -> UNat -> BNat.
[ n : BNat ] mod2 n dk_nat.O --> O
120
[ k : UNat ] mod2 O k --> O
121
[ n : BNat, k : UNat ]
122
    mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
123
[ n : BNat, k : UNat ]
124
    mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).