Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy

Inline directives in extraction.v make the Caml output efficient and almost nice.

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 :