[3] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "datatypes/sums.ma". |
---|
| 16 | include "datatypes/list.ma". |
---|
| 17 | include "Plogic/equality.ma". |
---|
[10] | 18 | include "binary/Z.ma". |
---|
| 19 | include "binary/positive.ma". |
---|
[3] | 20 | |
---|
| 21 | nlemma eq_rect_Type0_r: |
---|
| 22 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
| 23 | #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption. |
---|
| 24 | nqed. |
---|
| 25 | |
---|
| 26 | nlemma eq_rect_r2: |
---|
| 27 | ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. |
---|
| 28 | #A; #a; #x; #p; ncases p; #P; #H; nassumption. |
---|
| 29 | nqed. |
---|
| 30 | |
---|
| 31 | nlemma eq_rect_Type2_r: |
---|
| 32 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
| 33 | #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption. |
---|
| 34 | nqed. |
---|
| 35 | |
---|
| 36 | nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x. |
---|
| 37 | #A;#x;#y;*;#H;napply nmk;#H';/2/; |
---|
| 38 | nqed. |
---|
| 39 | |
---|
| 40 | (* stolen from logic/connectives.ma to give Prop version. *) |
---|
| 41 | notation > "hvbox(a break \liff b)" |
---|
| 42 | left associative with precedence 25 |
---|
| 43 | for @{ 'iff $a $b }. |
---|
| 44 | |
---|
| 45 | notation "hvbox(a break \leftrightarrow b)" |
---|
| 46 | left associative with precedence 25 |
---|
| 47 | for @{ 'iff $a $b }. |
---|
| 48 | |
---|
| 49 | interpretation "logical iff" 'iff x y = (iff x y). |
---|
| 50 | |
---|
| 51 | (* bool *) |
---|
| 52 | |
---|
| 53 | ndefinition xorb : bool → bool → bool ≝ |
---|
| 54 | λx,y. match x with [ false ⇒ y | true ⇒ notb y ]. |
---|
| 55 | |
---|
| 56 | |
---|
| 57 | (* TODO: move to Z.ma *) |
---|
| 58 | |
---|
| 59 | nlemma eqZb_z_z : ∀z.eqZb z z = true. |
---|
| 60 | #z;ncases z;nnormalize;//; |
---|
| 61 | nqed. |
---|
| 62 | |
---|
| 63 | (* XXX: divides goes to arithmetics *) |
---|
[10] | 64 | ninductive dividesP (n,m:Pos) : Prop ≝ |
---|
| 65 | | witness : ∀p:Pos.m = times n p → dividesP n m. |
---|
| 66 | interpretation "positive divides" 'divides n m = (dividesP n m). |
---|
| 67 | interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)). |
---|
[3] | 68 | |
---|
[10] | 69 | ndefinition dividesZ : Z → Z → Prop ≝ |
---|
| 70 | λx,y. match x with |
---|
| 71 | [ OZ ⇒ False |
---|
| 72 | | pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] |
---|
| 73 | | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] |
---|
| 74 | ]. |
---|
| 75 | |
---|
[3] | 76 | interpretation "integer divides" 'divides n m = (dividesZ n m). |
---|
| 77 | interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)). |
---|
| 78 | |
---|
| 79 | (* should be proved in nat.ma, but it's not! *) |
---|
[10] | 80 | naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
[3] | 81 | |
---|
[10] | 82 | nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
| 83 | #n m; napply eqb_elim; //; nqed. |
---|
| 84 | |
---|
[3] | 85 | nlemma injective_Z_of_nat : injective ? ? Z_of_nat. |
---|
| 86 | nnormalize; |
---|
| 87 | #n;#m;ncases n;ncases m;nnormalize;//; |
---|
| 88 | ##[ ##1,2: #n';#H;ndestruct |
---|
[10] | 89 | ##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); // |
---|
[3] | 90 | ##] nqed. |
---|
| 91 | |
---|
| 92 | nlemma reflexive_Zle : reflexive ? Zle. |
---|
| 93 | #x; ncases x; //; nqed. |
---|
| 94 | |
---|
| 95 | nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n). |
---|
| 96 | #n;ncases n;nnormalize;//;nqed. |
---|
| 97 | |
---|
| 98 | nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x. |
---|
| 99 | #x; ncases x; //; |
---|
| 100 | #n; ncases n; //; nqed. |
---|
| 101 | |
---|
| 102 | nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. |
---|
| 103 | #x;#y; |
---|
[10] | 104 | napply pos_elim |
---|
| 105 | ##[ ##2: #n'; #IH; ##] |
---|
[3] | 106 | nrewrite > (Zplus_Zsucc_Zpred y ?); |
---|
[10] | 107 | ##[ nrewrite > (Zpred_Zsucc (pos n')); |
---|
| 108 | #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??); |
---|
[3] | 109 | napply Zsucc_le; |
---|
| 110 | ##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le; |
---|
| 111 | ##] nqed. |
---|
| 112 | |
---|
| 113 | (* XXX: Zmax must go to arithmetics *) |
---|
| 114 | ndefinition Zmax : Z → Z → Z ≝ |
---|
| 115 | λx,y.match Z_compare x y with |
---|
| 116 | [ LT ⇒ y |
---|
| 117 | | _ ⇒ x ]. |
---|
| 118 | |
---|
| 119 | nlemma Zmax_l: ∀x,y. x ≤ Zmax x y. |
---|
| 120 | #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y); |
---|
| 121 | /3/; nqed. |
---|
| 122 | |
---|
| 123 | nlemma Zmax_r: ∀x,y. y ≤ Zmax x y. |
---|
| 124 | #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y); |
---|
| 125 | /3/; #H; nrewrite > H; //; nqed. |
---|
| 126 | |
---|
[10] | 127 | ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. |
---|
| 128 | #x y; ncases x; |
---|
| 129 | ##[ ncases y; |
---|
| 130 | ##[ ##1,2: // |
---|
| 131 | ##| #n; napply False_ind; |
---|
| 132 | ##] |
---|
| 133 | ##| #n; ncases y; |
---|
| 134 | ##[ nnormalize; napply False_ind; |
---|
| 135 | ##| #m; napply (pos_cases … n); /2/; |
---|
| 136 | ##| #m; nnormalize; napply False_ind; |
---|
| 137 | ##] |
---|
| 138 | ##| #n; ncases y; /2/; |
---|
| 139 | ##] nqed. |
---|
| 140 | |
---|
[3] | 141 | ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. |
---|
[10] | 142 | #n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt; |
---|
| 143 | napply (transitive_Zle … Hle); /2/; |
---|
| 144 | nqed. |
---|
[3] | 145 | |
---|
[10] | 146 | ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2). |
---|
[3] | 147 | #z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H; |
---|
| 148 | ##[@;// |
---|
| 149 | ##|@2;//##] |
---|
| 150 | nqed. |
---|
| 151 | |
---|
| 152 | nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false. |
---|
| 153 | #z1;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //; |
---|
| 154 | #H; #H'; napply False_ind; napply (absurd ? H H'); |
---|
| 155 | nqed. |
---|
| 156 | |
---|
| 157 | (* Z.ma *) |
---|
| 158 | |
---|
| 159 | ndefinition Zge: Z → Z → Prop ≝ |
---|
| 160 | λn,m:Z.m ≤ n. |
---|
| 161 | |
---|
| 162 | interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y). |
---|
| 163 | |
---|
| 164 | ndefinition Zgt: Z → Z → Prop ≝ |
---|
| 165 | λn,m:Z.m<n. |
---|
| 166 | |
---|
| 167 | interpretation "integer 'greater than'" 'gt x y = (Zgt x y). |
---|
| 168 | |
---|
| 169 | interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)). |
---|
| 170 | |
---|
| 171 | ndefinition Zleb : Z → Z → bool ≝ |
---|
| 172 | λx,y:Z. |
---|
| 173 | match x with |
---|
| 174 | [ OZ ⇒ |
---|
| 175 | match y with |
---|
| 176 | [ OZ ⇒ true |
---|
| 177 | | pos m ⇒ true |
---|
| 178 | | neg m ⇒ false ] |
---|
| 179 | | pos n ⇒ |
---|
| 180 | match y with |
---|
| 181 | [ OZ ⇒ false |
---|
| 182 | | pos m ⇒ leb n m |
---|
| 183 | | neg m ⇒ false ] |
---|
| 184 | | neg n ⇒ |
---|
| 185 | match y with |
---|
| 186 | [ OZ ⇒ true |
---|
| 187 | | pos m ⇒ true |
---|
| 188 | | neg m ⇒ leb m n ]]. |
---|
| 189 | |
---|
| 190 | ndefinition Zltb : Z → Z → bool ≝ |
---|
| 191 | λx,y:Z. |
---|
| 192 | match x with |
---|
| 193 | [ OZ ⇒ |
---|
| 194 | match y with |
---|
| 195 | [ OZ ⇒ false |
---|
| 196 | | pos m ⇒ true |
---|
| 197 | | neg m ⇒ false ] |
---|
| 198 | | pos n ⇒ |
---|
| 199 | match y with |
---|
| 200 | [ OZ ⇒ false |
---|
[10] | 201 | | pos m ⇒ leb (succ n) m |
---|
[3] | 202 | | neg m ⇒ false ] |
---|
| 203 | | neg n ⇒ |
---|
| 204 | match y with |
---|
| 205 | [ OZ ⇒ true |
---|
| 206 | | pos m ⇒ true |
---|
[10] | 207 | | neg m ⇒ leb (succ m) n ]]. |
---|
[3] | 208 | |
---|
| 209 | |
---|
| 210 | |
---|
| 211 | ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true. |
---|
| 212 | #n;#m;ncases n;ncases m; //; |
---|
| 213 | ##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H) |
---|
| 214 | ##| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true; |
---|
| 215 | ##| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H) |
---|
| 216 | ##] nqed. |
---|
| 217 | |
---|
| 218 | ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m. |
---|
| 219 | #n;#m;ncases n;ncases m; //; |
---|
| 220 | ##[ ##1,2: #m'; nnormalize; #H; ndestruct |
---|
| 221 | ##| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le; |
---|
| 222 | ##| ##4: #n';#m'; nnormalize; #H; ndestruct |
---|
| 223 | ##] nqed. |
---|
| 224 | |
---|
| 225 | ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. |
---|
[10] | 226 | #n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct; |
---|
[3] | 227 | nqed. |
---|
| 228 | |
---|
| 229 | ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true. |
---|
| 230 | #n;#m;ncases n;ncases m; //; |
---|
| 231 | ##[ nnormalize; #H; napply (False_ind ? H) |
---|
| 232 | ##| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H) |
---|
| 233 | ##| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true; |
---|
| 234 | ##| #n';#m'; nnormalize; #H; napply (False_ind ? H) |
---|
| 235 | ##] nqed. |
---|
| 236 | |
---|
| 237 | ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m. |
---|
| 238 | #n;#m;ncases n;ncases m; //; |
---|
| 239 | ##[ nnormalize; #H; ndestruct |
---|
| 240 | ##| ##2,3: #m'; nnormalize; #H; ndestruct |
---|
| 241 | ##| ##4,6: #n';#m'; napply leb_true_to_le; |
---|
| 242 | ##| #n';#m'; nnormalize; #H; ndestruct |
---|
| 243 | ##] nqed. |
---|
| 244 | |
---|
| 245 | ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. |
---|
[10] | 246 | #n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct; |
---|
| 247 | nqed. |
---|
[3] | 248 | |
---|
| 249 | ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. |
---|
| 250 | (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m). |
---|
| 251 | #n;#m;#P;#Hle;#Hnle; |
---|
| 252 | nlapply (refl ? (Zleb n m)); |
---|
| 253 | nelim (Zleb n m) in ⊢ ((???%)→%); |
---|
| 254 | #Hb; |
---|
| 255 | ##[ napply Hle; napply (Zleb_true_to_Zle … Hb) |
---|
| 256 | ##| napply Hnle; napply (Zleb_false_to_not_Zle … Hb) |
---|
| 257 | ##] nqed. |
---|
| 258 | |
---|
| 259 | ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. |
---|
| 260 | (n < m → P true) → (n ≮ m → P false) → P (Zltb n m). |
---|
| 261 | #n;#m;#P;#Hlt;#Hnlt; |
---|
| 262 | nlapply (refl ? (Zltb n m)); |
---|
| 263 | nelim (Zltb n m) in ⊢ ((???%)→%); |
---|
| 264 | #Hb; |
---|
| 265 | ##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb) |
---|
| 266 | ##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb) |
---|
| 267 | ##] nqed. |
---|
| 268 | |
---|
[11] | 269 | ndefinition Z_times : Z → Z → Z ≝ |
---|
| 270 | λx,y. match x with |
---|
| 271 | [ OZ ⇒ OZ |
---|
| 272 | | pos n ⇒ |
---|
| 273 | match y with |
---|
| 274 | [ OZ ⇒ OZ |
---|
| 275 | | pos m ⇒ pos (n*m) |
---|
| 276 | | neg m ⇒ neg (n*m) |
---|
| 277 | ] |
---|
| 278 | | neg n ⇒ |
---|
| 279 | match y with |
---|
| 280 | [ OZ ⇒ OZ |
---|
| 281 | | pos m ⇒ neg (n*m) |
---|
| 282 | | neg m ⇒ pos (n*m) |
---|
| 283 | ] |
---|
| 284 | ]. |
---|
[3] | 285 | interpretation "integer multiplication" 'times x y = (Z_times x y). |
---|
| 286 | |
---|
| 287 | (* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *) |
---|
[10] | 288 | notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. |
---|
| 289 | notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. |
---|
[3] | 290 | interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). |
---|
| 291 | |
---|
| 292 | (* datatypes/list.ma *) |
---|
| 293 | |
---|
| 294 | ntheorem nil_append_nil_both: |
---|
| 295 | ∀A:Type. ∀l1,l2:list A. |
---|
| 296 | l1 @ l2 = [] → l1 = [] ∧ l2 = []. |
---|
| 297 | #A l1 l2; ncases l1; |
---|
| 298 | ##[ ncases l2; |
---|
| 299 | ##[ /2/ |
---|
| 300 | ##| #h t H; ndestruct; |
---|
| 301 | ##] |
---|
| 302 | ##| ncases l2; |
---|
| 303 | ##[ nnormalize; #h t H; ndestruct; |
---|
| 304 | ##| nnormalize; #h1 t1 h2 h3 H; ndestruct; |
---|
| 305 | ##] |
---|
| 306 | ##] nqed. |
---|
| 307 | |
---|
| 308 | (* division *) |
---|
| 309 | |
---|
[10] | 310 | ninductive natp : Type ≝ |
---|
| 311 | | pzero : natp |
---|
| 312 | | ppos : Pos → natp. |
---|
[3] | 313 | |
---|
[10] | 314 | ndefinition natp0 ≝ |
---|
| 315 | λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ]. |
---|
| 316 | |
---|
| 317 | ndefinition natp1 ≝ |
---|
| 318 | λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ]. |
---|
| 319 | |
---|
| 320 | nlet rec divide (m,n:Pos) on m ≝ |
---|
| 321 | match m with |
---|
| 322 | [ one ⇒ |
---|
| 323 | match n with |
---|
| 324 | [ one ⇒ 〈ppos one,pzero〉 |
---|
| 325 | | _ ⇒ 〈pzero,ppos one〉 |
---|
| 326 | ] |
---|
| 327 | | p0 m' ⇒ |
---|
| 328 | match divide m' n with |
---|
| 329 | [ mk_pair q r ⇒ |
---|
| 330 | match r with |
---|
| 331 | [ pzero ⇒ 〈natp0 q,pzero〉 |
---|
| 332 | | ppos r' ⇒ |
---|
| 333 | match partial_minus (p0 r') n with |
---|
| 334 | [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉 |
---|
| 335 | | MinusZero ⇒ 〈natp1 q, pzero〉 |
---|
| 336 | | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 |
---|
| 337 | ] |
---|
| 338 | ] |
---|
| 339 | ] |
---|
| 340 | | p1 m' ⇒ |
---|
| 341 | match divide m' n with |
---|
| 342 | [ mk_pair q r ⇒ |
---|
| 343 | match r with |
---|
| 344 | [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ] |
---|
| 345 | | ppos r' ⇒ |
---|
| 346 | match partial_minus (p1 r') n with |
---|
| 347 | [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉 |
---|
| 348 | | MinusZero ⇒ 〈natp1 q, pzero〉 |
---|
| 349 | | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 |
---|
| 350 | ] |
---|
| 351 | ] |
---|
| 352 | ] |
---|
| 353 | ]. |
---|
| 354 | |
---|
[3] | 355 | ndefinition div ≝ λm,n. fst ?? (divide m n). |
---|
| 356 | ndefinition mod ≝ λm,n. snd ?? (divide m n). |
---|
| 357 | |
---|
| 358 | ndefinition pairdisc ≝ |
---|
| 359 | λA,B.λx,y:pair A B. |
---|
| 360 | match x with |
---|
| 361 | [(mk_pair t0 t1) ⇒ |
---|
| 362 | match y with |
---|
| 363 | [(mk_pair u0 u1) ⇒ |
---|
| 364 | ∀P: Type[1]. |
---|
| 365 | (∀e0: (eq A (R0 ? t0) u0). |
---|
| 366 | ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ]. |
---|
| 367 | |
---|
| 368 | nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y. |
---|
| 369 | #A;#B;#x;#y;#e;nrewrite > e;ncases y; |
---|
| 370 | #a;#b;nnormalize;#P;#PH;napply PH;@; |
---|
| 371 | nqed. |
---|
| 372 | |
---|
[10] | 373 | nlemma pred_minus: ∀n,m. pred n - m = pred (n-m). |
---|
| 374 | napply pos_elim; /3/; |
---|
| 375 | nqed. |
---|
[3] | 376 | |
---|
[10] | 377 | nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p. |
---|
| 378 | napply pos_elim; |
---|
| 379 | ##[ // |
---|
| 380 | ##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/; |
---|
| 381 | ##] nqed. |
---|
| 382 | |
---|
[3] | 383 | ntheorem plus_minus_r: |
---|
[10] | 384 | ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m. |
---|
[3] | 385 | #m;#n;#p;#le;nrewrite > (symmetric_plus …); |
---|
| 386 | nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed. |
---|
| 387 | |
---|
[10] | 388 | nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p. |
---|
[3] | 389 | #m;#n;#p;nelim m;/2/; nqed. |
---|
[10] | 390 | (* |
---|
[3] | 391 | nlemma le_to_minus: ∀m,n. m≤n → m-n = 0. |
---|
| 392 | #m;#n;nelim n; |
---|
| 393 | ##[ nrewrite < (minus_n_O …); /2/; |
---|
| 394 | ##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct; |
---|
| 395 | nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/ |
---|
| 396 | ##] nqed. |
---|
[10] | 397 | *) |
---|
| 398 | nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n). |
---|
| 399 | #n;#m;#p;(*nelim (decidable_lt n m);*)#lt; |
---|
| 400 | (*##[*) napply (pos_elim … p); //;#p'; #IH; |
---|
| 401 | nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); |
---|
| 402 | nrewrite > (minus_plus_distrib …); |
---|
| 403 | nrewrite < (plus_minus … lt); nrewrite < IH; |
---|
[3] | 404 | nrewrite > (plus_minus_r …); /2/; |
---|
[10] | 405 | nqed. |
---|
| 406 | (*##| |
---|
| 407 | nlapply (not_lt_to_le … lt); #le; |
---|
| 408 | napply (pos_elim … p); //; #p'; |
---|
| 409 | ncut (m-n = one); ##[ /3/ ##] |
---|
| 410 | #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …); |
---|
| 411 | #H; nrewrite < H in ⊢ (???%); |
---|
| 412 | napply sym_eq; napply le_n_one_to_eq; nrewrite < H; |
---|
[3] | 413 | nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l; |
---|
| 414 | /2/; |
---|
| 415 | ##] nqed. |
---|
| 416 | |
---|
| 417 | nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n. |
---|
| 418 | #m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//; |
---|
| 419 | #H'; nlapply (minus_to_plus … H'); /2/; |
---|
| 420 | nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H; |
---|
| 421 | napply False_ind; napply (absurd ? H ( not_le_Sn_n n)); |
---|
| 422 | nqed. |
---|
[10] | 423 | *) |
---|
[3] | 424 | |
---|
[10] | 425 | nlet rec natp_plus (n,m:natp) ≝ |
---|
| 426 | match n with |
---|
| 427 | [ pzero ⇒ m |
---|
| 428 | | ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ] |
---|
| 429 | ]. |
---|
[3] | 430 | |
---|
[10] | 431 | nlet rec natp_times (n,m:natp) ≝ |
---|
| 432 | match n with |
---|
| 433 | [ pzero ⇒ pzero |
---|
| 434 | | ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ] |
---|
| 435 | ]. |
---|
[3] | 436 | |
---|
[10] | 437 | ninductive natp_lt : natp → Pos → Prop ≝ |
---|
| 438 | | plt_zero : ∀n. natp_lt pzero n |
---|
| 439 | | plt_pos : ∀n,m. n < m → natp_lt (ppos n) m. |
---|
| 440 | |
---|
| 441 | nlemma lt_p0: ∀n:Pos. one < p0 n. |
---|
| 442 | #n; nnormalize; /2/; nqed. |
---|
| 443 | |
---|
| 444 | nlemma lt_p1: ∀n:Pos. one < p1 n. |
---|
| 445 | #n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed. |
---|
| 446 | |
---|
| 447 | nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉. |
---|
| 448 | #m; nelim m; |
---|
| 449 | ##[ //; |
---|
| 450 | ##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //; |
---|
| 451 | ##] nqed. |
---|
| 452 | |
---|
| 453 | nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n). |
---|
| 454 | #n P Q; napply succ_elim; /2/; nqed. |
---|
| 455 | |
---|
| 456 | nlemma partial_minus_to_Prop: ∀n,m. |
---|
| 457 | match partial_minus n m with |
---|
| 458 | [ MinusNeg ⇒ n < m |
---|
| 459 | | MinusZero ⇒ n = m |
---|
| 460 | | MinusPos r ⇒ n = m+r |
---|
| 461 | ]. |
---|
| 462 | #n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m); |
---|
| 463 | nnormalize; ncases (partial_minus n m); /2/; nqed. |
---|
| 464 | |
---|
| 465 | nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m. |
---|
| 466 | #n m lt; nelim lt; /2/; |
---|
[3] | 467 | nqed. |
---|
| 468 | |
---|
[10] | 469 | nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m. |
---|
| 470 | #n m lt; napply (transitive_lt ? (p0 m) ?); /2/; |
---|
| 471 | nqed. |
---|
| 472 | |
---|
| 473 | nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m. |
---|
| 474 | #n m lt; ninversion lt; |
---|
| 475 | ##[ #H; nrewrite > (succ_injective … H); //; |
---|
| 476 | ##| #p H1 H2 H3;nrewrite > (succ_injective … H3); |
---|
| 477 | napply (transitive_lt ? (p0 p) ?); /2/; |
---|
| 478 | ##] |
---|
| 479 | nqed. |
---|
| 480 | |
---|
| 481 | nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m. |
---|
| 482 | #n m lt; nelim lt; /2/; |
---|
| 483 | nqed. |
---|
| 484 | |
---|
| 485 | |
---|
| 486 | |
---|
| 487 | nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m. |
---|
| 488 | #n m lt;ninversion lt; |
---|
| 489 | ##[ #p H; ndestruct; |
---|
| 490 | ##| #n' m' lt e1 e2; ndestruct; //; |
---|
[3] | 491 | ##] nqed. |
---|
| 492 | |
---|
[10] | 493 | nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b. |
---|
| 494 | #a b; /2/; nqed. |
---|
| 495 | |
---|
| 496 | nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b. |
---|
| 497 | #a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed. |
---|
| 498 | |
---|
| 499 | nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m. |
---|
| 500 | /2/; nqed. |
---|
| 501 | |
---|
| 502 | nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. |
---|
| 503 | #A B a1 a2 b1 b2 H; ndestruct; //; |
---|
| 504 | nqed. |
---|
| 505 | |
---|
| 506 | nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. |
---|
| 507 | #A B a1 a2 b1 b2 H; ndestruct; //; |
---|
| 508 | nqed. |
---|
| 509 | |
---|
| 510 | ntheorem divide_ok : ∀m,n,dv,md. |
---|
| 511 | divide m n = 〈dv,md〉 → |
---|
| 512 | ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n. |
---|
| 513 | #m n; napply (pos_cases … n); |
---|
| 514 | ##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/; |
---|
| 515 | ##| #n'; nelim m; |
---|
| 516 | ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/; |
---|
| 517 | ##| #m' IH dv md; nnormalize; |
---|
| 518 | nlapply (refl ? (divide m' (succ n'))); |
---|
| 519 | nelim (divide m' (succ n')) in ⊢ (???% → % → ?); |
---|
| 520 | #dv' md' DIVr; nelim (IH … DIVr); |
---|
| 521 | nnormalize; ncases md'; |
---|
| 522 | ##[ ncases dv'; nnormalize; |
---|
| 523 | ##[ #H; ndestruct; |
---|
| 524 | ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/; |
---|
| 525 | ##] |
---|
| 526 | ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim; |
---|
| 527 | nnormalize; #n md'' Hr1 Hr2; |
---|
| 528 | nlapply (plt_lt … Hr2); #Hr2'; |
---|
| 529 | nlapply (partial_minus_to_Prop md'' n); |
---|
| 530 | ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize; |
---|
| 531 | #lt; #e; ndestruct; @; /2/; napply plt_pos; |
---|
| 532 | ##[ ##1,3,5,7: napply double_lt1; /2/; |
---|
| 533 | ##| ##2,4: napply double_lt3; /2/; |
---|
| 534 | ##| ##*: napply double_lt2; /2/; |
---|
| 535 | ##] |
---|
| 536 | ##] |
---|
| 537 | ##| #m' IH dv md; nwhd in ⊢ (??%? → ?); |
---|
| 538 | nlapply (refl ? (divide m' (succ n'))); |
---|
| 539 | nelim (divide m' (succ n')) in ⊢ (???% → % → ?); |
---|
| 540 | #dv' md' DIVr; nelim (IH … DIVr); |
---|
| 541 | nwhd in ⊢ (? → ? → ??%? → ?); ncases md'; |
---|
| 542 | ##[ ncases dv'; nnormalize; |
---|
| 543 | ##[ #H; ndestruct; |
---|
| 544 | ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/; |
---|
| 545 | ##] |
---|
| 546 | ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim; |
---|
| 547 | nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2; |
---|
| 548 | nlapply (plt_lt … Hr2); #Hr2'; |
---|
| 549 | nwhd in ⊢ (??%? → ?); |
---|
| 550 | nlapply (partial_minus_to_Prop (p0 md'') (succ n')); |
---|
| 551 | ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##] |
---|
| 552 | ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize; |
---|
| 553 | #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##] |
---|
| 554 | #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##] |
---|
| 555 | nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e); |
---|
| 556 | nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos; |
---|
| 557 | ##[ ncut (succ n' + r'' < p0 (succ n')); /2/; |
---|
| 558 | ##| ncut (succ n' + r'' < p0 (succ n')); /2/; |
---|
| 559 | ##| /2/; |
---|
| 560 | ##| /2/; |
---|
| 561 | ##] |
---|
| 562 | ##] |
---|
| 563 | ##] |
---|
| 564 | ##] nqed. |
---|
| 565 | |
---|
| 566 | nlemma mod0_divides: ∀m,n,dv:Pos. |
---|
| 567 | divide n m = 〈ppos dv,pzero〉 → m∣n. |
---|
| 568 | #m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *; |
---|
| 569 | nnormalize; #H; ndestruct; //; |
---|
| 570 | nqed. |
---|
| 571 | |
---|
| 572 | nlemma divides_mod0: ∀dv,m,n:Pos. |
---|
| 573 | n = dv*m → divide n m = 〈ppos dv,pzero〉. |
---|
| 574 | #dv;#m;#n;#DIV;nlapply (refl ? (divide n m)); |
---|
| 575 | nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE; |
---|
| 576 | nlapply (divide_ok … DIVIDE); *; |
---|
| 577 | ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##] |
---|
| 578 | ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE; nnormalize; |
---|
| 579 | nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct; |
---|
| 580 | ##[ nlapply (plus_to_minus … e0); |
---|
| 581 | nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …); |
---|
| 582 | ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt; |
---|
| 583 | nrewrite > (minus_times_distrib_l …); //; |
---|
| 584 | |
---|
| 585 | (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##] |
---|
| 586 | #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind; |
---|
| 587 | napply (absurd ? B (lt_to_not_le … A)); |
---|
| 588 | |
---|
| 589 | ##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/; |
---|
| 590 | |
---|
| 591 | ##| nrewrite > DIVIDE; ncut (dv = dv''); /2/; |
---|
| 592 | ##] |
---|
| 593 | nqed. |
---|
| 594 | |
---|
| 595 | nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n). |
---|
| 596 | #m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %); |
---|
| 597 | #dv;#md; ncases md; ncases dv; |
---|
| 598 | ##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct |
---|
| 599 | ##| #dv'; #H; @1; napply mod0_divides; /2/; |
---|
[3] | 600 | ##| #md'; #DIVIDES; @2; napply nmk; *; #dv'; |
---|
[10] | 601 | nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); |
---|
[3] | 602 | nrewrite > DIVIDES; #H'; |
---|
| 603 | ndestruct; |
---|
[10] | 604 | ##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv'; |
---|
| 605 | nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); |
---|
| 606 | nrewrite > DIVIDES; #H'; |
---|
| 607 | ndestruct; |
---|
[3] | 608 | ##] nqed. |
---|
| 609 | |
---|
[10] | 610 | ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q). |
---|
| 611 | #p;#q;ncases p; |
---|
| 612 | ##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##] |
---|
| 613 | ##| ##*: #n; ncases q; nnormalize; /2/; |
---|
[3] | 614 | ##] nqed. |
---|
| 615 | |
---|
[10] | 616 | ndefinition natp_to_Z ≝ |
---|
| 617 | λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ]. |
---|
[3] | 618 | |
---|
[10] | 619 | ndefinition natp_to_negZ ≝ |
---|
| 620 | λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ]. |
---|
[3] | 621 | |
---|
| 622 | (* TODO: check these definitions are right. They are supposed to be the same |
---|
| 623 | as Zdiv/Zmod in Coq. *) |
---|
| 624 | ndefinition divZ ≝ λx,y. |
---|
[10] | 625 | match x with |
---|
| 626 | [ OZ ⇒ OZ |
---|
| 627 | | pos n ⇒ |
---|
| 628 | match y with |
---|
[3] | 629 | [ OZ ⇒ OZ |
---|
[10] | 630 | | pos m ⇒ natp_to_Z (fst ?? (divide n m)) |
---|
| 631 | | neg m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
| 632 | match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] |
---|
[3] | 633 | ] |
---|
[10] | 634 | | neg n ⇒ |
---|
| 635 | match y with |
---|
| 636 | [ OZ ⇒ OZ |
---|
| 637 | | pos m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
| 638 | match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] |
---|
| 639 | | neg m ⇒ natp_to_Z (fst ?? (divide n m)) |
---|
| 640 | ] |
---|
[3] | 641 | ]. |
---|
| 642 | |
---|
| 643 | ndefinition modZ ≝ λx,y. |
---|
[10] | 644 | match x with |
---|
| 645 | [ OZ ⇒ OZ |
---|
| 646 | | pos n ⇒ |
---|
| 647 | match y with |
---|
[3] | 648 | [ OZ ⇒ OZ |
---|
[10] | 649 | | pos m ⇒ natp_to_Z (snd ?? (divide n m)) |
---|
| 650 | | neg m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
[14] | 651 | match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ] |
---|
[3] | 652 | ] |
---|
[10] | 653 | | neg n ⇒ |
---|
| 654 | match y with |
---|
| 655 | [ OZ ⇒ OZ |
---|
| 656 | | pos m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
[14] | 657 | match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ] |
---|
[10] | 658 | | neg m ⇒ natp_to_Z (snd ?? (divide n m)) |
---|
| 659 | ] |
---|
[3] | 660 | ]. |
---|
| 661 | |
---|
| 662 | interpretation "natural division" 'divide m n = (div m n). |
---|
| 663 | interpretation "natural modulus" 'module m n = (mod m n). |
---|
| 664 | interpretation "integer division" 'divide m n = (divZ m n). |
---|
| 665 | interpretation "integer modulus" 'module m n = (modZ m n). |
---|
[14] | 666 | |
---|
| 667 | nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x. |
---|
| 668 | #x y; ncases y; |
---|
| 669 | ##[ #H; napply (False_ind … H); |
---|
| 670 | ##| #m; #_; ncases x; //; #n; |
---|
| 671 | nwhd in ⊢ (?%?); |
---|
| 672 | nlapply (pos_compare_to_Prop n m); |
---|
| 673 | ncases (pos_compare n m); /2/; |
---|
| 674 | #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/; |
---|
| 675 | ##| #m H; napply (False_ind … H); |
---|
| 676 | ##] nqed. |
---|
| 677 | |
---|
| 678 | nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. |
---|
| 679 | #n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m); |
---|
| 680 | ##[ //; |
---|
| 681 | ##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/; |
---|
| 682 | ##] nqed. |
---|
| 683 | |
---|
| 684 | ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y. |
---|
| 685 | #x y; ncases y; |
---|
| 686 | ##[ #H; napply (False_ind … H); |
---|
| 687 | ##| #m; #_; ncases x; |
---|
| 688 | ##[ @;//; |
---|
| 689 | ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m)); |
---|
| 690 | ncases (divide n m) in ⊢ (???% → %); #dv md H; |
---|
| 691 | nelim (divide_ok … H); #e l; nelim l; /2/; |
---|
| 692 | ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m)); |
---|
| 693 | ncases (divide n m) in ⊢ (???% → %); #dv md H; |
---|
| 694 | nelim (divide_ok … H); #e l; nelim l; |
---|
| 695 | ##[ /2/; |
---|
| 696 | ##| #md' m' l'; @; |
---|
| 697 | ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …); |
---|
| 698 | nrewrite > (pos_compare_lt … l'); //; |
---|
| 699 | ##| /2/; |
---|
| 700 | ##] |
---|
| 701 | ##] |
---|
| 702 | ##] |
---|
| 703 | ##| #m H; napply (False_ind … H); |
---|
| 704 | ##] nqed. |
---|