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

6 files changed, 64 insertions, 44 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 8aeadb9..f58a894 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -556,7 +556,8 @@ Proof.
   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.
+Defined.
+Global Opaque Zdivide_dec.
 
 (** Conversion from [Z] to [nat]. *)
 
diff --git a/lib/Floats.v b/lib/Floats.v
index 63375ff..eb86027 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -854,6 +854,7 @@ Theorem floatofint_from_words:
     sub (from_words ox4330_0000 (Int.add x ox8000_0000))
         (from_words ox4330_0000 ox8000_0000).
 Proof.
+Local Transparent Int.repr Int64.repr.
   intros; destruct (Int.eq_dec x Int.zero); [subst; vm_compute; reflexivity|].
   assert (Int.signed x <> 0).
   intro; destruct n; rewrite <- (Int.repr_signed x), H; reflexivity.
diff --git a/lib/Integers.v b/lib/Integers.v
index 2c74e80..af9decd 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -227,7 +227,7 @@ Proof.
   intros. destruct x; destruct y. destruct (zeq intval0 intval1).
   left. apply mkint_eq. auto.
   right. red; intro. injection H. exact n.
-Qed.
+Defined.
 
 (** * Arithmetic and logical operations over machine integers *)
 
@@ -3711,4 +3711,4 @@ Module Int64 := Make(Wordsize_64).
 
 Notation int64 := Int64.int.
 
-
+Global Opaque Int.repr Int64.repr Byte.repr.
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 1c3c9cc..f2e85ec 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -48,7 +48,7 @@ Hypothesis step_decr: forall a a', step a = inr _ a' -> ord a' a.
 Definition step_info (a: A) : {b | step a = inl _ b} + {a' | step a = inr _ a' & ord a' a}.
 Proof.
   caseEq (step a); intros. left; exists b; auto. right; exists a0; auto. 
-Qed.
+Defined.
 
 Definition iterate_F (a: A) (rec: forall a', ord a' a -> B) : B :=
   match step_info a with
diff --git a/lib/Maps.v b/lib/Maps.v
index 0c97ba5..a0287a4 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -32,6 +32,7 @@
   inefficient implementation of maps as functions is also provided.
 *)
 
+Require Import EquivDec.
 Require Import Coqlib.
 
 (* To avoid useless definitions of inductors in extracted code. *)
@@ -79,9 +80,6 @@ Module Type TREE.
   Hypothesis grspec:
     forall (A: Type) (i j: elt) (m: t A),
     get i (remove j m) = if elt_eq i j then None else get i m.
-  Hypothesis set2:
-    forall (A: Type) (i: elt) (m: t A) (v1 v2: A),
-    set i v2 (set i v1 m) = set i v2 m.
 
   (** Extensional equality between trees. *)
   Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool.
@@ -144,17 +142,6 @@ Module Type TREE.
   Hypothesis elements_keys_norepet:
     forall (A: Type) (m: t A), 
     list_norepet (List.map (@fst elt A) (elements m)).
