求助：证明Coq中位运算优化定理——2的幂取模等价性

我正在尝试证明一个常见位运算技巧的等价性：

• 命题：0 < m ∧ land m (m - 1) = 0 → modulo i m = land i (m - 1)，即当m为2的幂时，对m取模可以等价于i和m-1做位与运算。

我已经完成了部分算术推导，但涉及位运算的部分不知道该用什么技巧推进证明，希望能得到帮助。

以下是我目前写的Coq代码：

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.

证明思路提示 #

1. 转化位运算条件为指数形式
   先证明引理：0 < m ∧ land m (m-1) = 0等价于存在自然数k，使得m = 2^k。这个转化能把位运算条件转化为更易处理的算术形式，Coq的Nat库中有Nat.land_pred_self等辅助定理可复用。
   示例引理框架：

   Lemma pow2_iff_land : forall m : nat, 0 < m -> (land m (m - 1) = 0) <-> exists k, m = 2 ^ k.
   

2. 分情况处理i与m的大小关系

   • 当i < m时：modulo i m = i，此时只需证明land i (m-1) = i。因为m是2的幂，m-1的二进制是连续的k个1，i < m意味着i的二进制位数不超过k，位与后结果就是自身。
   • 当i >= m时：设i = q*m + r（0 <= r < m），则modulo i m = r。由于q*m是2的幂的倍数，其二进制末尾k位全为0，因此land (q*m) (m-1) = 0，进而land i (m-1) = land r (m-1) = r。

3. 复用Coq库中位运算定理
   可借助Nat.land_comm（交换律）、Nat.land_distr_l（左分配律）、Nat.land_pow2_pred（land (2^k) (2^k - 1) = 0）等已有定理简化推导。

4. 按指数归纳而非直接对m/i归纳
   针对m=2^k中的k进行归纳，能直接利用2的幂的递推性质，比直接对m或i归纳更清晰。

内容的提问来源于stack exchange，提问作者limitedeternity