aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Coqlib.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r--lib/Coqlib.v25
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.