diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Integers.v | 41 | ||||
-rw-r--r-- | lib/Zbits.v | 58 |
2 files changed, 57 insertions, 42 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index f4213332..1b0375b1 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1139,6 +1139,12 @@ Proof. intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range. Qed. +Lemma bits_below: + forall x i, i < 0 -> testbit x i = false. +Proof. + intros. apply Z.testbit_neg_r; auto. +Qed. + Lemma bits_zero: forall i, testbit zero i = false. Proof. @@ -2511,12 +2517,11 @@ Proof. Qed. Lemma bits_sign_ext: - forall n x i, 0 <= i < zwordsize -> 0 < n -> + forall n x i, 0 <= i < zwordsize -> testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1). Proof. intros. unfold sign_ext. - rewrite testbit_repr; auto. rewrite Zsign_ext_spec. destruct (zlt i n); auto. - omega. auto. + rewrite testbit_repr; auto. apply Zsign_ext_spec. omega. Qed. Hint Rewrite bits_zero_ext bits_sign_ext: ints. @@ -2528,12 +2533,24 @@ Proof. rewrite bits_zero_ext. apply zlt_true. omega. omega. Qed. +Theorem zero_ext_below: + forall n x, n <= 0 -> zero_ext n x = zero. +Proof. + intros. bit_solve. destruct (zlt i n); auto. apply bits_below; omega. omega. +Qed. + Theorem sign_ext_above: forall n x, n >= zwordsize -> sign_ext n x = x. Proof. intros. apply same_bits_eq; intros. unfold sign_ext; rewrite testbit_repr; auto. - rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. omega. + rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. +Qed. + +Theorem sign_ext_below: + forall n x, n <= 0 -> sign_ext n x = zero. +Proof. + intros. bit_solve. apply bits_below. destruct (zlt i n); omega. Qed. Theorem zero_ext_and: @@ -2570,7 +2587,7 @@ Proof. Qed. Theorem sign_ext_widen: - forall x n n', 0 < n <= n' -> + forall x n n', 0 < n <= n' -> sign_ext n' (sign_ext n x) = sign_ext n x. Proof. intros. destruct (zlt n' zwordsize). @@ -2578,9 +2595,8 @@ Proof. auto. rewrite (zlt_false _ i n). destruct (zlt (n' - 1) n); f_equal; omega. - omega. omega. + omega. destruct (zlt i n'); omega. - omega. omega. apply sign_ext_above; auto. Qed. @@ -2594,7 +2610,6 @@ Proof. auto. rewrite !zlt_false. auto. omega. omega. omega. destruct (zlt i n'); omega. - omega. apply sign_ext_above; auto. Qed. @@ -2614,9 +2629,7 @@ Theorem sign_ext_narrow: Proof. intros. destruct (zlt n zwordsize). bit_solve. destruct (zlt i n); f_equal; apply zlt_true; omega. - omega. destruct (zlt i n); omega. - omega. omega. rewrite (sign_ext_above n'). auto. omega. Qed. @@ -2628,7 +2641,7 @@ Proof. bit_solve. destruct (zlt i n); auto. rewrite zlt_true; auto. omega. - omega. omega. omega. + omega. omega. rewrite sign_ext_above; auto. Qed. @@ -2643,7 +2656,7 @@ Theorem sign_ext_idem: Proof. intros. apply sign_ext_widen. omega. Qed. - + Theorem sign_ext_zero_ext: forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x. Proof. @@ -2706,7 +2719,7 @@ Proof. rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. omega. omega. omega. rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega. - omega. omega. omega. omega. omega. + omega. omega. omega. omega. Qed. (** [zero_ext n x] is the unique integer congruent to [x] modulo [2^n] @@ -2766,7 +2779,7 @@ Proof. apply eqmod_same_bits; intros. rewrite H0 in H1. rewrite H0. fold (testbit (sign_ext n x) i). rewrite bits_sign_ext. - rewrite zlt_true. auto. omega. omega. omega. + rewrite zlt_true. auto. omega. omega. Qed. Lemma eqmod_sign_ext: diff --git a/lib/Zbits.v b/lib/Zbits.v index 459e891b..fb40ccb5 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -557,7 +557,7 @@ Definition Zzero_ext (n: Z) (x: Z) : Z := Definition Zsign_ext (n: Z) (x: Z) : Z := Z.iter (Z.pred n) (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x))) - (fun x => if Z.odd x then -1 else 0) + (fun x => if Z.odd x && zlt 0 n then -1 else 0) x. Lemma Ziter_base: @@ -606,32 +606,34 @@ Proof. Qed. Lemma Zsign_ext_spec: - forall n x i, 0 <= i -> 0 < n -> + forall n x i, 0 <= i -> Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1). Proof. - intros n0 x i I0 N0. - revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1). - - unfold Zsign_ext. intros. - destruct (zeq x 1). - + subst x; simpl. - replace (if zlt i 1 then i else 0) with 0. - rewrite Ztestbit_base. - destruct (Z.odd x0). - apply Ztestbit_m1; auto. - apply Ztestbit_0. - destruct (zlt i 1); omega. - + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)). - rewrite Ziter_succ. rewrite Ztestbit_shiftin. - destruct (zeq i 0). - * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega. - * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)). - rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega. - rewrite zlt_false. rewrite (Ztestbit_eq (x - 1) x0). rewrite zeq_false; auto. - omega. omega. omega. unfold x1; omega. omega. - * omega. - * unfold x1; omega. - * omega. - - omega. + intros n0 x i I0. unfold Zsign_ext. + unfold proj_sumbool; destruct (zlt 0 n0) as [N0|N0]; simpl. +- revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1); [ | omega ]. + unfold Zsign_ext. intros. + destruct (zeq x 1). + + subst x; simpl. + replace (if zlt i 1 then i else 0) with 0. + rewrite Ztestbit_base. + destruct (Z.odd x0); [ apply Ztestbit_m1; auto | apply Ztestbit_0 ]. + destruct (zlt i 1); omega. + + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)) by omega. + rewrite Ziter_succ by (unfold x1; omega). rewrite Ztestbit_shiftin by auto. + destruct (zeq i 0). + * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega. + * rewrite H by (unfold x1; omega). + unfold x1; destruct (zlt (Z.pred i) (Z.pred x)). + ** rewrite zlt_true by omega. + rewrite (Ztestbit_eq i x0) by omega. + rewrite zeq_false by omega. auto. + ** rewrite zlt_false by omega. + rewrite (Ztestbit_eq (x - 1) x0) by omega. + rewrite zeq_false by omega. auto. +- rewrite Ziter_base by omega. rewrite andb_false_r. + rewrite Z.testbit_0_l, Z.testbit_neg_r. auto. + destruct (zlt i n0); omega. Qed. (** [Zzero_ext n x] is [x modulo 2^n] *) @@ -661,7 +663,7 @@ Qed. (** Relation between [Zsign_ext n x] and (Zzero_ext n x] *) Lemma Zsign_ext_zero_ext: - forall n, 0 < n -> forall x, + forall n, 0 <= n -> forall x, Zsign_ext n x = Zzero_ext n x - (if Z.testbit x (n - 1) then two_p n else 0). Proof. intros. apply equal_same_bits; intros. @@ -698,12 +700,12 @@ Proof. assert (C: two_p n = 2 * two_p (n - 1)). { rewrite <- two_p_S by omega. f_equal; omega. } rewrite Zzero_ext_spec, zlt_true in B by omega. - rewrite Zsign_ext_zero_ext by auto. rewrite B. + rewrite Zsign_ext_zero_ext by omega. rewrite B. destruct (zlt (Zzero_ext n x) (two_p (n - 1))); omega. Qed. Lemma eqmod_Zsign_ext: - forall n x, 0 < n -> + forall n x, 0 <= n -> eqmod (two_p n) (Zsign_ext n x) x. Proof. intros. rewrite Zsign_ext_zero_ext by auto. |