chore: upstream Nat.binaryRec
#3756
Conversation
|
Mathlib CI status (docs):
|
|
Please include in the PR description an explanation of why this should be moved to Lean. (Not just a link to zulip, which doesn't really explain either.) |
|
awaiting-review |
|
!bench (Looks like I can't trigger lean4 benchmark. The CI of my mathlib4 testing PR is very slow. Maybe I got something wrong.) Let me rebase to |
7db39b9 to
c751e82
Compare
| | 0, _ => .inl rfl | ||
| | 1, _ => .inr rfl | ||
|
|
||
| @[simp] theorem one_land_eq_mod_two (n : Nat) : 1 &&& n = n % 2 := by |
There was a problem hiding this comment.
Should be one_and_eq_mod_two for consistency?
There was a problem hiding this comment.
We have Nat.land_bit Nat.land_comm Nat.land_assoc Nat.testBit_land in Mathlib now.
There was a problem hiding this comment.
Maybe those should all be changed too. :-) I'm more concerned about internal consistency in lean4 here.
| | f b n n0 hyp => | ||
| obtain ⟨i, h⟩ := hyp n0 | ||
| refine ⟨i + 1, ?_⟩ | ||
| rwa [testBit_succ, bit_div_two] | ||
|
|
||
| theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by |
There was a problem hiding this comment.
This could be renamed (with a deprecation) to exists_testBit_ne_of_ne.
| @@ -88,51 +98,37 @@ theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := | |||
| | succ i hyp => | |||
| simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ'] | |||
|
|
|||
| @[simp] theorem _root_.Bool.toNat_testBit_zero (b : Bool) : b.toNat.testBit 0 = b := by | |||
| cases b <;> rfl | |||
|
|
|||
| theorem toNat_testBit (x i : Nat) : | |||
| (x.testBit i).toNat = x / 2 ^ i % 2 := by | |||
| rw [Nat.testBit_to_div_mod] | |||
| rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all | |||
|
|
|||
| theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by | |||
There was a problem hiding this comment.
exists_testBit_eq_true_of_ne_zero? or just exists_testBit?
| | n+1 => | ||
| obtain ⟨i, h⟩ := hyp (mul_two_le_bit.mp p) | ||
| refine ⟨i + 1, ?_⟩ | ||
| rwa [Nat.add_le_add_iff_right, testBit_succ, bit_div_two] | ||
|
|
||
| theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by |
There was a problem hiding this comment.
Hmm, all these implies in the names are bad. They predate this PR of course. Maybe we should deal with them separately.
|
I'm still uncertain about whether it is a good idea to move Would you consider splitting this into a PR that does all the cleanup that you do here without adding |
|
(This is not urgent at this point while we're still deciding what to do, but certainly for this PR to be merged we'll need a successful mathlib build, which I think hasn't occurred yet.) |
|
We had leanprover-community/mathlib4#12419 2 weeks ago. Should I force-push to lean-pr-testing-3756? |
Yes, you can keep pushing commits to lean-pr-testing-3756 to get it working. |
I split the change of |
This was a PR for Std, but everything in
Std.Data.Nat.Bitwisehas been moved to Init.Nat.binaryRec,Nat.binaryRec'andNat.binaryRecFromOnereplaceNat.div2Induction, which is noncomputable and more difficult to use. These definitions have been modified to be simpler and faster than the current version in Mathlib.We also need
Nat.bitbecause it is part of the type ofNat.binaryRecand we need some lemmas about it in this PR. If we do not introduce this definition, we'll have to usecond beverywhere. We cannot useBool.toNathere because we have the import chainInit.Data.Nat.Bitwise.Basic->Init.Data.Fin.Basic->Init.Data.Array.Basic->Init.Data.Array.Basic->Init.Data.Array.Subarray->Init.NotationExtra->Init.BinderPredicates->Init.Data.Bool.Was leanprover-community/batteries#314.
Zulip
mathlib adaptations: leanprover-community/mathlib4#12419