diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Coqlib.v | 100 | ||||
-rw-r--r-- | lib/Decidableplus.v | 4 | ||||
-rw-r--r-- | lib/Fappli_IEEE_extra.v | 62 | ||||
-rw-r--r-- | lib/Floats.v | 34 | ||||
-rw-r--r-- | lib/Integers.v | 114 | ||||
-rw-r--r-- | lib/Iteration.v | 4 | ||||
-rw-r--r-- | lib/Lattice.v | 12 | ||||
-rw-r--r-- | lib/Ordered.v | 28 | ||||
-rw-r--r-- | lib/Parmov.v | 2 | ||||
-rw-r--r-- | lib/Postorder.v | 2 | ||||
-rw-r--r-- | lib/UnionFind.v | 2 |
11 files changed, 182 insertions, 182 deletions
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: |