Changeset 234 for Deliverables/D4.1/Matita/Nat.ma
- Timestamp:
- Nov 12, 2010, 2:27:56 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Nat.ma
r233 r234 1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 2 (* Nat.ma: Natural numbers and common arithmetical functions. *) 3 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 1 4 include "Cartesian.ma". 2 5 include "Maybe.ma". … … 7 10 include "Plogic/connectives.ma". 8 11 12 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 13 (* The datatype. *) 14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 9 15 ninductive Nat: Type[0] ≝ 10 16 Z: Nat 11 17 | S: Nat → Nat. 12 18 19 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 20 (* Orderings. *) 21 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 22 23 ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝ 24 ltoe_refl: less_than_or_equal_p n n 25 | ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m). 26 27 nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝ 28 match m with 29 [ Z ⇒ True 30 | S o ⇒ 31 match n with 32 [ Z ⇒ False 33 | S p ⇒ less_than_or_equal_b o p 34 ] 35 ]. 36 37 notation "n break ≤ m" 38 non associative with precedence 47 39 for @{ 'less_than_or_equal $n $m }. 40 41 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). 42 interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). 43 44 ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ 45 λm, n: Nat. 46 n ≤ m. 47 48 ndefinition greater_than_or_equal_b ≝ 49 λm, n: Nat. 50 n ≤ m. 51 52 notation "n break ≥ m" 53 non associative with precedence 47 54 for @{ 'greater_than_or_equal $n $m }. 55 56 57 interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). 58 interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). 59 60 (* Add Boolean versions. *) 61 ndefinition less_than_p ≝ 62 λm, n: Nat. 63 m ≤ n ∧ ¬(m = n). 64 65 notation "n break < m" 66 non associative with precedence 47 67 for @{ 'less_than $n $m }. 68 69 interpretation "Nat less than prop" 'less_than n m = (less_than_p n m). 70 71 ndefinition greater_than_p ≝ 72 λm, n: Nat. 73 n < m. 74 75 notation "n break > m" 76 non associative with precedence 47 77 for @{ 'greater_than $n $m }. 78 79 interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m). 80 81 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 82 (* Addition and subtraction. *) 83 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 13 84 nlet rec plus (n: Nat) (o: Nat) on n ≝ 14 85 match n with … … 38 109 39 110 interpretation "Nat minus" 'minus n m = (minus n m). 111 112 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 113 (* Multiplication, modulus and division. *) 114 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 40 115 41 116 nlet rec multiplication (n: Nat) (o: Nat) on n ≝ … … 51 126 interpretation "Nat multiplication" 'times n m = (multiplication n m). 52 127 53 ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝ 54 ltoe_refl: less_than_or_equal_p n n 55 | ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m). 56 57 nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m ≝ 58 match m with 59 [ Z ⇒ True 60 | S o ⇒ 61 match n with 62 [ Z ⇒ False 63 | S p ⇒ less_than_or_equal_b o p 128 nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ 129 match n ≤ p with 130 [ True ⇒ Z 131 | False ⇒ 132 match m with 133 [ Z ⇒ Z 134 | (S q) ⇒ S (division_aux q (n - (S p)) p) 64 135 ] 65 136 ]. 66 137 67 notation "n break ≤ m" 68 non associative with precedence 47 69 for @{ 'less_than_or_equal $n $m }. 70 71 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). 72 interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). 73 74 ndefinition less_than_p ≝ 75 λm, n: Nat. 76 m ≤ n ∧ ¬(m = n). 77 78 notation "n break < m" 79 non associative with precedence 47 80 for @{ 'less_than $n $m }. 81 82 interpretation "Nat less than prop" 'less_than n m = (less_than_p n m). 83 84 (* 85 nlet rec greatest_common_divisor (m: Nat) (n: Nat) on n ≝ 86 match n with 87 [ Z ⇒ m 88 | S o ⇒ greatest_common_divisor n (modulus m n) 89 ]. 90 *) 138 ndefinition division ≝ 139 λm, n: Nat. 140 match n with 141 [ Z ⇒ S m 142 | S o ⇒ division_aux m m o 143 ]. 144 145 notation "n break ÷ m" 146 right associative with precedence 47 147 for @{ 'division $n $m }. 148 149 interpretation "Nat division" 'division n m = (division n m). 150 151 nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ 152 match n ≤ p with 153 [ True ⇒ n 154 | False ⇒ 155 match m with 156 [ Z ⇒ n 157 | S o ⇒ modulus_aux o (n - (S p)) p 158 ] 159 ]. 160 161 ndefinition modulus ≝ 162 λm, n: Nat. 163 match n with 164 [ Z ⇒ m 165 | S o ⇒ modulus_aux m m o 166 ]. 167 168 notation "n break % m" 169 right associative with precedence 47 170 for @{ 'modulus $n $m }. 171 172 interpretation "Nat modulus" 'modulus m n = (modulus m n). 173 174 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 175 (* Greatest common divisor and least common multiple. *) 176 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 177 178 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 179 (* Lemmas. *) 180 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 91 181 92 182 nlemma less_than_or_equal_zero: … … 97 187 //. 98 188 #N. 99 //.189 napply ltoe_step. 100 190 nqed. 101 191
Note: See TracChangeset
for help on using the changeset viewer.