Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (10 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r462 r465  
    1 include "Exponential.ma".
    21include "BitVector.ma".
     2include "Util.ma".
    33
    44ndefinition nat_of_bool ≝
    5   λb: Bool.
     5  λb: bool.
    66    match b with
    7       [ false ⇒ Z
    8       | true ⇒ S Z
     7      [ false ⇒ O
     8      | true ⇒ S O
    99      ].
    1010   
    1111ndefinition 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.
    1414  λb: BitVector n.
    1515  λc: BitVector n.
    16   λcarry: Bool.
     16  λcarry: bool.
    1717    let b_as_nat ≝ nat_of_bitvector n b in
    1818    let c_as_nat ≝ nat_of_bitvector n c in
    1919    let carry_as_nat ≝ nat_of_bool carry in
    2020    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
     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
    2929    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)
    3131                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3232
    33 ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
    34   λn: Nat.
     33ndefinition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     34  λn: nat.
    3535  λb: BitVector n.
    3636  λc: BitVector n.
    37   λcarry: Bool.
     37  λcarry: bool.
    3838     let b_as_nat ≝ nat_of_bitvector n b in
    3939     let c_as_nat ≝ nat_of_bitvector n c in
    4040     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
     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
    4444     let 〈b',cy_flag〉 ≝
    45        if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then
     45       if geb b_as_nat (c_as_nat + carry_as_nat) then
    4646         〈b_as_nat, false〉
    4747       else
    48          〈b_as_nat + (two^n), true〉
     48         〈b_as_nat + (2^n), true〉
    4949     in
    5050       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
    5151         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.         
    5252         
    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.
     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.
    5757
    5858ndefinition 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
     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
    6363      match overflow with
    6464        [ false ⇒ bitvector_of_nat n b_as_nat
     
    6767       
    6868ndefinition decrement ≝
    69   λn: Nat.
     69  λn: nat.
    7070  λb: BitVector n.
    7171    let b_as_nat ≝ nat_of_bitvector n b in
    7272      match b_as_nat with
    73         [ Z ⇒ max n
     73        [ O ⇒ max n
    7474        | S o ⇒ bitvector_of_nat n o
    7575        ].
    7676   
    7777ndefinition two_complement_negation ≝
    78   λn: Nat.
     78  λn: nat.
    7979  λb: BitVector n.
    8080    let new_b ≝ negation_bv n b in
     
    8282   
    8383ndefinition addition_n ≝
    84   λn: Nat.
     84  λn: nat.
    8585  λb, c: BitVector n.
    8686    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
     
    8888   
    8989ndefinition subtraction ≝
    90   λn: Nat.
     90  λn: nat.
    9191  λb, c: BitVector n.
    9292    addition_n n b (two_complement_negation n c).
    9393   
    9494ndefinition multiplication ≝
    95   λn: Nat.
     95  λn: nat.
    9696  λb, c: BitVector n.
    9797    let b_nat ≝ nat_of_bitvector ? b in
     
    101101     
    102102ndefinition division_u ≝
    103   λn: Nat.
     103  λn: nat.
    104104  λb, c: BitVector n.
    105105    let b_nat ≝ nat_of_bitvector ? b in
    106106    let c_nat ≝ nat_of_bitvector ? c in
    107107    match c_nat with
    108     [ Z ⇒ Nothing ?
     108    [ O ⇒ None ?
    109109    | _ ⇒
    110110      let result ≝ b_nat ÷ c_nat in
    111         Just ? (bitvector_of_nat n result)
     111        Some ? (bitvector_of_nat n result)
    112112    ].
    113113     
    114 ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe (BitVector n) ≝
     114ndefinition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
    115115  λn.
    116116    match n with
    117     [ Z ⇒ λb, c. Nothing ?
     117    [ O ⇒ λb, c. None ?
    118118    | 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
     119        let b_sign_bit ≝ get_index_v ? ? b O ? in
     120        let c_sign_bit ≝ get_index_v ? ? c O ? in
    121121        let b_as_nat ≝ nat_of_bitvector ? b in
    122122        let c_as_nat ≝ nat_of_bitvector ? c in
    123123        match c_as_nat with
    124         [ Z ⇒ Nothing ?
     124        [ O ⇒ None ?
    125125        | S o ⇒
    126126          match b_sign_bit with
    127127          [ true ⇒
    128             let temp_b ≝ (b_as_nat - (two^((S p)-one))) in
     128            let temp_b ≝ b_as_nat - (2^p) in
    129129            match c_sign_bit with
    130130            [ true ⇒
    131               let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
    132                 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))
    133133            | false ⇒
    134               let result ≝ (temp_b ÷ c_as_nat) + (two^((S p)-one)) in
    135                 Just ? (bitvector_of_nat ? result)
     134              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
     135                Some ? (bitvector_of_nat ? result)
    136136            ]
    137137          | false ⇒
    138138            match c_sign_bit with
    139139            [ 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))
     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))
    144144            ]
    145145          ]
     
    161161  λb, c: BitVector n.
    162162    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)
     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)
    167167      ].
    168168     
     
    172172    let b_nat ≝ nat_of_bitvector ? b in
    173173    let c_nat ≝ nat_of_bitvector ? c in
    174       less_than_b b_nat c_nat.
     174      ltb b_nat c_nat.
    175175     
    176176ndefinition gt_u ≝ λn, b, c. lt_u n c b.
    177177
    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).
     178ndefinition lte_u ≝ λn, b, c. ¬(gt_u n b c).
     179
     180ndefinition gte_u ≝ λn, b, c. ¬(lt_u n b c).
    181181     
    182182ndefinition lt_s ≝
     
    184184  λb, c: BitVector n.
    185185    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
    186     let ov_flag ≝ get_index_v ? ? flags two ? in
     186    let ov_flag ≝ get_index_v ? ? flags 2 ? in
    187187     if ov_flag then
    188188       true
    189189     else
    190        ((match n return λn'.BitVector n' → Bool with
    191        [ Z ⇒ λ_.false
     190       ((match n return λn'.BitVector n' → bool with
     191       [ O ⇒ λ_.false
    192192       | S o ⇒
    193          λresult'.(get_index_v ? ? result' Z ?)
     193         λresult'.(get_index_v ? ? result' O ?)
    194194       ]) result).
    195195      //;
     
    198198ndefinition gt_s ≝ λn,b,c. lt_s n c b.
    199199
    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".
     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".
    206205
    207206ndefinition 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⌉.
    212211 /2/.
    213212nqed.
    214213
    215214ndefinition full_add ≝
    216   λn: Nat.
     215  λn: nat.
    217216  λb, c: BitVector n.
    218217  λd: Bit.
    219218    fold_right2_i ? ? ? (
    220219      λn.
    221        λb1, b2: Bool.
     220       λb1, b2: bool.
    222221        λd: Bit × (BitVector n).
    223222        let 〈c1,r〉 ≝ d in
    224           〈inclusive_disjunction (conjunction b1 b2)
    225                                  (conjunction c1 (inclusive_disjunction b1 b2)),
     223          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
    226224           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
    227225     〈d, [[ ]]〉 ? b c.
    228226   
    229227ndefinition half_add ≝
    230   λn: Nat.
     228  λn: nat.
    231229  λb, c: BitVector n.
    232230    full_add n b c false.
Note: See TracChangeset for help on using the changeset viewer.