Changeset 465 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r462 r465 1 include "Exponential.ma".2 1 include "BitVector.ma". 2 include "Util.ma". 3 3 4 4 ndefinition nat_of_bool ≝ 5 λb: Bool.5 λb: bool. 6 6 match b with 7 [ false ⇒ Z8  true ⇒ S Z7 [ false ⇒ O 8  true ⇒ S O 9 9 ]. 10 10 11 11 ndefinition add_n_with_carry: 12 ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝13 λn: Nat.12 ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝ 13 λn: nat. 14 14 λb: BitVector n. 15 15 λc: BitVector n. 16 λcarry: Bool.16 λcarry: bool. 17 17 let b_as_nat ≝ nat_of_bitvector n b in 18 18 let c_as_nat ≝ nat_of_bitvector n c in 19 19 let carry_as_nat ≝ nat_of_bool carry in 20 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) in24 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)))) in27 let result ≝ modulus result_old ( (S (S Z))^n) in28 let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in21 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 29 let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in 30 mk_ Cartesian? ? (bitvector_of_nat n result)30 mk_pair ? ? (bitvector_of_nat n result) 31 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 32 32 33 ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝34 λn: Nat.33 ndefinition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝ 34 λn: nat. 35 35 λb: BitVector n. 36 36 λc: BitVector n. 37 λcarry: Bool.37 λcarry: bool. 38 38 let b_as_nat ≝ nat_of_bitvector n b in 39 39 let c_as_nat ≝ nat_of_bitvector n c in 40 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)) in42 let ac_flag ≝ l ess_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two* n)) + carry_as_nat) in43 let bit_six ≝ l ess_than_b (b_as_nat mod (two^(n  one))) ((c_as_nat mod (two^(n  one))) + carry_as_nat) in41 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 44 let 〈b',cy_flag〉 ≝ 45 if g reater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then45 if geb b_as_nat (c_as_nat + carry_as_nat) then 46 46 〈b_as_nat, false〉 47 47 else 48 〈b_as_nat + ( two^n), true〉48 〈b_as_nat + (2^n), true〉 49 49 in 50 50 let ov_flag ≝ exclusive_disjunction cy_flag bit_six in 51 51 〈bitvector_of_nat n ((b'  c_as_nat)  carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉. 52 52 53 ndefinition add_8_with_carry ≝ add_n_with_carry eight.54 ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.55 ndefinition sub_8_with_carry ≝ sub_n_with_carry eight.56 ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen.53 ndefinition add_8_with_carry ≝ add_n_with_carry 8. 54 ndefinition add_16_with_carry ≝ add_n_with_carry 16. 55 ndefinition sub_8_with_carry ≝ sub_n_with_carry 8. 56 ndefinition sub_16_with_carry ≝ sub_n_with_carry 16. 57 57 58 58 ndefinition increment ≝ 59 λn: Nat.60 λb: BitVector n. 61 let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in62 let overflow ≝ b_as_nat ≳ (S (S Z))^n in59 λ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 63 match overflow with 64 64 [ false ⇒ bitvector_of_nat n b_as_nat … … 67 67 68 68 ndefinition decrement ≝ 69 λn: Nat.69 λn: nat. 70 70 λb: BitVector n. 71 71 let b_as_nat ≝ nat_of_bitvector n b in 72 72 match b_as_nat with 73 [ Z⇒ max n73 [ O ⇒ max n 74 74  S o ⇒ bitvector_of_nat n o 75 75 ]. 76 76 77 77 ndefinition two_complement_negation ≝ 78 λn: Nat.78 λn: nat. 79 79 λb: BitVector n. 80 80 let new_b ≝ negation_bv n b in … … 82 82 83 83 ndefinition addition_n ≝ 84 λn: Nat.84 λn: nat. 85 85 λb, c: BitVector n. 86 86 let 〈res,flags〉 ≝ add_n_with_carry n b c false in … … 88 88 89 89 ndefinition subtraction ≝ 90 λn: Nat.90 λn: nat. 91 91 λb, c: BitVector n. 92 92 addition_n n b (two_complement_negation n c). 93 93 94 94 ndefinition multiplication ≝ 95 λn: Nat.95 λn: nat. 96 96 λb, c: BitVector n. 97 97 let b_nat ≝ nat_of_bitvector ? b in … … 101 101 102 102 ndefinition division_u ≝ 103 λn: Nat.103 λn: nat. 104 104 λb, c: BitVector n. 105 105 let b_nat ≝ nat_of_bitvector ? b in 106 106 let c_nat ≝ nat_of_bitvector ? c in 107 107 match c_nat with 108 [ Z ⇒ Nothing?108 [ O ⇒ None ? 109 109  _ ⇒ 110 110 let result ≝ b_nat ÷ c_nat in 111 Just? (bitvector_of_nat n result)111 Some ? (bitvector_of_nat n result) 112 112 ]. 113 113 114 ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe(BitVector n) ≝114 ndefinition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ 115 115 λn. 116 116 match n with 117 [ Z ⇒ λb, c. Nothing?117 [ O ⇒ λb, c. None ? 118 118  S p ⇒ λb, c: BitVector (S p). 119 let b_sign_bit ≝ get_index_v ? ? b Z? in120 let c_sign_bit ≝ get_index_v ? ? c Z? in119 let b_sign_bit ≝ get_index_v ? ? b O ? in 120 let c_sign_bit ≝ get_index_v ? ? c O ? in 121 121 let b_as_nat ≝ nat_of_bitvector ? b in 122 122 let c_as_nat ≝ nat_of_bitvector ? c in 123 123 match c_as_nat with 124 [ Z ⇒ Nothing?124 [ O ⇒ None ? 125 125  S o ⇒ 126 126 match b_sign_bit with 127 127 [ true ⇒ 128 let temp_b ≝ (b_as_nat  (two^((S p)one))) in128 let temp_b ≝ b_as_nat  (2^p) in 129 129 match c_sign_bit with 130 130 [ true ⇒ 131 let temp_c ≝ (c_as_nat  (two^((S p)one))) in132 Just? (bitvector_of_nat ? (temp_b ÷ temp_c))131 let temp_c ≝ c_as_nat  (2^p) in 132 Some ? (bitvector_of_nat ? (temp_b ÷ temp_c)) 133 133  false ⇒ 134 let result ≝ (temp_b ÷ c_as_nat) + ( two^((S p)one)) in135 Just? (bitvector_of_nat ? result)134 let result ≝ (temp_b ÷ c_as_nat) + (2^p) in 135 Some ? (bitvector_of_nat ? result) 136 136 ] 137 137  false ⇒ 138 138 match c_sign_bit with 139 139 [ true ⇒ 140 let temp_c ≝ (c_as_nat  (two^((S p)one))) in141 let result ≝ (b_as_nat ÷ temp_c) + ( two^((S p)one)) in142 Just? (bitvector_of_nat ? result)143  false ⇒ Just? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))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 144 ] 145 145 ] … … 161 161 λb, c: BitVector n. 162 162 match division_s n b c with 163 [ No thing ⇒ Nothing?164  Justresult ⇒165 let 〈high_bits, low_bits〉 ≝ split Bool ? n (multiplication n result c) in166 Just? (subtraction n b low_bits)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 167 ]. 168 168 … … 172 172 let b_nat ≝ nat_of_bitvector ? b in 173 173 let c_nat ≝ nat_of_bitvector ? c in 174 l ess_than_b b_nat c_nat.174 ltb b_nat c_nat. 175 175 176 176 ndefinition gt_u ≝ λn, b, c. lt_u n c b. 177 177 178 ndefinition lte_u ≝ λn, b, c. negation(gt_u n b c).179 180 ndefinition gte_u ≝ λn, b, c. negation(lt_u n b c).178 ndefinition lte_u ≝ λn, b, c. ¬(gt_u n b c). 179 180 ndefinition gte_u ≝ λn, b, c. ¬(lt_u n b c). 181 181 182 182 ndefinition lt_s ≝ … … 184 184 λb, c: BitVector n. 185 185 let 〈result, flags〉 ≝ sub_n_with_carry n b c false in 186 let ov_flag ≝ get_index_v ? ? flags two? in186 let ov_flag ≝ get_index_v ? ? flags 2 ? in 187 187 if ov_flag then 188 188 true 189 189 else 190 ((match n return λn'.BitVector n' → Bool with191 [ Z⇒ λ_.false190 ((match n return λn'.BitVector n' → bool with 191 [ O ⇒ λ_.false 192 192  S o ⇒ 193 λresult'.(get_index_v ? ? result' Z?)193 λresult'.(get_index_v ? ? result' O ?) 194 194 ]) result). 195 195 //; … … 198 198 ndefinition gt_s ≝ λn,b,c. lt_s n c b. 199 199 200 ndefinition lte_s ≝ λn,b,c. negation (gt_s n b c). 201 202 ndefinition gte_s ≝ λn. λb, c. 203 negation (lt_s n b c). 204 205 alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop". 200 ndefinition lte_s ≝ λn,b,c. ¬(gt_s n b c). 201 202 ndefinition gte_s ≝ λn. λb, c. ¬(lt_s n b c). 203 204 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". 206 205 207 206 ndefinition 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⌉.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⌉. 212 211 /2/. 213 212 nqed. 214 213 215 214 ndefinition full_add ≝ 216 λn: Nat.215 λn: nat. 217 216 λb, c: BitVector n. 218 217 λd: Bit. 219 218 fold_right2_i ? ? ? ( 220 219 λn. 221 λb1, b2: Bool.220 λb1, b2: bool. 222 221 λd: Bit × (BitVector n). 223 222 let 〈c1,r〉 ≝ d in 224 〈inclusive_disjunction (conjunction b1 b2) 225 (conjunction c1 (inclusive_disjunction b1 b2)), 223 〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)), 226 224 (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) 227 225 〈d, [[ ]]〉 ? b c. 228 226 229 227 ndefinition half_add ≝ 230 λn: Nat.228 λn: nat. 231 229 λb, c: BitVector n. 232 230 full_add n b c false.
Note: See TracChangeset
for help on using the changeset viewer.