diff options
Diffstat (limited to 'backend/Bounds.v')
-rw-r--r-- | backend/Bounds.v | 34 |
1 files changed, 17 insertions, 17 deletions
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. |