CODEWITHSUNDEEP
binarycoqcoq-tactic
limitedeternity
limitedeternity

Reputation: 202

Proving theorems containing bitwise operators

I'm trying to prove equivalency for a pretty common "bitwise hack", namely:

I've managed to get some arithmetic stuff out of the way, but when the actual binary stuff kicked in I figured out that I don't know any techniques to help me close the goal.

Could you aid me, please?

That's what I got so far:

Require Import Coq.Init.Nat Coq.Arith.PeanoNat Lia.

Theorem modulo_pow2 : forall (i m : nat),
                      0 < m /\ land m (m - 1) = 0 -> modulo i m = land i (m - 1).
Proof.
  intros. destruct H as [H1 H2].
  
  (* induction m route *)
  induction m.
  - replace (0 - 1) with (pred 0) by lia.
    rewrite Nat.pred_0. cbn. rewrite Nat.land_0_r.
    reflexivity.
  - (* ... *)
  
  (* induction i route *)
  induction i.
  + apply Nat.mod_0_l. apply Nat.neq_0_lt_0. assumption.
  + (* ... *)
Admitted.

Upvotes: 0

Views: 97

Answers (2)

limitedeternity
limitedeternity

Reputation: 202

Looked inside NBits.v and solved them:

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.

Upvotes: 0

Pierre Cast&#233;ran
Pierre Cast&#233;ran

Reputation: 916

pow2_checklooks to be unprovable. Take for instance n=4. log2 4 is equal to 2, but land 4 3 is equal to 0.

There seems to be a confusion between "n is a power of 2" and "log2 n = 0" (which holds iff n < 2).

About the second theorem: Stdlib contains the following lemma

Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n

Upvotes: 1

Related Questions