Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(number_theory/miller_rabin): adding lemmas about the miller rabin primality test. #12254

Open
wants to merge 304 commits into
base: master
Choose a base branch
from
Open

feat(number_theory/miller_rabin): adding lemmas about the miller rabin primality test. #12254

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
304 commits
Select commit Hold shift + click to select a range
847bbaf
progress
seangolinski7 Mar 17, 2022
7076b57
add new todos
BoltonBailey Mar 18, 2022
fe7ce5d
new todos
BoltonBailey Mar 20, 2022
7f450ed
progress
seangolinski7 Mar 20, 2022
4c75751
Merge branch 'miller-rabin' of https://github.com/leanprover-communit…
seangolinski7 Mar 20, 2022
c664e5c
mwe file
seangolinski7 Mar 23, 2022
e913de5
changed mwe
BoltonBailey Mar 23, 2022
424b22c
git task
BoltonBailey Mar 23, 2022
e90e47b
refactor task
BoltonBailey Mar 23, 2022
d4bcbf3
Changed recs
BoltonBailey Mar 27, 2022
1d373ed
typo
BoltonBailey Mar 27, 2022
03b3a70
simp lemmas for succinctness
BoltonBailey Mar 27, 2022
6dcc110
golfing
BoltonBailey Mar 27, 2022
94340ee
progress
seangolinski7 Mar 27, 2022
b87c722
fixed von_mangold_sum proof
seangolinski7 Mar 27, 2022
c2cc886
added gcd_mul_of_dvd_coprime
seangolinski7 Mar 27, 2022
2d603ba
progress
seangolinski7 Mar 27, 2022
2266b49
Merge branch 'master' of https://github.com/leanprover-community/math…
seangolinski7 Mar 27, 2022
6510dc2
Merge branch 'gcd_mul_of_dvd_coprime' of github.com:leanprover-commun…
BoltonBailey Mar 28, 2022
ef6280a
Merge branch 'BoltonBailey/nat_rec_edits' of github.com:leanprover-co…
BoltonBailey Mar 28, 2022
8ea067d
TODOs
BoltonBailey Mar 28, 2022
f9a1263
progress
seangolinski7 Mar 31, 2022
7e9798a
changes to gcd_mul_of_coprime_of_dvd name
seangolinski7 Mar 31, 2022
9e65ce9
Update src/data/nat/gcd.lean
seangolinski7 Mar 31, 2022
58da701
name change
seangolinski7 Mar 31, 2022
3484417
Merge branch 'gcd_mul_of_dvd_coprime' of https://github.com/leanprove…
seangolinski7 Mar 31, 2022
118195d
changes
BoltonBailey Apr 2, 2022
55f541c
Merge branch 'miller-rabin' of github.com:leanprover-community/mathli…
BoltonBailey Apr 2, 2022
5434550
progress
seangolinski7 Apr 3, 2022
f344b9a
Merge branch 'miller-rabin' of https://github.com/leanprover-communit…
seangolinski7 Apr 3, 2022
cd668ad
new fast multiplicity def
BoltonBailey Apr 3, 2022
352946a
add proper subgroup theorem
BoltonBailey Apr 4, 2022
6892c4f
correct definition
BoltonBailey Apr 4, 2022
cc42836
progress
seangolinski7 Apr 6, 2022
c3d431e
Merge branch 'miller-rabin' of https://github.com/leanprover-communit…
seangolinski7 Apr 6, 2022
93f6a90
progress
seangolinski7 Apr 6, 2022
52f9e49
resolved merge conflicts
seangolinski7 Apr 6, 2022
b4f7d16
resolved merge conflict
seangolinski7 Apr 10, 2022
8956e68
add rw
BoltonBailey Apr 10, 2022
cc4db1a
Merge branch 'miller-rabin' of github.com:leanprover-community/mathli…
BoltonBailey Apr 10, 2022
213e31b
TODOs for Bolton lol
seangolinski7 Apr 10, 2022
3fe90fc
fixed hypothesis
BoltonBailey Apr 11, 2022
e41d2f4
another todo
BoltonBailey Apr 13, 2022
c1fe337
Delete mwe.lean
BoltonBailey Apr 13, 2022
6de264c
solve goal
BoltonBailey Apr 13, 2022
be2385b
Merge branch 'miller-rabin' of github.com:leanprover-community/mathli…
BoltonBailey Apr 13, 2022
511c05b
progress
seangolinski7 Apr 13, 2022
f2c2c3b
Merge branch 'miller-rabin' of https://github.com/leanprover-communit…
seangolinski7 Apr 13, 2022
c15a370
progress
seangolinski7 Apr 13, 2022
f5434cb
work
BoltonBailey Apr 13, 2022
b169118
Merge branch 'miller-rabin' of github.com:leanprover-community/mathli…
BoltonBailey Apr 13, 2022
9c2b771
work on 1 case
BoltonBailey Apr 14, 2022
12b890b
testing in progress
seangolinski7 Apr 15, 2022
91e4979
Merge branch 'miller-rabin' of https://github.com/leanprover-communit…
seangolinski7 Apr 15, 2022
af09797
commit
BoltonBailey Apr 16, 2022
15bcea4
proofs
seangolinski7 Apr 17, 2022
8942d80
small change
seangolinski7 Apr 17, 2022
65534e3
changes
BoltonBailey Apr 17, 2022
b7656f5
changes
BoltonBailey Apr 17, 2022
8aa54ef
Merge branch 'miller-rabin' of github.com:leanprover-community/mathli…
BoltonBailey Apr 17, 2022
47681ed
made fermat test work
BoltonBailey Apr 17, 2022
92bc2cf
new tests
BoltonBailey Apr 17, 2022
39f296c
new test
BoltonBailey Apr 17, 2022
d9f42b8
fix card lemma
BoltonBailey Apr 21, 2022
43893a2
edits
BoltonBailey Apr 21, 2022
a712019
progress
BoltonBailey Apr 22, 2022
ccf9237
Define `padic_part` and `p_odd_part`
stuart-presnell Jul 20, 2022
df37af5
Add `padic_part_def` and `p_odd_part_def`
stuart-presnell Jul 20, 2022
6abeb94
Move `pow_factorization_dvd`
stuart-presnell Jul 20, 2022
beba86e
Edit `pow_factorization_dvd`
stuart-presnell Jul 20, 2022
4c59722
Move and edit `pow_factorization_le`
stuart-presnell Jul 20, 2022
34fcc20
Move and edit `div_pow_factorization_ne_zero`
stuart-presnell Jul 20, 2022
49a16e5
Add TODO
stuart-presnell Jul 20, 2022
3acab4d
Move lemmas back
stuart-presnell Jul 20, 2022
3dfa764
Add lemma `padic_part_ne_zero`
stuart-presnell Jul 20, 2022
a37db57
Rename to `padic_part_pos` and `padic_part_le`
stuart-presnell Jul 20, 2022
7d895e8
Add TODOs
stuart-presnell Jul 20, 2022
6fedd45
Rename `div_pow_factorization_ne_zero` to `p_odd_part`
stuart-presnell Jul 20, 2022
f2e1e82
Add `p_odd_part_le`
stuart-presnell Jul 20, 2022
ffac414
Add `p_odd_part_dvd`
stuart-presnell Jul 20, 2022
9197944
Move & edit `not_dvd_div_pow_factorization`
stuart-presnell Jul 20, 2022
3844701
Prove `padic_mul_p_odd_part_eq_self`
stuart-presnell Jul 20, 2022
b8379d6
Prove `mul_padic_part`
stuart-presnell Jul 20, 2022
df0c5ca
Prove `mul_p_odd_part`
stuart-presnell Jul 20, 2022
1afd8af
Edit `pow_dvd_iff_dvd_pow_factorization`
stuart-presnell Jul 20, 2022
7bdfd52
Fix TODO!
stuart-presnell Jul 20, 2022
33ff397
Prove `factorization_p_odd_part`
stuart-presnell Jul 20, 2022
5f38419
Merge branch 'master' into SP_padic_odd_part
stuart-presnell Jul 21, 2022
3a8d8e3
Delete `noncomputable` :)
stuart-presnell Jul 21, 2022
0cd8cad
Fix docstring!
stuart-presnell Jul 21, 2022
c02969e
Prove `dvd_p_odd_part_of_dvd_not_dvd`
stuart-presnell Jul 21, 2022
4a6d78c
Rename & edit `coprime_of_p_odd_part`
stuart-presnell Jul 21, 2022
cf99d54
Update TODO list
stuart-presnell Jul 21, 2022
60e9700
Add `dvd_padic_part_of_dvd`
stuart-presnell Jul 21, 2022
5d53981
Temp: add `eq_of_dvd_div_eq_one`
stuart-presnell Jul 21, 2022
351caae
Add `is_prime_pow_of_p_odd_part_eq_one`
stuart-presnell Jul 21, 2022
e01a328
Fix `is_prime_pow_iff_unique_prime_dvd`
stuart-presnell Jul 21, 2022
5cb97a7
Add lemmas for `¬ p.prime`
stuart-presnell Jul 21, 2022
ccfdc27
Remove `@simp` to fix lint; fix proofs
stuart-presnell Jul 21, 2022
8469358
Test: `reducible`
stuart-presnell Jul 22, 2022
bf59733
Change notation to `ord[p]` and `coord[p]`
stuart-presnell Jul 23, 2022
8b9f88d
Fix `factorization/prime_pow`
stuart-presnell Jul 23, 2022
ed189c8
Use `ord` in definition of `coord`
stuart-presnell Jul 23, 2022
4309129
delete `#lint`
stuart-presnell Jul 23, 2022
e4e44b4
Rename to `ord_proj` and `ord_compl`
stuart-presnell Jul 25, 2022
6de7264
Rename lemmas
stuart-presnell Jul 25, 2022
ca78de5
Swap in `mul_ord_compl`
stuart-presnell Jul 25, 2022
e9bf18c
Rename to `not_dvd_ord_compl`
stuart-presnell Jul 25, 2022
3dd2314
Fix docstring
stuart-presnell Jul 25, 2022
6f3be91
Add new section header
stuart-presnell Jul 25, 2022
7fcb8bd
Revert unrelated changes to be PRed elsewhere
stuart-presnell Jul 25, 2022
ae01773
Change docstrings
stuart-presnell Jul 26, 2022
1e0528a
Fix typo
stuart-presnell Jul 27, 2022
45579f7
Merge branch 'master' into miller-rabin
stuart-presnell Jul 27, 2022
a82de19
Merge branch 'SP_padic_odd_part' into miller-rabin
stuart-presnell Jul 27, 2022
0af5496
open nat
stuart-presnell Jul 27, 2022
be1ad67
Fix some fails
stuart-presnell Jul 28, 2022
191a284
Add `fintype.of_subgroup`
stuart-presnell Jul 28, 2022
e9af1f2
Fix another fail, comment out a rw
stuart-presnell Jul 28, 2022
e8617ee
Format brackets
stuart-presnell Jul 28, 2022
4b2766f
Add copyright notice
stuart-presnell Jul 28, 2022
88ec692
Fix overlong lines
stuart-presnell Jul 28, 2022
951ab25
Add temp docstring placeholders
stuart-presnell Jul 28, 2022
a4e5ec1
Fix overlong lines
stuart-presnell Jul 28, 2022
41df7d6
Add temp docstring
stuart-presnell Jul 28, 2022
7899b95
Add temp docstring
stuart-presnell Jul 28, 2022
e23746d
Properly format temp docstrings
stuart-presnell Jul 28, 2022
860e3fa
Comment out `set_option profiler true`
stuart-presnell Jul 28, 2022
c37acf9
Format bracket
stuart-presnell Jul 28, 2022
3c67ee2
Move up imports
stuart-presnell Jul 28, 2022
d0caa65
Comment out `#eval`; add trivial example
stuart-presnell Jul 28, 2022
2af14bb
Change `padic_val_nat` to `factorization`
stuart-presnell Jul 28, 2022
4f54ead
Change "two_power" to "even"
stuart-presnell Jul 28, 2022
605e356
docstring for `strong_probable_prime`
stuart-presnell Jul 28, 2022
cdb668f
Move up `square_roots_of_one`
stuart-presnell Jul 28, 2022
de0865b
Format `square_roots_of_one`
stuart-presnell Jul 28, 2022
729cb47
Golf `square_roots_of_one`
stuart-presnell Jul 28, 2022
59c6162
Move down `fermat_pseudoprime`
stuart-presnell Jul 28, 2022
bf61822
docstring for `repeated_halving_of_exponent`
stuart-presnell Jul 28, 2022
189c734
Golf `repeated_halving_of_exponent`
stuart-presnell Jul 28, 2022
25a9041
Implicit args in `repeated_halving_of_exponent`
stuart-presnell Jul 28, 2022
7ef0cd4
docstring for `strong_probable_prime_of_prime`
stuart-presnell Jul 28, 2022
fe6f242
Golf `nat.even_two_pow_iff`
stuart-presnell Jul 28, 2022
907cefc
Move up `nat.even_two_pow_iff`
stuart-presnell Jul 28, 2022
c3ce282
docstrings for `fermat_pseudoprime`
stuart-presnell Jul 28, 2022
e6f174d
Golf `fermat_..._probable_prime`
stuart-presnell Jul 28, 2022
2374207
Golf `fermat_..._prime`
stuart-presnell Jul 28, 2022
d9840e6
Move up `sub_one_dvd_pow_sub_one`
stuart-presnell Jul 28, 2022
b1fc8bf
Golf `sub_one_dvd_pow_sub_one`
stuart-presnell Jul 28, 2022
fbb3ce8
Move and golf `coprime_add_one`
stuart-presnell Jul 28, 2022
e58b3bb
Move and golf `coprime_self_sub_one`
stuart-presnell Jul 28, 2022
c7ad258
Start work on Theorem 3.4
stuart-presnell Jul 29, 2022
c03ad1d
Prove factorization on p. 1 of Conrad
stuart-presnell Jul 29, 2022
1847e57
Remove assumptions on polynomial factorization
stuart-presnell Jul 29, 2022
3b25ff5
Docstring for file explaining Miller-Rabin test
stuart-presnell Jul 29, 2022
9b2f259
Generalise to `factorise_pow_two_pow_sub_one`
stuart-presnell Jul 29, 2022
a6a7a62
Define `miller_rabin_witness`
stuart-presnell Jul 29, 2022
bdce481
Prove `one_not_miller_rabin_witness`
stuart-presnell Jul 29, 2022
1e18183
Prove `minus_one_not_miller_rabin_witness`
stuart-presnell Jul 29, 2022
0f7e7b7
Prove `odd_of_odd_part`
stuart-presnell Jul 29, 2022
dc9037a
Fix `minus_one_not_miller_rabin_witness`
stuart-presnell Jul 29, 2022
394b187
Edit definition of `miller_rabin_witness`
stuart-presnell Jul 29, 2022
bd88309
Edit docstring for `strong_probable_prime`; prove
stuart-presnell Jul 29, 2022
7a8d1a7
Define `miller_rabin_sequence` & eval examples
stuart-presnell Jul 29, 2022
aec59ca
Prove `length_miller_rabin_sequence`
stuart-presnell Jul 29, 2022
9146249
Name `strong_probable_prime_iff_nonwitness`
stuart-presnell Jul 29, 2022
1803884
Prove `strong_..._iff_miller_rabin_sequence`
stuart-presnell Jul 29, 2022
ebd69ed
Delete `import number_theory.padics.padic_norm`
stuart-presnell Jul 30, 2022
558827e
docstrings for `even_part` and `odd_part`
stuart-presnell Jul 30, 2022
6bfffab
Prove `factorization_two_pos_of_even_of_pos`
stuart-presnell Jul 30, 2022
da6c69c
Move down ±1 not witness
stuart-presnell Jul 30, 2022
d940243
Add `nat.mem_miller_rabin_sequence`
stuart-presnell Jul 30, 2022
a2ca8a3
Golf `minus_one_not_miller_rabin_witness`
stuart-presnell Jul 30, 2022
179ba00
Rename to `factorization_two_pos_sub_one`
stuart-presnell Jul 30, 2022
c76e06d
Prove `strong_probable_prime_of_prime'`
stuart-presnell Jul 30, 2022
2b39f44
Temporary name: `factorize_poly`
stuart-presnell Jul 30, 2022
3e296dc
Prove `factorize_poly'` for arbitrary `comm_ring`
stuart-presnell Jul 31, 2022
a497f3d
`strong_probable_prime_of_prime''` for zmod p
stuart-presnell Jul 31, 2022
cb8e3d7
Move up `strong_probable_prime_of_prime''`
stuart-presnell Jul 31, 2022
a5f93ec
Add section headers
stuart-presnell Jul 31, 2022
4aa125c
Rename Theorem 3.4
stuart-presnell Jul 31, 2022
2031937
Define Fermat witness and Fermat candidate-prime
stuart-presnell Jul 31, 2022
e2b58df
Prove `miller_rabin_witness_of_fermat_witness`
stuart-presnell Jul 31, 2022
aa45646
Golf `fermat_cprime_of_strong_probable_prime`
stuart-presnell Jul 31, 2022
6de9ec5
Golf `strong_probable_prime_of_prime_power_iff`
stuart-presnell Jul 31, 2022
defb221
open_locale nat to use `φ` for `nat.totient`
stuart-presnell Jul 31, 2022
7770439
Golf `euler`
stuart-presnell Jul 31, 2022
a01fe4c
Golf by `fermat_cprime_of_strong_probable_prime`
stuart-presnell Jul 31, 2022
e88c107
Golf 1st half of Theorem 3.4
stuart-presnell Jul 31, 2022
c6a50cb
Start 2nd half of Theorem 3.4
stuart-presnell Jul 31, 2022
2cff2b1
Golf j=0 case
stuart-presnell Jul 31, 2022
def57e0
Structure of (j ≠ 0) case
stuart-presnell Jul 31, 2022
f51f26a
Fill in `hk_odd`
stuart-presnell Jul 31, 2022
2f96f7d
Fill in `hfe`
stuart-presnell Jul 31, 2022
58cf591
Fill in `hx1`
stuart-presnell Jul 31, 2022
d801317
Clumsy draft of `hx2`
stuart-presnell Jul 31, 2022
81f1c3c
Fill in `h6`
stuart-presnell Jul 31, 2022
dc68987
Found an error in my write-up
stuart-presnell Jul 31, 2022
6fab088
Remove `hα : 1 ≤ α`
stuart-presnell Aug 1, 2022
15f903c
Add temp lemmas from #15793
stuart-presnell Aug 1, 2022
9768e28
Finish `hlk` with `ord_compl_dvd_ord_compl_of_dvd`
stuart-presnell Aug 1, 2022
24dc58f
Some minor edits
stuart-presnell Aug 1, 2022
c55803d
Add comments; rename `H` to `hjf`
stuart-presnell Aug 1, 2022
463467d
Introduce new hx1', hx2' to fix error; fill in h3
stuart-presnell Aug 1, 2022
4b2908b
Re-write proof structure to fix earlier big error
stuart-presnell Aug 1, 2022
d0137d1
Move exponents
stuart-presnell Aug 1, 2022
cc5bdaf
Factor `spp_of_prime_power_iff` thru `square_roots_of_one`
stuart-presnell Aug 2, 2022
e84fbe6
Prove `square_roots_of_one` for `x : ℕ`
stuart-presnell Aug 2, 2022
70e3dd8
Outline of `square_roots_of_one` for `zmod (p^α)`
stuart-presnell Aug 2, 2022
dfc31fe
Add `square_roots_of_one_int`
stuart-presnell Aug 3, 2022
b570938
Prove `square_roots_of_one''` for `zmod (p^α)`
stuart-presnell Aug 3, 2022
133c114
Patch `strong_probable_prime_of_prime_power_iff`
stuart-presnell Aug 3, 2022
25de5ec
Insert proof of `ord_compl_dvd_ord_compl_of_dvd`
stuart-presnell Aug 3, 2022
420f127
Add assumption `hp_odd` to `spp...power_iff`
stuart-presnell Aug 3, 2022
8b0cdc5
Confirm `spp...power_iff` has no `sorry`s
stuart-presnell Aug 3, 2022
55f80da
docstring for first draft of Conrad Theorem 3.4
stuart-presnell Aug 3, 2022
9b3d7c4
Golf & rename `square_roots_of_one_zmod`
stuart-presnell Aug 3, 2022
e8f82d7
Format and deal with some simps
stuart-presnell Aug 3, 2022
a3375f1
Format braces
stuart-presnell Aug 3, 2022
598b535
Fix error at end of Theorem 3.4
stuart-presnell Aug 3, 2022
98f2974
Tidy up `pow_eq_one_subgroup`
stuart-presnell Aug 3, 2022
adb9f2b
Tidy up `pow_alt_subgroup`
stuart-presnell Aug 3, 2022
fce4a16
Golf `coprime_factorization_or_prime_power`
stuart-presnell Aug 4, 2022
df79f88
Golf `one_or_coprime_factorization_or_prime_power`
stuart-presnell Aug 4, 2022
3c82d6a
Golf `card_closed_subset_dvd_card`
stuart-presnell Aug 4, 2022
8bc050e
Golf `card_le_half_of_proper_subgroup`
stuart-presnell Aug 4, 2022
31485e2
Golf `decidable_pred is_unit`
stuart-presnell Aug 4, 2022
49b9472
Add import of `is_prime_pow`; rename `coprime_add_one`
stuart-presnell Aug 11, 2022
1013549
Edit `square_roots_of_one_zmod`
stuart-presnell Aug 11, 2022
61a37d4
Add instance `decidable_witness`
stuart-presnell Aug 11, 2022
72a8e07
Add `mul_pow_pred` for `ℕ` and `zmod n`
stuart-presnell Aug 11, 2022
0469ec7
Add divider at end of Theorem 3.4
stuart-presnell Aug 11, 2022
e157954
Move up lemmas on subgroup cardinality
stuart-presnell Aug 11, 2022
f76ab4b
Edit Thm 3.4 to use `nat.miller_rabin_witness`
stuart-presnell Aug 11, 2022
e2527c0
Fix typo
stuart-presnell Aug 11, 2022
38af6ba
Rename to `MR_nonwitness_iff_miller_rabin_sequence`
stuart-presnell Aug 11, 2022
d3a29ee
Move up lemmas about Fermat witnesses
stuart-presnell Aug 12, 2022
c6e27e3
Prove `fermat_nonwitness_mul`
stuart-presnell Aug 12, 2022
7f6ab27
Prove `fermat_nonwitness_of_prime`
stuart-presnell Aug 12, 2022
0d1b390
Prove `MR_witness_iff_miller_rabin_sequence`
stuart-presnell Aug 12, 2022
ab22ffa
Some more computations
stuart-presnell Aug 13, 2022
fb1e428
Add `pow_mul_eq_pow_pow_comm`
stuart-presnell Aug 13, 2022
8411e2c
Add `even_not_dvd_odd`
stuart-presnell Aug 15, 2022
508e423
Add `eq_{neg_}one_of_eq_{neg_}one_modulus_dvd`
stuart-presnell Aug 15, 2022
94f2635
Add `pow_mul_eq_pow_pow_comm`
stuart-presnell Aug 15, 2022
26c8ee0
Merge branch 'master' into miller-rabin
stuart-presnell Aug 29, 2022
0ac6272
Fix after renaming `ord_{proj,compl}_mul`
stuart-presnell Aug 29, 2022
c9424ed
Comment out sorried lemmas
stuart-presnell Aug 29, 2022
42c9db8
Fix lint error
stuart-presnell Aug 29, 2022
54169ed
Remove unused args
stuart-presnell Aug 29, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view