From 02779dbc71c0f6985427c47ec05dd25b44dd859c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Mar 2013 12:13:12 +0000 Subject: 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 --- lib/Coqlib.v | 3 +- lib/Floats.v | 1 + lib/Integers.v | 4 +-- lib/Iteration.v | 2 +- lib/Maps.v | 86 ++++++++++++++++++++++++++++++++++----------------------- lib/Ordered.v | 12 ++++---- 6 files changed, 64 insertions(+), 44 deletions(-) (limited to 'lib') 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. -- cgit v1.2.3