lib/Integers.v: revised and extended, faster implementation based on

  bit-level operations provided by ZArith in Coq 8.4.
Other modules: adapted accordingly.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 38 insertions, 41 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index cff5b06..9bbf040 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1280,23 +1280,23 @@ Proof.
   assert (A: forall v, v = Val.zero_ext 8 v -> v = Val.zero_ext 16 v).
     intros. rewrite H.
     destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
+    apply Int.zero_ext_widen. omega. 
   assert (B: forall v, v = Val.sign_ext 8 v -> v = Val.sign_ext 16 v).
     intros. rewrite H.
     destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.sign_ext_widen. compute; auto. split. omega. compute; auto.
+    apply Int.sign_ext_widen. omega.
   assert (C: forall v, v = Val.zero_ext 8 v -> v = Val.sign_ext 16 v).
     intros. rewrite H.
     destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto.
+    apply Int.sign_zero_ext_widen. omega.
   assert (D: forall v, v = Val.zero_ext 1 v -> v = Val.zero_ext 8 v).
     intros. rewrite H.
     destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
+    apply Int.zero_ext_widen. omega. 
   assert (E: forall v, v = Val.zero_ext 1 v -> v = Val.sign_ext 8 v).
     intros. rewrite H.
     destruct v; simpl; auto. decEq. symmetry. 
-    apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto.
+    apply Int.sign_zero_ext_widen. omega.
   intros. 
   unfold Approx.bge in H; destruct a1; try discriminate; destruct a2; simpl in *; try discriminate; intuition.
 Qed.
@@ -1309,14 +1309,14 @@ Proof.
   destruct (Int.eq_dec n Int.one); simpl. subst; auto. 
   destruct (Int.eq_dec n (Int.zero_ext 7 n)). simpl.
     split.
-    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
-    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
+    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. omega.
+    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. omega.
   destruct (Int.eq_dec n (Int.zero_ext 8 n)). simpl; congruence.
   destruct (Int.eq_dec n (Int.sign_ext 8 n)). simpl; congruence.
   destruct (Int.eq_dec n (Int.zero_ext 15 n)). simpl.
     split.
-    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto.
-    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. 
+    decEq. rewrite e. symmetry. apply Int.zero_ext_widen. omega. 
+    decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. omega. 
   destruct (Int.eq_dec n (Int.zero_ext 16 n)). simpl; congruence.
   destruct (Int.eq_dec n (Int.sign_ext 16 n)). simpl; congruence.
   exact I.
@@ -1345,10 +1345,10 @@ Lemma approx_of_unop_sound:
   val_match_approx (Approx.unop op a1) v.
 Proof.
   destruct op; simpl; intros; auto; inv H.
-  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto.
-  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto.
-  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto.
-  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto.
+  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. omega. 
+  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. omega. 
+  destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. omega. 
+  destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. omega. 
   destruct v1; simpl; auto. rewrite Float.singleoffloat_idem; auto.
 Qed.
 
@@ -1650,10 +1650,11 @@ Proof.
   intros. inversion H; clear H.
   inversion H2. destruct v2; simpl; auto.
   apply val_lessdef_upto_int. rewrite Int.zero_ext_and; auto. 
-  rewrite Int.and_assoc. rewrite H0. auto. 
+  rewrite Int.and_assoc. rewrite H0. auto.
+  omega.
   simpl; auto.
   simpl. apply val_lessdef_upto_int. rewrite Int.zero_ext_and; auto.
-  rewrite Int.and_assoc. rewrite H0. auto.
+  rewrite Int.and_assoc. rewrite H0. auto. omega.
 Qed.
 
 Remark val_lessdef_upto_sign_ext:
@@ -1664,9 +1665,9 @@ Proof.
   intros.
   assert (A: forall x, Int.and (Int.sign_ext p x) m = Int.and x m).
     intros. transitivity (Int.and (Int.zero_ext p (Int.sign_ext p x)) m).
-    rewrite Int.zero_ext_and; auto. rewrite Int.and_assoc. congruence.
+    rewrite Int.zero_ext_and; auto. rewrite Int.and_assoc. congruence. omega.
     rewrite Int.zero_ext_sign_ext.
-    rewrite Int.zero_ext_and; auto. rewrite Int.and_assoc. congruence.
+    rewrite Int.zero_ext_and; auto. rewrite Int.and_assoc. congruence. omega. omega.
   inversion H; clear H.
   inversion H2. destruct v2; simpl; auto.
   apply val_lessdef_upto_int. auto. 
@@ -1811,28 +1812,24 @@ Proof.
   exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v' [A B]].
   exists v'; split; auto.
   inv B; auto. inv H0; auto. constructor.
-  assert (0 < 8 < Z_of_nat Int.wordsize) by (compute; auto).
-  apply Int.sign_ext_equal_if_zero_equal; auto.
-  repeat rewrite Int.zero_ext_and; auto.
+  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
+  repeat rewrite Int.zero_ext_and; auto. omega. omega.
   (* int8unsigned *)
   exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v' [A B]].
   exists v'; split; auto.
   inv B; auto. inv H0; auto. constructor.
