dk_machine_int.dk 6.59 KB
Newer Older
1
#NAME dk_machine_int
2
Bool : Type := dk_bool.Bool.
3

4
UNat : Type := dk_nat.Nat.
5
6
7
8
UO : UNat := dk_nat.O.
US : UNat -> UNat := dk_nat.S.

Mint : UNat -> cc.uT.
9
10
MInt : UNat -> Type.
[ N : UNat ] MInt N --> cc.eT (Mint N).
11
12
13
14
15
16

O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
S1 : N : UNat -> MInt N -> MInt (US N).

zero : N : UNat -> MInt N.
17
18
[] zero dk_nat.O --> O
[ N : UNat ] zero (dk_nat.S N) --> S0 N (zero N).
19
20

bound : N : UNat -> MInt N.
21
22
[] bound dk_nat.O --> O
[ N : UNat ] bound (dk_nat.S N) --> S1 N (bound N).
23
24
25

(; cast ;)
downcast : N : UNat -> MInt (US N) -> MInt N.
26
[n : MInt (US UO)] downcast _ n --> O
27
28
29
30
[N : UNat, n : MInt (US N)]
    downcast _ (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N : UNat, n : MInt (US N)]
    downcast _ (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
31
32

double : N : UNat ->     MInt N -> MInt N
33
       := N : UNat => n : MInt N => downcast N (S0 N n).
34
35

succ : N : UNat -> MInt N -> MInt N.
36
37
38
[] succ _ O --> O
[ N : UNat, n : MInt N ] succ _ (S0 N n) --> S1 N n
[ N : UNat, n : MInt N ] succ _ (S1 N n) --> S0 N (succ N n).
39
40

pred : N : UNat -> MInt N -> MInt N.
41
42
43
[] pred _ O --> O
[ N : UNat, n : MInt N ] pred _ (S1 N n) --> S0 N n
[ N : UNat, n : MInt N ] pred _ (S0 N n) --> S1 N (pred N n).
44
45

plus : N : UNat -> MInt N -> MInt N -> MInt N.
46
[ ] plus _ O O --> O
47
48
49
50
51
52
53
54
[ N : UNat, n : MInt N, m : MInt N ]
    plus _ (S0 _ n) (S0 N m) --> S0 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ]
    plus _ (S0 _ n) (S1 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ]
    plus _ (S1 _ n) (S0 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ]
    plus _ (S1 _ n) (S1 N m) --> S0 N (succ N (plus N n m)).
55
56

complement : N : UNat -> MInt N -> MInt N.
57
58
59
[] complement _ O --> O
[ N : UNat, n : MInt N ] complement _ (S0 N n) --> S1 N (complement N n)
[ N : UNat, n : MInt N ] complement _ (S1 N n) --> S0 N (complement N n).
60
61
62
63
64
65
66
67
68

opp : N : UNat -> MInt N -> MInt N.
[ N : UNat, n : MInt N ] opp N n --> succ N (complement N n).

sub : N : UNat -> MInt N -> MInt N -> MInt N.
[ N : UNat, n : MInt N, m : MInt N ] sub N n m --> plus N n (opp N m).

(; Product ;)
mult : N : UNat -> MInt N -> MInt N -> MInt N.
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
[ ] mult _ O O --> O
[ N : UNat, n : MInt N, m : MInt N ]
    mult _ (S0 _ n) (S0 N m)
      -->
    double (US N) (S0 N (mult N n m))
