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

Last change on this file since 275 was 275, checked in by mulligan, 11 years ago

Removed all axioms from Arithmetic.ma and replaced them with implemented functions from other files. Implemented decidable equality on Nats.

File size: 5.3 KB
Line 
1include "Universes.ma".
2include "Plogic/equality.ma".
3include "Connectives.ma".
4include "Nat.ma".
5include "Exponential.ma".
6include "Bool.ma".
7include "BitVector.ma".
8include "List.ma".
9
10ndefinition one ≝ S Z.
11ndefinition two ≝ (S(S(Z))).
12ndefinition three ≝ two + one.
13ndefinition four ≝ two + two.
14ndefinition five ≝ three + two.
15ndefinition six ≝ three + three.
16ndefinition seven ≝ three + four.
17ndefinition eight ≝ four + four.
18ndefinition nine ≝ five + four.
19ndefinition ten ≝ five + five.
20ndefinition eleven ≝ six + five.
21ndefinition twelve ≝ six + six.
22ndefinition thirteen ≝ seven + six.
23ndefinition fourteen ≝ seven + seven.
24ndefinition fifteen ≝ eight + seven.
25ndefinition sixteen ≝ eight + eight.
26ndefinition seventeen ≝ nine + eight.
27ndefinition eighteen ≝ nine + nine.
28ndefinition nineteen ≝ ten + nine.
29ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
30ndefinition two_hundred_and_fifty_six ≝
31  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                         
32   
33ndefinition nat_of_bool ≝
34  λb: Bool.
35    match b with
36      [ false ⇒ Z
37      | true ⇒ S Z
38      ].
39   
40ndefinition add_n_with_carry:
41      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝
42  λn: Nat.
43  λb: BitVector n.
44  λc: BitVector n.
45  λcarry: Bool.
46    let b_as_nat ≝ nat_of_bitvector n b in
47    let c_as_nat ≝ nat_of_bitvector n c in
48    let carry_as_nat ≝ nat_of_bool carry in
49    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
50    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
51                  (modulus c_as_nat ((S (S Z)) * n)) +
52                  c_as_nat) ≥ ((S (S Z)) * n) in
53    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
54                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
55                  c_as_nat) ≥ ((S (S Z))^(n - (S Z)))) in
56    let result ≝ modulus result_old ((S (S Z))^n) in
57    let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in
58    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
59      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
60                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
61    #H; nassumption;
62nqed.
63
64ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝
65  λb: BitVector eight.
66  λc: BitVector eight.
67  λcarry: Bool.
68    let b_as_nat ≝ nat_of_bitvector eight b in
69    let c_as_nat ≝ nat_of_bitvector eight c in
70    let carry_as_nat ≝ nat_of_bool carry in
71    let temporary ≝ minus (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) in
72    let ac_flag ≝ inclusive_disjunction
73                    (negation (conjunction (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat)))
74                    (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in
75    let bit_six ≝ inclusive_disjunction
76                    (negation (conjunction (less_than_or_equal_b (modulus b_as_nat one_hundred_and_twenty_eight) (modulus c_as_nat one_hundred_and_twenty_eight)) (less_than_or_equal_b temporary carry_as_nat)))
77                    (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in
78    let old_result_1 ≝ b_as_nat - c_as_nat in
79    let old_result_2 ≝ old_result_1 - carry_as_nat in
80    let ov_flag ≝ exclusive_disjunction carry bit_six in
81      match less_than_or_equal_b b_as_nat c_as_nat with
82        [ true ⇒
83          match less_than_or_equal_b old_result_1 carry_as_nat with
84            [ true ⇒
85              let cy_flag ≝ false in
86                mk_Cartesian … (bitvector_of_nat eight old_result_2) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool))
87            | false ⇒
88              let cy_flag ≝ true in
89              let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
90                mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool))
91            ]
92        | false ⇒
93            let cy_flag ≝ true in
94            let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
95              mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool))
96        ].
97   
98ndefinition add_8_with_carry ≝ add_n_with_carry eight.
99ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
100
101ndefinition increment ≝
102  λn: Nat.
103  λb: BitVector n.
104    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
105    let overflow ≝ b_as_nat ≥ (S (S Z))^n in
106      match overflow with
107        [ false ⇒ bitvector_of_nat n b_as_nat
108        | true ⇒ zero n
109        ].
110       
111ndefinition decrement ≝
112  λn: Nat.
113  λb: BitVector n.
114    let b_as_nat ≝ nat_of_bitvector n b in
115      match b_as_nat with
116        [ Z ⇒ max n
117        | S o ⇒ bitvector_of_nat n o
118        ].
119       
120alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
121
122ndefinition bitvector_of_bool:
123      ∀n: Nat. ∀b: Bool. BitVector n ≝
124  λn: Nat.
125  λb: Bool.
126    ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
127  nrewrite > (plus_minus_inverse_right n ?);
128  #H;
129  nassumption;
130nqed.
Note: See TracBrowser for help on using the repository browser.