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

include "Exponential.ma".
include "BitVector.ma".

ndefinition nat_of_bool ≝
  λb: Bool.
    match b with
      [ false ⇒ Z
      | true ⇒ S Z
      ].
    
ndefinition add_n_with_carry:
      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝
  λn: Nat.
  λb: BitVector n.
  λc: BitVector n.
  λcarry: Bool.
    let b_as_nat ≝ nat_of_bitvector n b in
    let c_as_nat ≝ nat_of_bitvector n c in
    let carry_as_nat ≝ nat_of_bool carry in
    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
                  (modulus c_as_nat ((S (S Z)) * n)) +
                  c_as_nat) ≳ ((S (S Z)) * n) in
    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
                  c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in
    let result ≝ modulus result_old ((S (S Z))^n) in
    let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in
    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
    #H; nassumption;
nqed.

ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝
  λb: BitVector eight.
  λc: BitVector eight.
  λcarry: Bool.
    let b_as_nat ≝ nat_of_bitvector eight b in
    let c_as_nat ≝ nat_of_bitvector eight c in
    let carry_as_nat ≝ nat_of_bool carry in
    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
    let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in
    let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≲ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≲ carry_as_nat)) in
    let old_result_1 ≝ b_as_nat - c_as_nat in
    let old_result_2 ≝ old_result_1 - carry_as_nat in
    let ov_flag ≝ exclusive_disjunction carry bit_six in
      match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
        [ false ⇒
           let cy_flag ≝ false in
            〈 bitvector_of_nat eight old_result_2, [cy_flag ; ac_flag ; ov_flag ] 〉
        | true ⇒
           let cy_flag ≝ true in
           let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
            〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ] 〉
        ].
         
ndefinition add_8_with_carry ≝ add_n_with_carry eight.
ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.

ndefinition increment ≝
  λn: Nat.
  λb: BitVector n.
    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
    let overflow ≝ b_as_nat ≳ (S (S Z))^n in
      match overflow with
        [ false ⇒ bitvector_of_nat n b_as_nat
        | true ⇒ zero n
        ].
        
ndefinition decrement ≝
  λn: Nat.
  λb: BitVector n.
    let b_as_nat ≝ nat_of_bitvector n b in
      match b_as_nat with
        [ Z ⇒ max n
        | S o ⇒ bitvector_of_nat n o
        ].
        
alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".

ndefinition bitvector_of_bool:
      ∀n: Nat. ∀b: Bool. BitVector (S n) ≝
  λn: Nat.
  λb: Bool.
    ? (pad (S n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
  nrewrite > plus_minus_inverse_right
   [ napply (λx.x) | /2/]
nqed.

ndefinition full_add ≝
  λn: Nat.
  λb, c: BitVector n.
  λd: Bit.
    fold_right2_i ? ? ? (
      λn.
       λb1, b2: Bool.
        λd: Bit × (BitVector n).
        let 〈c1,r〉 ≝ d in
          〈inclusive_disjunction (conjunction b1 b2)
                                 (conjunction c1 (inclusive_disjunction b1 b2)),
           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     〈d, [[ ]]〉 ? b c.
    
ndefinition half_add ≝
  λn: Nat.
  λb, c: BitVector n.
    full_add n b c false.