[Merged by Bors] - chore: remove bit0/bit1 and associated lemmas#14745
[Merged by Bors] - chore: remove bit0/bit1 and associated lemmas#14745
Conversation
|
|
PR summary aa3889edc7
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Init.Data.Nat.Basic | 39 | 7 | -32 (-82.05%) |
| Mathlib.Init.Data.Nat.Lemmas | 43 | 12 | -31 (-72.09%) |
| Mathlib.Data.Num.Prime | 544 | 543 | -1 (-0.18%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Init.Data.Nat.Basic |
-32 |
Mathlib.Init.Data.Nat.Lemmas |
-31 |
Mathlib.Data.Num.Prime |
-1 |
Declarations diff
+-+- not_even_bit1
+-+- pointReflection_fixed_iff_of_injective_bit0
+-+--+ bit1_of_bit1
+--+-+- cast_bit0
+--+-+- cast_bit1
- bit0_apply_eq_zero
- bit0_comp
- bit0_div_bit0
- bit0_div_two
- bit0_eq_bit0
- bit0_eq_two_mul
- bit0_mod_bit0
- bit0_zero
- bit1
- bit1_apply_eq_one
- bit1_comp
- bit1_div_bit0
- bit1_div_two
- bit1_eq_bit1
- bit1_mod_bit0
- bit1_zero
- coeff_cos_bit0
- coeff_cos_bit1
- coeff_sin_bit0
- coeff_sin_bit1
- even_bit0
- fib_bit0
- fib_bit0_succ
- fib_bit1
- fib_bit1_succ
- odd_bit1
- one_eq_bit1
- pow_bit0_nonneg
- pow_bit0_pos
- pow_bit0_pos_iff
- pow_bit1_neg_iff
- pow_bit1_nonneg_iff
- pow_bit1_nonpos_iff
- pow_bit1_pos_iff
- strictMono_pow_bit1
- two_dvd_bit0
- two_dvd_bit1
- zero_eq_bit0
- zpow_bit0_abs
-+- bit0_ne_bit1
-+- bit0_ne_zero
-+- bit1_ne_bit0
-+- bit1_ne_zero
-+- zero_ne_bit0
-+-+-+ bit0_of_bit0
-- bit0
-- bit0_val
-- bit1_eq_one
-- bit1_val
-- bodd_bit0
-- bodd_bit1
--++ bit_to_nat
--+- bit0_eq_zero
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>|
|
|
|
|
LGTM thanks! (I don't understand the mergify error). bors d+ |
|
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
This PR replaces `bit0 x` resp. `bit1 x` with: - `2 * x` resp. `2 * x + 1` if possible, or - `2 • x` resp. `2 • x + 1` if possible, or - `x + x` resp. `x + x + 1` as fallback. The versions `Num.bit0` and `Num.bit1` (as well as the `PosNum` and `ZNum` versions) are left alone. All lemmas that mention `bit0`/`bit1` have been adapted. A follow-up PR can remove these lemmas. Deletions: - bit0 - bit1 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
This PR replaces
bit0 xresp.bit1 xwith:2 * xresp.2 * x + 1if possible, or2 • xresp.2 • x + 1if possible, orx + xresp.x + x + 1as fallback.The versions
Num.bit0andNum.bit1(as well as thePosNumandZNumversions) are left alone.All lemmas that mention
bit0/bit1have been adapted. A follow-up PR can remove these lemmas.Deletions:
This PR combines #14644 and #14744. It might be easier to review those separately.
But I think that this current PR is the one that should be merged in the end.