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 --- Changelog | 3 ++ arm/Asmgenproof.v | 3 +- arm/Asmgenproof1.v | 4 +- arm/Machregs.v | 2 +- arm/Op.v | 8 ++-- backend/CSE.v | 6 +-- backend/Constprop.v | 2 +- backend/Locations.v | 9 +++-- backend/RRE.v | 2 +- backend/Reloadproof.v | 4 +- backend/Stackingproof.v | 11 ------ cfrontend/Cexec.v | 7 ++-- cfrontend/Cshmgen.v | 7 +--- cfrontend/Initializersproof.v | 8 ++-- common/AST.v | 6 ++- common/Memdata.v | 1 + common/Memory.v | 37 +++++++++---------- ia32/Asmgenproof.v | 4 +- ia32/Machregs.v | 3 +- ia32/Op.v | 6 ++- lib/Coqlib.v | 3 +- lib/Floats.v | 1 + lib/Integers.v | 4 +- lib/Iteration.v | 2 +- lib/Maps.v | 86 ++++++++++++++++++++++++++----------------- lib/Ordered.v | 12 +++--- powerpc/Asmgenproof.v | 1 - powerpc/Asmgenproof1.v | 5 ++- powerpc/Op.v | 6 ++- 29 files changed, 133 insertions(+), 120 deletions(-) diff --git a/Changelog b/Changelog index 670a6d0..5bf7335 100644 --- a/Changelog +++ b/Changelog @@ -17,6 +17,9 @@ Development version that are passed on the call stack. - ARM port; slightly better code generated for some indirect memory accesses. +- Coq cleanups: a number of definitions that were opaque for no good reason + are now properly transparent. + Release 1.12.1, 2013-01-29 ========================== diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index dcae740..0760eb0 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -261,7 +261,7 @@ Qed. Remark transl_op_label: forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c. Proof. -Opaque Int.repr Int.eq. +Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. destruct (ireg_eq x x0 || ireg_eq x x1); TailNoLabel. @@ -671,7 +671,6 @@ Opaque loadind. Simpl. rewrite <- H2. auto. - (* Mtailcall *) -Opaque Int.repr. assert (f0 = f) by congruence. subst f0. inversion AT; subst. assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 9d90d1f..06d6d17 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -813,8 +813,8 @@ Proof. split. unfold rs3. Simpl. replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)). destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *. - rewrite B. simpl. Simpl. - rewrite B. simpl. unfold rs2. Simpl. + rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero. + rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl. auto. destruct cmp; reflexivity. intros. transitivity (rs2 r). diff --git a/arm/Machregs.v b/arm/Machregs.v index f5b5329..317515c 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -45,7 +45,7 @@ Inductive mreg: Type := | FT1: mreg (* F6 *) | FT2: mreg (* F7 *). Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. -Proof. decide equality. Qed. +Proof. decide equality. Defined. Definition mreg_type (r: mreg): typ := match r with diff --git a/arm/Op.v b/arm/Op.v index 291d64f..06d0705 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -137,7 +137,7 @@ Proof. subst x. rewrite (proof_irr Px Py). left; auto. right. red; intro. elim n. inversion H0. auto. decide equality. -Qed. +Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. @@ -148,14 +148,16 @@ Proof. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. assert (forall (x y: condition), {x=y}+{x<>y}). decide equality. decide equality. -Qed. +Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec; intro. generalize eq_shift; intro. decide equality. -Qed. +Defined. + +Global Opaque eq_shift eq_operation eq_addressing. (** * Evaluation functions *) diff --git a/backend/CSE.v b/backend/CSE.v index 1888fb8..45a804e 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -60,9 +60,7 @@ Inductive rhs : Type := Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq. Definition eq_list_valnum (x y: list valnum) : {x=y}+{x<>y}. -Proof. - decide equality. apply eq_valnum. -Qed. +Proof. decide equality. apply eq_valnum. Defined. Definition eq_rhs (x y: rhs) : {x=y}+{x<>y}. Proof. @@ -74,7 +72,7 @@ Proof. generalize eq_valnum; intro. generalize eq_list_valnum; intro. decide equality. -Qed. +Defined. (** A value numbering is a collection of equations between value numbers plus a partial map from registers to value numbers. Additionally, diff --git a/backend/Constprop.v b/backend/Constprop.v index 8fa0691..2f3123f 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -49,7 +49,7 @@ Module Approx <: SEMILATTICE_WITH_TOP. apply Int.eq_dec. apply ident_eq. apply Int.eq_dec. - Qed. + Defined. Definition beq (x y: t) := if eq_dec x y then true else false. Lemma beq_correct: forall x y, beq x y = true -> x = y. Proof. diff --git a/backend/Locations.v b/backend/Locations.v index ba2fb06..2381fea 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -89,7 +89,8 @@ Proof. decide equality. generalize zeq; intro. decide equality. -Qed. +Defined. +Global Opaque slot_eq. Open Scope Z_scope. @@ -122,7 +123,7 @@ Module Loc. Lemma eq: forall (p q: loc), {p = q} + {p <> q}. Proof. decide equality. apply mreg_eq. apply slot_eq. - Qed. + Defined. (** As mentioned previously, two locations can be different (in the sense of the [<>] mathematical disequality), yet denote @@ -286,7 +287,7 @@ Module Loc. case_eq (overlap l1 l2); intros. right. apply overlap_not_diff; auto. left. apply non_overlap_diff; auto. - Qed. + Defined. (** We now redefine some standard notions over lists, using the [Loc.diff] predicate instead of standard disequality [<>]. @@ -383,6 +384,8 @@ Module Loc. End Loc. +Global Opaque Loc.eq Loc.diff_dec. + (** * Mappings from locations to values *) (** The [Locmap] module defines mappings from locations to values, diff --git a/backend/RRE.v b/backend/RRE.v index ece6051..b8409e3 100644 --- a/backend/RRE.v +++ b/backend/RRE.v @@ -37,7 +37,7 @@ Fixpoint find_reg_containing (s: slot) (eqs: equations) : option mreg := Definition eq_equation (eq1 eq2: equation) : {eq1=eq2} + {eq1<>eq2}. Proof. generalize slot_eq mreg_eq. decide equality. -Qed. +Defined. Definition contains_equation (s: slot) (r: mreg) (eqs: equations) : bool := In_dec eq_equation (mkeq r s) eqs. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 1d49909..6402237 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -267,8 +267,8 @@ Proof. destruct s; unfold undef_getstack; unfold loc_acceptable in H; auto. apply Locmap.gso. tauto. apply Loc.diff_sym. simpl in H0; unfold t; destruct (slot_type s); tauto. - rewrite Locmap.gso. unfold undef_getstack. destruct s; auto. - apply Locmap.gso. red; congruence. + rewrite Locmap.gso. unfold undef_getstack. + destruct s; simpl in H; reflexivity || contradiction. unfold t; destruct (slot_type s); red; congruence. Qed. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 4ce8c25..d97ec93 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -779,9 +779,6 @@ Lemma agree_frame_set_reg: Proof. intros. inv H; constructor; auto; intros. rewrite Locmap.gso. auto. red. intuition congruence. - rewrite Locmap.gso; auto. red; auto. - rewrite Locmap.gso; auto. red; auto. - rewrite Locmap.gso; auto. red; auto. apply wt_setloc; auto. Qed. @@ -857,8 +854,6 @@ Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. constructor; auto; intros. -(* unused *) - rewrite Locmap.gso; auto. red; auto. (* local *) unfold Locmap.set. simpl. destruct (Loc.eq (S (Local ofs ty)) (S (Local ofs0 ty0))). inv e. eapply gss_index_contains_inj; eauto. @@ -867,8 +862,6 @@ Proof. (* outgoing *) rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. simpl; auto. red; auto. -(* incoming *) - rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto. red; auto. (* retaddr *) @@ -899,8 +892,6 @@ Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3. constructor; auto; intros. -(* unused *) - rewrite Locmap.gso; auto. red; auto. (* local *) rewrite Locmap.gso. eapply gso_index_contains_inj; eauto. simpl; auto. red; auto. (* outgoing *) @@ -911,8 +902,6 @@ Proof. red; intros. eapply Mem.perm_store_1; eauto. eapply gso_index_contains_inj; eauto. red. eapply Loc.overlap_aux_false_1; eauto. -(* incoming *) - rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto with stacking. red; auto. (* retaddr *) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index c638259..ebc27ad 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -92,7 +92,7 @@ Fixpoint is_val_list (al: exprlist) : option (list (val * type)) := Definition is_skip (s: statement) : {s = Sskip} + {s <> Sskip}. Proof. destruct s; (left; congruence) || (right; congruence). -Qed. +Defined. (** * Events, volatile memory accesses, and external functions. *) @@ -303,7 +303,7 @@ Proof with try (right; intuition omega). destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto. right; intuition omega. destruct Y... left; intuition omega. -Qed. +Defined. Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v: val): option (world * trace * mem) := match access_mode ty with @@ -464,7 +464,7 @@ Proof with try (right; intuition omega). destruct (zle (odst + sz) osrc); auto. right; intuition omega. destruct Y... left; intuition omega. -Qed. +Defined. Definition do_ef_memcpy (sz al: Z) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := @@ -2180,7 +2180,6 @@ Proof with (unfold ret; auto with coqlib). rewrite H0... rewrite H0... rewrite pred_dec_false... - rewrite pred_dec_true... rewrite H0... rewrite H0... destruct H0; subst x... diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 9d518cb..51f89da 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -486,11 +486,8 @@ Definition transl_function (f: Clight.function) : res function := (map fst (Clight.fn_temps f)) tbody). -Definition list_typ_eq: - forall (l1 l2: list typ), {l1=l2} + {l1<>l2}. -Proof. - generalize typ_eq; intro. decide equality. -Qed. +Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} + := list_eq_dec typ_eq. Definition transl_fundef (f: Clight.fundef) : res fundef := match f with diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index b64c309..b0884ac 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -397,13 +397,11 @@ Proof. Opaque zeq. intros. unfold sem_cmp in *. destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. - destruct (Int.eq n Int.zero); try discriminate. +- destruct (Int.eq n Int.zero); try discriminate. unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor. - destruct (Int.eq n Int.zero); try discriminate. +- destruct (Int.eq n Int.zero); try discriminate. unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor. - rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. - rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4. - destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. +- destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. Qed. Lemma sem_binary_match: 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. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 860f04c..060d018 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -879,8 +879,8 @@ Opaque loadind. intros [m3' [P Q]]. left; econstructor; split. apply plus_one. econstructor; eauto. - subst x; simpl. eauto. -Opaque Int.repr. + subst x; simpl. + rewrite Int.unsigned_zero. simpl. eauto. simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F. simpl in P. rewrite ATLR. rewrite P. eauto. econstructor; eauto. diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 9935efa..df96393 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -40,7 +40,8 @@ Inductive mreg: Type := | FT1: mreg (* X6 *) | FT2: mreg (* X7 *) | FP0: mreg (* top of FP stack *). Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. -Proof. decide equality. Qed. +Proof. decide equality. Defined. +Global Opaque mreg_eq. Definition mreg_type (r: mreg): typ := match r with diff --git a/ia32/Op.v b/ia32/Op.v index 66ee633..a23e8ac 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -124,7 +124,7 @@ Proof. generalize Int.eq_dec; intro. assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. decide equality. -Qed. +Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. @@ -135,7 +135,9 @@ Proof. assert (forall (x y: condition), {x=y}+{x<>y}). decide equality. decide equality. apply eq_addressing. -Qed. +Defined. + +Global Opaque eq_addressing eq_operation. (** * Evaluation functions *) 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. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 7699fef..658653f 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -642,7 +642,6 @@ Opaque loadind. Simpl. rewrite <- H2. auto. - (* Mtailcall *) -Opaque Int.repr. assert (f0 = f) by congruence. subst f0. inversion AT; subst. assert (NOOV: list_length_z tf <= Int.max_unsigned). diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 1e16a0d..0e6d3e1 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -84,7 +84,7 @@ Proof. set (x := Int.sub n (low_s n)). assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536)) (Int.modu x (Int.repr 65536))). - apply Int.modu_divu_Euclid. compute; congruence. + apply Int.modu_divu_Euclid. vm_compute; congruence. assert (Int.modu x (Int.repr 65536) = Int.zero). unfold Int.modu, Int.zero. decEq. change 0 with (0 mod 65536). @@ -710,6 +710,7 @@ Proof. assert (Int.unsigned (Int.not i) <> Int.modulus - 1). red; intros. assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone). +Local Transparent Int.repr. rewrite H1. apply Int.mkint_eq. reflexivity. rewrite Int.repr_unsigned in H2. assert (Int.not (Int.not i) = Int.zero). @@ -813,7 +814,7 @@ Lemma transl_op_correct_aux: match op with Omove => data_preg r = true | _ => nontemp_preg r = true end -> r <> preg_of res -> rs'#r = rs#r. Proof. -Opaque Int.eq. Opaque Int.repr. +Opaque Int.eq. intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl. (* Omove *) destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H. diff --git a/powerpc/Op.v b/powerpc/Op.v index a8936fe..110796b 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -120,14 +120,16 @@ Proof. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. assert (forall (x y: condition), {x=y}+{x<>y}). decide equality. decide equality. -Qed. +Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. generalize Int.eq_dec; intro. assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. decide equality. -Qed. +Defined. + +Global Opaque eq_addressing eq_operation. (** * Evaluation functions *) -- cgit v1.2.3