diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
commit | bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (patch) | |
tree | 3efa5cb51e9bb3edc935f42dbd630fce9a170804 /lib/Coqlib.v | |
parent | cd2449aabe7b259b0fdb8aaa2af65c2b8957ab32 (diff) | |
download | compcert-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.tar.gz compcert-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.zip |
- Added alignment constraints to memory loads and stores.
- In Cminor and below, removed pointer validity check in semantics of
comparisons, so that evaluation of expressions is independent of
memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index ff6e9ae8..a79ea29c 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -18,6 +18,7 @@ library. *) Require Export ZArith. +Require Export Znumtheory. Require Export List. Require Export Bool. Require Import Wf_nat. @@ -526,6 +527,25 @@ Proof. omega. Qed. +(** Properties of divisibility. *) + +Lemma Zdivides_trans: + forall x y z, (x | y) -> (y | z) -> (x | z). +Proof. + intros. inv H. inv H0. exists (q0 * q). ring. +Qed. + +Definition Zdivide_dec: + forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }. +Proof. + intros. destruct (zeq (Zmod q p) 0). + left. exists (q / p). + transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto. + transitivity (p * (q / p)). omega. ring. + right; red; intros. elim n. apply Z_div_exact_1; auto. + inv H0. rewrite Z_div_mult; auto. ring. +Qed. + (** Alignment: [align n amount] returns the smallest multiple of [amount] greater than or equal to [n]. *) @@ -542,6 +562,11 @@ Proof. rewrite Zmult_comm. omega. Qed. +Lemma align_divides: forall x y, y > 0 -> (y | align x y). +Proof. + intros. unfold align. apply Zdivide_factor_l. +Qed. + (** * Definitions and theorems on the data types [option], [sum] and [list] *) Set Implicit Arguments. |