I'm trying to prove equivalency for a pretty common "bitwise hack", namely:
0 < m /\ land m (m - 1) = 0 -> modulo i m = land i (m - 1): modulo operation optimization for case when m is a power of two.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.
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