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

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

No more axioms but the paralogisms.

File size: 6.9 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 twenty_four ≝ sixteen + eight.
30ndefinition thirty_two ≝ sixteen + sixteen.
31ndefinition one_hundred ≝ ten * ten.
32ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
33ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
34ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
35ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
36ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
37ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
38ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
39ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
40ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
41ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
42ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
43ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
44ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
45ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
46ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
47ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
48ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
49ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
50ndefinition two_hundred ≝ one_hundred + one_hundred.
51ndefinition two_hundred_and_two ≝ two_hundred + two.
52ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
53ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
54ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
55ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
56ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
57ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
58ndefinition two_hundred_and_fifty_six ≝
59  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
60   
61ndefinition nat_of_bool ≝
62  λb: Bool.
63    match b with
64      [ false ⇒ Z
65      | true ⇒ S Z
66      ].
67   
68ndefinition add_n_with_carry:
69      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝
70  λn: Nat.
71  λb: BitVector n.
72  λc: BitVector n.
73  λcarry: Bool.
74    let b_as_nat ≝ nat_of_bitvector n b in
75    let c_as_nat ≝ nat_of_bitvector n c in
76    let carry_as_nat ≝ nat_of_bool carry in
77    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
78    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
79                  (modulus c_as_nat ((S (S Z)) * n)) +
80                  c_as_nat) ≳ ((S (S Z)) * n) in
81    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
82                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
83                  c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in
84    let result ≝ modulus result_old ((S (S Z))^n) in
85    let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in
86    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
87      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
88                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
89    #H; nassumption;
90nqed.
91
92ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝
93  λb: BitVector eight.
94  λc: BitVector eight.
95  λcarry: Bool.
96    let b_as_nat ≝ nat_of_bitvector eight b in
97    let c_as_nat ≝ nat_of_bitvector eight c in
98    let carry_as_nat ≝ nat_of_bool carry in
99    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
100    let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in
101    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
102    let old_result_1 ≝ b_as_nat - c_as_nat in
103    let old_result_2 ≝ old_result_1 - carry_as_nat in
104    let ov_flag ≝ exclusive_disjunction carry bit_six in
105      match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
106        [ false ⇒
107           let cy_flag ≝ false in
108            〈 bitvector_of_nat eight old_result_2, [cy_flag ; ac_flag ; ov_flag ] 〉
109        | true ⇒
110           let cy_flag ≝ true in
111           let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
112            〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ] 〉
113        ].
114         
115ndefinition add_8_with_carry ≝ add_n_with_carry eight.
116ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
117
118ndefinition increment ≝
119  λn: Nat.
120  λb: BitVector n.
121    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
122    let overflow ≝ b_as_nat ≳ (S (S Z))^n in
123      match overflow with
124        [ false ⇒ bitvector_of_nat n b_as_nat
125        | true ⇒ zero n
126        ].
127       
128ndefinition decrement ≝
129  λn: Nat.
130  λb: BitVector n.
131    let b_as_nat ≝ nat_of_bitvector n b in
132      match b_as_nat with
133        [ Z ⇒ max n
134        | S o ⇒ bitvector_of_nat n o
135        ].
136       
137alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
138
139ndefinition bitvector_of_bool:
140      ∀n: Nat. ∀b: Bool. BitVector (S n) ≝
141  λn: Nat.
142  λb: Bool.
143    ? (pad (S n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
144  nrewrite > plus_minus_inverse_right
145   [ napply (λx.x) | /2/]
146nqed.
147
148ndefinition full_add ≝
149  λn: Nat.
150  λb, c: BitVector n.
151  λd: Bit.
152    fold_right2_i ? ? ? (
153      λn.
154       λb1, b2: Bool.
155        λd: Bit × (BitVector n).
156        let 〈c1,r〉 ≝ d in
157          〈inclusive_disjunction (conjunction b1 b2)
158                                 (conjunction c1 (inclusive_disjunction b1 b2)),
159           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
160     〈d, [[ ]]〉 ? b c.
161   
162ndefinition half_add ≝
163  λn: Nat.
164  λb, c: BitVector n.
165    full_add n b c false.
166
Note: See TracBrowser for help on using the repository browser.