-  assert (0 < 8 < Z_of_nat Int.wordsize) by (compute; auto).
-  repeat rewrite Int.zero_ext_and; auto.
+  repeat rewrite Int.zero_ext_and; auto. omega. omega.
   (* int16signed *)
   exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v' [A B]].
   exists v'; split; auto.
   inv B; auto. inv H0; auto. constructor.
-  assert (0 < 16 < Z_of_nat Int.wordsize) by (compute; auto).
-  apply Int.sign_ext_equal_if_zero_equal; auto.
-  repeat rewrite Int.zero_ext_and; auto.
+  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
+  repeat rewrite Int.zero_ext_and; auto. omega. omega.
   (* int16unsigned *)
   exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v' [A B]].
   exists v'; split; auto.
   inv B; auto. inv H0; auto. constructor.
-  assert (0 < 16 < Z_of_nat Int.wordsize) by (compute; auto).
-  repeat rewrite Int.zero_ext_and; auto.
+  repeat rewrite Int.zero_ext_and; auto. omega. omega.
   (* int32 *)
   exists va; auto.
   (* float32 *)
@@ -1915,30 +1912,30 @@ Proof.
   exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v1 [A B]].
   exists (Val.zero_ext 8 v1); split. econstructor; eauto. 
   inv B. apply Val.zero_ext_lessdef; auto. simpl.
-  assert (0 < 8 < Z_of_nat Int.wordsize) by (compute; auto).
-  repeat rewrite Int.zero_ext_and; auto. change (two_p 8 - 1) with 255. rewrite H0. auto. 
+  repeat rewrite Int.zero_ext_and; auto.
+  change (two_p 8 - 1) with 255. rewrite H0. auto.
+  omega. omega.
 (* cast8signed *)
   exploit (eval_uncast_int (Int.repr 255)); eauto. intros [v1 [A B]].
   exists (Val.sign_ext 8 v1); split. econstructor; eauto. 
   inv B. apply Val.sign_ext_lessdef; auto. simpl.
-  assert (0 < 8 < Z_of_nat Int.wordsize) by (compute; auto).
   replace (Int.sign_ext 8 n2) with (Int.sign_ext 8 n1). auto.
-  apply Int.sign_ext_equal_if_zero_equal; auto.
-  repeat rewrite Int.zero_ext_and; auto.
+  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
+  repeat rewrite Int.zero_ext_and; auto. omega. omega.
 (* cast16unsigned *)
   exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v1 [A B]].
   exists (Val.zero_ext 16 v1); split. econstructor; eauto. 
   inv B. apply Val.zero_ext_lessdef; auto. simpl.
-  assert (0 < 16 < Z_of_nat Int.wordsize) by (compute; auto).
-  repeat rewrite Int.zero_ext_and; auto. change (two_p 16 - 1) with 65535. rewrite H0. auto. 
+  repeat rewrite Int.zero_ext_and; auto.
+  change (two_p 16 - 1) with 65535. rewrite H0. auto.
+  omega. omega.
 (* cast16signed *)
   exploit (eval_uncast_int (Int.repr 65535)); eauto. intros [v1 [A B]].
   exists (Val.sign_ext 16 v1); split. econstructor; eauto. 
   inv B. apply Val.sign_ext_lessdef; auto. simpl.
-  assert (0 < 16 < Z_of_nat Int.wordsize) by (compute; auto).
   replace (Int.sign_ext 16 n2) with (Int.sign_ext 16 n1). auto.
-  apply Int.sign_ext_equal_if_zero_equal; auto.
-  repeat rewrite Int.zero_ext_and; auto.
+  apply Int.sign_ext_equal_if_zero_equal; auto. omega.
+  repeat rewrite Int.zero_ext_and; auto. omega. omega.
 (* singleoffloat *)
   exploit eval_uncast_float32; eauto. intros [v1 [A B]].
   exists (Val.singleoffloat v1); split. econstructor; eauto. 
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 5cb0f18..b31738b 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -591,7 +591,7 @@ Lemma within_widen:
 Proof.
   intros. destruct H. split. 
   eapply Ple_trans; eauto.
-  unfold Plt, Ple in *. omega. 
+  eapply Plt_Ple_trans; eauto.
 Qed.
 
 Definition contained (l: list ident) (g1 g2: generator) : Prop :=
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 8df7b6e..c496a5e 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -219,8 +219,8 @@ Remark cast_int_int_idem:
   forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i.
 Proof.
   intros. destruct sz; simpl; auto. 
-  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; auto.
-  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; auto.
+  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
+  destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence.
   destruct (Int.eq i Int.zero); auto.
 Qed.
 
@@ -288,7 +288,7 @@ Proof.
   destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence.
   clear H1. inv H0. auto.
   inversion H0; clear H0; subst chunk. simpl in *. 
-  destruct (Int.eq n Int.zero); subst n; auto.
+  destruct (Int.eq n Int.zero); subst n; reflexivity.
   destruct sz; inversion H0; clear H0; subst chunk; simpl in *; congruence.
   inv H0; auto.
   inv H0; auto.