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

Last change on this file since 275 was 275, checked in by mulligan, 9 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.