[Merged by Bors] - feat: port Mathlib 3's `Nat.factors` norm_num extension to a `simproc` by eric-wieser · Pull Request #15420 · leanprover-community/mathlib4

eric-wieser · 2024-08-01T22:26:11Z

This is a partial attempt at #15410, porting #8009

github-actions · 2024-08-01T22:26:52Z

please_merge_master.md

YaelDillies

Could you add more inline comments in the meta code? It would help maintainability

Mathlib/Tactic/NormNum/Factors.lean

Ruben-VandeVelde · 2025-01-14T21:17:32Z

@YaelDillies do you want to take another look?

Mathlib/Tactic/NormNum/Factors.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

github-actions · 2025-02-14T10:28:58Z

please_merge_master.md

github-actions · 2025-02-14T10:29:03Z

please_merge_master.md

YaelDillies · 2025-02-15T12:33:21Z

I still maintain that this shouldn't be in the NormNum folder. I am writing the simproc from https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Compute.20pairs.20of.20divisors and thinking of putting it in a new Mathlib.Tactic.Simp folder.

Mathlib/Tactic/NormNum/Factors.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

…-norm_num

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-06-12T11:25:11Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

fpvandoorn · 2025-06-12T11:36:05Z

reviewing it right now

fpvandoorn · 2025-06-12T13:01:37Z

Mathlib/Tactic/Simproc/Factors.lean

+      -- Otherwise when we recurse, we should use `b` as the new minimum factor. Note that
+      -- we must use `evalMinFac.core` to get a proof that `b` is what we computed it as.
+      have eb : Q(ℕ) := mkRawNatLit b
+      have ehb : Q(IsNat $eb $eb) := q(⟨rfl⟩)


Can you add ofNat here (and quickly check whether it needs to be added elsewhere)?

Otherwise, LGTM

bors d+

Done, there was one more.

mathlib-bors · 2025-06-12T13:01:39Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

ghost · 2025-06-13T10:06:26Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

#15420) This is a partial attempt at #15410, porting [#8009](leanprover-community/mathlib3#8009) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-06-13T10:15:12Z

Pull request successfully merged into master.

Build succeeded:

CI Success

leanprover-community#15420) This is a partial attempt at leanprover-community#15410, porting [leanprover-community#8009](leanprover-community/mathlib3#8009) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser force-pushed the eric-wieser/factors-norm_num branch from ccce0b1 to 3ad9f80 Compare August 1, 2024 22:26

grunweg added the t-meta Tactics, attributes or user commands label Aug 15, 2024

eric-wieser changed the title ~~feat: port the Nat.factors norm_num extension from Mathlib 3~~ feat: port Mathlib 3's Nat.factors norm_num extension to a simproc Jan 3, 2025

eric-wieser and others added 2 commits January 3, 2025 16:11

feat: port the Nat.factors norm_num extension from Mathlib 3

bdf5c17

style: add proofs that expressions are well-formed

0d7f7d1

eric-wieser force-pushed the eric-wieser/factors-norm_num branch 2 times, most recently from 8a9e35c to 5ebced1 Compare January 3, 2025 16:12

eric-wieser marked this pull request as ready for review January 3, 2025 16:15

eric-wieser requested a review from digama0 January 3, 2025 16:15

tidy

16ed74f

eric-wieser force-pushed the eric-wieser/factors-norm_num branch from 8343d39 to 16ed74f Compare January 3, 2025 16:27

more lint

7b220bf

YaelDillies reviewed Jan 4, 2025

View reviewed changes

eric-wieser added 2 commits January 4, 2025 22:44

tidy and rename

b9fadc9

Comments

3da8b59

YaelDillies reviewed Jan 15, 2025

View reviewed changes

Mathlib/Tactic/NormNum/Factors.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/NormNum/Factors.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/NormNum/Factors.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/NormNum/Factors.lean Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 15, 2025

eric-wieser requested a review from kmill February 14, 2025 10:26

eric-wieser and others added 3 commits February 14, 2025 10:27

Update Mathlib/Tactic/NormNum/Factors.lean

c93e030

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Tactic/NormNum/Factors.lean

d35f9bc

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Tactic/NormNum/Factors.lean

88dd0eb

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

eric-wieser removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 14, 2025

kim-em reviewed Feb 21, 2025

View reviewed changes

Mathlib/Tactic/NormNum/Factors.lean Outdated Show resolved Hide resolved

eric-wieser and others added 3 commits April 13, 2025 01:29

Update MathlibTest/norm_num_ext.lean

5c7bc18

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Tactic/Simproc/Factors.lean

6b7fa3f

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Tactic/Simproc/Factors.lean

5c62945

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

eric-wieser removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 13, 2025

eric-wieser added 2 commits June 12, 2025 11:02

fix imports

5d7fd05

Merge remote-tracking branch 'origin/master' into eric-wieser/factors…

a69b612

…-norm_num

YaelDillies approved these changes Jun 12, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 12, 2025

fpvandoorn reviewed Jun 12, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 12, 2025

OfNat

32002a2

eric-wieser added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jun 13, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jun 13, 2025

mathlib-bors bot changed the title ~~feat: port Mathlib 3's Nat.factors norm_num extension to a simproc~~ [Merged by Bors] - feat: port Mathlib 3's Nat.factors norm_num extension to a simproc Jun 13, 2025

mathlib-bors bot closed this Jun 13, 2025

mathlib-bors bot deleted the eric-wieser/factors-norm_num branch June 13, 2025 10:15

Conversation

eric-wieser commented Aug 1, 2024 • edited by ocfnash Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 1, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde commented Jan 14, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Feb 14, 2025

Uh oh!

github-actions bot commented Feb 14, 2025

Uh oh!

YaelDillies commented Feb 15, 2025 • edited by Parcly-Taxel Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jun 12, 2025

Uh oh!

fpvandoorn commented Jun 12, 2025

Uh oh!

fpvandoorn Jun 12, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jun 13, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

ghost commented Jun 13, 2025

Uh oh!

mathlib-bors bot commented Jun 13, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

eric-wieser commented Aug 1, 2024 •

edited by ocfnash

Loading

github-actions bot commented Aug 1, 2024 •

edited

Loading

YaelDillies commented Feb 15, 2025 •

edited by Parcly-Taxel

Loading