Useful lemmas for simplification of bitwise operations
Require Import Coqlib.
Theorem bin_decomp :
forall (
fZ :
Z ->
Z ->
Z) (
fbool :
bool ->
bool ->
bool),
(
forall a b n :
Z, 0 <=
n ->
Z.testbit (
fZ a b)
n =
fbool (
Z.testbit a n) (
Z.testbit b n)) ->
forall (
x y:
Z) (
xb yb:
bool),
fZ (2 *
x +
Z.b2z xb) (2 *
y +
Z.b2z yb) = 2 * (
fZ x y) +
Z.b2z (
fbool xb yb).
Proof.
intros fZ fbool H x y xb yb .
apply Z.bits_inj'.
intros i POS0.
rewrite H;
try omega.
destruct (
zeq i 0).
-
subst.
rewrite !
Z.testbit_0_r.
reflexivity.
-
rewrite (
Zsucc_pred i).
rewrite !
Z.testbit_succ_r;
try omega.
rewrite H;
try omega.
reflexivity.
Qed.
Theorem un_decomp :
forall (
fZ :
Z ->
Z) (
fbool :
bool ->
bool),
(
forall a n :
Z, 0 <=
n ->
Z.testbit (
fZ a)
n =
fbool (
Z.testbit a n)) ->
forall (
x:
Z) (
xb:
bool),
fZ (2 *
x +
Z.b2z xb) = 2 * (
fZ x) +
Z.b2z (
fbool xb).
Proof.
intros fZ fbool H x xb .
apply Z.bits_inj'.
intros i POS0.
rewrite H;
try omega.
destruct (
zeq i 0).
-
subst.
rewrite !
Z.testbit_0_r.
reflexivity.
-
rewrite (
Zsucc_pred i).
rewrite !
Z.testbit_succ_r;
try omega.
rewrite H;
try omega.
reflexivity.
Qed.
Corollary and_decomp :
forall (
x y:
Z) (
xb yb:
bool),
Z.land (2 *
x +
Z.b2z xb) (2 *
y +
Z.b2z yb) =
2 * (
Z.land x y) +
Z.b2z (
andb xb yb).
Proof.
Corollary xor_decomp :
forall (
x y:
Z) (
xb yb:
bool),
Z.lxor (2 *
x +
Z.b2z xb) (2 *
y +
Z.b2z yb) =
2 * (
Z.lxor x y) +
Z.b2z (
xorb xb yb).
Proof.
Corollary or_decomp :
forall (
x y:
Z) (
xb yb:
bool),
Z.lor (2 *
x +
Z.b2z xb) (2 *
y +
Z.b2z yb) =
2 * (
Z.lor x y) +
Z.b2z (
orb xb yb).
Proof.
Corollary not_decomp :
forall (
x:
Z) (
xb:
bool),
Z.lnot (2 *
x +
Z.b2z xb) = 2 * (
Z.lnot x) +
Z.b2z (
negb xb).
Proof.
Ltac bool_decomp :=
repeat (
try rewrite xor_decomp;
try rewrite and_decomp;
try rewrite or_decomp;
try rewrite not_decomp).