diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 15:11:48 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 15:11:48 +0200 |
commit | 322f3c865341fdfd5d22ab885b2934a5213ddbaa (patch) | |
tree | 70912af2a6cd75d72b57172d910d71a6abd2d447 /lib | |
parent | 6b87278c399332f67a4b40958ea2386bb3c1c66e (diff) | |
download | compcert-322f3c865341fdfd5d22ab885b2934a5213ddbaa.tar.gz compcert-322f3c865341fdfd5d22ab885b2934a5213ddbaa.zip |
Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy
Inline directives in extraction.v make the Caml output efficient and almost nice.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Decidableplus.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 7772e07b..3bb6eee7 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -122,6 +122,34 @@ Next Obligation. apply Z.ltb_lt. Qed. +Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { + Decidable_witness := Z.geb x y +}. +Next Obligation. + rewrite Z.geb_le. intuition omega. +Qed. + +Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { + Decidable_witness := Z.gtb x y +}. +Next Obligation. + rewrite Z.gtb_lt. intuition omega. +Qed. + +Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { + Decidable_witness := Z.eqb y ((y / x) * x)%Z +}. +Next Obligation. + split. + intros. apply Z.eqb_eq in H. exists (y / x). auto. + intros [k EQ]. apply Z.eqb_eq. + destruct (Z.eq_dec x 0). + subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity. + assert (k = y / x). + { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. } + congruence. +Qed. + (** Deciding properties over lists *) Program Instance Decidable_forall_in_list : |