From 1b21b6d72a4cdeb07ad646e7573983faaae47399 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 22 Jun 2011 16:02:21 +0000 Subject: Relating neg and not git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1678 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 47 ++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 5 deletions(-) diff --git a/lib/Integers.v b/lib/Integers.v index 4ed13962..30f692a8 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: -- cgit