Glasnost: making transparent a number of definitions that were opaque

for no good reason.



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

3 files changed, 22 insertions, 22 deletions

diff --git a/common/AST.v b/common/AST.v
index 44811b2..8595b95 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -47,10 +47,12 @@ Lemma typesize_pos: forall ty, typesize ty > 0.
 Proof. destruct ty; simpl; omega. Qed.
 
 Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
+Global Opaque typ_eq.
 
 Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. apply typ_eq. Qed.
+Proof. decide equality. apply typ_eq. Defined.
+Global Opaque opt_typ_eq.
 
 (** Additionally, function definitions and function calls are annotated
   by function signatures indicating the number and types of arguments,
diff --git a/common/Memdata.v b/common/Memdata.v
index 8afe752..3de5f39 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -190,6 +190,7 @@ Opaque Byte.wordsize.
   replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega.
   rewrite two_p_is_exp; try omega. 
   rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm. 
+  change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x). 
   rewrite Byte.Z_mod_modulus_eq. reflexivity. 
   apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
 Qed.
diff --git a/common/Memory.v b/common/Memory.v
index bfaf67d..12a0f45 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -26,6 +26,7 @@
 - [free]: invalidate a memory block.
 *)
 
+Require Import Zwf.
 Require Import Axioms.
 Require Import Coqlib.
 Require Import Maps.
@@ -155,7 +156,7 @@ Remark perm_order_dec:
   forall p1 p2, {perm_order p1 p2} + {~perm_order p1 p2}.
 Proof.
   intros. destruct p1; destruct p2; (left; constructor) || (right; intro PO; inversion PO).
-Qed.
+Defined.
 
 Remark perm_order'_dec:
   forall op p, {perm_order' op p} + {~perm_order' op p}.
@@ -163,14 +164,14 @@ Proof.
   intros. destruct op; unfold perm_order'.
   apply perm_order_dec.
   right; tauto.
-Qed.
+Defined.
 
 Theorem perm_dec:
   forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.
 Proof.
   unfold perm; intros.
   apply perm_order'_dec.
-Qed.
+Defined.
 
 Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop :=
   forall ofs, lo <= ofs < hi -> perm m b ofs k p.
@@ -202,19 +203,15 @@ Lemma range_perm_dec:
   forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}.
 Proof.
   intros. 
-  assert (forall n, 0 <= n ->
-          {range_perm m b lo (lo + n) k p} + {~ range_perm m b lo (lo + n) k p}).
-    apply natlike_rec2.
-    left. red; intros. omegaContradiction.
-    intros. destruct H0. 
-    destruct (perm_dec m b (lo + z) k p). 
-    left. red; intros. destruct (zeq ofs (lo + z)). congruence. apply r. omega. 
-    right; red; intro. elim n. apply H0. omega. 
-    right; red; intro. elim n. red; intros. apply H0. omega. 
+  induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)).
   destruct (zlt lo hi).
-  replace hi with (lo + (hi - lo)) by omega. apply H. omega.
-  left; red; intros. omegaContradiction. 
-Qed.
+  destruct (perm_dec m b lo k p).
+  destruct (H (lo + 1)). red. omega. 
+  left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega. 
+  right; red; intros. elim n. red; intros; apply H0; omega.
+  right; red; intros. elim n. apply H0. omega. 
+  left; red; intros. omegaContradiction.
+Defined.
 
 (** [valid_access m chunk b ofs p] holds if a memory access
     of the given chunk is possible in [m] at address [b, ofs]
@@ -289,7 +286,7 @@ Proof.
   left; constructor; auto.
   right; red; intro V; inv V; contradiction.
   right; red; intro V; inv V; contradiction.
-Qed.
+Defined.
 
 (** [valid_pointer m b ofs] returns [true] if the address [b, ofs]
   is nonempty in [m] and [false] if it is empty. *)
@@ -877,7 +874,7 @@ Proof.
   destruct (valid_access_dec m1 chunk b ofs Writable).
   eauto.
   contradiction.
-Qed.
+Defined.
 
 Hint Local Resolve valid_access_store: mem.
 
@@ -1363,7 +1360,7 @@ Proof.
   destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
   reflexivity. 
   contradiction.
-Qed.
+Defined.
 
 Theorem storebytes_store:
   forall m1 b ofs chunk v m2,
@@ -1774,7 +1771,7 @@ Theorem range_perm_free:
   { m2: mem | free m1 b lo hi = Some m2 }.
 Proof.
   intros; unfold free. rewrite pred_dec_true; auto. econstructor; eauto.
-Qed.
+Defined.
 
 Section FREE.
 
@@ -1949,7 +1946,7 @@ Theorem range_perm_drop_2:
 Proof.
   unfold drop_perm; intros. 
   destruct (range_perm_dec m b lo hi Cur Freeable). econstructor. eauto. contradiction.
-Qed.
+Defined.
 
 Section DROP.