Relating neg and not

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1678 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 42 insertions, 5 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 4ed1396..30f692a 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1213,16 +1213,28 @@ Proof.
   intros; apply H; omega. omega.
 Qed.
 
+Lemma Z_of_bits_complement:
+  forall f n i,
+  Z_of_bits n (fun j => negb (f j)) i = two_power_nat n - 1 - Z_of_bits n f i.
+Proof.
+  induction n; intros; simpl Z_of_bits.
+  auto.
+  rewrite two_power_nat_S. rewrite IHn.
+Opaque Zmult Zplus Zminus.
+  destruct (f i); simpl. ring. ring.
+Transparent Zmult Zplus Zminus.
+Qed.
+
 Lemma Z_of_bits_true:
   forall f n i,
   (forall j, i <= j < i + Z_of_nat n -> f j = true) ->
   Z_of_bits n f i = two_power_nat n - 1.
 Proof.
-  induction n; intros.
-  simpl. auto.
-  rewrite two_power_nat_S. simpl Z_of_bits. rewrite inj_S in H.
-  rewrite H. rewrite IHn. unfold Z_shift_add. omega.  
-  intros; apply H. omega. omega.
+  intros. set (z := fun (i: Z) => false). 
+  transitivity (Z_of_bits n (fun j => negb (z j)) i). 
+  apply Z_of_bits_exten; intros. unfold z. rewrite H. auto. omega. 
+  rewrite Z_of_bits_complement. rewrite Z_of_bits_false. omega. 
+  unfold z; auto.
 Qed.
 
 (** ** Properties of bitwise and, or, xor *)
@@ -1430,6 +1442,31 @@ Proof.
   intros. unfold not. rewrite <- xor_assoc. rewrite xor_idem. apply not_zero. 
 Qed.
 
+Theorem not_neg:
+  forall x, not x = add (neg x) mone.
+Proof.
+  intros.
+  unfold not, xor, bitwise_binop. rewrite unsigned_mone.
+  set (ux := unsigned x).
+  set (bx := bits_of_Z wordsize ux).
+  transitivity (repr (Z_of_bits wordsize (fun i => negb (bx i)) 0)).
+  decEq. apply Z_of_bits_exten. intros. rewrite bits_of_Z_mone; auto. omega.
+  rewrite Z_of_bits_complement. apply eqm_samerepr. rewrite unsigned_mone. fold modulus. 
+  replace (modulus - 1 - Z_of_bits wordsize bx 0)
+     with ((- Z_of_bits wordsize bx 0) + (modulus - 1)) by omega.
+  apply eqm_add. unfold neg. apply eqm_unsigned_repr_r. apply eqm_neg. 
+  apply Z_of_bits_of_Z. apply eqm_refl. 
+Qed.
+
+Theorem neg_not:
+  forall x, neg x = add (not x) one.
+Proof.
+  intros. rewrite not_neg. rewrite add_assoc. 
+  replace (add mone one) with zero. rewrite add_zero. auto. 
+  apply eqm_samerepr. rewrite unsigned_mone. rewrite unsigned_one. 
+  exists (-1). ring. 
+Qed.
+
 (** Connections between [add] and bitwise logical operations. *)
 
 Theorem add_is_or: