"Bitwise hacks" proofs

pow2_equiv.v

Require Import Coq.Init.Nat Coq.Arith.PeanoNat Coq.Numbers.NatInt.NZPow Coq.Numbers.NatInt.NZBits Lia.

Theorem shiftr_div_pow2 : forall (a n : nat),
                          shiftr a n = a / 2 ^ n.
Proof.
  intros. Nat.bitwise. rewrite Nat.shiftr_spec'. symmetry. apply Nat.div_pow2_bits.
Qed.

Lemma shiftl_mul_pow2 : forall (a n : nat), 
                        shiftl a n = a * 2 ^ n.
Proof.
  intros. Nat.bitwise. destruct (Nat.le_gt_cases n m) as [H | H].
  - now rewrite Nat.shiftl_spec_high', Nat.mul_pow2_bits_high.
  - now rewrite Nat.shiftl_spec_low, Nat.mul_pow2_bits_low.  
Qed.

Theorem pow2_check : forall (n : nat),
                     land (2 ^ n) (2 ^ n - 1) = 0.
Proof.
 intros. replace (2 ^ n - 1) with (pred (2 ^ n)) by lia.
 rewrite <- Nat.ones_equiv. rewrite Nat.land_ones.
 rewrite Nat.mod_same.
 - reflexivity.
 - rewrite Nat.neq_0_lt_0. induction n; simpl; lia.
Qed.

Theorem modulo_pow2 : forall (a n : nat),
                      a mod 2 ^ n = land a (2 ^ n - 1).
Proof.
  intros. replace (2 ^ n - 1) with (pred (2 ^ n)) by lia. rewrite <- Nat.ones_equiv. 
  now rewrite Nat.land_ones.
Qed.