# source:Deliverables/D4.1/Matita/Arithmetic.ma@462

Last change on this file since 462 was 462, checked in by mulligan, 10 years ago

File size: 7.2 KB
Line
1include "Exponential.ma".
2include "BitVector.ma".
3
4ndefinition nat_of_bool ≝
5  λb: Bool.
6    match b with
7      [ false ⇒ Z
8      | true ⇒ S Z
9      ].
10
12      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
13  λn: Nat.
14  λb: BitVector n.
15  λc: BitVector n.
16  λcarry: Bool.
17    let b_as_nat ≝ nat_of_bitvector n b in
18    let c_as_nat ≝ nat_of_bitvector n c in
19    let carry_as_nat ≝ nat_of_bool carry in
20    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
21    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
22                  (modulus c_as_nat ((S (S Z)) * n)) +
23                  c_as_nat) ≳ ((S (S Z)) * n) in
24    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
25                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
26                  c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in
27    let result ≝ modulus result_old ((S (S Z))^n) in
28    let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in
29    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
30      mk_Cartesian ? ? (bitvector_of_nat n result)
31                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
32
33ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
34  λn: Nat.
35  λb: BitVector n.
36  λc: BitVector n.
37  λcarry: Bool.
38     let b_as_nat ≝ nat_of_bitvector n b in
39     let c_as_nat ≝ nat_of_bitvector n c in
40     let carry_as_nat ≝ nat_of_bool carry in
41     let temporary ≝ (b_as_nat mod (two * n)) - (c_as_nat mod (two * n)) in
42     let ac_flag ≝ less_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two * n)) + carry_as_nat) in
43     let bit_six ≝ less_than_b (b_as_nat mod (two^(n - one))) ((c_as_nat mod (two^(n - one))) + carry_as_nat) in
44     let 〈b',cy_flag〉 ≝
45       if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then
46         〈b_as_nat, false〉
47       else
48         〈b_as_nat + (two^n), true〉
49     in
50       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
51         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.
52
55ndefinition sub_8_with_carry ≝ sub_n_with_carry eight.
56ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen.
57
58ndefinition increment ≝
59  λn: Nat.
60  λb: BitVector n.
61    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
62    let overflow ≝ b_as_nat ≳ (S (S Z))^n in
63      match overflow with
64        [ false ⇒ bitvector_of_nat n b_as_nat
65        | true ⇒ zero n
66        ].
67
68ndefinition decrement ≝
69  λn: Nat.
70  λb: BitVector n.
71    let b_as_nat ≝ nat_of_bitvector n b in
72      match b_as_nat with
73        [ Z ⇒ max n
74        | S o ⇒ bitvector_of_nat n o
75        ].
76
77ndefinition two_complement_negation ≝
78  λn: Nat.
79  λb: BitVector n.
80    let new_b ≝ negation_bv n b in
81      increment n new_b.
82
84  λn: Nat.
85  λb, c: BitVector n.
86    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
87      res.
88
89ndefinition subtraction ≝
90  λn: Nat.
91  λb, c: BitVector n.
92    addition_n n b (two_complement_negation n c).
93
94ndefinition multiplication ≝
95  λn: Nat.
96  λb, c: BitVector n.
97    let b_nat ≝ nat_of_bitvector ? b in
98    let c_nat ≝ nat_of_bitvector ? c in
99    let result ≝ b_nat * c_nat in
100      bitvector_of_nat (n + n) result.
101
102ndefinition division_u ≝
103  λn: Nat.
104  λb, c: BitVector n.
105    let b_nat ≝ nat_of_bitvector ? b in
106    let c_nat ≝ nat_of_bitvector ? c in
107    match c_nat with
108    [ Z ⇒ Nothing ?
109    | _ ⇒
110      let result ≝ b_nat ÷ c_nat in
111        Just ? (bitvector_of_nat n result)
112    ].
113
114ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe (BitVector n) ≝
115  λn.
116    match n with
117    [ Z ⇒ λb, c. Nothing ?
118    | S p ⇒ λb, c: BitVector (S p).
119        let b_sign_bit ≝ get_index_v ? ? b Z ? in
120        let c_sign_bit ≝ get_index_v ? ? c Z ? in
121        let b_as_nat ≝ nat_of_bitvector ? b in
122        let c_as_nat ≝ nat_of_bitvector ? c in
123        match c_as_nat with
124        [ Z ⇒ Nothing ?
125        | S o ⇒
126          match b_sign_bit with
127          [ true ⇒
128            let temp_b ≝ (b_as_nat - (two^((S p)-one))) in
129            match c_sign_bit with
130            [ true ⇒
131              let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
132                Just ? (bitvector_of_nat ? (temp_b ÷ temp_c))
133            | false ⇒
134              let result ≝ (temp_b ÷ c_as_nat) + (two^((S p)-one)) in
135                Just ? (bitvector_of_nat ? result)
136            ]
137          | false ⇒
138            match c_sign_bit with
139            [ true ⇒
140              let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
141              let result ≝ (b_as_nat ÷ temp_c) + (two^((S p)-one)) in
142                Just ? (bitvector_of_nat ? result)
143            | false ⇒ Just ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
144            ]
145          ]
146        ]
147    ].
148    //;
149nqed.
150
151ndefinition modulus_u ≝
152  λn.
153  λb, c: BitVector n.
154    let b_nat ≝ nat_of_bitvector ? b in
155    let c_nat ≝ nat_of_bitvector ? c in
156    let result ≝ modulus b_nat c_nat in
157      bitvector_of_nat (n + n) result.
158
159ndefinition modulus_s ≝
160  λn.
161  λb, c: BitVector n.
162    match division_s n b c with
163      [ Nothing ⇒ Nothing ?
164      | Just result ⇒
165          let 〈high_bits, low_bits〉 ≝ split Bool ? n (multiplication n result c) in
166            Just ? (subtraction n b low_bits)
167      ].
168
169ndefinition lt_u ≝
170  λn.
171  λb, c: BitVector n.
172    let b_nat ≝ nat_of_bitvector ? b in
173    let c_nat ≝ nat_of_bitvector ? c in
174      less_than_b b_nat c_nat.
175
176ndefinition gt_u ≝ λn, b, c. lt_u n c b.
177
178ndefinition lte_u ≝ λn, b, c. negation (gt_u n b c).
179
180ndefinition gte_u ≝ λn, b, c. negation (lt_u n b c).
181
182ndefinition lt_s ≝
183  λn.
184  λb, c: BitVector n.
185    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
186    let ov_flag ≝ get_index_v ? ? flags two ? in
187     if ov_flag then
188       true
189     else
190       ((match n return λn'.BitVector n' → Bool with
191       [ Z ⇒ λ_.false
192       | S o ⇒
193         λresult'.(get_index_v ? ? result' Z ?)
194       ]) result).
195      //;
196nqed.
197
198ndefinition gt_s ≝ λn,b,c. lt_s n c b.
199
200ndefinition lte_s ≝ λn,b,c. negation (gt_s n b c).
201
202ndefinition gte_s ≝ λn. λb, c.
203  negation (lt_s n b c).
204
205alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
206
207ndefinition bitvector_of_bool:
208      ∀n: Nat. ∀b: Bool. BitVector (S n) ≝
209  λn: Nat.
210  λb: Bool.
211   (pad (S n - (S Z)) (S Z) [[b]])⌈(S n - (S Z)) + S Z ↦ S n⌉.
212 /2/.
213nqed.
214
216  λn: Nat.
217  λb, c: BitVector n.
218  λd: Bit.
219    fold_right2_i ? ? ? (
220      λn.
221       λb1, b2: Bool.
222        λd: Bit × (BitVector n).
223        let 〈c1,r〉 ≝ d in
224          〈inclusive_disjunction (conjunction b1 b2)
225                                 (conjunction c1 (inclusive_disjunction b1 b2)),
226           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
227     〈d, [[ ]]〉 ? b c.
228