Added new lemma: mod_false_spec

[Shark-with-Blue-Shoes]

• Added mod_false_spec.

I added and proved this lemma to the NBits.v file:

Lemma mod_false_spec :
  forall a n j, testbit a n = false -> testbit (a mod 2 ^ j) n = false.

[Shark-with-Blue-Shoes]

Let me know if there is any issue with how I formatted the PR! I'd like to get this lemma added to the standard lib soon.

[andres-erbsen]

Our apologies for the slow reply.

Could you motivate the usefulness and naming of this lemma a bit? If I saw the LHS in a goal, i'd rewrite with the generic lemma for testbit of mod-2^_, and then with the hypothesis.

[Shark-with-Blue-Shoes]

Can you clarify what you mean by LHS? Also, which lemma are you referring to when you say "the generic lemma for testbit of mod-2^_"?

[ErrWare]

Chiming in. At the bottom are the results for Search N.testbit N.modulo 2. in Rocq 9.0.0. The most similar to mod_false_spec are N.mod_pow2_bits_{high,low} which state:

N.mod_pow2_bits_low:
  forall a n m : N, m < n -> testbit (a mod 2 ^ n) m = testbit a m

N.mod_pow2_bits_high:
  forall a n m : N, n <= m -> testbit (a mod 2 ^ n) m = false

Both of these require proving a relationship about the index tested and the modulo taken, which is fundamentally different than throwing the modulo away and reasoning exclusively about testing the unmodulo'd value a. Perhaps an isolated goal where mod_false_spec was used in the proof script may help demonstrating its helpfulness.

---

I think LHS refers to the left-hand-side of the consequent equation, i.e., the testbit (a mod 2 ^ j) n part of the testbit (a mod 2 ^ j) n = false consequent of mod_false_spec. Confusing because there are two equations and which you default to thinking about depends on whether you're used to forward or backward reasoning.

An alternative name might be mod_pow2_false or mod_pow2_bits_false to align better with the mod pow2 lemmas.

(* results of `Search N.testbit N.modulo 2.`*)
N.bit0_mod: forall a : N, N.b2n (N.testbit a 0) = a mod 2

N.bit0_eqb: forall a : N, N.testbit a 0 = (a mod 2 =? 1)

N.testbit_spec': forall a n : N, N.b2n (N.testbit a n) = (a / 2 ^ n) mod 2

N.mod_pow2_bits_low:
  forall a n m : N, m < n -> N.testbit (a mod 2 ^ n) m = N.testbit a m

N.mod_pow2_bits_high:
  forall a n m : N, n <= m -> N.testbit (a mod 2 ^ n) m = false

N.testbit_eqb: forall a n : N, N.testbit a n = ((a / 2 ^ n) mod 2 =? 1)

N.testbit_true:
  forall a n : N, N.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1

N.testbit_false:
  forall a n : N, N.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0

[andres-erbsen]

The lemma I had in mind was Z.testbit_mod_pow2, but indeed, looks like there is no N version of it. If there was, would that solve your use case?

(If we want to go ahead with adding this lemma, maybe testbit_false_mod_pow2 could be a good name)

[Shark-with-Blue-Shoes]

I agree with the name testbit_false_mod_pow2. An N version of Z.testbit_mod_pow2 might be useful, but I like the simplicity of testbit_false_mod_pow2.

[andres-erbsen]

The job was not acquired by Runner of type hosted even after multiple attempts
Internal server error. Correlation ID: fdac14b1-efbb-4fd2-9d70-a7dad37cc082

:/

[andres-erbsen]

Thank you for the contribution!

[Shark-with-Blue-Shoes]

@ErrWare Thanks for chiming in!