# Library Coq.ZArith.Zbitwise

Require Import BinInt Lia Btauto. Local Open Scope Z_scope.
Import (ltac.notations) BinInt.Z.

Module Z.

Local Infix ".|" := Z.lor (at level 40).
Local Infix ".&" := Z.land (at level 40).
Local Infix ".^" := Z.lxor (at level 40).
Local Notation ".~ x" := (Z.lnot x) (at level 35).
Local Notation "x .[ i ]" := (Z.testbit x i) (at level 9, format "x .[ i ]").

Local Infix "^^" := xorb (at level 40).

Local Hint Rewrite
Z.b2z_bit0
Z.bits_opp
Z.lnot_spec
Z.testbit_ones_nonneg
Z.testbit_ones
Z.shiftl_spec
Z.shiftr_spec
using solve [trivial] : bitwise.

Local Ltac to_bitwise :=
let i := fresh "i" in
bitwise as i ?Hi;
repeat match goal with H : ?a = ?b :> Z |- _ =>
apply (f_equal (fun x => Z.testbit x i)) in H end.
Local Ltac prove_bitwise :=
apply Bool.eqb_true_iff;
repeat match goal with H : _ = _ :> bool |- _ =>
apply Bool.eqb_true_iff in H; revert H end;
rewrite <-?Bool.negb_xorb, <-?Bool.implb_true_iff, ?Bool.implb_orb;
autorewrite with bitwise;
btauto.
Local Ltac p := to_bitwise; prove_bitwise.

Bitwise operations alone

Lemma lnot_lnot x : Z.lnot (Z.lnot x) = x.

Lemma ldiff_lor_land x y : Z.ldiff (x .| y) (x .& y) = x .^ y.

Bitwise complement and +1/-1

Lemma succ_lnot x : Z.lnot x + 1 = - x.

Lemma lnot_pred x : Z.lnot (x - 1) = - x.

Lemma lnot_eq_pred_opp x : Z.lnot x = -x-1.

Lemma opp_lnot x : - (Z.lnot x) = x+1.

Lemma lnot_opp x : Z.lnot (-x) = x-1.

Bitwise complement as an input to + or -

Lemma sub_lnot_r x y : x - Z.lnot y = x + y + 1.

Lemma pred_sub_lnot_r x y : x - Z.lnot y - 1 = x + y.

Lemma add_lnot_r x y : x + Z.lnot y = x - y - 1.

Lemma succ_add_lnot_r x y : x + Z.lnot y + 1 = x - y.

Lemma lnot_sub x y : Z.lnot (x - y) = Z.lnot x + y.

Explicit formulas for carry bits during addition. Conceptually, the theory

# generalization adccarries is provided as the same theory applies.

Bitwise operations, addition, subtraction, and doubling

Lemma add_lxor_2land x y : (x .^ y) + 2*(x .& y) = x + y.

Lemma sub_2lor_lxor x y : 2*(x .| y) - x .^ y = x + y.

Lemma sub_lxor_2rlandn x y : x .^ y - 2*(.~x .& y) = x - y.

Lemma sub_2landn_lxor x y : 2*(x.&.~y) - x.^y = x - y.

End Z.