diff options
72 files changed, 638 insertions, 638 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index c1c3900c..9e6b2c98 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -870,7 +870,7 @@ Opaque loadind. save_lr ra_ofs (Pcfi_rel_offset ra_ofs' :: x0)) in *. set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 86be8c95..c5277e8d 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -298,7 +298,7 @@ Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with - | nil => Zmax 0 ofs + | nil => Z.max 0 ofs | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1) | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2) end. @@ -369,8 +369,8 @@ Proof. destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. omega. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. - (* long *) set (ir' := align ir 2) in *. assert (ofs <= align ofs 2) by (apply align_le; omega). @@ -395,17 +395,17 @@ Proof. destruct (zlt fr 8); destruct H. subst. apply freg_param_caller_save. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. auto. - eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. + subst. split. apply Z.le_ge. apply align_le. omega. auto. + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; omega. omega. Qed. Remark loc_arguments_sf_charact: forall tyl ofs p, - In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Zmax 0 ofs)) p. + In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Z.max 0 ofs)) p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_charact (Zmax 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Zmax 0 ofs1) l). + assert (X: forall ofs1 ofs2 l, loc_argument_charact (Z.max 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Z.max 0 ofs1) l). { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Zmax 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Zmax 0 ofs1)) p). + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Z.max 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Z.max 0 ofs1)) p). { destruct p; simpl; intuition eauto. } induction tyl; simpl loc_arguments_sf; intros. elim H. @@ -482,29 +482,29 @@ Proof. induction tyl; simpl; intros. omega. destruct a. - destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. set (ir' := align ir 2). destruct (zlt ir' 4); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (ofs0 + 1); eauto. omega. - destruct (zlt ir 4); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + apply Z.le_trans with (ofs0 + 1); eauto. omega. + destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (zlt fr 8); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. Qed. Remark size_arguments_sf_above: forall tyl ofs0, - Zmax 0 ofs0 <= size_arguments_sf tyl ofs0. + Z.max 0 ofs0 <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. omega. - destruct a; (eapply Zle_trans; [idtac|eauto]). + destruct a; (eapply Z.le_trans; [idtac|eauto]). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. @@ -516,9 +516,9 @@ Qed. Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. + intros; unfold size_arguments. apply Z.le_ge. assert (0 <= size_arguments_sf (sig_args s) (-4)). - { change 0 with (Zmax 0 (-4)). apply size_arguments_sf_above. } + { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. } assert (0 <= size_arguments_hf (sig_args s) 0 0 0). { apply size_arguments_hf_above. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. @@ -549,14 +549,14 @@ Proof. destruct H. discriminate. destruct H. discriminate. eauto. destruct Archi.big_endian. destruct H. inv H. - eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. destruct H. inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. eauto. destruct H. inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. destruct H. inv H. - eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. eauto. - (* float *) destruct (zlt fr 8); destruct H. @@ -581,7 +581,7 @@ Qed. Lemma loc_arguments_sf_bounded: forall ofs ty tyl ofs0, In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) -> - Zmax 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. + Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. Proof. induction tyl; simpl; intros. elim H. @@ -598,15 +598,15 @@ Proof. destruct H. destruct Archi.big_endian. destruct (zlt (align ofs0 2) 0); inv H. - eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. + eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. destruct H. destruct Archi.big_endian. destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. + rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. destruct (zlt (align ofs0 2) 0); inv H. - eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. + eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. eauto. - (* float *) destruct H. @@ -630,7 +630,7 @@ Proof. unfold loc_arguments, size_arguments; intros. assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) -> ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)). - { intros. eapply Zle_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } + { intros. eapply Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) -> ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0). { intros. eapply loc_arguments_hf_bounded; eauto. } @@ -522,7 +522,7 @@ End SOUNDNESS. Program Definition mk_shift_amount (n: int) : shift_amount := {| s_amount := Int.modu n Int.iwordsize; s_range := _ |}. Next Obligation. - assert (0 <= Zmod (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. + assert (0 <= Z.modulo (Int.unsigned n) 32 < 32). apply Z_mod_lt. omega. unfold Int.ltu, Int.modu. change (Int.unsigned Int.iwordsize) with 32. rewrite Int.unsigned_repr. apply zlt_true. omega. assert (32 < Int.max_unsigned). compute; auto. omega. @@ -983,7 +983,7 @@ Remark weak_valid_pointer_no_overflow_extends: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index 043393bf..462d83ad 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -133,7 +133,7 @@ Proof. set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); set (ostkdata := align (size_callee_save_area b ocs) 8). - split. apply Zdivide_0. + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. unfold ora, olink; auto using Z.divide_mul_l, Z.divide_add_r, Z.divide_refl. diff --git a/backend/Allocation.v b/backend/Allocation.v index 3ac99a47..cf62295d 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -404,11 +404,11 @@ Module OrderedEquation <: OrderedType. (OrderedLoc.lt (eloc x) (eloc y) \/ (eloc x = eloc y /\ OrderedEqKind.lt (ekind x) (ekind y)))). Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof (@sym_equal t). + Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof (@trans_equal t). + Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. @@ -466,11 +466,11 @@ Module OrderedEquation' <: OrderedType. (Plt (ereg x) (ereg y) \/ (ereg x = ereg y /\ OrderedEqKind.lt (ekind x) (ekind y)))). Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof (@sym_equal t). + Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof (@trans_equal t). + Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 6c10d27f..4b75e34d 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2444,7 +2444,7 @@ Proof. (* internal function *) - monadInv FUN. simpl in *. destruct (transf_function_inv _ _ EQ). - exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. rewrite H8; apply Z.le_refl. intros [m'' [U V]]. assert (WTRS: wt_regset env (init_regs args (fn_params f))). { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. } diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 0250628b..f6f03868 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -103,7 +103,7 @@ Lemma nextinstr_set_preg: (nextinstr (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one. Proof. intros. unfold nextinstr. rewrite Pregmap.gss. - rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. + rewrite Pregmap.gso. auto. apply not_eq_sym. apply preg_of_not_PC. Qed. Lemma undef_regs_other: @@ -211,7 +211,7 @@ Lemma agree_set_mreg: agree (Regmap.set r v ms) sp rs'. Proof. intros. destruct H. split; auto. - rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP. + rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP. intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. rewrite H1. auto. apply preg_of_data. red; intros; elim n. eapply preg_of_injective; eauto. diff --git a/backend/Bounds.v b/backend/Bounds.v index 93a4b504..fa695234 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -136,7 +136,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) := end. Definition max_over_list {A: Type} (valu: A -> Z) (l: list A) : Z := - List.fold_left (fun m l => Zmax m (valu l)) l 0. + List.fold_left (fun m l => Z.max m (valu l)) l 0. Definition max_over_instrs (valu: instruction -> Z) : Z := max_over_list valu f.(fn_code). @@ -161,10 +161,10 @@ Lemma max_over_list_pos: max_over_list valu l >= 0. Proof. intros until valu. unfold max_over_list. - assert (forall l z, fold_left (fun x y => Zmax x (valu y)) l z >= z). + assert (forall l z, fold_left (fun x y => Z.max x (valu y)) l z >= z). induction l; simpl; intros. - omega. apply Zge_trans with (Zmax z (valu a)). - auto. apply Zle_ge. apply Zmax1. auto. + omega. apply Zge_trans with (Z.max z (valu a)). + auto. apply Z.le_ge. apply Z.le_max_l. auto. Qed. Lemma max_over_slots_of_funct_pos: @@ -225,18 +225,18 @@ Qed. Program Definition function_bounds := {| used_callee_save := RegSet.elements record_regs_of_function; bound_local := max_over_slots_of_funct local_slot; - bound_outgoing := Zmax (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot); - bound_stack_data := Zmax f.(fn_stacksize) 0 + bound_outgoing := Z.max (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot); + bound_stack_data := Z.max f.(fn_stacksize) 0 |}. Next Obligation. apply max_over_slots_of_funct_pos. Qed. Next Obligation. - apply Zle_ge. eapply Zle_trans. 2: apply Zmax2. - apply Zge_le. apply max_over_slots_of_funct_pos. + apply Z.le_ge. eapply Z.le_trans. 2: apply Z.le_max_r. + apply Z.ge_le. apply max_over_slots_of_funct_pos. Qed. Next Obligation. - apply Zle_ge. apply Zmax2. + apply Z.le_ge. apply Z.le_max_r. Qed. Next Obligation. generalize (RegSet.elements_3w record_regs_of_function). @@ -304,15 +304,15 @@ Lemma max_over_list_bound: Proof. intros until x. unfold max_over_list. assert (forall c z, - let f := fold_left (fun x y => Zmax x (valu y)) c z in + let f := fold_left (fun x y => Z.max x (valu y)) c z in z <= f /\ (In x c -> valu x <= f)). induction c; simpl; intros. split. omega. tauto. - elim (IHc (Zmax z (valu a))); intros. - split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto. + elim (IHc (Z.max z (valu a))); intros. + split. apply Z.le_trans with (Z.max z (valu a)). apply Z.le_max_l. auto. intro H1; elim H1; intro. - subst a. apply Zle_trans with (Zmax z (valu x)). - apply Zmax2. auto. auto. + subst a. apply Z.le_trans with (Z.max z (valu x)). + apply Z.le_max_r. auto. auto. intro. elim (H l 0); intros. auto. Qed. @@ -329,7 +329,7 @@ Lemma max_over_slots_of_funct_bound: valu s <= max_over_slots_of_funct valu. Proof. intros. unfold max_over_slots_of_funct. - apply Zle_trans with (max_over_slots_of_instr valu i). + apply Z.le_trans with (max_over_slots_of_instr valu i). unfold max_over_slots_of_instr. apply max_over_list_bound. auto. apply max_over_instrs_bound. auto. Qed. @@ -447,9 +447,9 @@ Proof. Local Opaque mreg_type. induction l as [ | r l]; intros; simpl. - omega. -- eapply Zle_trans. 2: apply IHl. +- eapply Z.le_trans. 2: apply IHl. generalize (AST.typesize_pos (mreg_type r)); intros. - apply Zle_trans with (align ofs (AST.typesize (mreg_type r))). + apply Z.le_trans with (align ofs (AST.typesize (mreg_type r))). apply align_le; auto. omega. Qed. diff --git a/backend/CSE.v b/backend/CSE.v index 4fa1bd6c..bc3fdba5 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -50,7 +50,7 @@ Definition valnum_reg (n: numbering) (r: reg) : numbering * valnum := | Some v => (n, v) | None => let v := n.(num_next) in - ( {| num_next := Psucc v; + ( {| num_next := Pos.succ v; num_eqs := n.(num_eqs); num_reg := PTree.set r v n.(num_reg); num_val := PMap.set v (r :: nil) n.(num_val) |}, @@ -161,7 +161,7 @@ Definition add_rhs (n: numbering) (rd: reg) (rh: rhs) : numbering := num_reg := PTree.set rd vres n.(num_reg); num_val := update_reg n rd vres |} | None => - {| num_next := Psucc n.(num_next); + {| num_next := Pos.succ n.(num_next); num_eqs := Eq n.(num_next) true rh :: n.(num_eqs); num_reg := PTree.set rd n.(num_next) n.(num_reg); num_val := update_reg n rd n.(num_next) |} @@ -331,7 +331,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) := let j := i + delta in if zle src i && zle (i + size_chunk chunk) (src + sz) - && zeq (Zmod delta (align_chunk chunk)) 0 + && zeq (Z.modulo delta (align_chunk chunk)) 0 && zle 0 j && zle j Ptrofs.max_unsigned then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil)) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 8516e384..d6bde348 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -35,8 +35,8 @@ Remark wf_equation_incr: wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e. Proof. unfold wf_equation; intros; destruct e. destruct H. split. - apply Plt_le_trans with next1; auto. - red; intros. apply Plt_le_trans with next1; auto. apply H1; auto. + apply Pos.lt_le_trans with next1; auto. + red; intros. apply Pos.lt_le_trans with next1; auto. apply H1; auto. Qed. (** Extensionality with respect to valuations. *) @@ -95,7 +95,7 @@ Proof. - auto. - apply equation_holds_exten. auto. eapply wf_equation_incr; eauto with cse. -- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto. +- rewrite AGREE. eauto. eapply Pos.lt_le_trans; eauto. eapply wf_num_reg; eauto. Qed. End EXTEN. @@ -523,7 +523,7 @@ Proof. exists valu3. constructor; simpl; intros. + constructor; simpl; intros; eauto with cse. destruct H4; eauto with cse. subst e. split. - eapply Plt_le_trans; eauto. + eapply Pos.lt_le_trans; eauto. red; simpl; intros. auto. + destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src). apply load_eval_to with a. rewrite <- Q; auto. @@ -1187,7 +1187,7 @@ Proof. - (* internal function *) monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ. destruct (analyze cu f) as [approx|] eqn:?; inv EQ. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros (m'' & A & B). econstructor; split. eapply exec_function_internal; simpl; eauto. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b14c4be0..e28519ca 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -493,7 +493,7 @@ Opaque builtin_strength_reduction. assert (C: cmatch (eval_condition cond rs ## args m) ac) by (eapply eval_static_condition_sound; eauto with va). rewrite H0 in C. - generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)). + generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (eq_refl _)). destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args']. intros EV1 TCODE. left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m'); split. @@ -532,7 +532,7 @@ Opaque builtin_strength_reduction. destruct or; simpl; auto. - (* internal function *) - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m2' [A B]]. simpl. unfold transf_function. left; exists O; econstructor; split. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index e23fdfd3..ca6ad649 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -69,7 +69,7 @@ Proof. - replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto. - eauto. - exploit mi_memval; eauto. unfold inject_id; eauto. - rewrite Zplus_0_r. auto. + rewrite Z.add_0_r. auto. - auto. Qed. @@ -79,9 +79,9 @@ Lemma magree_extends: magree m1 m2 P -> Mem.extends m1 m2. Proof. intros. destruct H0. constructor; auto. constructor; unfold inject_id; intros. -- inv H0. rewrite Zplus_0_r. eauto. -- inv H0. apply Zdivide_0. -- inv H0. rewrite Zplus_0_r. eapply ma_memval0; eauto. +- inv H0. rewrite Z.add_0_r. eauto. +- inv H0. apply Z.divide_0_r. +- inv H0. rewrite Z.add_0_r. eapply ma_memval0; eauto. Qed. Lemma magree_loadbytes: @@ -97,7 +97,7 @@ Proof. { induction n; intros; simpl. constructor. - rewrite inj_S in H. constructor. + rewrite Nat2Z.inj_succ in H. constructor. apply H. omega. apply IHn. intros; apply H; omega. } @@ -131,7 +131,7 @@ Lemma magree_storebytes_parallel: magree m1 m2 P -> Mem.storebytes m1 b ofs bytes1 = Some m1' -> (forall b' i, Q b' i -> - b' <> b \/ i < ofs \/ ofs + Z_of_nat (length bytes1) <= i -> + b' <> b \/ i < ofs \/ ofs + Z.of_nat (length bytes1) <= i -> P b' i) -> list_forall2 memval_lessdef bytes1 bytes2 -> exists m2', Mem.storebytes m2 b ofs bytes2 = Some m2' /\ magree m1' m2' Q. @@ -146,7 +146,7 @@ Proof. { induction 1; intros; simpl. - apply H; auto. simpl. omega. - - simpl length in H1; rewrite inj_S in H1. + - simpl length in H1; rewrite Nat2Z.inj_succ in H1. apply IHlist_forall2; auto. intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto. apply H1; auto. unfold ZIndexed.t in *; omega. @@ -200,7 +200,7 @@ Lemma magree_storebytes_left: forall m1 m2 P b ofs bytes1 m1', magree m1 m2 P -> Mem.storebytes m1 b ofs bytes1 = Some m1' -> - (forall i, ofs <= i < ofs + Z_of_nat (length bytes1) -> ~(P b i)) -> + (forall i, ofs <= i < ofs + Z.of_nat (length bytes1) -> ~(P b i)) -> magree m1' m2 P. Proof. intros. constructor; intros. @@ -1081,7 +1081,7 @@ Ltac UseTransfer := - (* internal function *) monadInv FUN. generalize EQ. unfold transf_function. fold (vanalyze cu f). intros EQ'. destruct (analyze (vanalyze cu f) f) as [an|] eqn:AN; inv EQ'. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros (tm' & A & B). econstructor; split. econstructor; simpl; eauto. diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v index 0b8ff3c7..d31c63ec 100644 --- a/backend/Debugvarproof.v +++ b/backend/Debugvarproof.v @@ -157,11 +157,11 @@ Proof. - intuition congruence. - destruct (Pos.compare_spec v v0); simpl in H1. + subst v0. destruct H1. inv H1; auto. right; split. - apply sym_not_equal. apply Plt_ne. eapply H; eauto. + apply not_eq_sym. apply Plt_ne. eapply H; eauto. auto. + destruct H1. inv H1; auto. - destruct H1. inv H1. right; split; auto. apply sym_not_equal. apply Plt_ne. auto. - right; split; auto. apply sym_not_equal. apply Plt_ne. apply Plt_trans with v0; eauto. + destruct H1. inv H1. right; split; auto. apply not_eq_sym. apply Plt_ne. auto. + right; split; auto. apply not_eq_sym. apply Plt_ne. apply Plt_trans with v0; eauto. + destruct H1. inv H1. right; split; auto. apply Plt_ne. auto. destruct IHwf_avail as [A | [A B]]; auto. Qed. @@ -211,9 +211,9 @@ Proof. induction 1; simpl; intros. - contradiction. - destruct (Pos.compare_spec v v0); simpl in H1. -+ subst v0. split; auto. apply sym_not_equal; apply Plt_ne; eauto. -+ destruct H1. inv H1. split; auto. apply sym_not_equal; apply Plt_ne; eauto. - split; auto. apply sym_not_equal; apply Plt_ne. apply Plt_trans with v0; eauto. ++ subst v0. split; auto. apply not_eq_sym; apply Plt_ne; eauto. ++ destruct H1. inv H1. split; auto. apply not_eq_sym; apply Plt_ne; eauto. + split; auto. apply not_eq_sym; apply Plt_ne. apply Plt_trans with v0; eauto. + destruct H1. inv H1. split; auto. apply Plt_ne; auto. destruct IHwf_avail as [A B] ; auto. Qed. diff --git a/backend/Inlining.v b/backend/Inlining.v index 17139dbd..91cc119d 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -113,7 +113,7 @@ Program Definition add_instr (i: instruction): mon node := fun s => let pc := s.(st_nextnode) in R pc - (mkstate s.(st_nextreg) (Psucc pc) (PTree.set pc i s.(st_code)) s.(st_stksize)) + (mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -122,7 +122,7 @@ Qed. Program Definition reserve_nodes (numnodes: positive): mon positive := fun s => R s.(st_nextnode) - (mkstate s.(st_nextreg) (Pplus s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize)) + (mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -131,7 +131,7 @@ Qed. Program Definition reserve_regs (numregs: positive): mon positive := fun s => R s.(st_nextreg) - (mkstate (Pplus s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize)) + (mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -140,7 +140,7 @@ Qed. Program Definition request_stack (sz: Z): mon unit := fun s => R tt - (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Zmax s.(st_stksize) sz)) + (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz)) _. Next Obligation. intros; constructor; simpl; xomega. @@ -181,7 +181,7 @@ Record context: Type := mkcontext { (** The following functions "shift" (relocate) PCs, registers, operations, etc. *) -Definition shiftpos (p amount: positive) := Ppred (Pplus p amount). +Definition shiftpos (p amount: positive) := Pos.pred (Pos.add p amount). Definition spc (ctx: context) (pc: node) := shiftpos pc ctx.(dpc). @@ -220,7 +220,7 @@ Definition initcontext (dpc dreg nreg: positive) (sz: Z) := dreg := dreg; dstk := 0; mreg := nreg; - mstk := Zmax sz 0; + mstk := Z.max sz 0; retinfo := None |}. (** The context used to inline a call to another function. *) @@ -237,7 +237,7 @@ Definition callcontext (ctx: context) dreg := dreg; dstk := align (ctx.(dstk) + ctx.(mstk)) (min_alignment sz); mreg := nreg; - mstk := Zmax sz 0; + mstk := Z.max sz 0; retinfo := Some (spc ctx retpc, sreg ctx retreg) |}. (** The context used to inline a tail call to another function. *) @@ -247,7 +247,7 @@ Definition tailcontext (ctx: context) (dpc dreg nreg: positive) (sz: Z) := dreg := dreg; dstk := align ctx.(dstk) (min_alignment sz); mreg := nreg; - mstk := Zmax sz 0; + mstk := Z.max sz 0; retinfo := ctx.(retinfo) |}. (** ** Recursive expansion and copying of a CFG *) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index c3b0cfc3..2dcb8956 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -184,7 +184,7 @@ Proof. unfold agree_regs; intros. destruct H. split; intros. rewrite H0. auto. apply shiftpos_above. - eapply Plt_le_trans. apply shiftpos_below. xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. xomega. apply H1; auto. Qed. @@ -242,7 +242,7 @@ Proof. split. destruct H3 as [[P Q] | [P Q]]. subst a1. eapply agree_set_reg_undef; eauto. eapply agree_set_reg; eauto. rewrite C; auto. apply context_below_lt; auto. - intros. rewrite Regmap.gso. auto. apply sym_not_equal. eapply sreg_below_diff; eauto. + intros. rewrite Regmap.gso. auto. apply not_eq_sym. eapply sreg_below_diff; eauto. destruct H2; discriminate. Qed. @@ -290,10 +290,10 @@ Lemma range_private_alloc_left: Mem.alloc m 0 sz = (m1, sp) -> F1 sp = Some(sp', base) -> (forall b, b <> sp -> F1 b = F b) -> - range_private F1 m1 m' sp' (base + Zmax sz 0) hi. + range_private F1 m1 m' sp' (base + Z.max sz 0) hi. Proof. intros; red; intros. - exploit (H ofs). generalize (Zmax2 sz 0). omega. intros [A B]. + exploit (H ofs). generalize (Z.le_max_r sz 0). omega. intros [A B]. split; auto. intros; red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b sp); intros. @@ -304,14 +304,14 @@ Qed. Lemma range_private_free_left: forall F m m' sp base sz hi b m1, - range_private F m m' sp (base + Zmax sz 0) hi -> + range_private F m m' sp (base + Z.max sz 0) hi -> Mem.free m b 0 sz = Some m1 -> F b = Some(sp, base) -> Mem.inject F m m' -> range_private F m1 m' sp base hi. Proof. intros; red; intros. - destruct (zlt ofs (base + Zmax sz 0)) as [z|z]. + destruct (zlt ofs (base + Z.max sz 0)) as [z|z]. red; split. replace ofs with ((ofs - base) + base) by omega. eapply Mem.perm_inject; eauto. @@ -560,8 +560,8 @@ Lemma match_stacks_bound: Proof. intros. inv H. apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto. - eapply match_stacks_cons; eauto. eapply Plt_le_trans; eauto. - eapply match_stacks_untailcall; eauto. eapply Plt_le_trans; eauto. + eapply match_stacks_cons; eauto. eapply Pos.lt_le_trans; eauto. + eapply match_stacks_untailcall; eauto. eapply Pos.lt_le_trans; eauto. Qed. Variable F1: meminj. @@ -602,7 +602,7 @@ Proof. (* nil *) apply match_stacks_nil with (bound1 := bound1). inv MG. constructor; auto. - intros. apply IMAGE with delta. eapply INJ; eauto. eapply Plt_le_trans; eauto. + intros. apply IMAGE with delta. eapply INJ; eauto. eapply Pos.lt_le_trans; eauto. auto. auto. (* cons *) apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto. @@ -768,8 +768,8 @@ Proof. destruct (zle sz 4). omegaContradiction. auto. destruct chunk; simpl in *; auto. - apply Zone_divide. - apply Zone_divide. + apply Z.divide_1_l. + apply Z.divide_1_l. apply H2; omega. apply H2; omega. Qed. @@ -845,7 +845,7 @@ Proof. intros. inv H. (* base *) eapply match_stacks_inside_base; eauto. congruence. - rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Zdivide_0. + rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Z.divide_0_r. (* inlined *) assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos. eapply match_stacks_inside_inlined; eauto. @@ -1164,7 +1164,7 @@ Proof. assert (TR: tr_function prog f f'). { eapply tr_function_linkorder; eauto. } inversion TR; subst. - exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. + exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. instantiate (1 := fn_stacksize f'). inv H1. xomega. intros [F' [m1' [sp' [A [B [C [D E]]]]]]]. left; econstructor; split. @@ -1203,7 +1203,7 @@ Proof. (* sp' is valid *) instantiate (1 := sp'). auto. (* offset is representable *) - instantiate (1 := dstk ctx). generalize (Zmax2 (fn_stacksize f) 0). omega. + instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). omega. (* size of target block is representable *) intros. right. exploit SSZ2; eauto with mem. inv FB; omega. (* we have full permissions on sp' at and above dstk ctx *) diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index d79132d6..6e8a94a6 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -105,7 +105,7 @@ Proof. Qed. Lemma shiftpos_below: - forall x n, Plt (shiftpos x n) (Pplus x n). + forall x n, Plt (shiftpos x n) (Pos.add x n). Proof. intros. unfold Plt; zify. rewrite shiftpos_eq. omega. Qed. @@ -250,7 +250,7 @@ Section INLINING_SPEC. Variable fenv: funenv. Definition context_below (ctx1 ctx2: context): Prop := - Ple (Pplus ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg). + Ple (Pos.add ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg). Definition context_stack_call (ctx1 ctx2: context): Prop := ctx1.(mstk) >= 0 /\ ctx1.(dstk) + ctx1.(mstk) <= ctx2.(dstk). @@ -331,7 +331,7 @@ with tr_funbody: context -> function -> code -> Prop := | tr_funbody_intro: forall ctx f c, (forall r, In r f.(fn_params) -> Ple r ctx.(mreg)) -> (forall pc i, f.(fn_code)!pc = Some i -> tr_instr ctx pc i c) -> - ctx.(mstk) = Zmax f.(fn_stacksize) 0 -> + ctx.(mstk) = Z.max f.(fn_stacksize) 0 -> (min_alignment f.(fn_stacksize) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> ctx.(dstk) + ctx.(mstk) <= stacksize -> tr_funbody ctx f c. @@ -451,9 +451,9 @@ Hypothesis rec_spec: fenv_agree fe' -> Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) -> ctx.(mreg) = max_reg_function f -> - Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) -> + Ple (Pos.add ctx.(dreg) ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> - ctx.(mstk) = Zmax (fn_stacksize f) 0 -> + ctx.(mstk) = Z.max (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> @@ -599,7 +599,7 @@ Proof. elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto. (* older pc *) inv_incr. eapply IHl; eauto. - intros. eapply Plt_le_trans. eapply H2. right; eauto. xomega. + intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. xomega. intros; eapply Ple_trans; eauto. intros. apply H7; auto. xomega. Qed. @@ -611,7 +611,7 @@ Lemma expand_cfg_rec_spec: ctx.(mreg) = max_reg_function f -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> - ctx.(mstk) = Zmax (fn_stacksize f) 0 -> + ctx.(mstk) = Z.max (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> @@ -629,13 +629,13 @@ Proof. intros. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Plt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. subst s0; simpl; auto. intros. apply H8; auto. subst s0; simpl in H11; xomega. intros. apply H8. apply shiftpos_above. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Plt_le_trans. apply shiftpos_below. inversion i; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; xomega. apply PTree.elements_correct; auto. auto. auto. auto. inversion INCR0. subst s0; simpl in STKSIZE; xomega. @@ -664,7 +664,7 @@ Lemma expand_cfg_spec: ctx.(mreg) = max_reg_function f -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> - ctx.(mstk) = Zmax (fn_stacksize f) 0 -> + ctx.(mstk) = Z.max (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> @@ -724,7 +724,7 @@ Opaque initstate. unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega. simpl. xomega. - simpl. apply Zdivide_0. + simpl. apply Z.divide_0_r. simpl. omega. simpl. omega. simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. diff --git a/backend/Kildall.v b/backend/Kildall.v index a2b49d56..8e712c05 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -1373,7 +1373,7 @@ Proof. replace (st1.(aval)!!pc) with res!!pc. fold l. destruct (basic_block_map s) eqn:BB. rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto. - elim (C H0 (refl_equal _)). intros X Y. rewrite Y. apply L.refl_ge. + elim (C H0 (eq_refl _)). intros X Y. rewrite Y. apply L.refl_ge. elim (U pc); intros E F. rewrite F. reflexivity. destruct (In_dec peq pc (successors instr)). right. eapply no_self_loop; eauto. diff --git a/backend/Locations.v b/backend/Locations.v index ca148761..c437df5d 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -471,11 +471,11 @@ Module OrderedLoc <: OrderedType. (ofs1 < ofs2 \/ (ofs1 = ofs2 /\ OrderedTyp.lt ty1 ty2))) end. Lemma eq_refl : forall x : t, eq x x. - Proof (@refl_equal t). + Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. - Proof (@sym_equal t). + Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - Proof (@trans_equal t). + Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. @@ -542,12 +542,12 @@ Module OrderedLoc <: OrderedType. intros. destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto. - assert (IndexedMreg.index mr <> IndexedMreg.index mr'). - { destruct H. apply sym_not_equal. apply Plt_ne; auto. apply Plt_ne; auto. } + { destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. } congruence. - assert (RANGE: forall ty, 1 <= typesize ty <= 2). { intros; unfold typesize. destruct ty0; omega. } destruct H. - + destruct H. left. apply sym_not_equal. apply OrderedSlot.lt_not_eq; auto. + + destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto. destruct H. right. destruct H0. right. generalize (RANGE ty'); omega. destruct H0. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 8e8b9c0b..d431f3d8 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -329,7 +329,7 @@ Lemma eqmod_iagree: Proof. intros. set (p := nat_of_Z (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. } rewrite EQ in H; rewrite <- two_power_nat_two_p in H. red; intros. rewrite ! Int.testbit_repr by auto. destruct (zlt i (Int.size m)). @@ -347,7 +347,7 @@ Lemma iagree_eqmod: Proof. intros. set (p := nat_of_Z (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. } rewrite EQ; rewrite <- two_power_nat_two_p. apply Int.eqmod_same_bits. intros. apply H. omega. unfold complete_mask. rewrite Int.bits_zero_ext by omega. @@ -829,7 +829,7 @@ Let weak_valid_pointer_no_overflow: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - unfold inject_id; intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Let valid_different_pointers_inj: @@ -1003,9 +1003,9 @@ Module NVal <: SEMILATTICE. Definition t := nval. Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Definition eq_refl: forall x, eq x x := (@eq_refl t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t). Definition beq (x y: t) : bool := proj_sumbool (eq_nval x y). Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. unfold beq; intros. InvBooleans. auto. Qed. diff --git a/backend/RTL.v b/backend/RTL.v index d191918c..16723d96 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -437,7 +437,7 @@ Definition instr_defs (i: instruction) : option reg := the CFG of [f] are between 1 and [max_pc_function f] (inclusive). *) Definition max_pc_function (f: function) := - PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive. + PTree.fold (fun m pc i => Pos.max m pc) f.(fn_code) 1%positive. Lemma max_pc_function_sound: forall f pc i, f.(fn_code)!pc = Some i -> Ple pc (max_pc_function f). @@ -461,32 +461,32 @@ Qed. Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := match i with | Inop s => m - | Iop op args res s => fold_left Pmax args (Pmax res m) - | Iload chunk addr args dst s => fold_left Pmax args (Pmax dst m) - | Istore chunk addr args src s => fold_left Pmax args (Pmax src m) - | Icall sig (inl r) args res s => fold_left Pmax args (Pmax r (Pmax res m)) - | Icall sig (inr id) args res s => fold_left Pmax args (Pmax res m) - | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m) - | Itailcall sig (inr id) args => fold_left Pmax args m + | Iop op args res s => fold_left Pos.max args (Pos.max res m) + | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) + | Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m) + | Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) + | Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) + | Itailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m) + | Itailcall sig (inr id) args => fold_left Pos.max args m | Ibuiltin ef args res s => - fold_left Pmax (params_of_builtin_args args) - (fold_left Pmax (params_of_builtin_res res) m) - | Icond cond args ifso ifnot => fold_left Pmax args m - | Ijumptable arg tbl => Pmax arg m + fold_left Pos.max (params_of_builtin_args args) + (fold_left Pos.max (params_of_builtin_res res) m) + | Icond cond args ifso ifnot => fold_left Pos.max args m + | Ijumptable arg tbl => Pos.max arg m | Ireturn None => m - | Ireturn (Some arg) => Pmax arg m + | Ireturn (Some arg) => Pos.max arg m end. Definition max_reg_function (f: function) := - Pmax + Pos.max (PTree.fold max_reg_instr f.(fn_code) 1%positive) - (fold_left Pmax f.(fn_params) 1%positive). + (fold_left Pos.max f.(fn_params) 1%positive). Remark max_reg_instr_ge: forall m pc i, Ple m (max_reg_instr m pc i). Proof. intros. - assert (X: forall l n, Ple m n -> Ple m (fold_left Pmax l n)). + assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)). { induction l; simpl; intros. auto. apply IHl. xomega. } @@ -498,7 +498,7 @@ Remark max_reg_instr_def: forall m pc i r, instr_defs i = Some r -> Ple r (max_reg_instr m pc i). Proof. intros. - assert (X: forall l n, Ple r n -> Ple r (fold_left Pmax l n)). + assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. xomega. apply IHl. xomega. } destruct i; simpl in *; inv H. - apply X. xomega. @@ -511,7 +511,7 @@ Remark max_reg_instr_uses: forall m pc i r, In r (instr_uses i) -> Ple r (max_reg_instr m pc i). Proof. intros. - assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)). + assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } @@ -564,11 +564,11 @@ Lemma max_reg_function_params: forall f r, In r f.(fn_params) -> Ple r (max_reg_function f). Proof. intros. - assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)). + assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } - assert (Y: Ple r (fold_left Pmax f.(fn_params) 1%positive)). + assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)). { apply X; auto. } unfold max_reg_function. xomega. Qed. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 6d81f84b..9d7a8506 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -161,7 +161,7 @@ Definition init_state : state := Remark add_instr_wf: forall s i pc, let n := s.(st_nextnode) in - Plt pc (Psucc n) \/ (PTree.set n i s.(st_code))!pc = None. + Plt pc (Pos.succ n) \/ (PTree.set n i s.(st_code))!pc = None. Proof. intros. case (peq pc n); intro. subst pc; left; apply Plt_succ. @@ -175,7 +175,7 @@ Remark add_instr_incr: forall s i, let n := s.(st_nextnode) in state_incr s (mkstate s.(st_nextreg) - (Psucc n) + (Pos.succ n) (PTree.set n i s.(st_code)) (add_instr_wf s i)). Proof. @@ -189,7 +189,7 @@ Definition add_instr (i: instruction) : mon node := fun s => let n := s.(st_nextnode) in OK n - (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code)) + (mkstate s.(st_nextreg) (Pos.succ n) (PTree.set n i s.(st_code)) (add_instr_wf s i)) (add_instr_incr s i). @@ -199,7 +199,7 @@ Definition add_instr (i: instruction) : mon node := Remark reserve_instr_wf: forall s pc, - Plt pc (Psucc s.(st_nextnode)) \/ s.(st_code)!pc = None. + Plt pc (Pos.succ s.(st_nextnode)) \/ s.(st_code)!pc = None. Proof. intros. elim (st_wf s pc); intro. left; apply Plt_trans_succ; auto. @@ -210,7 +210,7 @@ Remark reserve_instr_incr: forall s, let n := s.(st_nextnode) in state_incr s (mkstate s.(st_nextreg) - (Psucc n) + (Pos.succ n) s.(st_code) (reserve_instr_wf s)). Proof. @@ -224,7 +224,7 @@ Definition reserve_instr: mon node := fun (s: state) => let n := s.(st_nextnode) in OK n - (mkstate s.(st_nextreg) (Psucc n) s.(st_code) (reserve_instr_wf s)) + (mkstate s.(st_nextreg) (Pos.succ n) s.(st_code) (reserve_instr_wf s)) (reserve_instr_incr s). Remark update_instr_wf: @@ -275,7 +275,7 @@ Definition update_instr (n: node) (i: instruction) : mon unit := Remark new_reg_incr: forall s, - state_incr s (mkstate (Psucc s.(st_nextreg)) + state_incr s (mkstate (Pos.succ s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)). Proof. constructor; simpl. apply Ple_refl. apply Ple_succ. auto. @@ -284,7 +284,7 @@ Qed. Definition new_reg : mon reg := fun s => OK s.(st_nextreg) - (mkstate (Psucc s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)) + (mkstate (Pos.succ s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf)) (new_reg_incr s). (** ** Operations on mappings *) @@ -651,7 +651,7 @@ Definition alloc_label (lbl: Cminor.label) (maps: labelmap * state) : labelmap * let (map, s) := maps in let n := s.(st_nextnode) in (PTree.set lbl n map, - mkstate s.(st_nextreg) (Psucc s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)). + mkstate s.(st_nextreg) (Pos.succ s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)). Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) {struct s} : labelmap * state := diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 93f209b7..072db138 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -301,7 +301,7 @@ Proof. destruct (map_letvars x0). auto. simpl in me_letvars0. inversion me_letvars0. intros. rewrite Regmap.gso. apply UNDEF. apply reg_fresh_decr with s2; eauto with rtlg. - apply sym_not_equal. apply valid_fresh_different with s2; auto. + apply not_eq_sym. apply valid_fresh_different with s2; auto. Qed. Lemma match_set_locals: @@ -1535,7 +1535,7 @@ Proof. assert (map_valid init_mapping s0) by apply init_mapping_valid. exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B]. eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf. - edestruct Mem.alloc_extends as [tm' []]; eauto; try apply Zle_refl. + edestruct Mem.alloc_extends as [tm' []]; eauto; try apply Z.le_refl. econstructor; split. left; apply plus_one. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index fe5bfe28..75713289 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -36,7 +36,7 @@ Lemma Zdiv_mul_pos: two_p (N+l) <= m * d <= two_p (N+l) + two_p l -> forall n, 0 <= n < two_p N -> - Zdiv n d = Zdiv (m * n) (two_p (N + l)). + Z.div n d = Z.div (m * n) (two_p (N + l)). Proof. intros m l l_pos [LO HI] n RANGE. exploit (Z_div_mod_eq n d). auto. @@ -54,9 +54,9 @@ Proof. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. assert (0 <= k * n). - apply Zmult_le_0_compat; omega. + apply Z.mul_nonneg_nonneg; omega. assert (k * n <= two_p (N + l) - two_p l). - apply Zle_trans with (two_p l * n). + apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. replace (N + l) with (l + N) by omega. rewrite two_p_is_exp. @@ -66,7 +66,7 @@ Proof. apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. omega. omega. assert (0 <= two_p (N + l) * r). - apply Zmult_le_0_compat. + apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). @@ -81,7 +81,7 @@ Proof. assert (m * n - two_p (N + l) * q < two_p (N + l)). apply Zmult_lt_reg_r with d. omega. rewrite H2. - apply Zle_lt_trans with (two_p (N + l) * d - two_p l). + apply Z.le_lt_trans with (two_p (N + l) * d - two_p l). omega. exploit (two_p_gt_ZERO l). omega. omega. symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). @@ -89,7 +89,7 @@ Proof. Qed. Lemma Zdiv_unique_2: - forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1. + forall x y q, y > 0 -> 0 < y * q - x <= y -> Z.div x y = q - 1. Proof. intros. apply Zdiv_unique with (x - (q - 1) * y). ring. replace ((q - 1) * y) with (y * q - y) by ring. omega. @@ -101,7 +101,7 @@ Lemma Zdiv_mul_opp: two_p (N+l) < m * d <= two_p (N+l) + two_p l -> forall n, 0 < n <= two_p N -> - Zdiv n d = - Zdiv (m * (-n)) (two_p (N + l)) - 1. + Z.div n d = - Z.div (m * (-n)) (two_p (N + l)) - 1. Proof. intros m l l_pos [LO HI] n RANGE. replace (m * (-n)) with (- (m * n)) by ring. @@ -114,7 +114,7 @@ Proof. assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. exploit (two_p_gt_ZERO (N + l)). omega. omega. - cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1). + cut (Z.div (- (m * n)) (two_p (N + l)) = -q - 1). omega. apply Zdiv_unique_2. apply two_p_gt_ZERO. omega. @@ -130,15 +130,15 @@ Proof. apply Zmult_lt_reg_r with d. omega. replace (0 * d) with 0 by omega. rewrite H2. - assert (0 < k * n). apply Zmult_lt_0_compat; omega. + assert (0 < k * n). apply Z.mul_pos_pos; omega. assert (0 <= two_p (N + l) * r). - apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega. + apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); omega. omega. omega. apply Zmult_le_reg_r with d. omega. rewrite H2. assert (k * n <= two_p (N + l)). - rewrite Zplus_comm. rewrite two_p_is_exp; try omega. - apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. + rewrite Z.add_comm. rewrite two_p_is_exp; try omega. + apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) @@ -156,7 +156,7 @@ Lemma Zquot_mul: two_p (N+l) < m * d <= two_p (N+l) + two_p l -> forall n, - two_p N <= n < two_p N -> - Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). + Z.quot n d = Z.div (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). Proof. intros. destruct (zlt n 0). exploit (Zdiv_mul_opp m l H H0 (-n)). omega. @@ -164,7 +164,7 @@ Proof. replace (Z.quot n d) with (- Z.quot (-n) d). rewrite Zquot_Zdiv_pos by omega. omega. rewrite Z.quot_opp_l by omega. ring. - rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. + rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by omega. apply Zdiv_mul_pos; omega. Qed. @@ -178,7 +178,7 @@ Lemma divs_mul_params_sound: 0 <= m < Int.modulus /\ 0 <= p < 32 /\ forall n, Int.min_signed <= n <= Int.max_signed -> - Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). + Z.quot n d = Z.div (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). Proof with (try discriminate). unfold divs_mul_params; intros d m' p'. destruct (find_div_mul_params Int.wordsize @@ -207,7 +207,7 @@ Lemma divu_mul_params_sound: 0 <= m < Int.modulus /\ 0 <= p < 32 /\ forall n, 0 <= n < Int.modulus -> - Zdiv n d = Zdiv (m * n) (two_p (32 + p)). + Z.div n d = Z.div (m * n) (two_p (32 + p)). Proof with (try discriminate). unfold divu_mul_params; intros d m' p'. destruct (find_div_mul_params Int.wordsize @@ -246,9 +246,9 @@ Proof. unfold Int.max_signed; omega. apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. apply Int.modulus_pos. - split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. + split. apply Z.le_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto. - apply Zle_lt_trans with (Int.half_modulus * m). + apply Z.le_lt_trans with (Int.half_modulus * m). apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto. apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. assert (32 < Int.max_unsigned) by (compute; auto). omega. @@ -310,7 +310,7 @@ Proof. unfold Int.max_unsigned; omega. apply Zdiv_interval_1. omega. compute; auto. compute; auto. split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. - apply Zle_lt_trans with (Int.modulus * m). + apply Z.le_lt_trans with (Int.modulus * m). apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. apply Zmult_lt_compat_l. compute; auto. omega. unfold Int.max_unsigned; omega. @@ -325,7 +325,7 @@ Lemma divls_mul_params_sound: 0 <= m < Int64.modulus /\ 0 <= p < 64 /\ forall n, Int64.min_signed <= n <= Int64.max_signed -> - Z.quot n d = Zdiv (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0). + Z.quot n d = Z.div (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0). Proof with (try discriminate). unfold divls_mul_params; intros d m' p'. destruct (find_div_mul_params Int64.wordsize @@ -354,7 +354,7 @@ Lemma divlu_mul_params_sound: 0 <= m < Int64.modulus /\ 0 <= p < 64 /\ forall n, 0 <= n < Int64.modulus -> - Zdiv n d = Zdiv (m * n) (two_p (64 + p)). + Z.div n d = Z.div (m * n) (two_p (64 + p)). Proof with (try discriminate). unfold divlu_mul_params; intros d m' p'. destruct (find_div_mul_params Int64.wordsize @@ -399,9 +399,9 @@ Proof. unfold Int64.max_signed; omega. apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos. apply Int64.modulus_pos. - split. apply Zle_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega. + split. apply Z.le_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega. apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto. - apply Zle_lt_trans with (Int64.half_modulus * m). + apply Z.le_lt_trans with (Int64.half_modulus * m). apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto. apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto. assert (64 < Int.max_unsigned) by (compute; auto). omega. @@ -469,7 +469,7 @@ Proof. unfold Int64.max_unsigned; omega. apply Zdiv_interval_1. omega. compute; auto. compute; auto. split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega. - apply Zle_lt_trans with (Int64.modulus * m). + apply Z.le_lt_trans with (Int64.modulus * m). apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega. apply Zmult_lt_compat_l. compute; auto. omega. unfold Int64.max_unsigned; omega. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index ebc64c6f..86d7ff21 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -209,7 +209,7 @@ Lemma eval_load: Proof. intros. generalize H0; destruct v; simpl; intro; try discriminate. unfold load. - generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)). destruct (addressing chunk a). intros [vl [EV EQ]]. eapply eval_Eload; eauto. Qed. @@ -224,7 +224,7 @@ Lemma eval_store: Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. - generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)). destruct (addressing chunk a1). intros [vl [EV EQ]]. eapply step_store; eauto. Qed. @@ -1036,7 +1036,7 @@ Proof. - (* internal function *) destruct TF as (hf & HF & TF). specialize (MC cunit hf). monadInv TF. generalize EQ; intros TF; monadInv TF. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m2' [A B]]. left; econstructor; split. econstructor; simpl; eauto. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d3d901b6..f7570f57 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -133,7 +133,7 @@ Qed. Remark bound_stack_data_stacksize: f.(Linear.fn_stacksize) <= b.(bound_stack_data). Proof. - unfold b, function_bounds, bound_stack_data. apply Zmax1. + unfold b, function_bounds, bound_stack_data. apply Z.le_max_l. Qed. (** * Memory assertions used to describe the contents of stack frames *) @@ -217,7 +217,7 @@ Proof. - red; intros. apply Mem.perm_implies with Freeable; auto with mem. apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. - rewrite align_type_chunk. apply Z.divide_add_r. - apply Zdivide_trans with 8; auto. + apply Z.divide_trans with 8; auto. exists (8 / (4 * typealign ty)); destruct ty; reflexivity. apply Z.mul_divide_mono_l. auto. Qed. @@ -962,7 +962,7 @@ Local Opaque mreg_type. assert (SZREC: pos1 + sz <= size_callee_save_area_rec l (pos1 + sz)) by (apply size_callee_save_area_rec_incr). assert (POS1: pos <= pos1) by (apply align_le; auto). assert (AL1: (align_chunk (chunk_of_type ty) | pos1)). - { unfold pos1. apply Zdivide_trans with sz. + { unfold pos1. apply Z.divide_trans with sz. unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides. apply align_divides; auto. } apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. @@ -1984,7 +1984,7 @@ Proof. econstructor; eauto with coqlib. apply Val.Vptr_has_type. intros; red. - apply Zle_trans with (size_arguments (Linear.funsig f')); auto. + apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. apply loc_arguments_bounded; auto. simpl; red; auto. simpl. rewrite sep_assoc. exact SEP. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 6acf2bbd..c6644ceb 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -505,7 +505,7 @@ Proof. eapply exec_Lreturn; eauto. constructor; eauto using return_regs_lessdef, match_parent_locset. - (* internal function *) - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros (tm' & ALLOC & MEM'). left; simpl; econstructor; split. eapply exec_function_internal; eauto. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 446ffb7f..7899a04c 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -835,7 +835,7 @@ Proof. - econstructor; eauto with barg. - econstructor; eauto with barg. - econstructor; eauto with barg. -- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. +- simpl in H. exploit Mem.load_inject; eauto. rewrite Z.add_0_r. intros (v' & A & B). exists v'; auto with barg. - econstructor; split; eauto with barg. simpl. econstructor; eauto. rewrite Ptrofs.add_zero; auto. - assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). @@ -956,7 +956,7 @@ Proof. eapply match_stacks_preserves_globals; eauto. eauto. destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto. intros (A & B). - exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D). + exploit Mem.free_parallel_inject; eauto. rewrite ! Z.add_0_r. intros (tm' & C & D). econstructor; split. eapply exec_Itailcall; eauto. econstructor; eauto. @@ -999,7 +999,7 @@ Proof. econstructor; eauto. - (* return *) - exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D). + exploit Mem.free_parallel_inject; eauto. rewrite ! Z.add_0_r. intros (tm' & C & D). econstructor; split. eapply exec_Ireturn; eauto. econstructor; eauto. @@ -1011,7 +1011,7 @@ Proof. destruct or; simpl; auto. - (* internal function *) - exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros (j' & tm' & tstk & C & D & E & F & G). assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto). @@ -1124,7 +1124,7 @@ Lemma Mem_getN_forall2: Proof. induction n; simpl Mem.getN; intros. - simpl in H1. omegaContradiction. -- inv H. rewrite inj_S in H1. destruct (zeq i p0). +- inv H. rewrite Nat2Z.inj_succ in H1. destruct (zeq i p0). + congruence. + apply IHn with (p0 + 1); auto. omega. omega. Qed. @@ -1145,7 +1145,7 @@ Proof. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. apply P2. omega. - exploit init_meminj_invert; eauto. intros (A & id & B & C). - subst delta. apply Zdivide_0. + subst delta. apply Z.divide_0_r. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). exploit (Genv.init_mem_characterization_gen p); eauto. exploit (Genv.init_mem_characterization_gen tp); eauto. @@ -1159,7 +1159,7 @@ Proof. Local Transparent Mem.loadbytes. generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1. generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2. - rewrite Zplus_0_r. + rewrite Z.add_0_r. apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))). rewrite H3, H4. apply bytes_of_init_inject. auto. omega. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 7c4c0525..8aa4878a 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -875,7 +875,7 @@ Proof. apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r. + (* below *) red; simpl; intros. destruct (eq_block b sp). - subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. + subst b. apply Pos.lt_le_trans with bound. apply BELOW. congruence. auto. eapply mmatch_below; eauto. - (* genv *) eapply genv_match_exten; eauto. @@ -1008,7 +1008,7 @@ Proof. + apply SMTOP; auto. + apply SMTOP; auto. + red; simpl; intros. destruct (plt b (Mem.nextblock m)). - eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. + eapply Pos.lt_le_trans. eauto. eapply external_call_nextblock; eauto. destruct (j' b) as [[bx deltax] | ] eqn:J'. eapply Mem.valid_block_inject_1; eauto. congruence. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f905ffa2..d7eaa228 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -750,7 +750,7 @@ Definition sgn (p: aptr) (n: Z) : aval := if zle n 8 then Sgn p 8 else if zle n 16 then Sgn p 16 else Ifptr p. Lemma vmatch_uns': - forall p i n, is_uns (Zmax 0 n) i -> vmatch (Vint i) (uns p n). + forall p i n, is_uns (Z.max 0 n) i -> vmatch (Vint i) (uns p n). Proof. intros. assert (A: forall n', n' >= 0 -> n' >= n -> is_uns n' i) by (eauto with va). @@ -780,7 +780,7 @@ Proof. Qed. Lemma vmatch_sgn': - forall p i n, is_sgn (Zmax 1 n) i -> vmatch (Vint i) (sgn p n). + forall p i n, is_sgn (Z.max 1 n) i -> vmatch (Vint i) (sgn p n). Proof. intros. assert (A: forall n', n' >= 1 -> n' >= n -> is_sgn n' i) by (eauto with va). @@ -3476,7 +3476,7 @@ Lemma ablock_storebytes_contents: forall ab p i sz j chunk' av', (ablock_storebytes ab p i sz).(ab_contents)##j = Some(ACval chunk' av') -> ab.(ab_contents)##j = Some (ACval chunk' av') - /\ (j + size_chunk chunk' <= i \/ i + Zmax sz 0 <= j). + /\ (j + size_chunk chunk' <= i \/ i + Z.max sz 0 <= j). Proof. unfold ablock_storebytes; simpl; intros. exploit inval_before_contents; eauto. clear H. intros [A B]. @@ -4284,13 +4284,13 @@ Proof. intros. constructor. constructor. - (* perms *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. auto. + rewrite Z.add_0_r. auto. - (* alignment *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - apply Zdivide_0. + apply Z.divide_0_r. - (* contents *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. + rewrite Z.add_0_r. set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))). assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)). { @@ -4317,10 +4317,10 @@ Proof. auto. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r. split. omega. apply Ptrofs.unsigned_range_2. + rewrite Z.add_0_r. split. omega. apply Ptrofs.unsigned_range_2. - (* perm inv *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Zplus_0_r in H2. auto. + rewrite Z.add_0_r in H2. auto. Qed. Lemma inj_of_bc_preserves_globals: @@ -4371,9 +4371,9 @@ Module AVal <: SEMILATTICE_WITH_TOP. Definition t := aval. Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Definition eq_refl: forall x, eq x x := (@eq_refl t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t). Definition beq (x y: t) : bool := proj_sumbool (eq_aval x y). Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. unfold beq; intros. InvBooleans. auto. Qed. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index a9ffcd3d..15818317 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -1769,7 +1769,7 @@ Lemma not_stuckred_imm_safe: Proof. intros. generalize (step_expr_sound a k m). intros [A B]. destruct (step_expr k a m) as [|[C rd] res] eqn:?. - specialize (B (refl_equal _)). destruct k. + specialize (B (eq_refl _)). destruct k. destruct a; simpl in B; try congruence. constructor. destruct a; simpl in B; try congruence. constructor. assert (NOTSTUCK: rd <> Stuckred). diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 5017fc8e..45c21f96 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -226,7 +226,7 @@ Definition assign_variable let (id, sz) := id_sz in let (cenv, stacksize) := cenv_stacksize in let ofs := align stacksize (block_alignment sz) in - (PTree.set id ofs cenv, ofs + Zmax 0 sz). + (PTree.set id ofs cenv, ofs + Z.max 0 sz). Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z := List.fold_left assign_variable vars cenv_stacksize. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a6d58f17..ffafc5d2 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -96,7 +96,7 @@ Proof. intros m1 FR1 FRL. transitivity (Mem.load chunk m1 b ofs). eapply IHfbl; eauto. intros. eapply H. eauto with coqlib. - eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib. + eapply Mem.load_free; eauto. left. apply not_eq_sym. eapply H. auto with coqlib. Qed. Lemma perm_freelist: @@ -775,7 +775,7 @@ Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Pro PTree.get id cenv = Some ofs /\ Mem.inj_offset_aligned ofs sz /\ 0 <= ofs - /\ ofs + Zmax 0 sz <= tsz. + /\ ofs + Z.max 0 sz <= tsz. Definition cenv_separated (cenv: compilenv) (vars: list (ident * Z)) : Prop := forall id1 sz1 ofs1 id2 sz2 ofs2, @@ -901,7 +901,7 @@ Remark assign_variable_incr: Proof. simpl; intros. inv H. generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)). - assert (0 <= Zmax 0 sz). apply Zmax_bound_l. omega. + assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega. omega. Qed. @@ -914,7 +914,7 @@ Proof. Opaque assign_variable. destruct a as [id s]. simpl. intros. destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. - apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto. + apply Z.le_trans with sz1. eapply assign_variable_incr; eauto. eauto. Transparent assign_variable. Qed. @@ -925,8 +925,8 @@ Proof. intros; red; intros. apply Zdivides_trans with (block_alignment sz). unfold align_chunk. unfold block_alignment. - generalize Zone_divide; intro. - generalize Zdivide_refl; intro. + generalize Z.divide_1_l; intro. + generalize Z.divide_refl; intro. assert (2 | 4). exists 2; auto. assert (2 | 8). exists 4; auto. assert (4 | 8). exists 2; auto. @@ -942,10 +942,10 @@ Qed. Remark inj_offset_aligned_block': forall stacksize sz, - Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Zmax 0 sz). + Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz). Proof. intros. - replace (block_alignment sz) with (block_alignment (Zmax 0 sz)). + replace (block_alignment sz) with (block_alignment (Z.max 0 sz)). apply inj_offset_aligned_block. rewrite Zmax_spec. destruct (zlt sz 0); auto. transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 8d6cdb24..036b768b 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -373,15 +373,15 @@ Lemma sizeof_alignof_compat: forall env t, naturally_aligned t -> (alignof env t | sizeof env t). Proof. induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. -- apply Zdivide_refl. -- destruct i; apply Zdivide_refl. +- apply Z.divide_refl. +- destruct i; apply Z.divide_refl. - exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. -- apply Zdivide_refl. +- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. +- apply Z.divide_refl. - apply Z.divide_mul_l; auto. -- apply Zdivide_refl. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- apply Z.divide_refl. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. Qed. (** ** Size and alignment for composite definitions *) @@ -435,9 +435,9 @@ Lemma sizeof_struct_incr: Proof. induction m as [|[id t]]; simpl; intros. - omega. -- apply Zle_trans with (align cur (alignof env t)). +- apply Z.le_trans with (align cur (alignof env t)). apply align_le. apply alignof_pos. - apply Zle_trans with (align cur (alignof env t) + sizeof env t). + apply Z.le_trans with (align cur (alignof env t) + sizeof env t). generalize (sizeof_pos env t); omega. apply IHm. Qed. @@ -488,7 +488,7 @@ Proof. inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. exploit IHfld; eauto. intros [A B]. split; auto. - eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)). + eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)). apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. Qed. @@ -627,7 +627,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := Lemma alignof_blockcopy_1248: forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. Proof. - assert (X: forall co, let a := Zmin 8 (co_alignof co) in + assert (X: forall co, let a := Z.min 8 (co_alignof co) in a = 1 \/ a = 2 \/ a = 4 \/ a = 8). { intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. @@ -635,7 +635,7 @@ Proof. destruct n; auto. destruct n; auto. right; right; right. apply Z.min_l. - rewrite two_power_nat_two_p. rewrite ! inj_S. + rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ. change 8 with (two_p 3). apply two_p_monotone. omega. } induction ty; simpl. @@ -661,28 +661,28 @@ Lemma sizeof_alignof_blockcopy_compat: Proof. assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)). { - intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof. + intros. apply Z.divide_trans with (co_alignof co). 2: apply co_sizeof_alignof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. apply Z.min_case. exists (two_p (Z.of_nat n)). change 8 with (two_p 3). rewrite <- two_p_is_exp by omega. - rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. - apply Zdivide_refl. + rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega. + apply Z.divide_refl. } induction ty; simpl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. apply Z.divide_mul_l. auto. - apply Zdivide_refl. - destruct (env!i). apply X. apply Zdivide_0. - destruct (env!i). apply X. apply Zdivide_0. + apply Z.divide_refl. + destruct (env!i). apply X. apply Z.divide_0_r. + destruct (env!i). apply X. apply Z.divide_0_r. Qed. (** Type ranks *) @@ -707,7 +707,7 @@ Fixpoint rank_type (ce: composite_env) (t: type) : nat := Fixpoint rank_members (ce: composite_env) (m: members) : nat := match m with | nil => 0%nat - | (id, t) :: m => Peano.max (rank_type ce t) (rank_members ce m) + | (id, t) :: m => Init.Nat.max (rank_type ce t) (rank_members ce m) end. (** ** C types and back-end types *) @@ -818,7 +818,7 @@ Program Definition composite_of_def co_sizeof_alignof := _ |} end. Next Obligation. - apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. + apply Z.le_ge. eapply Z.le_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. Defined. Next Obligation. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 388b6544..77d6cfea 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -186,7 +186,7 @@ Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer) | Init_single a, _ => do d <- transl_init_single ce ty a; OK (d :: k) | Init_array il, Tarray tyelt nelt _ => - transl_init_array ce tyelt il (Zmax 0 nelt) k + transl_init_array ce tyelt il (Z.max 0 nelt) k | Init_struct il, Tstruct id _ => do co <- lookup_composite ce id; match co_su co with diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 524bc631..272b929f 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -486,7 +486,7 @@ Inductive tr_init: type -> initializer -> list init_data -> Prop := transl_init_single ge ty a = OK d -> tr_init ty (Init_single a) (d :: nil) | tr_init_arr: forall tyelt nelt attr il d, - tr_init_array tyelt il (Zmax 0 nelt) d -> + tr_init_array tyelt il (Z.max 0 nelt) d -> tr_init (Tarray tyelt nelt attr) (Init_array il) d | tr_init_str: forall id attr il co d, lookup_composite ge id = OK co -> co_su co = Struct -> @@ -723,7 +723,7 @@ Local Opaque sizeof. + rewrite idlsize_app, padding_size. exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. - apply Zle_trans with (sizeof_union ge (co_members co)). + apply Z.le_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite H0. apply align_le. @@ -816,9 +816,9 @@ Lemma store_init_data_list_app: Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''. Proof. induction data1; simpl; intros. - inv H. rewrite Zplus_0_r in H0. auto. + inv H. rewrite Z.add_0_r in H0. auto. destruct (Genv.store_init_data ge m b ofs a); try discriminate. - rewrite Zplus_assoc in H0. eauto. + rewrite Z.add_assoc in H0. eauto. Qed. Remark store_init_data_list_padding: @@ -874,7 +874,7 @@ Local Opaque sizeof. eapply store_init_data_list_app. eauto. rewrite (tr_init_size _ _ _ H9). - rewrite <- Zplus_assoc. eapply H2. eauto. eauto. + rewrite <- Z.add_assoc. eapply H2. eauto. eauto. apply align_le. apply alignof_pos. Qed. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 0a191f29..45b686f3 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -80,7 +80,7 @@ Definition initial_generator (x: unit) : generator := Definition gensym (ty: type): mon ident := fun (g: generator) => Res (gen_next g) - (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g)) + (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g)) (Ple_succ (gen_next g)). (** Construct a sequence from a list of statements. To facilitate the diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 8ed924e5..7af499f4 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -604,7 +604,7 @@ Proof. destruct (peq id id0). inv A. right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C. - subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. + subst b. split. apply Ple_refl. eapply Pos.lt_le_trans; eauto. rewrite B. apply Plt_succ. auto. right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. Qed. @@ -696,7 +696,7 @@ Proof. (* variable is not lifted out of memory *) exploit Mem.alloc_parallel_inject. - eauto. eauto. apply Zle_refl. apply Zle_refl. + eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [j1 [tm1 [tb1 [A [B [C [D E]]]]]]]. exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te). intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]]. @@ -778,8 +778,8 @@ Proof. apply IHalloc_variables. red; intros. rewrite PTree.gsspec in H2. destruct (peq id0 id). inv H2. eapply Mem.load_alloc_same'; eauto. - omega. rewrite Zplus_0_l. eapply sizeof_by_value; eauto. - apply Zdivide_0. + omega. rewrite Z.add_0_l. eapply sizeof_by_value; eauto. + apply Z.divide_0_r. eapply Mem.load_alloc_other; eauto. Qed. @@ -1053,7 +1053,7 @@ Proof. assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). - replace (sizeof tge ty) with (Z_of_nat (length bytes)). + replace (sizeof tge ty) with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). diff --git a/common/AST.v b/common/AST.v index 9eeca5b1..a072ef29 100644 --- a/common/AST.v +++ b/common/AST.v @@ -214,7 +214,7 @@ Definition init_data_size (i: init_data) : Z := | Init_float32 _ => 4 | Init_float64 _ => 8 | Init_addrof _ _ => if Archi.ptr64 then 8 else 4 - | Init_space n => Zmax n 0 + | Init_space n => Z.max n 0 end. Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := diff --git a/common/Behaviors.v b/common/Behaviors.v index ef99b205..92bd708f 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -187,7 +187,7 @@ CoFixpoint build_traceinf' (s1: state L) (t1: trace) (ST: Star L s0 t1 s1) : tra match reacts' ST with | existT s2 (exist t2 (conj A B)) => Econsinf' t2 - (build_traceinf' (star_trans ST A (refl_equal _))) + (build_traceinf' (star_trans ST A (eq_refl _))) B end. diff --git a/common/Events.v b/common/Events.v index ab804aa7..63922bc5 100644 --- a/common/Events.v +++ b/common/Events.v @@ -999,7 +999,7 @@ Proof. assert (SZ: v2 = Vptrofs sz). { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } subst v2. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros [m3' [A B]]. exploit Mem.store_within_extends. eexact B. eauto. eauto. intros [m2' [C D]]. @@ -1011,11 +1011,11 @@ Proof. assert (SZ: v' = Vptrofs sz). { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } subst v'. - exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_parallel_inject; eauto. apply Z.le_refl. apply Z.le_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. instantiate (1 := Vptrofs sz). unfold Vptrofs; destruct Archi.ptr64; constructor. - rewrite Zplus_0_r. intros [m2' [E G]]. + rewrite Z.add_0_r. intros [m2' [E G]]. exists f'; exists (Vptr b' Ptrofs.zero); exists m2'; intuition auto. econstructor; eauto. econstructor. eauto. auto. @@ -1206,7 +1206,7 @@ Proof. assert (RPSRC: Mem.range_perm m1 bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sz) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty). - replace sz with (Z_of_nat (length bytes)). + replace sz with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty). diff --git a/common/Globalenvs.v b/common/Globalenvs.v index dd8a1eb9..72b48529 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -229,7 +229,7 @@ Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (PTree.set ge.(genv_next) idg#2 ge.(genv_defs)) - (Psucc ge.(genv_next)) + (Pos.succ ge.(genv_next)) _ _ _. Next Obligation. destruct ge; simpl in *. @@ -567,7 +567,7 @@ Proof. Qed. Definition advance_next (gl: list (ident * globdef F V)) (x: positive) := - List.fold_left (fun n g => Psucc n) gl x. + List.fold_left (fun n g => Pos.succ n) gl x. Remark genv_next_add_globals: forall gl ge, @@ -722,7 +722,7 @@ Qed. Remark alloc_global_nextblock: forall g m m', alloc_global m g = Some m' -> - Mem.nextblock m' = Psucc(Mem.nextblock m). + Mem.nextblock m' = Pos.succ(Mem.nextblock m). Proof. unfold alloc_global. intros. destruct g as [id [f|v]]. @@ -896,10 +896,10 @@ Lemma store_zeros_loadbytes: Proof. intros until n; functional induction (store_zeros m b p n); red; intros. - destruct n0. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. omegaContradiction. + rewrite Nat2Z.inj_succ in H1. omegaContradiction. - destruct (zeq p0 p). + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. rewrite inj_S. + rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ. replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega. change (list_repeat (S n0) (Byte Byte.zero)) with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). @@ -1052,7 +1052,7 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s /\ load_store_init_data m b (p + size_chunk Mptr) il' | Init_space n :: il' => read_as_zero m b p n - /\ load_store_init_data m b (p + Zmax n 0) il' + /\ load_store_init_data m b (p + Z.max n 0) il' end. Lemma store_init_data_list_charact: @@ -1425,7 +1425,7 @@ Remark advance_next_le: forall gl x, Ple x (advance_next gl x). Proof. induction gl; simpl; intros. apply Ple_refl. - apply Ple_trans with (Psucc x). apply Ple_succ. eauto. + apply Ple_trans with (Pos.succ x). apply Ple_succ. eauto. Qed. Lemma alloc_globals_neutral: @@ -1440,7 +1440,7 @@ Proof. exploit alloc_globals_nextblock; eauto. intros EQ. simpl in *. destruct (alloc_global ge m a) as [m1|] eqn:E; try discriminate. exploit alloc_global_neutral; eauto. - assert (Ple (Psucc (Mem.nextblock m)) (Mem.nextblock m')). + assert (Ple (Pos.succ (Mem.nextblock m)) (Mem.nextblock m')). { rewrite EQ. apply advance_next_le. } unfold Plt, Ple in *; zify; omega. Qed. diff --git a/common/Memdata.v b/common/Memdata.v index 0aed4644..a9ed48b4 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -53,7 +53,7 @@ Definition size_chunk_nat (chunk: memory_chunk) : nat := nat_of_Z(size_chunk chunk). Lemma size_chunk_conv: - forall chunk, size_chunk chunk = Z_of_nat (size_chunk_nat chunk). + forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk). Proof. intros. destruct chunk; reflexivity. Qed. @@ -111,7 +111,7 @@ Qed. Lemma align_size_chunk_divides: forall chunk, (align_chunk chunk | size_chunk chunk). Proof. - intros. destruct chunk; simpl; try apply Zdivide_refl; exists 2; auto. + intros. destruct chunk; simpl; try apply Z.divide_refl; exists 2; auto. Qed. Lemma align_le_divides: @@ -120,7 +120,7 @@ Lemma align_le_divides: Proof. intros. destruct chunk1; destruct chunk2; simpl in *; solve [ omegaContradiction - | apply Zdivide_refl + | apply Z.divide_refl | exists 2; reflexivity | exists 4; reflexivity | exists 8; reflexivity ]. @@ -209,15 +209,15 @@ Qed. Lemma int_of_bytes_of_int: forall n x, - int_of_bytes (bytes_of_int n x) = x mod (two_p (Z_of_nat n * 8)). + int_of_bytes (bytes_of_int n x) = x mod (two_p (Z.of_nat n * 8)). Proof. induction n; intros. simpl. rewrite Zmod_1_r. auto. Opaque Byte.wordsize. - rewrite inj_S. simpl. - replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. + rewrite Nat2Z.inj_succ. simpl. + replace (Z.succ (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. + rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_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. @@ -232,7 +232,7 @@ Proof. Qed. Lemma decode_encode_int: - forall n x, decode_int (encode_int n x) = x mod (two_p (Z_of_nat n * 8)). + forall n x, decode_int (encode_int n x) = x mod (two_p (Z.of_nat n * 8)). Proof. unfold decode_int, encode_int; intros. rewrite rev_if_be_involutive. apply int_of_bytes_of_int. @@ -272,19 +272,19 @@ Qed. Lemma bytes_of_int_mod: forall n x y, - Int.eqmod (two_p (Z_of_nat n * 8)) x y -> + Int.eqmod (two_p (Z.of_nat n * 8)) x y -> bytes_of_int n x = bytes_of_int n y. Proof. induction n. intros; simpl; auto. intros until y. - rewrite inj_S. - replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. + rewrite Nat2Z.inj_succ. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. rewrite two_p_is_exp; try omega. intro EQM. simpl; decEq. apply Byte.eqm_samerepr. red. - eapply Int.eqmod_divides; eauto. apply Zdivide_factor_l. + eapply Int.eqmod_divides; eauto. apply Z.divide_factor_r. apply IHn. destruct EQM as [k EQ]. exists k. rewrite EQ. rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. @@ -354,7 +354,7 @@ Fixpoint check_value (n: nat) (v: val) (q: quantity) (vl: list memval) match n, vl with | O, nil => true | S m, Fragment v' q' m' :: vl' => - Val.eq v v' && quantity_eq q q' && beq_nat m m' && check_value m v q vl' + Val.eq v v' && quantity_eq q q' && Nat.eqb m m' && check_value m v q vl' | _, _ => false end. @@ -728,7 +728,7 @@ Proof. destruct (size_quantity_nat_pos q) as [sz EQ]. rewrite EQ. simpl. unfold proj_sumbool. rewrite dec_eq_true. destruct (quantity_eq q q0); auto. - destruct (beq_nat sz n) eqn:EQN; auto. + destruct (Nat.eqb sz n) eqn:EQN; auto. destruct (check_value sz v q mvl) eqn:CHECK; auto. simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. @@ -943,22 +943,22 @@ Qed. Lemma int_of_bytes_append: forall l2 l1, - int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z_of_nat (length l1) * 8). + int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z.of_nat (length l1) * 8). Proof. induction l1; simpl int_of_bytes; intros. simpl. ring. - simpl length. rewrite inj_S. - replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z_of_nat (length l1) * 8 + 8) by omega. + simpl length. rewrite Nat2Z.inj_succ. + replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega. rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring. omega. omega. Qed. Lemma int_of_bytes_range: - forall l, 0 <= int_of_bytes l < two_p (Z_of_nat (length l) * 8). + forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8). Proof. induction l; intros. simpl. omega. - simpl length. rewrite inj_S. + simpl length. rewrite Nat2Z.inj_succ. replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega. rewrite two_p_is_exp. change (two_p 8) with 256. simpl int_of_bytes. generalize (Byte.unsigned_range a). @@ -1024,21 +1024,21 @@ Qed. Lemma bytes_of_int_append: forall n2 x2 n1 x1, - 0 <= x1 < two_p (Z_of_nat n1 * 8) -> - bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z_of_nat n1 * 8)) = + 0 <= x1 < two_p (Z.of_nat n1 * 8) -> + bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z.of_nat n1 * 8)) = bytes_of_int n1 x1 ++ bytes_of_int n2 x2. Proof. induction n1; intros. - simpl in *. f_equal. omega. - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256). { - rewrite inj_S. change 256 with (two_p 8). rewrite <- two_p_is_exp. + rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp. f_equal. omega. omega. omega. } rewrite E in *. simpl. f_equal. apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). change Byte.modulus with 256. ring. - rewrite Zmult_assoc. rewrite Z_div_plus. apply IHn1. + rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1. apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. assumption. omega. Qed. @@ -1051,8 +1051,8 @@ Proof. intros. transitivity (bytes_of_int (4 + 4) (Int64.unsigned (Int64.ofwords (Int64.hiword i) (Int64.loword i)))). f_equal. f_equal. rewrite Int64.ofwords_recompose. auto. rewrite Int64.ofwords_add'. - change 32 with (Z_of_nat 4 * 8). - rewrite Zplus_comm. apply bytes_of_int_append. apply Int.unsigned_range. + change 32 with (Z.of_nat 4 * 8). + rewrite Z.add_comm. apply bytes_of_int_append. apply Int.unsigned_range. Qed. Lemma encode_val_int64: diff --git a/common/Memory.v b/common/Memory.v index 8bb69c02..2cf1c3ab 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -275,7 +275,7 @@ Lemma valid_access_compat: valid_access m chunk2 b ofs p. Proof. intros. inv H1. rewrite H in H2. constructor; auto. - eapply Zdivide_trans; eauto. eapply align_le_divides; eauto. + eapply Z.divide_trans; eauto. eapply align_le_divides; eauto. Qed. Lemma valid_access_dec: @@ -311,7 +311,7 @@ Proof. intros. rewrite valid_pointer_nonempty_perm. split; intros. split. simpl; red; intros. replace ofs0 with ofs by omega. auto. - simpl. apply Zone_divide. + simpl. apply Z.divide_1_l. destruct H. apply H. simpl. omega. Qed. @@ -367,7 +367,7 @@ Program Definition alloc (m: mem) (lo hi: Z) := (PMap.set m.(nextblock) (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None) m.(mem_access)) - (Psucc m.(nextblock)) + (Pos.succ m.(nextblock)) _ _ _, m.(nextblock)). Next Obligation. @@ -475,12 +475,12 @@ Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t me Remark setN_other: forall vl c p q, - (forall r, p <= r < p + Z_of_nat (length vl) -> r <> q) -> + (forall r, p <= r < p + Z.of_nat (length vl) -> r <> q) -> ZMap.get q (setN vl p c) = ZMap.get q c. Proof. induction vl; intros; simpl. auto. - simpl length in H. rewrite inj_S in H. + simpl length in H. rewrite Nat2Z.inj_succ in H. transitivity (ZMap.get q (ZMap.set p a c)). apply IHvl. intros. apply H. omega. apply ZMap.gso. apply not_eq_sym. apply H. omega. @@ -488,7 +488,7 @@ Qed. Remark setN_outside: forall vl c p q, - q < p \/ q >= p + Z_of_nat (length vl) -> + q < p \/ q >= p + Z.of_nat (length vl) -> ZMap.get q (setN vl p c) = ZMap.get q c. Proof. intros. apply setN_other. @@ -508,16 +508,16 @@ Qed. Remark getN_exten: forall c1 c2 n p, - (forall i, p <= i < p + Z_of_nat n -> ZMap.get i c1 = ZMap.get i c2) -> + (forall i, p <= i < p + Z.of_nat n -> ZMap.get i c1 = ZMap.get i c2) -> getN n p c1 = getN n p c2. Proof. - induction n; intros. auto. rewrite inj_S in H. simpl. decEq. + induction n; intros. auto. rewrite Nat2Z.inj_succ in H. simpl. decEq. apply H. omega. apply IHn. intros. apply H. omega. Qed. Remark getN_setN_disjoint: forall vl q c n p, - Intv.disjoint (p, p + Z_of_nat n) (q, q + Z_of_nat (length vl)) -> + Intv.disjoint (p, p + Z.of_nat n) (q, q + Z.of_nat (length vl)) -> getN n p (setN vl q c) = getN n p c. Proof. intros. apply getN_exten. intros. apply setN_other. @@ -526,7 +526,7 @@ Qed. Remark getN_setN_outside: forall vl q c n p, - p + Z_of_nat n <= q \/ q + Z_of_nat (length vl) <= p -> + p + Z.of_nat n <= q \/ q + Z.of_nat (length vl) <= p -> getN n p (setN vl q c) = getN n p c. Proof. intros. apply getN_setN_disjoint. apply Intv.disjoint_range. auto. @@ -575,7 +575,7 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := or [None] if the accessed locations are not writable. *) Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem := - if range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Cur Writable then + if range_perm_dec m b ofs (ofs + Z.of_nat (length bytes)) Cur Writable then Some (mkmem (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents)) m.(mem_access) @@ -797,12 +797,12 @@ Qed. Lemma getN_concat: forall c n1 n2 p, - getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z_of_nat n1) c. + getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z.of_nat n1) c. Proof. induction n1; intros. simpl. decEq. omega. - rewrite inj_S. simpl. decEq. - replace (p + Zsucc (Z_of_nat n1)) with ((p + 1) + Z_of_nat n1) by omega. + rewrite Nat2Z.inj_succ. simpl. decEq. + replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by omega. auto. Qed. @@ -861,14 +861,14 @@ Proof. remember (size_chunk_nat ch) as n; clear Heqn. revert ofs H; induction n; intros; simpl; auto. f_equal. - rewrite inj_S in H. + rewrite Nat2Z.inj_succ in H. replace ofs with (ofs+0) by omega. apply H; omega. apply IHn. intros. - rewrite <- Zplus_assoc. + rewrite <- Z.add_assoc. apply H. - rewrite inj_S. omega. + rewrite Nat2Z.inj_succ. omega. Qed. Theorem load_int64_split: @@ -891,7 +891,7 @@ Proof. intros L1. change 4 with (size_chunk Mint32) in LB2. exploit loadbytes_load. eexact LB2. - simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. + simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. intros L2. exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2)); exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)). @@ -1059,7 +1059,7 @@ Proof. replace (size_chunk_nat chunk') with (length (encode_val chunk v)). rewrite getN_setN_same. apply decode_encode_val_general. rewrite encode_val_length. repeat rewrite size_chunk_conv in H. - apply inj_eq_rev; auto. + apply Nat2Z.inj; auto. Qed. Theorem load_store_similar_2: @@ -1139,12 +1139,12 @@ Qed. Lemma setN_in: forall vl p q c, - p <= q < p + Z_of_nat (length vl) -> + p <= q < p + Z.of_nat (length vl) -> In (ZMap.get q (setN vl p c)) vl. Proof. induction vl; intros. simpl in H. omegaContradiction. - simpl length in H. rewrite inj_S in H. simpl. + simpl length in H. rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. auto with coqlib. omega. right. apply IHvl. omega. @@ -1152,12 +1152,12 @@ Qed. Lemma getN_in: forall c q n p, - p <= q < p + Z_of_nat n -> + p <= q < p + Z.of_nat n -> In (ZMap.get q c) (getN n p c). Proof. induction n; intros. simpl in H; omegaContradiction. - rewrite inj_S in H. simpl. destruct (zeq p q). + rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q). subst q. auto. right. apply IHn. omega. Qed. @@ -1206,7 +1206,7 @@ Proof. + left; split. omega. unfold c'. simpl. apply setN_in. assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk). { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. } - simpl length in H3. rewrite inj_S in H3. omega. + simpl length in H3. rewrite Nat2Z.inj_succ in H3. omega. (* If ofs > ofs': the load reads (at ofs) the first byte from the write. ofs' ofs ofs'+|chunk'| [-------------------] write @@ -1214,8 +1214,8 @@ Proof. *) + right; split. omega. replace mv1 with (ZMap.get ofs c'). apply getN_in. - assert (size_chunk chunk' = Zsucc (Z.of_nat sz')). - { rewrite size_chunk_conv. rewrite SIZE'. rewrite inj_S; auto. } + assert (size_chunk chunk' = Z.succ (Z.of_nat sz')). + { rewrite size_chunk_conv. rewrite SIZE'. rewrite Nat2Z.inj_succ; auto. } omega. unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss. Qed. @@ -1391,11 +1391,11 @@ Qed. Theorem range_perm_storebytes: forall m1 b ofs bytes, - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable -> + range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable -> { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. Proof. intros. unfold storebytes. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable). + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable). econstructor; reflexivity. contradiction. Defined. @@ -1407,7 +1407,7 @@ Theorem storebytes_store: store chunk m1 b ofs v = Some m2. Proof. unfold storebytes, store. intros. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable); inv H. + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length (encode_val chunk v))) Cur Writable); inv H. destruct (valid_access_dec m1 chunk b ofs Writable). f_equal. apply mkmem_ext; auto. elim n. constructor; auto. @@ -1421,7 +1421,7 @@ Theorem store_storebytes: Proof. unfold storebytes, store. intros. destruct (valid_access_dec m1 chunk b ofs Writable); inv H. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable). + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length (encode_val chunk v))) Cur Writable). f_equal. apply mkmem_ext; auto. destruct v0. elim n. rewrite encode_val_length. rewrite <- size_chunk_conv. auto. @@ -1438,7 +1438,7 @@ Hypothesis STORE: storebytes m1 b ofs bytes = Some m2. Lemma storebytes_access: mem_access m2 = mem_access m1. Proof. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. @@ -1447,7 +1447,7 @@ Lemma storebytes_mem_contents: mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents). Proof. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. @@ -1487,7 +1487,7 @@ Theorem nextblock_storebytes: Proof. intros. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. @@ -1507,20 +1507,20 @@ Qed. Local Hint Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem. Theorem storebytes_range_perm: - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable. + range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable. Proof. intros. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. Theorem loadbytes_storebytes_same: - loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. + loadbytes m2 b ofs (Z.of_nat (length bytes)) = Some bytes. Proof. intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable); try discriminate. rewrite pred_dec_true. decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat. @@ -1531,7 +1531,7 @@ Qed. Theorem loadbytes_storebytes_disjoint: forall b' ofs' len, len >= 0 -> - b' <> b \/ Intv.disjoint (ofs', ofs' + len) (ofs, ofs + Z_of_nat (length bytes)) -> + b' <> b \/ Intv.disjoint (ofs', ofs' + len) (ofs, ofs + Z.of_nat (length bytes)) -> loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. Proof. intros. unfold loadbytes. @@ -1551,7 +1551,7 @@ Theorem loadbytes_storebytes_other: len >= 0 -> b' <> b \/ ofs' + len <= ofs - \/ ofs + Z_of_nat (length bytes) <= ofs' -> + \/ ofs + Z.of_nat (length bytes) <= ofs' -> loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. Proof. intros. apply loadbytes_storebytes_disjoint; auto. @@ -1562,7 +1562,7 @@ Theorem load_storebytes_other: forall chunk b' ofs', b' <> b \/ ofs' + size_chunk chunk <= ofs - \/ ofs + Z_of_nat (length bytes) <= ofs' -> + \/ ofs + Z.of_nat (length bytes) <= ofs' -> load chunk m2 b' ofs' = load chunk m1 b' ofs'. Proof. intros. unfold load. @@ -1581,29 +1581,29 @@ End STOREBYTES. Lemma setN_concat: forall bytes1 bytes2 ofs c, - setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z_of_nat (length bytes1)) (setN bytes1 ofs c). + setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z.of_nat (length bytes1)) (setN bytes1 ofs c). Proof. induction bytes1; intros. simpl. decEq. omega. - simpl length. rewrite inj_S. simpl. rewrite IHbytes1. decEq. omega. + simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. omega. Qed. Theorem storebytes_concat: forall m b ofs bytes1 m1 bytes2 m2, storebytes m b ofs bytes1 = Some m1 -> - storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 -> + storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2 -> storebytes m b ofs (bytes1 ++ bytes2) = Some m2. Proof. intros. generalize H; intro ST1. generalize H0; intro ST2. unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2. - destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Cur Writable); try congruence. - destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Cur Writable); try congruence. - destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Cur Writable). + destruct (range_perm_dec m b ofs (ofs + Z.of_nat(length bytes1)) Cur Writable); try congruence. + destruct (range_perm_dec m1 b (ofs + Z.of_nat(length bytes1)) (ofs + Z.of_nat(length bytes1) + Z.of_nat(length bytes2)) Cur Writable); try congruence. + destruct (range_perm_dec m b ofs (ofs + Z.of_nat (length (bytes1 ++ bytes2))) Cur Writable). inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto. rewrite PMap.gss. rewrite setN_concat. symmetry. apply PMap.set2. elim n. - rewrite app_length. rewrite inj_plus. red; intros. - destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))). + rewrite app_length. rewrite Nat2Z.inj_add. red; intros. + destruct (zlt ofs0 (ofs + Z.of_nat(length bytes1))). apply r. omega. eapply perm_storebytes_2; eauto. apply r0. omega. Qed. @@ -1613,15 +1613,15 @@ Theorem storebytes_split: storebytes m b ofs (bytes1 ++ bytes2) = Some m2 -> exists m1, storebytes m b ofs bytes1 = Some m1 - /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2. + /\ storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2. Proof. intros. destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1]. red; intros. exploit storebytes_range_perm; eauto. rewrite app_length. - rewrite inj_plus. omega. - destruct (range_perm_storebytes m1 b (ofs + Z_of_nat (length bytes1)) bytes2) as [m2' ST2]. + rewrite Nat2Z.inj_add. omega. + destruct (range_perm_storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2) as [m2' ST2]. red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm. - eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite inj_plus. omega. + eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. omega. auto. assert (Some m2 = Some m2'). rewrite <- H. eapply storebytes_concat; eauto. @@ -1646,7 +1646,7 @@ Proof. apply storebytes_store. exact SB1. simpl. apply Zdivides_trans with 8; auto. exists 2; auto. apply storebytes_store. exact SB2. - simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. + simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. Qed. Theorem storev_int64_split: @@ -1676,7 +1676,7 @@ Variable b: block. Hypothesis ALLOC: alloc m1 lo hi = (m2, b). Theorem nextblock_alloc: - nextblock m2 = Psucc (nextblock m1). + nextblock m2 = Pos.succ (nextblock m1). Proof. injection ALLOC; intros. rewrite <- H0; auto. Qed. @@ -1808,7 +1808,7 @@ Proof. subst b'. elimtype False. eauto with mem. rewrite pred_dec_true; auto. injection ALLOC; intros. rewrite <- H2; simpl. - rewrite PMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem. + rewrite PMap.gso. auto. rewrite H1. apply not_eq_sym; eauto with mem. rewrite pred_dec_false. auto. eauto with mem. Qed. @@ -2301,14 +2301,14 @@ Lemma getN_inj: mem_inj f m1 m2 -> f b1 = Some(b2, delta) -> forall n ofs, - range_perm m1 b1 ofs (ofs + Z_of_nat n) Cur Readable -> + range_perm m1 b1 ofs (ofs + Z.of_nat n) Cur Readable -> list_forall2 (memval_inject f) (getN n ofs (m1.(mem_contents)#b1)) (getN n (ofs + delta) (m2.(mem_contents)#b2)). Proof. induction n; intros; simpl. constructor. - rewrite inj_S in H1. + rewrite Nat2Z.inj_succ in H1. constructor. eapply mi_memval; eauto. apply H1. omega. @@ -2487,9 +2487,9 @@ Lemma storebytes_mapped_inj: /\ mem_inj f n1 n2. Proof. intros. inversion H. - assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Cur Writable). - replace (ofs + delta + Z_of_nat (length bytes2)) - with ((ofs + Z_of_nat (length bytes1)) + delta). + assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z.of_nat (length bytes2)) Cur Writable). + replace (ofs + delta + Z.of_nat (length bytes2)) + with ((ofs + Z.of_nat (length bytes1)) + delta). eapply range_perm_inj; eauto with mem. eapply storebytes_range_perm; eauto. rewrite (list_forall2_length H3). omega. @@ -2557,7 +2557,7 @@ Lemma storebytes_outside_inj: (forall b' delta ofs', f b' = Some(b, delta) -> perm m1 b' ofs' Cur Readable -> - ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) -> + ofs <= ofs' + delta < ofs + Z.of_nat (length bytes2) -> False) -> storebytes m2 b ofs bytes2 = Some m2' -> mem_inj f m1 m2'. Proof. @@ -2572,7 +2572,7 @@ Proof. rewrite PMap.gsspec. destruct (peq b2 b). subst b2. rewrite setN_outside. auto. destruct (zlt (ofs0 + delta) ofs); auto. - destruct (zle (ofs + Z_of_nat (length bytes2)) (ofs0 + delta)). omega. + destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). omega. byContradiction. eapply H0; eauto. omega. eauto with mem. Qed. @@ -2975,7 +2975,7 @@ Theorem storebytes_outside_extends: forall m1 m2 b ofs bytes2 m2', extends m1 m2 -> storebytes m2 b ofs bytes2 = Some m2' -> - (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) -> + (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z.of_nat (length bytes2) -> False) -> extends m1 m2'. Proof. intros. inversion H. constructor. @@ -3009,7 +3009,7 @@ Proof. eapply alloc_left_mapped_inj with (m1 := m1) (m2 := m2') (b2 := b) (delta := 0); eauto. eapply alloc_right_inj; eauto. eauto with mem. - red. intros. apply Zdivide_0. + red. intros. apply Z.divide_0_r. intros. eapply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. @@ -3419,8 +3419,8 @@ Theorem aligned_area_inject: Proof. intros. assert (P: al > 0) by omega. - assert (Q: Zabs al <= Zabs sz). apply Zdivide_bounds; auto. omega. - rewrite Zabs_eq in Q; try omega. rewrite Zabs_eq in Q; try omega. + assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. omega. + rewrite Z.abs_eq in Q; try omega. rewrite Z.abs_eq in Q; try omega. assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk). destruct H0. subst; exists Mint8unsigned; auto. destruct H0. subst; exists Mint16unsigned; auto. @@ -3629,7 +3629,7 @@ Theorem storebytes_outside_inject: (forall b' delta ofs', f b' = Some(b, delta) -> perm m1 b' ofs' Cur Readable -> - ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) -> + ofs <= ofs' + delta < ofs + Z.of_nat (length bytes2) -> False) -> storebytes m2 b ofs bytes2 = Some m2' -> inject f m1 m2'. Proof. @@ -3863,7 +3863,7 @@ Proof. auto. intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. - red; intros. apply Zdivide_0. + red; intros. apply Z.divide_0_r. intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem. intros [f' [A [B [C D]]]]. exists f'; exists m2'; exists b2; auto. @@ -4205,7 +4205,7 @@ Proof. (* perm inv *) unfold flat_inj; intros. destruct (plt b1 (nextblock m)); inv H0. - rewrite Zplus_0_r in H1; auto. + rewrite Z.add_0_r in H1; auto. Qed. Theorem empty_inject_neutral: @@ -4231,7 +4231,7 @@ Proof. intros; red. eapply alloc_left_mapped_inj with (m1 := m) (b2 := b) (delta := 0). eapply alloc_right_inj; eauto. eauto. eauto with mem. - red. intros. apply Zdivide_0. + red. intros. apply Z.divide_0_r. intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. @@ -4264,7 +4264,7 @@ Proof. unfold inject_neutral; intros. exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap. unfold flat_inj. apply pred_dec_true; eauto. - repeat rewrite Zplus_0_r. intros [m'' [A B]]. congruence. + repeat rewrite Z.add_0_r. intros [m'' [A B]]. congruence. Qed. (** * Invariance properties between two memory states *) @@ -4407,7 +4407,7 @@ Qed. Lemma storebytes_unchanged_on: forall m b ofs bytes m', storebytes m b ofs bytes = Some m' -> - (forall i, ofs <= i < ofs + Z_of_nat (length bytes) -> ~ P b i) -> + (forall i, ofs <= i < ofs + Z.of_nat (length bytes) -> ~ P b i) -> unchanged_on m m'. Proof. intros; constructor; intros. @@ -4416,7 +4416,7 @@ Proof. - erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec. destruct (peq b0 b); auto. subst b0. apply setN_outside. destruct (zlt ofs0 ofs); auto. - destruct (zlt ofs0 (ofs + Z_of_nat (length bytes))); auto. + destruct (zlt ofs0 (ofs + Z.of_nat (length bytes))); auto. elim (H0 ofs0). omega. auto. Qed. diff --git a/common/Memtype.v b/common/Memtype.v index b055668c..ae4fa5fd 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -515,11 +515,11 @@ Axiom store_int16_sign_ext: Axiom range_perm_storebytes: forall m1 b ofs bytes, - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable -> + range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable -> { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. Axiom storebytes_range_perm: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable. + range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable. Axiom perm_storebytes_1: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p. @@ -561,21 +561,21 @@ Axiom store_storebytes: Axiom loadbytes_storebytes_same: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> - loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. + loadbytes m2 b ofs (Z.of_nat (length bytes)) = Some bytes. Axiom loadbytes_storebytes_other: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> forall b' ofs' len, len >= 0 -> b' <> b \/ ofs' + len <= ofs - \/ ofs + Z_of_nat (length bytes) <= ofs' -> + \/ ofs + Z.of_nat (length bytes) <= ofs' -> loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. Axiom load_storebytes_other: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> forall chunk b' ofs', b' <> b \/ ofs' + size_chunk chunk <= ofs - \/ ofs + Z_of_nat (length bytes) <= ofs' -> + \/ ofs + Z.of_nat (length bytes) <= ofs' -> load chunk m2 b' ofs' = load chunk m1 b' ofs'. (** Composing or decomposing [storebytes] operations at adjacent addresses. *) @@ -583,14 +583,14 @@ Axiom load_storebytes_other: Axiom storebytes_concat: forall m b ofs bytes1 m1 bytes2 m2, storebytes m b ofs bytes1 = Some m1 -> - storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 -> + storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2 -> storebytes m b ofs (bytes1 ++ bytes2) = Some m2. Axiom storebytes_split: forall m b ofs bytes1 bytes2 m2, storebytes m b ofs (bytes1 ++ bytes2) = Some m2 -> exists m1, storebytes m b ofs bytes1 = Some m1 - /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2. + /\ storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2. (** ** Properties of [alloc]. *) @@ -605,7 +605,7 @@ Axiom alloc_result: Axiom nextblock_alloc: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - nextblock m2 = Psucc (nextblock m1). + nextblock m2 = Pos.succ (nextblock m1). Axiom valid_block_alloc: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> @@ -867,7 +867,7 @@ Axiom storebytes_outside_extends: forall m1 m2 b ofs bytes2 m2', extends m1 m2 -> storebytes m2 b ofs bytes2 = Some m2' -> - (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) -> + (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z.of_nat (length bytes2) -> False) -> extends m1 m2'. Axiom alloc_extends: @@ -1113,7 +1113,7 @@ Axiom storebytes_outside_inject: (forall b' delta ofs', f b' = Some(b, delta) -> perm m1 b' ofs' Cur Readable -> - ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) -> + ofs <= ofs' + delta < ofs + Z.of_nat (length bytes2) -> False) -> storebytes m2 b ofs bytes2 = Some m2' -> inject f m1 m2'. diff --git a/common/Separation.v b/common/Separation.v index c27148aa..a9642d72 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -680,7 +680,7 @@ Lemma alloc_parallel_rule: Mem.alloc m2 0 sz2 = (m2', b2) -> (8 | delta) -> lo = delta -> - hi = delta + Zmax 0 sz1 -> + hi = delta + Z.max 0 sz1 -> 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', @@ -740,7 +740,7 @@ Lemma free_parallel_rule: m2 |= range b2 0 lo ** range b2 hi sz2 ** minjection j m1 ** P -> Mem.free m1 b1 0 sz1 = Some m1' -> j b1 = Some (b2, delta) -> - lo = delta -> hi = delta + Zmax 0 sz1 -> + lo = delta -> hi = delta + Z.max 0 sz1 -> exists m2', Mem.free m2 b2 0 sz2 = Some m2' /\ m2' |= minjection j m1' ** P. @@ -841,7 +841,7 @@ Proof. - eauto. - destruct (j b1) as [[b0 delta0]|] eqn:JB1. + erewrite H in H1 by eauto. inv H1. eauto. -+ exploit H0; eauto. intros (X & Y). elim Y. apply Plt_le_trans with bound; auto. ++ exploit H0; eauto. intros (X & Y). elim Y. apply Pos.lt_le_trans with bound; auto. - eauto. - eauto. - eauto. @@ -890,7 +890,7 @@ Lemma alloc_parallel_rule_2: Mem.alloc m2 0 sz2 = (m2', b2) -> (8 | delta) -> lo = delta -> - hi = delta + Zmax 0 sz1 -> + hi = delta + Z.max 0 sz1 -> 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', diff --git a/common/Switch.v b/common/Switch.v index 0df2bbc8..0ef91d60 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -123,8 +123,8 @@ Fixpoint validate_jumptable (cases: ZMap.t nat) match tbl with | nil => true | act :: rem => - beq_nat act (ZMap.get n cases) - && validate_jumptable cases rem (Zsucc n) + Nat.eqb act (ZMap.get n cases) + && validate_jumptable cases rem (Z.succ n) end. Fixpoint validate (default: nat) (cases: table) (t: comptree) @@ -133,9 +133,9 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree) | CTaction act => match cases with | nil => - beq_nat act default + Nat.eqb act default | (key1, act1) :: _ => - zeq key1 lo && zeq lo hi && beq_nat act act1 + zeq key1 lo && zeq lo hi && Nat.eqb act act1 end | CTifeq pivot act t' => zle 0 pivot && zlt pivot modulus && @@ -143,7 +143,7 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree) | (None, _) => false | (Some act', others) => - beq_nat act act' + Nat.eqb act act' && validate default others t' (refine_low_bound pivot lo) (refine_high_bound pivot hi) diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index ca71bf59..a13f69b0 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -61,13 +61,13 @@ Qed. (** nat is comparable. **) Program Instance natComparable : Comparable nat := - { compare := nat_compare }. + { compare := Nat.compare }. Next Obligation. symmetry. -destruct (nat_compare x y) as [] eqn:?. -rewrite nat_compare_eq_iff in Heqc. +destruct (Nat.compare x y) as [] eqn:?. +rewrite Nat.compare_eq_iff in Heqc. destruct Heqc. -rewrite nat_compare_eq_iff. +rewrite Nat.compare_eq_iff. trivial. rewrite <- nat_compare_lt in *. rewrite <- nat_compare_gt in *. @@ -78,9 +78,9 @@ trivial. Qed. Next Obligation. destruct c. -rewrite nat_compare_eq_iff in *; destruct H; assumption. +rewrite Nat.compare_eq_iff in *; destruct H; assumption. rewrite <- nat_compare_lt in *. -apply (lt_trans _ _ _ H H0). +apply (Nat.lt_trans _ _ _ H H0). rewrite <- nat_compare_gt in *. apply (gt_trans _ _ _ H H0). Qed. @@ -149,7 +149,7 @@ destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..]; right; intro; destruct H; rewrite compare_refl in Heqc; discriminate. Defined. -Instance NComparableUsualEq : ComparableUsualEq natComparable := nat_compare_eq. +Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq. (** A pair of ComparableUsualEq is ComparableUsualEq **) Instance PairComparableUsualEq @@ -223,33 +223,33 @@ inversion Heqp. subst. clear Heqp. rewrite phi_incr in H. pose proof (phi_bounded i0). pose proof (phi_bounded (inj x)). -destruct (Z_lt_le_dec (Zsucc (phi i0)) (2 ^ Z_of_nat size)%Z). +destruct (Z_lt_le_dec (Z.succ (phi i0)) (2 ^ Z.of_nat size)%Z). rewrite Zmod_small in H by omega. apply Zlt_succ_le, Zle_lt_or_eq in H. destruct H; simpl; auto. left. rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity. -replace (Zsucc (phi i0)) with (2 ^ Z_of_nat size)%Z in H by omega. +replace (Z.succ (phi i0)) with (2 ^ Z.of_nat size)%Z in H by omega. rewrite Z_mod_same_full in H. exfalso; omega. rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). -rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega. +rewrite <- Z.abs_eq with (phi i), <- Z.abs_eq with (phi inj_bound) by omega. clear H H0 H1. -do 2 rewrite <- inj_Zabs_nat. +do 2 rewrite <- Zabs2Nat.id_abs. f_equal. revert l i Heqp. -assert (Zabs_nat (phi inj_bound) < Zabs_nat (2^31)). +assert (Z.abs_nat (phi inj_bound) < Z.abs_nat (2^31)). apply Zabs_nat_lt, phi_bounded. -induction (Zabs_nat (phi inj_bound)); intros. +induction (Z.abs_nat (phi inj_bound)); intros. inversion Heqp; reflexivity. inversion Heqp; clear H1 H2 Heqp. match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end. pose proof (phi_bounded i0). -erewrite <- IHn, <- Zabs_nat_Zsucc in H |- *; eauto; try omega. +erewrite <- IHn, <- Zabs2Nat.inj_succ in H |- *; eauto; try omega. rewrite phi_incr, Zmod_small; intuition; try omega. apply inj_lt in H. -pose proof Zle_le_succ. -do 2 rewrite inj_Zabs_nat, Zabs_eq in H; now eauto. +pose proof Z.le_le_succ_r. +do 2 rewrite Zabs2Nat.id_abs, Z.abs_eq in H; now eauto. Qed. (** Previous class instances for [option A] **) diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index ff88571b..f76731d5 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -304,7 +304,7 @@ reflexivity. destruct p. reflexivity. simpl; rewrite build_pt_dot_cost. -simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity. +simpl; rewrite <- plus_n_Sm, Nat.add_assoc; reflexivity. Qed. Lemma build_pt_dot_buffer: @@ -593,12 +593,12 @@ Lemma parse_fix_complete: Proof. fix 3. destruct n_steps; intros; simpl. -apply lt_0_Sn. +apply Nat.lt_0_succ. apply step_next_ptd in H. pose proof (next_ptd_cost ptd). destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition. rewrite H3 in H0; rewrite H0. -apply le_n_S, le_0_n. +apply le_n_S, Nat.le_0_l. destruct (next_ptd ptd); intuition; subst. eapply parse_fix_complete with (n_steps:=n_steps) in H1. rewrite H0. @@ -648,7 +648,7 @@ generalize (start_nt init). dependent destruction full_pt0. intros. rewrite build_pt_dot_cost; simpl. -rewrite H, plus_0_r; reflexivity. +rewrite H, Nat.add_0_r; reflexivity. Qed. Lemma init_ptd_buffer: diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 18d4d7e1..3fe1ea2e 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -32,7 +32,7 @@ Ltac predSpec pred predspec x y := generalize (predspec x y); case (pred x y); intro. Ltac caseEq name := - generalize (refl_equal name); pattern name at -1 in |- *; case name. + generalize (eq_refl name); pattern name at -1 in |- *; case name. Ltac destructEq name := destruct name eqn:?. @@ -125,21 +125,21 @@ Lemma Plt_trans: Proof (Pos.lt_trans). Lemma Plt_succ: - forall (x: positive), Plt x (Psucc x). + forall (x: positive), Plt x (Pos.succ x). Proof. unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl. Qed. Hint Resolve Plt_succ: coqlib. Lemma Plt_trans_succ: - forall (x y: positive), Plt x y -> Plt x (Psucc y). + forall (x y: positive), Plt x y -> Plt x (Pos.succ y). Proof. intros. apply Plt_trans with y. assumption. apply Plt_succ. Qed. Hint Resolve Plt_succ: coqlib. Lemma Plt_succ_inv: - forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y. + forall (x y: positive), Plt x (Pos.succ y) -> Plt x y \/ x = y. Proof. unfold Plt; intros. rewrite Pos.lt_succ_r in H. apply Pos.le_lteq; auto. @@ -165,7 +165,7 @@ Proof (Pos.le_trans). Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q. Proof (Pos.lt_le_incl). -Lemma Ple_succ: forall (p: positive), Ple p (Psucc p). +Lemma Ple_succ: forall (p: positive), Ple p (Pos.succ p). Proof. intros. apply Plt_Ple. apply Plt_succ. Qed. @@ -188,7 +188,7 @@ Section POSITIVE_ITERATION. Lemma Plt_wf: well_founded Plt. Proof. - apply well_founded_lt_compat with nat_of_P. + apply well_founded_lt_compat with Pos.to_nat. intros. apply nat_of_P_lt_Lt_compare_morphism. exact H. Qed. @@ -197,16 +197,16 @@ Variable v1: A. Variable f: positive -> A -> A. Lemma Ppred_Plt: - forall x, x <> xH -> Plt (Ppred x) x. + forall x, x <> xH -> Plt (Pos.pred x) x. Proof. - intros. elim (Psucc_pred x); intro. contradiction. - set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ. + intros. elim (Pos.succ_pred_or x); intro. contradiction. + set (y := Pos.pred x) in *. rewrite <- H0. apply Plt_succ. Qed. Let iter (x: positive) (P: forall y, Plt y x -> A) : A := match peq x xH with | left EQ => v1 - | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ)) + | right NOTEQ => f (Pos.pred x) (P (Pos.pred x) (Ppred_Plt x NOTEQ)) end. Definition positive_rec : positive -> A := @@ -228,18 +228,18 @@ Proof. Qed. Lemma positive_rec_succ: - forall x, positive_rec (Psucc x) = f x (positive_rec x). + forall x, positive_rec (Pos.succ x) = f x (positive_rec x). Proof. intro. rewrite unroll_positive_rec. unfold iter. - case (peq (Psucc x) 1); intro. + case (peq (Pos.succ x) 1); intro. destruct x; simpl in e; discriminate. - rewrite Ppred_succ. auto. + rewrite Pos.pred_succ. auto. Qed. Lemma positive_Peano_ind: forall (P: positive -> Prop), P xH -> - (forall x, P x -> P (Psucc x)) -> + (forall x, P x -> P (Pos.succ x)) -> forall x, P x. Proof. intros. @@ -247,7 +247,7 @@ Proof. intros. case (peq x0 xH); intro. subst x0; auto. - elim (Psucc_pred x0); intro. contradiction. rewrite <- H2. + elim (Pos.succ_pred_or x0); intro. contradiction. rewrite <- H2. apply H0. apply H1. apply Ppred_Plt. auto. Qed. @@ -327,10 +327,10 @@ Proof. Qed. Lemma two_power_nat_two_p: - forall x, two_power_nat x = two_p (Z_of_nat x). + forall x, two_power_nat x = two_p (Z.of_nat x). Proof. induction x. auto. - rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega. + rewrite two_power_nat_S. rewrite Nat2Z.inj_succ. rewrite two_p_S. omega. omega. Qed. Lemma two_p_monotone: @@ -350,7 +350,7 @@ Lemma two_p_monotone_strict: Proof. intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; omega. assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. omega. - replace y with (Zsucc (y - 1)) by omega. rewrite two_p_S. omega. omega. + replace y with (Z.succ (y - 1)) by omega. rewrite two_p_S. omega. omega. Qed. Lemma two_p_strict: @@ -375,37 +375,37 @@ Qed. (** Properties of [Zmin] and [Zmax] *) Lemma Zmin_spec: - forall x y, Zmin x y = if zlt x y then x else y. + forall x y, Z.min x y = if zlt x y then x else y. Proof. - intros. case (zlt x y); unfold Zlt, Zge; intro z. - unfold Zmin. rewrite z. auto. - unfold Zmin. caseEq (x ?= y); intro. - apply Zcompare_Eq_eq. auto. + intros. case (zlt x y); unfold Z.lt, Z.ge; intro z. + unfold Z.min. rewrite z. auto. + unfold Z.min. caseEq (x ?= y); intro. + apply Z.compare_eq. auto. contradiction. reflexivity. Qed. Lemma Zmax_spec: - forall x y, Zmax x y = if zlt y x then x else y. + forall x y, Z.max x y = if zlt y x then x else y. Proof. - intros. case (zlt y x); unfold Zlt, Zge; intro z. - unfold Zmax. rewrite <- (Zcompare_antisym y x). + intros. case (zlt y x); unfold Z.lt, Z.ge; intro z. + unfold Z.max. rewrite <- (Zcompare_antisym y x). rewrite z. simpl. auto. - unfold Zmax. rewrite <- (Zcompare_antisym y x). + unfold Z.max. rewrite <- (Zcompare_antisym y x). caseEq (y ?= x); intro; simpl. - symmetry. apply Zcompare_Eq_eq. auto. + symmetry. apply Z.compare_eq. auto. contradiction. reflexivity. Qed. Lemma Zmax_bound_l: - forall x y z, x <= y -> x <= Zmax y z. + forall x y z, x <= y -> x <= Z.max y z. Proof. - intros. generalize (Zmax1 y z). omega. + intros. generalize (Z.le_max_l y z). omega. Qed. Lemma Zmax_bound_r: - forall x y z, x <= z -> x <= Zmax y z. + forall x y z, x <= z -> x <= Z.max y z. Proof. - intros. generalize (Zmax2 y z). omega. + intros. generalize (Z.le_max_r y z). omega. Qed. (** Properties of Euclidean division and modulus. *) @@ -444,7 +444,7 @@ Lemma Zmod_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x mod y = b. Proof. - intros. subst x. rewrite Zplus_comm. + intros. subst x. rewrite Z.add_comm. rewrite Z_mod_plus. apply Zmod_small. auto. omega. Qed. @@ -452,7 +452,7 @@ Lemma Zdiv_unique: forall x y a b, x = a * y + b -> 0 <= b < y -> x / y = a. Proof. - intros. subst x. rewrite Zplus_comm. + intros. subst x. rewrite Z.add_comm. rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega. Qed. @@ -468,7 +468,7 @@ Proof. symmetry. apply Zdiv_unique with (r2 * b + r1). rewrite H2. rewrite H4. ring. split. - assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega. + assert (0 <= r2 * b). apply Z.mul_nonneg_nonneg. omega. omega. omega. assert ((r2 + 1) * b <= c * b). apply Zmult_le_compat_r. omega. omega. replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring. @@ -498,7 +498,7 @@ Proof. split. assert (lo < (q + 1)). apply Zmult_lt_reg_r with b. omega. - apply Zle_lt_trans with a. omega. + apply Z.le_lt_trans with a. omega. replace ((q + 1) * b) with (b * q + b) by ring. omega. omega. @@ -534,11 +534,11 @@ Proof. generalize (Z_div_mod_eq x b H0); fold xb; intro EQ1. generalize (Z_div_mod_eq xb a H); intro EQ2. rewrite EQ2 in EQ1. - eapply trans_eq. eexact EQ1. ring. + eapply eq_trans. eexact EQ1. ring. generalize (Z_mod_lt x b H0). intro. generalize (Z_mod_lt xb a H). intro. assert (0 <= xb mod a * b <= a * b - b). - split. apply Zmult_le_0_compat; omega. + split. apply Z.mul_nonneg_nonneg; omega. replace (a * b - b) with ((a - 1) * b) by ring. apply Zmult_le_compat; omega. omega. @@ -555,7 +555,7 @@ Qed. Definition Zdivide_dec: forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }. Proof. - intros. destruct (zeq (Zmod q p) 0). + intros. destruct (zeq (Z.modulo q p) 0). left. exists (q / p). transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto. transitivity (p * (q / p)). omega. ring. @@ -579,21 +579,21 @@ Qed. Definition nat_of_Z: Z -> nat := Z.to_nat. Lemma nat_of_Z_of_nat: - forall n, nat_of_Z (Z_of_nat n) = n. + forall n, nat_of_Z (Z.of_nat n) = n. Proof. exact Nat2Z.id. Qed. Lemma nat_of_Z_max: - forall z, Z_of_nat (nat_of_Z z) = Zmax z 0. + forall z, Z.of_nat (nat_of_Z z) = Z.max z 0. Proof. - intros. unfold Zmax. destruct z; simpl; auto. + intros. unfold Z.max. destruct z; simpl; auto. change (Z.of_nat (Z.to_nat (Zpos p)) = Zpos p). apply Z2Nat.id. compute; intuition congruence. Qed. Lemma nat_of_Z_eq: - forall z, z >= 0 -> Z_of_nat (nat_of_Z z) = z. + forall z, z >= 0 -> Z.of_nat (nat_of_Z z) = z. Proof. unfold nat_of_Z; intros. apply Z2Nat.id. omega. Qed. @@ -601,7 +601,7 @@ Qed. Lemma nat_of_Z_neg: forall n, n <= 0 -> nat_of_Z n = O. Proof. - destruct n; unfold Zle; simpl; auto. congruence. + destruct n; unfold Z.le; simpl; auto. congruence. Qed. Lemma nat_of_Z_plus: @@ -626,12 +626,12 @@ Proof. replace ((x + y - 1) / y * y) with ((x + y - 1) - (x + y - 1) mod y). generalize (Z_mod_lt (x + y - 1) y H). omega. - rewrite Zmult_comm. omega. + rewrite Z.mul_comm. omega. Qed. Lemma align_divides: forall x y, y > 0 -> (y | align x y). Proof. - intros. unfold align. apply Zdivide_factor_l. + intros. unfold align. apply Z.divide_factor_r. Qed. (** * Definitions and theorems on the data types [option], [sum] and [list] *) @@ -697,7 +697,7 @@ Hint Resolve nth_error_nil: coqlib. Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z := match l with | nil => acc - | hd :: tl => list_length_z_aux tl (Zsucc acc) + | hd :: tl => list_length_z_aux tl (Z.succ acc) end. Remark list_length_z_aux_shift: @@ -706,7 +706,7 @@ Remark list_length_z_aux_shift: Proof. induction l; intros; simpl. omega. - replace (n - m) with (Zsucc n - Zsucc m) by omega. auto. + replace (n - m) with (Z.succ n - Z.succ m) by omega. auto. Qed. Definition list_length_z (A: Type) (l: list A) : Z := @@ -741,7 +741,7 @@ Qed. Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A := match l with | nil => None - | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n) + | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Z.pred n) end. Lemma list_nth_z_in: @@ -998,7 +998,7 @@ Lemma list_disjoint_sym: list_disjoint l1 l2 -> list_disjoint l2 l1. Proof. unfold list_disjoint; intros. - apply sym_not_equal. apply H; auto. + apply not_eq_sym. apply H; auto. Qed. Lemma list_disjoint_dec: diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 6383794d..66dffb3a 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -86,10 +86,10 @@ Next Obligation. Qed. Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { - Decidable_witness := beq_nat x y + Decidable_witness := Nat.eqb x y }. Next Obligation. - apply beq_nat_true_iff. + apply Nat.eqb_eq. Qed. Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := { diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v index c134a3b6..85fadc16 100644 --- a/lib/Fappli_IEEE_extra.v +++ b/lib/Fappli_IEEE_extra.v @@ -104,15 +104,15 @@ Proof. destruct f1 as [| |? []|], f2 as [| |? []|]; try destruct b; try destruct b0; try solve [left; auto]; try_not_eq. - destruct (positive_eq_dec x x0); try_not_eq; + destruct (Pos.eq_dec x x0); try_not_eq; subst; left; f_equal; f_equal; apply UIP_bool. - destruct (positive_eq_dec x x0); try_not_eq; + destruct (Pos.eq_dec x x0); try_not_eq; subst; left; f_equal; f_equal; apply UIP_bool. - destruct (positive_eq_dec m m0); try_not_eq; - destruct (Z_eq_dec e e1); try solve [right; intro H; inversion H; congruence]; + destruct (Pos.eq_dec m m0); try_not_eq; + destruct (Z.eq_dec e e1); try solve [right; intro H; inversion H; congruence]; subst; left; f_equal; apply UIP_bool. - destruct (positive_eq_dec m m0); try_not_eq; - destruct (Z_eq_dec e e1); try solve [right; intro H; inversion H; congruence]; + destruct (Pos.eq_dec m m0); try_not_eq; + destruct (Z.eq_dec e e1); try solve [right; intro H; inversion H; congruence]; subst; left; f_equal; apply UIP_bool. Defined. @@ -155,7 +155,7 @@ Proof. intros; split. - red in prec_gt_0_. rewrite Z.abs_eq by (apply (Zpower_ge_0 radix2)). - apply Zle_trans with (2^(emax-1)). + apply Z.le_trans with (2^(emax-1)). apply (Zpower_le radix2); omega. assert (2^emax = 2^(emax-1)*2). { change 2 with (2^1) at 3. rewrite <- (Zpower_plus radix2) by omega. @@ -233,9 +233,9 @@ Theorem BofZ_correct: then B2R prec emax (BofZ n) = round radix2 fexp (round_mode mode_NE) (Z2R n) /\ is_finite _ _ (BofZ n) = true /\ - Bsign prec emax (BofZ n) = Zlt_bool n 0 + Bsign prec emax (BofZ n) = Z.ltb n 0 else - B2FF prec emax (BofZ n) = binary_overflow prec emax mode_NE (Zlt_bool n 0). + B2FF prec emax (BofZ n) = binary_overflow prec emax mode_NE (Z.ltb n 0). Proof. intros. generalize (binary_normalize_correct prec emax prec_gt_0_ Hmax mode_NE n 0 false). @@ -246,9 +246,9 @@ Proof. + auto. + auto. + rewrite C. change 0%R with (Z2R 0). rewrite Rcompare_Z2R. - unfold Zlt_bool. auto. + unfold Z.ltb. auto. - intros A; rewrite A. f_equal. change 0%R with (Z2R 0). - generalize (Zlt_bool_spec n 0); intros SPEC; inversion SPEC. + generalize (Z.ltb_spec n 0); intros SPEC; inversion SPEC. apply Rlt_bool_true; apply Z2R_lt; auto. apply Rlt_bool_false; apply Z2R_le; auto. - unfold F2R; simpl. ring. @@ -259,7 +259,7 @@ Theorem BofZ_finite: Z.abs n <= 2^emax - 2^(emax-prec) -> B2R _ _ (BofZ n) = round radix2 fexp (round_mode mode_NE) (Z2R n) /\ is_finite _ _ (BofZ n) = true - /\ Bsign _ _ (BofZ n) = Zlt_bool n 0%Z. + /\ Bsign _ _ (BofZ n) = Z.ltb n 0%Z. Proof. intros. generalize (BofZ_correct n). rewrite Rlt_bool_true. auto. @@ -282,7 +282,7 @@ Theorem BofZ_exact: -2^prec <= n <= 2^prec -> B2R _ _ (BofZ n) = Z2R n /\ is_finite _ _ (BofZ n) = true - /\ Bsign _ _ (BofZ n) = Zlt_bool n 0%Z. + /\ Bsign _ _ (BofZ n) = Z.ltb n 0%Z. Proof. intros. apply BofZ_representable. apply integer_representable_n; auto. Qed. @@ -340,7 +340,7 @@ Proof. apply B2R_Bsign_inj; auto. rewrite P, U; auto. rewrite R, W, C, F. - change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Zlt_bool at 3. + change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Z.ltb at 3. generalize (Zcompare_spec (p + q) 0); intros SPEC; inversion SPEC; auto. assert (EITHER: 0 <= p \/ 0 <= q) by omega. destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2]; @@ -370,7 +370,7 @@ Proof. apply B2R_Bsign_inj; auto. rewrite P, U; auto. rewrite R, W, C, F. - change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Zlt_bool at 3. + change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Z.ltb at 3. generalize (Zcompare_spec (p - q) 0); intros SPEC; inversion SPEC; auto. assert (EITHER: 0 <= p \/ q < 0) by omega. destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2]. @@ -554,7 +554,7 @@ Lemma Zrnd_odd_int: Proof. intros. assert (0 < 2^p) by (apply (Zpower_gt_0 radix2); omega). - assert (n = (n / 2^p) * 2^p + n mod 2^p) by (rewrite Zmult_comm; apply Z.div_mod; omega). + assert (n = (n / 2^p) * 2^p + n mod 2^p) by (rewrite Z.mul_comm; apply Z.div_mod; omega). assert (0 <= n mod 2^p < 2^p) by (apply Z_mod_lt; omega). unfold int_round_odd. set (q := n / 2^p) in *; set (r := n mod 2^p) in *. f_equal. @@ -606,8 +606,8 @@ Lemma int_round_odd_exact: (2^p | x) -> int_round_odd x p = x. Proof. intros. unfold int_round_odd. apply Znumtheory.Zdivide_mod in H0. - rewrite H0. simpl. rewrite Zmult_comm. symmetry. apply Z_div_exact_2. - apply Zlt_gt. apply (Zpower_gt_0 radix2). auto. auto. + rewrite H0. simpl. rewrite Z.mul_comm. symmetry. apply Z_div_exact_2. + apply Z.lt_gt. apply (Zpower_gt_0 radix2). auto. auto. Qed. Theorem BofZ_round_odd: @@ -693,9 +693,9 @@ Qed. Definition ZofB (f: binary_float): option Z := match f with - | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z + | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Z.pow_pos radix2 e)%Z | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m)) - | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z + | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Z.pow_pos radix2 e))%Z | B754_zero _ _ _ => Some 0%Z | _ => None end. @@ -715,7 +715,7 @@ Proof. intros. destruct b; simpl; auto. apply Ztrunc_opp. } rewrite EQ. f_equal. - generalize (Zpower_pos_gt_0 2 p (refl_equal _)); intros. + generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros. rewrite Ztrunc_floor. symmetry. apply Zfloor_div. omega. apply Rmult_le_pos. apply (Z2R_le 0). compute; congruence. apply Rlt_le. apply Rinv_0_lt_compat. apply (Z2R_lt 0). auto. @@ -844,14 +844,14 @@ Qed. Definition ZofB_range (f: binary_float) (zmin zmax: Z): option Z := match ZofB f with | None => None - | Some z => if Zle_bool zmin z && Zle_bool z zmax then Some z else None + | Some z => if Z.leb zmin z && Z.leb z zmax then Some z else None end. Theorem ZofB_range_correct: forall f min max, let n := Ztrunc (B2R _ _ f) in ZofB_range f min max = - if is_finite _ _ f && Zle_bool min n && Zle_bool n max then Some n else None. + if is_finite _ _ f && Z.leb min n && Z.leb n max then Some n else None. Proof. intros. unfold ZofB_range. rewrite ZofB_correct. fold n. destruct (is_finite prec emax f); auto. @@ -910,8 +910,8 @@ Proof. - rewrite NAN; auto. - rewrite NAN; auto. - rewrite NAN; auto. -- generalize (H (refl_equal _) (refl_equal _)); clear H. - generalize (H0 (refl_equal _) (refl_equal _)); clear H0. +- generalize (H (eq_refl _) (eq_refl _)); clear H. + generalize (H0 (eq_refl _) (eq_refl _)); clear H0. fold emin. fold fexp. set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x). set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y). @@ -1007,7 +1007,7 @@ Proof. assert (REC: forall n, Z.pos (nat_rect _ xH (fun _ => xO) n) = 2 ^ (Z.of_nat n)). { induction n. reflexivity. simpl nat_rect. transitivity (2 * Z.pos (nat_rect _ xH (fun _ => xO) n)). reflexivity. - rewrite inj_S. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega. + rewrite Nat2Z.inj_succ. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega. change (2 ^ 1) with 2. ring. } red in prec_gt_0_. unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite REC. @@ -1042,7 +1042,7 @@ Qed. Program Definition Bexact_inverse (f: binary_float) : option binary_float := match f with | B754_finite _ _ s m e B => - if positive_eq_dec m Bexact_inverse_mantissa then + if Pos.eq_dec m Bexact_inverse_mantissa then let e' := -e - (prec - 1) * 2 in if Z_le_dec emin e' then if Z_le_dec e' emax then @@ -1171,7 +1171,7 @@ Proof. destruct (Z.log2_spec base) as [D E]; auto. destruct (Z.log2_up_spec base) as [F G]. apply radix_gt_1. assert (K: 0 <= 2 ^ Z.log2 base) by (apply Z.pow_nonneg; omega). - rewrite ! (Zmult_comm n). rewrite ! Z.pow_mul_r by omega. + rewrite ! (Z.mul_comm n). rewrite ! Z.pow_mul_r by omega. split; apply Z.pow_le_mono_l; omega. Qed. @@ -1182,7 +1182,7 @@ Lemma bpow_log_pos: Proof. intros. rewrite <- ! Z2R_Zpower. apply Z2R_le; apply Zpower_log; auto. omega. - rewrite Zmult_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg. + rewrite Z.mul_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg. Qed. Lemma bpow_log_neg: @@ -1291,7 +1291,7 @@ Proof. rewrite pos_pow_spec. rewrite <- Z2R_Zpower by (zify; omega). rewrite <- Z2R_mult. replace false with (Z.pos m * Z.pos b ^ Z.pos e <? 0). exact (BofZ_correct (Z.pos m * Z.pos b ^ Z.pos e)). - rewrite Z.ltb_ge. rewrite Zmult_comm. apply Zmult_gt_0_le_0_compat. zify; omega. apply (Zpower_ge_0 base). + rewrite Z.ltb_ge. rewrite Z.mul_comm. apply Zmult_gt_0_le_0_compat. zify; omega. apply (Zpower_ge_0 base). + (* overflow *) rewrite Rlt_bool_false. auto. eapply Rle_trans; [idtac|apply Rle_abs]. apply (round_integer_overflow base). zify; omega. auto. @@ -1425,7 +1425,7 @@ Proof. destruct Rlt_bool. - intros (P & Q & R) (D & E & F). apply B2R_Bsign_inj; auto. congruence. rewrite F, C, R. change 0%R with (Z2R 0). rewrite Rcompare_Z2R. - unfold Zlt_bool. auto. + unfold Z.ltb. auto. - intros P Q. apply B2FF_inj. rewrite P, Q. rewrite C. f_equal. change 0%R with (Z2R 0). generalize (Zlt_bool_spec n 0); intros LT; inversion LT. rewrite Rlt_bool_true; auto. apply Z2R_lt; auto. diff --git a/lib/Floats.v b/lib/Floats.v index aa52b197..0c8ff5a4 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -92,10 +92,10 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. -Local Notation __ := (refl_equal Datatypes.Lt). +Local Notation __ := (eq_refl Datatypes.Lt). -Local Hint Extern 1 (Prec_gt_0 _) => exact (refl_equal Datatypes.Lt). -Local Hint Extern 1 (_ < _) => exact (refl_equal Datatypes.Lt). +Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). +Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt). (** * Double-precision FP numbers *) @@ -266,13 +266,13 @@ Ltac compute_this val := let x := fresh in set val as x in *; vm_compute in x; subst x. Ltac smart_omega := - simpl radix_val in *; simpl Zpower in *; + simpl radix_val in *; simpl Z.pow in *; compute_this Int.modulus; compute_this Int.half_modulus; compute_this Int.max_unsigned; compute_this Int.min_signed; compute_this Int.max_signed; compute_this Int64.modulus; compute_this Int64.half_modulus; compute_this Int64.max_unsigned; - compute_this (Zpower_pos 2 1024); compute_this (Zpower_pos 2 53); compute_this (Zpower_pos 2 52); compute_this (Zpower_pos 2 32); + compute_this (Z.pow_pos 2 1024); compute_this (Z.pow_pos 2 53); compute_this (Z.pow_pos 2 52); compute_this (Z.pow_pos 2 32); zify; omega. (** Commutativity properties of addition and multiplication. *) @@ -510,10 +510,10 @@ Proof. intros; unfold from_words, of_bits, b64_of_bits, binary_float_of_bits. rewrite B2R_FF2B, is_finite_FF2B, Bsign_FF2B. unfold binary_float_of_bits_aux; rewrite split_bits_or; simpl; pose proof (Int.unsigned_range x). - destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?. + destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?. exfalso; now smart_omega. simpl; rewrite <- Heqz; unfold F2R; simpl. split; auto. - rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Zplus_comm. auto. + rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Z.add_comm. auto. exfalso; now smart_omega. Qed. @@ -593,11 +593,11 @@ Proof. intros; unfold from_words, of_bits, b64_of_bits, binary_float_of_bits. rewrite B2R_FF2B, is_finite_FF2B, Bsign_FF2B. unfold binary_float_of_bits_aux; rewrite split_bits_or'; simpl; pose proof (Int.unsigned_range x). - destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?. + destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?. exfalso; now smart_omega. simpl; rewrite <- Heqz; unfold F2R; simpl. split; auto. rewrite <- (Z2R_plus 19342813113834066795298816), <- (Z2R_mult _ 4294967296). - f_equal; compute_this (Zpower_pos 2 52); compute_this (two_power_pos 32); ring. + f_equal; compute_this (Z.pow_pos 2 52); compute_this (two_power_pos 32); ring. assert (Zneg p < 0) by reflexivity. exfalso; now smart_omega. Qed. @@ -807,10 +807,10 @@ Proof. rewrite BofZ_mult_2p. - change (2^1) with 2. rewrite EQ. apply BofZ_round_odd with (p := 1). + omega. -+ apply Zle_trans with Int64.modulus; trivial. smart_omega. ++ apply Z.le_trans with Int64.modulus; trivial. smart_omega. + omega. -+ apply Zle_trans with (2^63). compute; intuition congruence. xomega. -- apply Zle_trans with Int64.modulus; trivial. ++ apply Z.le_trans with (2^63). compute; intuition congruence. xomega. +- apply Z.le_trans with Int64.modulus; trivial. pose proof (Int64.signed_range n). compute_this Int64.min_signed; compute_this Int64.max_signed; compute_this Int64.modulus; xomega. @@ -1191,7 +1191,7 @@ Proof. assert (E: forall i, p < i -> Z.testbit m i = false). { intros. apply Z.testbit_false. omega. replace (m / 2^i) with 0. auto. symmetry. apply Zdiv_small. - unfold m. split. omega. apply Zlt_le_trans with (2 * 2^p). omega. + unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega. change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega. apply Zpower_le. omega. } assert (F: forall i, 0 <= i -> Z.testbit (-2^p) i = if zlt i p then false else true). @@ -1222,7 +1222,7 @@ Proof. rewrite Bconv_BofZ. apply BofZ_round_odd with (p := 11). omega. - apply Zle_trans with (2^64). omega. compute; intuition congruence. + apply Z.le_trans with (2^64). omega. compute; intuition congruence. omega. exact (proj1 H). unfold int_round_odd. apply integer_representable_n2p_wide. auto. omega. @@ -1260,7 +1260,7 @@ Proof. assert (0 <= n'). { rewrite <- H1. change 0 with (int_round_odd 0 11). apply (int_round_odd_le 0 0); omega. } assert (n' < Int64.modulus). - { apply Zle_lt_trans with (int_round_odd (Int64.modulus - 1) 11). + { apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11). rewrite <- H1. apply (int_round_odd_le 0 0); omega. compute; auto. } rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega). @@ -1306,7 +1306,7 @@ Proof. assert (Int64.min_signed <= n'). { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply (int_round_odd_le 0 0); omega. } assert (n' <= Int64.max_signed). - { apply Zle_trans with (int_round_odd Int64.max_signed 11). + { apply Z.le_trans with (int_round_odd Int64.max_signed 11). rewrite <- H1. apply (int_round_odd_le 0 0); omega. compute; intuition congruence. } rewrite <- (Int64.signed_repr n') by omega. @@ -1321,7 +1321,7 @@ Proof. change (Int64.unsigned (Int64.repr 2047)) with 2047. change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega. rewrite Int64.unsigned_repr. apply Int64.eqmod_mod_eq. - apply Zlt_gt. apply (Zpower_gt_0 radix2); omega. + apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega. apply Int64.eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. exists (2^(64-11)); auto. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. diff --git a/lib/Integers.v b/lib/Integers.v index 5fe8202d..b849872f 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -63,7 +63,7 @@ Local Unset Case Analysis Schemes. Module Make(WS: WORDSIZE). Definition wordsize: nat := WS.wordsize. -Definition zwordsize: Z := Z_of_nat wordsize. +Definition zwordsize: Z := Z.of_nat wordsize. Definition modulus : Z := two_power_nat wordsize. Definition half_modulus : Z := modulus / 2. Definition max_unsigned : Z := modulus - 1. @@ -211,7 +211,7 @@ Proof. intros. subst y. assert (forall (n m: Z) (P1 P2: n < m), P1 = P2). { - unfold Zlt; intros. + unfold Z.lt; intros. apply eq_proofs_unicity. intros c1 c2. destruct c1; destruct c2; (left; reflexivity) || (right; congruence). } @@ -423,8 +423,8 @@ Remark half_modulus_power: Proof. unfold half_modulus. rewrite modulus_power. set (ws1 := zwordsize - 1). - replace (zwordsize) with (Zsucc ws1). - rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega. + replace (zwordsize) with (Z.succ ws1). + rewrite two_p_S. rewrite Z.mul_comm. apply Z_div_mult. omega. unfold ws1. generalize wordsize_pos; omega. unfold ws1. omega. Qed. @@ -484,13 +484,13 @@ Proof. Qed. Lemma unsigned_repr_eq: - forall x, unsigned (repr x) = Zmod x modulus. + forall x, unsigned (repr x) = Z.modulo x modulus. Proof. intros. simpl. apply Z_mod_modulus_eq. Qed. Lemma signed_repr_eq: - forall x, signed (repr x) = if zlt (Zmod x modulus) half_modulus then Zmod x modulus else Zmod x modulus - modulus. + forall x, signed (repr x) = if zlt (Z.modulo x modulus) half_modulus then Z.modulo x modulus else Z.modulo x modulus - modulus. Proof. intros. unfold signed. rewrite unsigned_repr_eq. auto. Qed. @@ -540,14 +540,14 @@ Lemma eqmod_mod_eq: forall x y, eqmod x y -> x mod modul = y mod modul. Proof. intros x y [k EQ]. subst x. - rewrite Zplus_comm. apply Z_mod_plus. auto. + rewrite Z.add_comm. apply Z_mod_plus. auto. Qed. Lemma eqmod_mod: forall x, eqmod x (x mod modul). Proof. intros; red. exists (x / modul). - rewrite Zmult_comm. apply Z_div_mod_eq. auto. + rewrite Z.mul_comm. apply Z_div_mod_eq. auto. Qed. Lemma eqmod_add: @@ -582,10 +582,10 @@ Qed. End EQ_MODULO. Lemma eqmod_divides: - forall n m x y, eqmod n x y -> Zdivide m n -> eqmod m x y. + forall n m x y, eqmod n x y -> Z.divide m n -> eqmod m x y. Proof. intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2]. - exists (k1*k2). rewrite <- Zmult_assoc. rewrite <- EQ2. auto. + exists (k1*k2). rewrite <- Z.mul_assoc. rewrite <- EQ2. auto. Qed. (** We then specialize these definitions to equality modulo @@ -777,8 +777,8 @@ Qed. Theorem unsigned_one: unsigned one = 1. Proof. unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega. - unfold modulus. replace wordsize with (S(pred wordsize)). - rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)). + unfold modulus. replace wordsize with (S(Init.Nat.pred wordsize)). + rewrite two_power_nat_S. generalize (two_power_nat_pos (Init.Nat.pred wordsize)). omega. generalize wordsize_pos. unfold zwordsize. omega. Qed. @@ -879,7 +879,7 @@ Proof. intros; unfold add. decEq. omega. Qed. Theorem add_zero: forall x, add x zero = x. Proof. intros. unfold add. rewrite unsigned_zero. - rewrite Zplus_0_r. apply repr_unsigned. + rewrite Z.add_0_r. apply repr_unsigned. Qed. Theorem add_zero_l: forall x, add zero x = x. @@ -896,7 +896,7 @@ Proof. apply eqm_samerepr. apply eqm_trans with ((x' + y') + z'). auto with ints. - rewrite <- Zplus_assoc. auto with ints. + rewrite <- Z.add_assoc. auto with ints. Qed. Theorem add_permut: forall x y z, add x (add y z) = add y (add x z). @@ -916,7 +916,7 @@ Theorem unsigned_add_carry: unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) * modulus. Proof. intros. - unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r. + unfold add, add_carry. rewrite unsigned_zero. rewrite Z.add_0_r. rewrite unsigned_repr_eq. generalize (unsigned_range x) (unsigned_range y). intros. destruct (zlt (unsigned x + unsigned y) modulus). @@ -930,7 +930,7 @@ Corollary unsigned_add_either: \/ unsigned (add x y) = unsigned x + unsigned y - modulus. Proof. intros. rewrite unsigned_add_carry. unfold add_carry. - rewrite unsigned_zero. rewrite Zplus_0_r. + rewrite unsigned_zero. rewrite Z.add_0_r. destruct (zlt (unsigned x + unsigned y) modulus). rewrite unsigned_zero. left; omega. rewrite unsigned_one. right; omega. @@ -1025,7 +1025,7 @@ Theorem unsigned_sub_borrow: unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus. Proof. intros. - unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r. + unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Z.sub_0_r. rewrite unsigned_repr_eq. generalize (unsigned_range x) (unsigned_range y). intros. destruct (zlt (unsigned x - unsigned y) 0). @@ -1070,7 +1070,7 @@ Proof. set (z' := unsigned z). apply eqm_samerepr. apply eqm_trans with ((x' * y') * z'). auto with ints. - rewrite <- Zmult_assoc. auto with ints. + rewrite <- Z.mul_assoc. auto with ints. Qed. Theorem mul_add_distr_l: @@ -1130,7 +1130,7 @@ Proof. apply eqm_samerepr. set (x' := unsigned x). set (y' := unsigned y). apply eqm_trans with ((x' / y') * y' + x' mod y'). - apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq. + apply eqm_refl2. rewrite Z.mul_comm. apply Z_div_mod_eq. generalize (unsigned_range y); intro. assert (unsigned y <> 0). red; intro. elim H. rewrite <- (repr_unsigned y). unfold zero. congruence. @@ -1156,7 +1156,7 @@ Proof. apply eqm_samerepr. set (x' := signed x). set (y' := signed y). apply eqm_trans with ((Z.quot x' y') * y' + Z.rem x' y'). - apply eqm_refl2. rewrite Zmult_comm. apply Z.quot_rem'. + apply eqm_refl2. rewrite Z.mul_comm. apply Z.quot_rem'. apply eqm_add; auto with ints. apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints. unfold y'. apply eqm_signed_unsigned. @@ -1280,7 +1280,7 @@ Proof. assert (Z.abs (Z.quot N D) < half_modulus). { rewrite <- Z.quot_abs by omega. apply Zquot_lt_upper_bound. xomega. xomega. - apply Zle_lt_trans with (half_modulus * 1). + apply Z.le_lt_trans with (half_modulus * 1). rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega. apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. } rewrite Z.abs_lt in H4. @@ -1344,13 +1344,13 @@ Proof. intros. rewrite Zshiftin_spec. destruct (zeq n 0). - subst n. destruct b. + apply Z.testbit_odd_0. - + rewrite Zplus_0_r. apply Z.testbit_even_0. + + rewrite Z.add_0_r. apply Z.testbit_even_0. - assert (0 <= Z.pred n) by omega. set (n' := Z.pred n) in *. replace n with (Z.succ n') by (unfold n'; omega). destruct b. + apply Z.testbit_odd_succ; auto. - + rewrite Zplus_0_r. apply Z.testbit_even_succ; auto. + + rewrite Z.add_0_r. apply Z.testbit_even_succ; auto. Qed. Remark Ztestbit_shiftin_base: @@ -1395,13 +1395,13 @@ Proof. - change (two_power_nat 0) with 1. exists (x-y); ring. - rewrite two_power_nat_S. assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)). - apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega. + apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; omega. omega. omega. destruct H0 as [k EQ]. exists k. rewrite (Zdecomp x). rewrite (Zdecomp y). replace (Z.odd y) with (Z.odd x). rewrite EQ. rewrite !Zshiftin_spec. ring. - exploit (H 0). rewrite inj_S; omega. + exploit (H 0). rewrite Nat2Z.inj_succ; omega. rewrite !Ztestbit_base. auto. Qed. @@ -1418,7 +1418,7 @@ Lemma same_bits_eqmod: Proof. induction n; intros. - simpl in H0. omegaContradiction. - - rewrite inj_S in H0. rewrite two_power_nat_S in H. + - rewrite Nat2Z.inj_succ in H0. rewrite two_power_nat_S in H. rewrite !(Ztestbit_eq i); intuition. destruct H as [k EQ]. assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) = @@ -1494,7 +1494,7 @@ Proof. - change (two_power_nat 0) with 1 in H. replace x with 0 by omega. apply Z.testbit_0_l. - - rewrite inj_S in H0. rewrite Ztestbit_eq. rewrite zeq_false. + - rewrite Nat2Z.inj_succ in H0. rewrite Ztestbit_eq. rewrite zeq_false. apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H. rewrite Zshiftin_spec in H. destruct (Z.odd x); omega. omega. omega. omega. @@ -1518,13 +1518,13 @@ Qed. Lemma Zsign_bit: forall n x, 0 <= x < two_power_nat (S n) -> - Z.testbit x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true. + Z.testbit x (Z.of_nat n) = if zlt x (two_power_nat n) then false else true. Proof. induction n; intros. - change (two_power_nat 1) with 2 in H. assert (x = 0 \/ x = 1) by omega. destruct H0; subst x; reflexivity. - - rewrite inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. + - rewrite Nat2Z.inj_succ. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. rewrite IHn. rewrite two_power_nat_S. destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec. rewrite zlt_true. auto. destruct (Z.odd x); omega. @@ -1573,7 +1573,7 @@ Proof. rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto. exploit H; eauto. rewrite Ztestbit_0. auto. - assert (Z.div2 x0 <= x). - { apply H0. intros. exploit (H1 (Zsucc i)). + { apply H0. intros. exploit (H1 (Z.succ i)). omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. } rewrite (Zdecomp x0). rewrite !Zshiftin_spec. @@ -1635,12 +1635,12 @@ Lemma sign_bit_of_unsigned: forall x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true. Proof. intros. unfold testbit. - set (ws1 := pred wordsize). - assert (zwordsize - 1 = Z_of_nat ws1). + set (ws1 := Init.Nat.pred wordsize). + assert (zwordsize - 1 = Z.of_nat ws1). unfold zwordsize, ws1, wordsize. destruct WS.wordsize as [] eqn:E. elim WS.wordsize_not_zero; auto. - rewrite inj_S. simpl. omega. + rewrite Nat2Z.inj_succ. simpl. omega. assert (half_modulus = two_power_nat ws1). rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power. rewrite H; rewrite H0. @@ -2346,7 +2346,7 @@ Proof. rewrite bits_shru; auto. rewrite unsigned_repr. destruct (zeq i 0). - subst i. rewrite Zplus_0_l. rewrite zlt_true. + subst i. rewrite Z.add_0_l. rewrite zlt_true. rewrite sign_bit_of_unsigned. unfold lt. rewrite signed_zero. unfold signed. destruct (zlt (unsigned x) half_modulus). @@ -2478,7 +2478,7 @@ Theorem rol_zero: forall x, rol x zero = x. Proof. - bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r. + bit_solve. f_equal. rewrite unsigned_zero. rewrite Z.sub_0_r. apply Zmod_small; auto. Qed. @@ -2515,7 +2515,7 @@ Qed. Theorem rol_rol: forall x n m, - Zdivide zwordsize modulus -> + Z.divide zwordsize modulus -> rol (rol x n) m = rol x (modu (add n m) iwordsize). Proof. bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos. @@ -2527,7 +2527,7 @@ Proof. replace (i - M - N) with (i - (M + N)) by omega. apply eqmod_sub. apply eqmod_refl. - apply eqmod_trans with (Zmod (unsigned n + unsigned m) zwordsize). + apply eqmod_trans with (Z.modulo (unsigned n + unsigned m) zwordsize). replace (M + N) with (N + M) by omega. apply eqmod_mod. apply wordsize_pos. unfold modu, add. fold M; fold N. rewrite unsigned_repr_wordsize. assert (forall a, eqmod zwordsize a (unsigned (repr a))). @@ -2546,7 +2546,7 @@ Qed. Theorem rolm_rolm: forall x n1 m1 n2 m2, - Zdivide zwordsize modulus -> + Z.divide zwordsize modulus -> rolm (rolm x n1 m1) n2 m2 = rolm x (modu (add n1 n2) iwordsize) (and (rol m1 n2) m2). @@ -2651,11 +2651,11 @@ Lemma Z_one_bits_range: forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < zwordsize. Proof. assert (forall n x i j, - In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n). + In j (Z_one_bits n x i) -> i <= j < i + Z.of_nat n). { induction n; simpl In. tauto. - intros x i j. rewrite inj_S. + intros x i j. rewrite Nat2Z.inj_succ. assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)). intros. exploit IHn; eauto. omega. destruct (Z.odd x); simpl. @@ -2729,16 +2729,16 @@ Qed. Remark Z_one_bits_two_p: forall n x i, - 0 <= x < Z_of_nat n -> + 0 <= x < Z.of_nat n -> Z_one_bits n (two_p x) i = (i + x) :: nil. Proof. induction n; intros; simpl. simpl in H. omegaContradiction. - rewrite inj_S in H. + rewrite Nat2Z.inj_succ in H. assert (x = 0 \/ 0 < x) by omega. destruct H0. subst x; simpl. decEq. omega. apply Z_one_bits_zero. assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)). apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec. - rewrite <- two_p_S. rewrite Zplus_0_r. f_equal; omega. omega. + rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; omega. omega. destruct H1 as [A B]; rewrite A; rewrite B. rewrite IHn. f_equal; omega. omega. Qed. @@ -2838,7 +2838,7 @@ Proof. + intros. rewrite Pos.iter_succ. rewrite H0. rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp. change (two_power_pos 1) with 2. - rewrite Zdiv2_div. rewrite Zmult_comm. apply Zdiv_Zdiv. + rewrite Zdiv2_div. rewrite Z.mul_comm. apply Zdiv_Zdiv. rewrite two_power_pos_nat. apply two_power_nat_pos. omega. - compute in H. congruence. Qed. @@ -2904,7 +2904,7 @@ Proof. * omega. + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry. apply Zmod_unique with (x1 / two_p x). - rewrite !Zshiftin_spec. rewrite Zplus_assoc. f_equal. + rewrite !Zshiftin_spec. rewrite Z.add_assoc. f_equal. transitivity (2 * (two_p x * (x1 / two_p x) + x1 mod two_p x)). f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto. ring. @@ -3038,7 +3038,7 @@ Qed. Lemma Zdiv_shift: forall x y, y > 0 -> - (x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1. + (x + (y - 1)) / y = x / y + if zeq (Z.modulo x y) 0 then 0 else 1. Proof. intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H). set (q := x / y). set (r := x mod y). intros. @@ -3258,7 +3258,7 @@ Qed. Theorem zero_ext_mod: forall n x, 0 <= n < zwordsize -> - unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n). + unsigned (zero_ext n x) = Z.modulo (unsigned x) (two_p n). Proof. intros. apply equal_same_bits. intros. rewrite Ztestbit_mod_two_p; auto. @@ -3651,7 +3651,7 @@ Theorem lt_sub_overflow: xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero. Proof. intros. unfold negative, sub_overflow, lt. rewrite sub_signed. - rewrite signed_zero. rewrite Zminus_0_r. + rewrite signed_zero. rewrite Z.sub_0_r. generalize (signed_range x) (signed_range y). set (X := signed x); set (Y := signed y). intros RX RY. unfold min_signed, max_signed in *. @@ -3777,7 +3777,7 @@ Proof. Qed. Lemma Zsize_shiftin: - forall b x, 0 < x -> Zsize (Zshiftin b x) = Zsucc (Zsize x). + forall b x, 0 < x -> Zsize (Zshiftin b x) = Z.succ (Zsize x). Proof. intros. destruct x; compute in H; try discriminate. destruct b. @@ -3788,7 +3788,7 @@ Proof. Qed. Lemma Ztestbit_size_1: - forall x, 0 < x -> Z.testbit x (Zpred (Zsize x)) = true. + forall x, 0 < x -> Z.testbit x (Z.pred (Zsize x)) = true. Proof. intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto. intros. rewrite Zsize_shiftin; auto. @@ -3832,14 +3832,14 @@ Proof. destruct (zeq x 0). subst x; simpl; omega. destruct (zlt n (Zsize x)); auto. - exploit (Ztestbit_above N x (Zpred (Zsize x))). auto. omega. + exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. omega. rewrite Ztestbit_size_1. congruence. omega. Qed. Lemma Zsize_monotone: forall x y, 0 <= x <= y -> Zsize x <= Zsize y. Proof. - intros. apply Zge_le. apply Zsize_interval_2. apply Zsize_pos. + intros. apply Z.ge_le. apply Zsize_interval_2. apply Zsize_pos. exploit (Zsize_interval_1 y). omega. omega. Qed. @@ -3850,7 +3850,7 @@ Proof. Qed. Theorem bits_size_1: - forall x, x = zero \/ testbit x (Zpred (size x)) = true. + forall x, x = zero \/ testbit x (Z.pred (size x)) = true. Proof. intros. destruct (zeq (unsigned x) 0). left. rewrite <- (repr_unsigned x). rewrite e; auto. @@ -3890,7 +3890,7 @@ Qed. Theorem bits_size_4: forall x n, 0 <= n -> - testbit x (Zpred n) = true -> + testbit x (Z.pred n) = true -> (forall i, n <= i < zwordsize -> testbit x i = false) -> size x = n. Proof. @@ -4005,7 +4005,7 @@ Strategy 0 [Wordsize_32.wordsize]. Notation int := Int.int. Remark int_wordsize_divides_modulus: - Zdivide (Z_of_nat Int.wordsize) Int.modulus. + Z.divide (Z.of_nat Int.wordsize) Int.modulus. Proof. exists (two_p (32-5)); reflexivity. Qed. @@ -4799,7 +4799,7 @@ Proof. set (p := Int.unsigned x * Int.unsigned y). set (ph := p / Int.modulus). set (pl := p mod Int.modulus). transitivity (repr (ph * Int.modulus + pl)). -- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. +- f_equal. rewrite Z.mul_comm. apply Z_div_mod_eq. apply Int.modulus_pos. - apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints. rewrite Int.unsigned_repr_eq. apply eqm_refl. Qed. @@ -4832,7 +4832,7 @@ Proof. apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. unfold mul'. apply eqm_unsigned_repr_l. apply eqm_refl. transitivity (repr (0 + (XL * YL + (XL * YH + XH * YL) * two_p 32))). - rewrite Zplus_0_l; auto. + rewrite Z.add_0_l; auto. transitivity (repr (XH * YH * (two_p 32 * two_p 32) + (XL * YL + (XL * YH + XH * YL) * two_p 32))). apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring. diff --git a/lib/Iteration.v b/lib/Iteration.v index 4398f96d..6a9d3253 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -146,7 +146,7 @@ Definition iter_step (x: positive) | right NOTEQ => match step s with | inl res => Some res - | inr s' => next (Ppred x) (Ppred_Plt x NOTEQ) s' + | inr s' => next (Pos.pred x) (Ppred_Plt x NOTEQ) s' end end. @@ -176,7 +176,7 @@ Proof. specialize (step_prop a H0). destruct (step a) as [b'|a'] eqn:?. inv H1. auto. - apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto. + apply H with (Pos.pred x) a'. apply Ppred_Plt; auto. auto. auto. Qed. Lemma iterate_prop: diff --git a/lib/Lattice.v b/lib/Lattice.v index 6eebca99..b7ae837b 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -662,9 +662,9 @@ Inductive t' : Type := Definition t : Type := t'. Definition eq (x y: t) := (x = y). -Definition eq_refl: forall x, eq x x := (@refl_equal t). -Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). -Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). +Definition eq_refl: forall x, eq x x := (@eq_refl t). +Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t). +Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t). Definition beq (x y: t) : bool := match x, y with @@ -746,9 +746,9 @@ Module LBoolean <: SEMILATTICE_WITH_TOP. Definition t := bool. Definition eq (x y: t) := (x = y). -Definition eq_refl: forall x, eq x x := (@refl_equal t). -Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). -Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). +Definition eq_refl: forall x, eq x x := (@eq_refl t). +Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t). +Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t). Definition beq : t -> t -> bool := eqb. diff --git a/lib/Ordered.v b/lib/Ordered.v index a2c36673..c333cc50 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -31,11 +31,11 @@ Definition eq (x y: t) := x = y. Definition lt := Plt. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof Plt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. @@ -58,16 +58,16 @@ Module OrderedZ <: OrderedType. Definition t := Z. Definition eq (x y: t) := x = y. -Definition lt := Zlt. +Definition lt := Z.lt. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. -Proof Zlt_trans. +Proof Z.lt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. unfold lt, eq, t; intros. omega. Qed. Lemma compare : forall x y : t, Compare lt eq x y. @@ -91,11 +91,11 @@ Definition eq (x y: t) := x = y. Definition lt (x y: t) := Int.unsigned x < Int.unsigned y. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. omega. @@ -129,11 +129,11 @@ Definition eq (x y: t) := x = y. Definition lt (x y: t) := Plt (A.index x) (A.index y). Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. diff --git a/lib/Parmov.v b/lib/Parmov.v index 92bba559..2d09171d 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -1564,7 +1564,7 @@ Proof. subst. rewrite update_s. rewrite weak_update_s. apply H1. destruct H. apply no_adherence_src; auto. apply no_adherence_tmp; auto. rewrite update_o. rewrite weak_update_d. apply H1. auto. - auto. apply sym_not_equal. apply disjoint_not_equal. auto. + auto. apply not_eq_sym. apply disjoint_not_equal. auto. Qed. Lemma weak_exec_seq_match: diff --git a/lib/Postorder.v b/lib/Postorder.v index 0215a829..3181c4cc 100644 --- a/lib/Postorder.v +++ b/lib/Postorder.v @@ -79,7 +79,7 @@ Definition transition (s: state) : PTree.t positive + state := inr _ {| gr := s.(gr); wrk := l; map := PTree.set x s.(next) s.(map); - next := Psucc s.(next) |} + next := Pos.succ s.(next) |} | (x, y :: succs_x) :: l => (**r consider [y], the next unnumbered successor of [x] *) match s.(gr)!y with | None => (**r [y] is already numbered: discard from worklist *) diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 27278b01..20bb91cd 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -422,7 +422,7 @@ Definition merge (uf: t) (a b: elt) : t := let b' := repr uf b in match M.elt_eq a' b' with | left EQ => uf - | right NEQ => identify uf a' b (repr_res_none uf a) (sym_not_equal NEQ) + | right NEQ => identify uf a' b (repr_res_none uf a) (not_eq_sym NEQ) end. Lemma repr_merge: diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index bf75d2e0..9f258e3d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -854,7 +854,7 @@ Local Transparent destroyed_by_jumptable. generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index e5736277..460fa670 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -39,9 +39,9 @@ Proof. intros. unfold high_u, low_u. rewrite Int.shl_rolm. rewrite Int.shru_rolm. rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) + change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) - (Int.repr (Z_of_nat Int.wordsize))) + (Int.repr (Z.of_nat Int.wordsize))) with (Int.zero). rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib. exact (Int.and_mone n). @@ -54,9 +54,9 @@ Proof. intros. unfold high_u, low_u. rewrite Int.shl_rolm. rewrite Int.shru_rolm. rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) + change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) - (Int.repr (Z_of_nat Int.wordsize))) + (Int.repr (Z.of_nat Int.wordsize))) with (Int.zero). rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib. exact (Int.and_mone n). @@ -198,7 +198,7 @@ Hint Resolve ireg_of_not_GPR0': asmgen. Lemma preg_of_not_LR: forall r, LR <> preg_of r. Proof. - intros. auto using sym_not_equal with asmgen. + intros. auto using not_eq_sym with asmgen. Qed. Lemma preg_notin_LR: @@ -1243,7 +1243,7 @@ Opaque Val.add. econstructor; split. eapply exec_straight_trans. eapply exec_straight_two; simpl; reflexivity. eapply exec_straight_two; simpl; reflexivity. - split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen). + split. assert (GPR0 <> x0) by (apply not_eq_sym; eauto with asmgen). Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl. rewrite low_high_half_zero. auto. intros; Simpl. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 2793fbfb..1de55c1a 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -370,30 +370,30 @@ Proof. induction tyl; simpl; intros. omega. destruct a. - destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (list_nth_z float_param_regs fr); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. set (ir' := align ir 2). destruct (list_nth_z int_param_regs ir'); eauto. destruct (list_nth_z int_param_regs (ir' + 1)); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. destruct (list_nth_z float_param_regs fr); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. - destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. + destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. destruct (list_nth_z float_param_regs fr); eauto. - apply Zle_trans with (align ofs0 2). apply align_le; omega. - apply Zle_trans with (align ofs0 2 + 2); auto; omega. + apply Z.le_trans with (align ofs0 2). apply align_le; omega. + apply Z.le_trans with (align ofs0 2 + 2); auto; omega. Qed. Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. + intros; unfold size_arguments. apply Z.le_ge. apply size_arguments_rec_above. Qed. diff --git a/powerpc/Op.v b/powerpc/Op.v index 263c1bd8..e6f942c1 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1042,7 +1042,7 @@ Remark weak_valid_pointer_no_overflow_extends: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index 17104b33..cb3806bd 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -138,8 +138,8 @@ Proof. split. exists (fe_ofs_arg / 8); reflexivity. split. apply align_divides; omega. split. apply align_divides; omega. - split. apply Zdivide_0. + split. apply Z.divide_0_r. apply Z.divide_add_r. - apply Zdivide_trans with 8. exists 2; auto. apply align_divides; omega. + apply Z.divide_trans with 8. exists 2; auto. apply align_divides; omega. apply Z.divide_factor_l. Qed. diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index da444a4b..cc45a8de 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -920,7 +920,7 @@ Local Transparent destroyed_by_op. generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index ff993650..df7ddfd2 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -420,7 +420,7 @@ Proof. ofs + typesize ty <= max_outgoing_2 n p). { intros. destruct p; simpl in H; intuition; subst; simpl. - xomega. - - eapply Zle_trans. 2: apply A. xomega. + - eapply Z.le_trans. 2: apply A. xomega. - xomega. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> @@ -428,7 +428,7 @@ Proof. { induction l; simpl; intros. - contradiction. - rewrite in_app_iff in H. destruct H. - + eapply Zle_trans. eapply B; eauto. apply Zge_le. apply fold_max_outgoing_above. + + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. + apply IHl; auto. } apply C. @@ -1194,7 +1194,7 @@ Remark weak_valid_pointer_no_overflow_extends: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index ba116380..d0c6a526 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -139,7 +139,7 @@ Proof. set (ostkdata := align (ol + 4 * b.(bound_local)) 8). assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). - split. apply Zdivide_0. + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. split. apply align_divides; omega. diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 6caf4531..38816fd2 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -825,7 +825,7 @@ Transparent destroyed_by_jumptable. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inv EQ1. monadInv EQ0. rewrite transl_code'_transl_code in EQ1. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. diff --git a/x86/Conventions1.v b/x86/Conventions1.v index ecfb85bf..646c4afb 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -299,7 +299,7 @@ Proof. assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). - { intros. apply Z.divide_add_r; auto. apply Zdivide_refl. } + { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } Opaque list_nth_z. induction tyl; simpl loc_arguments_64; intros. elim H. @@ -339,10 +339,10 @@ Proof. assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l). { unfold loc_argument_64_charact, loc_argument_acceptable. destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. - intros [C D]. split; auto. apply Zdivide_trans with 2; auto. + intros [C D]. split; auto. apply Z.divide_trans with 2; auto. exists (2 / typealign ty); destruct ty; reflexivity. } - exploit loc_arguments_64_charact; eauto using Zdivide_0. + exploit loc_arguments_64_charact; eauto using Z.divide_0_r. unfold forall_rpair; destruct p; intuition auto. - (* 32 bits *) assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). @@ -360,7 +360,7 @@ Remark size_arguments_32_above: Proof. induction tyl; simpl; intros. omega. - apply Zle_trans with (ofs0 + typesize a); auto. + apply Z.le_trans with (ofs0 + typesize a); auto. generalize (typesize_pos a); omega. Qed. @@ -376,21 +376,21 @@ Proof. | None => size_arguments_64 tyl ir fr (ofs0 + 2) end). { destruct (list_nth_z int_param_regs ir); eauto. - apply Zle_trans with (ofs0 + 2); auto. omega. } + apply Z.le_trans with (ofs0 + 2); auto. omega. } assert (B: ofs0 <= match list_nth_z float_param_regs fr with | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 | None => size_arguments_64 tyl ir fr (ofs0 + 2) end). { destruct (list_nth_z float_param_regs fr); eauto. - apply Zle_trans with (ofs0 + 2); auto. omega. } + apply Z.le_trans with (ofs0 + 2); auto. omega. } destruct a; auto. Qed. Lemma size_arguments_above: forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. + intros; unfold size_arguments. apply Z.le_ge. destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above]. Qed. @@ -402,7 +402,7 @@ Proof. induction tyl as [ | t l]; simpl; intros x IN. - contradiction. - rewrite in_app_iff in IN; destruct IN as [IN|IN]. -+ apply Zle_trans with (x + typesize t); [|apply size_arguments_32_above]. ++ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above]. Ltac decomp := match goal with | [ H: _ \/ _ |- _ ] => destruct H; decomp @@ -437,7 +437,7 @@ Proof. { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. - discriminate. - eapply IHtyl; eauto. - - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - eapply IHtyl; eauto. } assert (B: forall ty0, In (S Outgoing ofs ty) (regs_of_rpairs @@ -454,7 +454,7 @@ Proof. { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. - discriminate. - eapply IHtyl; eauto. - - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - eapply IHtyl; eauto. } destruct a; eauto. Qed. @@ -1311,7 +1311,7 @@ Remark weak_valid_pointer_no_overflow_extends: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index 22c68099..d375febf 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -140,7 +140,7 @@ Proof. set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). - split. apply Zdivide_0. + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. split. apply align_divides; omega. |