Module BooleanDecomposition

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.

apply bin_decomp. intros. apply Z.land_spec.
Qed.

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.

apply bin_decomp. intros. apply Z.lxor_spec.
Qed.

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.

apply bin_decomp. intros. apply Z.lor_spec.
Qed.

Corollary not_decomp : forall (x: Z) (xb: bool),
Z.lnot (2 * x + Z.b2z xb) = 2 * (Z.lnot x) + Z.b2z (negb xb).

Proof.

apply un_decomp. apply Z.lnot_spec.
Qed.

Ltac bool_decomp :=
  repeat (try rewrite xor_decomp;
          try rewrite and_decomp;
          try rewrite or_decomp;
          try rewrite not_decomp).