source: Deliverables/D4.1/Matita/Arithmetic.ma @ 475

Last change on this file since 475 was 465, checked in by mulligan, 9 years ago

Moved over to standard library.

File size: 6.8 KB
Line 
1include "BitVector.ma".
2include "Util.ma".
3
4ndefinition nat_of_bool ≝
5  λb: bool.
6    match b with
7      [ false ⇒ O
8      | true ⇒ S O
9      ].
10   
11ndefinition add_n_with_carry:
12      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
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 ≝ geb ((modulus b_as_nat (2 * n)) +
22                  (modulus c_as_nat (2 * n)) +
23                  c_as_nat) (2 * n) in
24    let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
25                  (modulus c_as_nat (2^(n - 1))) +
26                  c_as_nat) (2^(n - 1)) in
27    let result ≝ modulus result_old (2^n) in
28    let cy_flag ≝ geb result_old (2^n) in
29    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
30      mk_pair ? ? (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. (BitVector n) × (BitVector 3) ≝
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 (2 * n)) - (c_as_nat mod (2 * n)) in
42     let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
43     let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
44     let 〈b',cy_flag〉 ≝
45       if geb b_as_nat (c_as_nat + carry_as_nat) then
46         〈b_as_nat, false〉
47       else
48         〈b_as_nat + (2^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         
53ndefinition add_8_with_carry ≝ add_n_with_carry 8.
54ndefinition add_16_with_carry ≝ add_n_with_carry 16.
55ndefinition sub_8_with_carry ≝ sub_n_with_carry 8.
56ndefinition sub_16_with_carry ≝ sub_n_with_carry 16.
57
58ndefinition increment ≝
59  λn: nat.
60  λb: BitVector n.
61    let b_as_nat ≝ (nat_of_bitvector n b) + (S O) in
62    let overflow ≝ geb b_as_nat (S (S O))^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        [ O ⇒ 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   
83ndefinition addition_n ≝
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    [ O ⇒ None ?
109    | _ ⇒
110      let result ≝ b_nat ÷ c_nat in
111        Some ? (bitvector_of_nat n result)
112    ].
113     
114ndefinition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
115  λn.
116    match n with
117    [ O ⇒ λb, c. None ?
118    | S p ⇒ λb, c: BitVector (S p).
119        let b_sign_bit ≝ get_index_v ? ? b O ? in
120        let c_sign_bit ≝ get_index_v ? ? c O ? 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        [ O ⇒ None ?
125        | S o ⇒
126          match b_sign_bit with
127          [ true ⇒
128            let temp_b ≝ b_as_nat - (2^p) in
129            match c_sign_bit with
130            [ true ⇒
131              let temp_c ≝ c_as_nat - (2^p) in
132                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
133            | false ⇒
134              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
135                Some ? (bitvector_of_nat ? result)
136            ]
137          | false ⇒
138            match c_sign_bit with
139            [ true ⇒
140              let temp_c ≝ c_as_nat - (2^p) in
141              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
142                Some ? (bitvector_of_nat ? result)
143            | false ⇒ Some ? (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      [ None ⇒ None ?
164      | Some result ⇒
165          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
166            Some ? (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      ltb b_nat c_nat.
175     
176ndefinition gt_u ≝ λn, b, c. lt_u n c b.
177
178ndefinition lte_u ≝ λn, b, c. ¬(gt_u n b c).
179
180ndefinition gte_u ≝ λn, b, c. ¬(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 2 ? in
187     if ov_flag then
188       true
189     else
190       ((match n return λn'.BitVector n' → bool with
191       [ O ⇒ λ_.false
192       | S o ⇒
193         λresult'.(get_index_v ? ? result' O ?)
194       ]) result).
195      //;
196nqed.
197
198ndefinition gt_s ≝ λn,b,c. lt_s n c b.
199
200ndefinition lte_s ≝ λn,b,c. ¬(gt_s n b c).
201
202ndefinition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
203     
204alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
205
206ndefinition bitvector_of_bool:
207      ∀n: nat. ∀b: bool. BitVector (S n) ≝
208  λn: nat.
209  λb: bool.
210   (pad (S n - (S O)) (S O) [[b]])⌈(S n - (S O)) + S O ↦ S n⌉.
211 /2/.
212nqed.
213
214ndefinition full_add ≝
215  λn: nat.
216  λb, c: BitVector n.
217  λd: Bit.
218    fold_right2_i ? ? ? (
219      λn.
220       λb1, b2: bool.
221        λd: Bit × (BitVector n).
222        let 〈c1,r〉 ≝ d in
223          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
224           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
225     〈d, [[ ]]〉 ? b c.
226   
227ndefinition half_add ≝
228  λn: nat.
229  λb, c: BitVector n.
230    full_add n b c false.
Note: See TracBrowser for help on using the repository browser.