[ N : UNat, n : MInt N, m : MInt N ]
    mult _ (S0 _ n) (S1 N m)
      -->
    S0 N (plus N m (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ]
    mult _ (S1 _ n) (S0 N m)
      -->
    S0 N (plus N n (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ]
    mult _ (S1 _ n) (S1 N m)
      -->
    S1 N (plus N (double N (mult N m n)) (plus N n m)).
86
87

(; equality ;)
88
equal : N : UNat -> MInt N -> MInt N -> Bool.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
89
[ N : UNat, n : MInt N ] equal N n n --> dk_bool.true
90
91
92
93
94
95
96
97
[ N : UNat, n : MInt N, m : MInt N ]
    equal _ (S0 _ n) (S0 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ]
    equal _ (S1 _ n) (S1 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ]
    equal _ (S0 _ n) (S1 N m) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ]
    equal _ (S1 _ n) (S0 N m) --> dk_bool.false.
98
99

(; unsigned comparison ;)
100
101
unsigned_lt : N : UNat -> MInt N -> MInt N -> Bool.
unsigned_leq : N : UNat -> MInt N -> MInt N -> Bool.
102

103
[] unsigned_lt _ O O --> dk_bool.false
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_lt _ (S0 _ n) (S0 N m)
      -->
    unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_lt _ (S1 _ n) (S1 N m)
      -->
    unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_lt _ (S0 _ n) (S1 N m)
      -->
    unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_lt _ (S1 _ n) (S0 N m)
      -->
    unsigned_lt N n m.
120

121
[] unsigned_leq _ O O --> dk_bool.true
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_leq _ (S0 _ n) (S0 N m)
      -->
    unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_leq _ (S1 _ n) (S1 N m)
      -->
    unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_leq _ (S0 _ n) (S1 N m)
      -->
    unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
    unsigned_leq _ (S1 _ n) (S0 N m)
      -->
    unsigned_lt N n m.

139
unsigned_gt : N : UNat -> MInt N -> MInt N -> Bool
140
141
            := N : UNat => n : MInt N => m : MInt N => unsigned_lt N m n.

142
unsigned_geq : N : UNat -> MInt N -> MInt N -> Bool
143
             := N : UNat => n : MInt N => m : MInt N => unsigned_leq N m n.
144
145

(; signed comparison ;)
146
positive : N : UNat -> MInt N -> Bool.
147
148
149
150
151
[] positive _ O --> dk_bool.true
[] positive _ (S0 _ O) --> dk_bool.true
[] positive _ (S1 _ O) --> dk_bool.false
[ N : UNat, n : MInt N ] positive _ (S0 N n) --> positive N n
[ N : UNat, n : MInt N ] positive _ (S1 N n) --> positive N n.
152

153
154
155
signed_leq : N : UNat ->
             n : MInt N ->
             m : MInt N ->
156
             Bool
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
           :=
             N : UNat =>
             n : MInt N =>
             m : MInt N =>
             dk_bool.iteb (dk_bool.and
                            (positive N m)
                            (dk_bool.not (positive N n)))
                          dk_bool.true
                            (dk_bool.iteb (dk_bool.and
                                            (positive N n)
                                            (dk_bool.not (positive N m)))
                                          dk_bool.false
                                            (positive N (sub N m n))).

signed_geq : N : UNat ->
             n : MInt N ->
             m : MInt N ->
174
             Bool
175
176
177
178
179
180
181
182
183
           :=
             N : UNat =>
             n : MInt N =>
             m : MInt N =>
             signed_leq N m n.

signed_lt : N : UNat ->
            n : MInt N ->
            m : MInt N ->
184
            Bool
185
186
187
188
189
190
191
192
193
          :=
            N : UNat =>
            n : MInt N =>
            m : MInt N =>
            dk_bool.not (signed_geq N m n).

signed_gt : N : UNat ->
            n : MInt N ->
            m : MInt N ->
194
            Bool
195
196
197
198
199
          :=
            N : UNat =>
            n : MInt N =>
            m : MInt N =>
            dk_bool.not (signed_leq N m n).
200

201
202
(; Casting Peano natural numbers ;)
cast_peano : N : UNat -> n : UNat -> MInt N.
203
204
[ N : UNat ] cast_peano N dk_nat.O --> zero N
[ N : UNat, n : UNat ] cast_peano N (dk_nat.S n) --> succ N (cast_peano N n).
205
206

(; Casting binary natural numbers ;)
207

208
cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
209
[ N : UNat ] cast_bnat N dk_binary_nat.O --> zero N
210
211
[ bn : dk_binary_nat.BNat ] cast_bnat dk_nat.O bn --> O.
[ N : UNat, bn : dk_binary_nat.BNat ]
212
213
214
    cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
      -->
    S0 N (cast_bnat N bn)
215
[ N : UNat, bn : dk_binary_nat.BNat ]
216
217
218
    cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
      -->
    S1 N (cast_bnat N bn).