From 76d688dac0565545d53f02f735f89d1f0e9d690b Mon Sep 17 00:00:00 2001 From: Humam Alhusaini Date: Wed, 30 Jul 2025 14:25:29 -0500 Subject: [PATCH 1/2] added mod_false_spec --- theories/Numbers/Natural/Abstract/NBits.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 2a7b44cb19..f142797982 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -1312,6 +1312,13 @@ Proof. - now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r. Qed. +Lemma mod_false_spec : + forall a n j, testbit a n = false -> testbit (a mod 2 ^ j) n = false. +Proof. + intros a n j H. rewrite <- land_ones. rewrite land_spec. + rewrite H. rewrite Bool.andb_false_l. reflexivity. +Qed. + Lemma land_ones_low : forall a n, log2 a < n -> land a (ones n) == a. Proof. From 51bf4436cb96f29d8bc2ca89c5ab5538ba68f752 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 21 Aug 2025 12:41:32 -0400 Subject: [PATCH 2/2] rename new lemma to `testbit_false_mod_pow2` --- theories/Numbers/Natural/Abstract/NBits.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index f142797982..b85bab19e4 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -1312,7 +1312,7 @@ Proof. - now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r. Qed. -Lemma mod_false_spec : +Lemma testbit_false_mod_pow2 : forall a n j, testbit a n = false -> testbit (a mod 2 ^ j) n = false. Proof. intros a n j H. rewrite <- land_ones. rewrite land_spec.