From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - 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 --- lib/Coqlib.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'lib/Coqlib.v') 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. -- cgit