dk_binary_nat.dk 3.05 KB
Newer Older
1
#NAME dk_binary_nat
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

UNat : Type := cc.eT dk_nat.Nat.
B : Type := cc.eT dk_bool.bool.

BNat : cc.uT.
N : Type := cc.eT BNat.

O : N.
S0 : N -> N.
S1 : N -> N.
(; twice zero is zero ;)
[] S0 O --> O.

nat_of_bnat : N -> UNat.
[] nat_of_bnat O --> dk_nat.O
[ bn : N ] nat_of_bnat (S0 bn) --> dk_nat.mult dk_nat.__2 (nat_of_bnat bn)
[ bn : N ] nat_of_bnat (S1 bn) --> dk_nat.S (dk_nat.mult dk_nat.__2 (nat_of_bnat bn)).

succ : N -> N.
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
[ n : N ] succ (S0 n) --> S1 n
(; 2n + 1 + 1 = 2 (n+1) ;)
[ n : N ] succ (S1 n) --> S0 (succ n).

bnat_of_nat : UNat -> N.
[] bnat_of_nat dk_nat.O --> O
[ n : UNat ] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).

(; Order ;)
lt : N -> N -> B.
gt : N -> N -> B.
leq : N -> N -> B.
geq : N -> N -> B.

[ n : N ] lt n O --> dk_bool.false
[ m : N ] lt O m --> dk_bool.true
[ n : N, m : N ] lt (S0 n) (S0 m) --> lt n m
[ n : N, m : N ] lt (S0 n) (S1 m) --> leq n m
[ n : N, m : N ] lt (S1 n) (S0 m) --> lt n m
[ n : N, m : N ] lt (S1 n) (S1 m) --> lt n m.

[ n : N, m : N ] gt n m --> lt m n.

[ m : N ] leq O m --> dk_bool.true
[ n : N ] leq n O --> dk_bool.false
[ n : N, m : N ] leq (S0 n) (S0 m) --> leq n m
[ n : N, m : N ] leq (S0 n) (S1 m) --> leq n m
[ n : N, m : N ] leq (S1 n) (S0 m) --> lt n m
[ n : N, m : N ] leq (S1 n) (S1 m) --> leq n m.

[ n : N, m : N ] geq n m --> leq m n.

(; Equality ;)
eq : N -> N -> B.
[ n : N, m : N ] eq n m
59
      --> dk_bool.and (leq n m) (geq n m).
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

(; Operations ;)

(; Addition ;)
plus : N -> N -> N.
[ m : N ] plus O m --> m
[ n : N ] plus n O --> n
[ n : N, m : N ] plus (S0 n) (S0 m) --> S0 (plus n m)
[ n : N, m : N ] plus (S0 n) (S1 m) --> S1 (plus n m)
[ n : N, m : N ] plus (S1 n) (S0 m) --> S1 (plus n m)
[ n : N, m : N ] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).

(; Product ;)
mult : N -> N -> N.
[ m : N ] mult O m --> O
[ n : N ] mult n O --> O
[ n : N, m : N ] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[ n : N, m : N ] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[ n : N, m : N ] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[ n : N, m : N ] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).

(; Min and Max ;)
max : N -> N -> N.
[ m : N, n : N ]
84
    max m n --> dk_bool.ite BNat (leq m n) n m.
85
86
87

min : N -> N -> N.
[ m : N, n : N ]
88
    min m n --> dk_bool.ite BNat (leq m n) m n.
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

(; Euclidian division ;)
(; by a power of 2 ;)
div2 : N -> N.
[] div2 O --> O
[ n : N ] div2 (S0 n) --> n
[ n : N ] div2 (S1 n) --> n.

length : N -> UNat.
[] length O --> dk_nat.O
[ n : N ] length (S0 n) --> dk_nat.S (length n)
[ n : N ] length (S1 n) --> dk_nat.S (length n).

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

(; mod2 n k = n % 2^k ;)
mod2 : N -> UNat -> N.
[ n : N ] mod2 n dk_nat.O --> O
[ k : UNat ] mod2 O k --> O
[ n : N, k : UNat ]
116
    mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
117
[ n : N, k : UNat ]
118
    mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).