-  Hypothesis elements_canonical_order:
-    forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B),
-    (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) ->
-    (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) ->
-    list_forall2
-      (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
-      (elements m) (elements n).
-  Hypothesis elements_extensional:
-    forall (A: Type) (m n: t A),
-    (forall i, get i m = get i n) ->
-    elements m = elements n.
 
   (** Folding a function over all bindings of a tree. *)
   Variable fold:
@@ -200,8 +187,8 @@ Module PTree <: TREE.
 
   Inductive tree (A : Type) : Type :=
     | Leaf : tree A
-    | Node : tree A -> option A -> tree A -> tree A
-  .
+    | Node : tree A -> option A -> tree A -> tree A.
+
   Implicit Arguments Leaf [A].
   Implicit Arguments Node [A].
   Scheme tree_ind := Induction for tree Sort Prop.
@@ -378,15 +365,6 @@ Module PTree <: TREE.
     Variable A: Type.
     Variable eqA: A -> A -> Prop.
     Variable beqA: A -> A -> bool.
-    Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
-
-    Definition exteq (m1 m2: t A) : Prop :=
-      forall (x: elt),
-      match get x m1, get x m2 with
-      | None, None => True
-      | Some y1, Some y2 => eqA y1 y2
-      | _, _ => False
-      end.
 
     Fixpoint bempty (m: t A) : bool :=
       match m with
@@ -395,15 +373,6 @@ Module PTree <: TREE.
       | Node l (Some _) r => false
       end.
 
-    Lemma bempty_correct:
-      forall m, bempty m = true -> forall x, get x m = None.
-    Proof.
-      induction m; simpl; intros. 
-      change (@Leaf A) with (empty A). apply gempty.
-      destruct o. congruence. destruct (andb_prop _ _ H). 
-      destruct x; simpl; auto.
-    Qed.
-
     Fixpoint beq (m1 m2: t A) {struct m1} : bool :=
       match m1, m2 with
       | Leaf, _ => bempty m2
@@ -417,6 +386,36 @@ Module PTree <: TREE.
           && beq l1 l2 && beq r1 r2
       end.
 
+    Lemma bempty_correct:
+      forall m, bempty m = true -> forall x, get x m = None.
+    Proof.
+      induction m; simpl; intros. 
+      change (@Leaf A) with (empty A). apply gempty.
+      destruct o. congruence. destruct (andb_prop _ _ H). 
+      destruct x; simpl; auto.
+    Qed.
+
+    Lemma bempty_complete:
+      forall m, (forall x, get x m = None) -> bempty m = true.
+    Proof.
+      induction m; simpl; intros.
+      auto.
+      destruct o. generalize (H xH); simpl; congruence.
+      rewrite IHm1. rewrite IHm2. auto. 
+      intros; apply (H (xI x)).
+      intros; apply (H (xO x)).
+    Qed.
+
+    Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y.
+
+    Definition exteq (m1 m2: t A) : Prop :=
+      forall (x: elt),
+      match get x m1, get x m2 with
+      | None, None => True
+      | Some y1, Some y2 => eqA y1 y2
+      | _, _ => False
+      end.
+
     Lemma beq_correct:
       forall m1 m2, beq m1 m2 = true -> exteq m1 m2.
     Proof.
@@ -440,6 +439,25 @@ Module PTree <: TREE.
       auto.
     Qed.
 
+    Hypothesis beqA_complete: forall x y, eqA x y -> beqA x y = true.
+
+    Lemma beq_complete:
+      forall m1 m2, exteq m1 m2 -> beq m1 m2 = true.
+    Proof.
+      induction m1; destruct m2; simpl; intros. 
+      auto.
+      change (bempty (Node m2_1 o m2_2) = true).
+      apply bempty_complete. intros. generalize (H x). rewrite gleaf.
+      destruct (get x (Node m2_1 o m2_2)); tauto. 
+      change (bempty (Node m1_1 o m1_2) = true).
+      apply bempty_complete. intros. generalize (H x). rewrite gleaf.
+      destruct (get x (Node m1_1 o m1_2)); tauto.
+      apply andb_true_intro. split. apply andb_true_intro. split. 
+      generalize (H xH); simpl. destruct o; destruct o0; auto.
+      apply IHm1_1. red; intros. apply (H (xO x)). 
+      apply IHm1_2. red; intros. apply (H (xI x)). 
+    Qed.
+
   End EXTENSIONAL_EQUALITY.
 
     Fixpoint append (i j : positive) {struct i} : positive :=
diff --git a/lib/Ordered.v b/lib/Ordered.v
index ce1eca8..f52a7ef 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -42,7 +42,7 @@ Proof.
   apply EQ. red. apply Pos.compare_eq_iff. assumption.
   apply LT. assumption.
   apply GT. apply Pos.compare_gt_iff. assumption.
-Qed.
+Defined.
 
 Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
 
@@ -80,7 +80,7 @@ Proof.
   assert (Int.unsigned x <> Int.unsigned y).
     red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence.
   red. omega.
-Qed.
+Defined.
 
 Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec.
 
@@ -118,14 +118,14 @@ Proof.
   apply LT. exact l. 
   apply EQ. red; red in e. apply A.index_inj; auto.
   apply GT. exact l.
-Qed.
+Defined.
 
 Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 Proof.
   intros. case (peq (A.index x) (A.index y)); intros.
   left. apply A.index_inj; auto.
   right; red; unfold eq; intros; subst. congruence. 
-Qed.
+Defined.
 
 End OrderedIndexed.
 
@@ -208,7 +208,7 @@ Proof.
   apply EQ. red. tauto.
   apply GT. red. right. split. apply A.eq_sym. auto. auto.
   apply GT. red. left. auto.
-Qed.
+Defined.
 
 Lemma eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 Proof.
@@ -218,7 +218,7 @@ Proof.
   left; auto.
   right; intuition.
   right; intuition.
-Qed.
+Defined.
 
 End OrderedPair.