Changeset 10 for Csemantics/Coqlib.ma
 Timestamp:
 Jul 6, 2010, 11:53:23 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Coqlib.ma
r3 r10 18 18 library. *) 19 19 20 include " arithmetics/Z.ma".20 include "binary/Z.ma". 21 21 include "datatypes/sums.ma". 22 22 include "datatypes/list.ma". … … 347 347 auto. 348 348 Qed. 349 350 (** Properties of powers of two. *) 351 352 Lemma two_power_nat_O : two_power_nat O = 1. 353 Proof. reflexivity. Qed. 354 355 Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0. 356 Proof. 357 induction n. rewrite two_power_nat_O. omega. 358 rewrite two_power_nat_S. omega. 359 Qed. 360 361 Lemma two_power_nat_two_p: 362 forall x, two_power_nat x = two_p (Z_of_nat x). 363 Proof. 364 induction x. auto. 365 rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega. 366 Qed. 367 349 *) 350 (* * Properties of powers of two. *) 351 352 nlemma two_power_nat_O : two_power_nat O = one. 353 //; nqed. 354 355 nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0. 356 //; nqed. 357 358 nlemma two_power_nat_two_p: 359 ∀x. Z_two_power_nat x = two_p (Z_of_nat x). 360 #x; ncases x; 361 ##[ //; 362 ## nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //; 363 ##] nqed. 364 (* 368 365 Lemma two_p_monotone: 369 366 forall x y, 0 <= x <= y > two_p x <= two_p y. … … 577 574 (* * Alignment: [align n amount] returns the smallest multiple of [amount] 578 575 greater than or equal to [n]. *) 579 naxiom align : Z → Z → Z. 580 (* 576 (*naxiom align : Z → Z → Z.*) 577 581 578 ndefinition align ≝ λn: Z. λamount: Z. 582 579 ((n + amount  1) / amount) * amount. 583 580 (* 584 581 Lemma align_le: forall x y, y > 0 > x <= align x y. 585 582 Proof.
Note: See TracChangeset
for help on using the changeset viewer.