[Merged by Bors] - feat: port Data.Nat.PrimeNormNum#3892
[Merged by Bors] - feat: port Data.Nat.PrimeNormNum#3892fpvandoorn wants to merge 23 commits intomasterfrom
Conversation
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
|
Rather than using let binders (which I'm not sure work anyway for this kind of thing), I would simply suggest using tree-like proofs instead of list-like: it's a search, so we can easily use branching proofs saying that if you are good from k=a to k=b and also from k=b to k=c then you are good from k=a to k=c, and apply that instead of just adding 2 and using a subterm for the rest. |
|
Can we do this in a follow-up PR? The current function works well for primes up to 25 bits. For much larger primes we'll want a more efficient implementation anyway. |
|
|
||
| theorem minFacHelper_0 (n : ℕ) (h1 : ¬ n = 1) (h2 : ¬ n % 2 = 0) : MinFacHelper n 3 := by | ||
| theorem minFacHelper_0 (n : ℕ) | ||
| (h1 : Nat.ble (nat_lit 2) n = true) (h2 : nat_lit 1 = n % (nat_lit 2)) : |
There was a problem hiding this comment.
The h2 equality is flipped here because the elaborator doesn't seem to like it the other way around, when you copy and paste a norm_num proof directly (useful for debugging). We might consider doing this more broadly...
| theorem isNat_prime_2 : {n n' : ℕ} → IsNat n n' → Nat.ble 2 n' = true → minFac n = n → n.Prime | ||
| | _, _, ⟨rfl⟩, h1, h2 => prime_def_minFac.mpr ⟨ble_eq.mp h1, h2⟩ | ||
|
|
||
| theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime := isNat.natElim h |
There was a problem hiding this comment.
This is to avoid bound variables / lambda abstraction in norm_num proofs
|
I take it you don't really like the |
|
@digama0 Shall we merge this? |
|
I wasn't sure whether we should merge #4048 before or after this one since otherwise there is this bad interaction with bors r+ |
* Excluding computing `Nat.factors`, which requires a little bit of generalization of `NormNum.Result`. * It's a lot faster than in Lean 3: ``` 2 ^ 19 - 1 is prime: Lean 3: 330ms, Lean 4: 36ms 2 ^ 25 - 39 is prime: Lean 3: 3300ms + multiple seconds type-checking, Lean 4 165ms + <100ms type-checking (2 ^ 19 - 1) * (2 ^ 25 - 39) is not prime: Lean 3: 300ms, Lean 4: 90ms ``` * Simplify the definition of `Nat.minFac` a bit * Added some remarks in the code, explaining why some parts are a bit more verbose than necessary. In these cases, simplifying the code would cause a significant slow-down (my first version of this port was 100x slower). * Note: Calling the function on larger numbers currently does cause panics/stack overflows in Lean 4 Co-authored-by: Mario Carneiro <di.gama@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
* Uses `deriveBool`, which was added in #3892, and allows removal of some `have` lines. * Changes an `if then else` into a match. This is more readable in my opinion.
* Uses `deriveBool`, which was added in #3892, and allows removal of some `have` lines. * Changes an `if then else` into a match. This is more readable in my opinion.
Nat.factors, which requires a little bit of generalization ofNormNum.Result.Nat.minFaca bit