Define integer sign extension for zero bits

Just ensure sign_ext 0 x = zero.  This simplifies some statements and proofs.

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.