feat: grind_pattern mod_eq_of_lt #11584

pirapira · 2025-12-10T11:57:02Z

This PR enables grind to notice _ mod n is identity if n is bigger than the argument.

This PR was developed a part of Italean2025 project work. I want to add grind annotations on ZMod.val. First I want this annotation on %.

leanprover-community-bot · 2025-12-10T17:04:08Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 088f8b0b9cda2195c2ef10a436573c20f776ea29 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-10 17:04:07)
✅ Mathlib branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-10 20:28:51) View Log
🟡 Mathlib branch lean-pr-testing-11584 build this PR didn't complete normally. (2025-12-11 07:52:02) View Log
✅ Mathlib branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-11 08:56:10) View Log
✅ Mathlib branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-12 10:23:03) View Log

leanprover-bot · 2025-12-10T17:04:10Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 088f8b0b9cda2195c2ef10a436573c20f776ea29 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-10 17:04:09)
✅ Reference manual branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-10 19:31:13) View Log
🟡 Reference manual branch lean-pr-testing-11584 build against this PR didn't complete normally. (2025-12-10 19:32:16) View Log
✅ Reference manual branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-11 06:58:57) View Log
🟡 Reference manual branch lean-pr-testing-11584 build against this PR didn't complete normally. (2025-12-11 06:59:56) View Log
✅ Reference manual branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-11 07:54:54) View Log
🟡 Reference manual branch lean-pr-testing-11584 build against this PR didn't complete normally. (2025-12-11 07:56:25) View Log
✅ Reference manual branch lean-pr-testing-11584 has successfully built against this PR. (2025-12-12 09:25:35) View Log
🟡 Reference manual branch lean-pr-testing-11584 build against this PR didn't complete normally. (2025-12-12 09:26:17) View Log

kim-em · 2025-12-11T00:51:59Z

Tests should go in tests/lean/run/. No need for this test.

I wonder if adding isNotValue b to the guard conditions makes sense. There's no point have this theorem fire because grind sees 1 % 1024. (Not sure about this, isNotValue is brand new and we haven't really explored it yet.)

pirapira · 2025-12-11T06:18:51Z

I removed the test.

I think I came up with a reasonable way to avoid 2 % 1024 while supporting a % 1024 and 2 % b.

src/Init/Data/Nat/Div/Basic.lean

pirapira · 2025-12-12T08:08:12Z

changelog-library

pirapira force-pushed the grind_mod_eq_of_lt branch from 7bfd03d to 59e30f7 Compare December 10, 2025 11:59

pirapira changed the title ~~need help: Add grind_pattern on Nat.mod_eq_of_lt~~ feat: Add grind_pattern on Nat.mod_eq_of_lt Dec 10, 2025

pirapira force-pushed the grind_mod_eq_of_lt branch from 59e30f7 to 0620221 Compare December 10, 2025 14:16

pirapira changed the title ~~feat: Add grind_pattern on Nat.mod_eq_of_lt~~ feat: grind_pattern mod_eq_of_lt Dec 10, 2025

pirapira marked this pull request as ready for review December 10, 2025 14:29

pirapira requested a review from kim-em as a code owner December 10, 2025 14:29

pirapira marked this pull request as draft December 10, 2025 15:27

pirapira marked this pull request as ready for review December 10, 2025 15:42

pirapira marked this pull request as draft December 10, 2025 15:52

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 10, 2025

pirapira added 4 commits December 10, 2025 19:04

feat: Add grind_pattern on Nat.mod_eq_of_lt

8119c86

test: add test for new grind annotation

4dab7bb

test: document new test

1c5fd4d

fix: change test expectation with Nat.mod_eq_of_lt

cfd2ce5

pirapira force-pushed the grind_mod_eq_of_lt branch from 498ffe9 to cfd2ce5 Compare December 10, 2025 18:04

style: remove unneeded parentheses

035d7d7

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 10, 2025

Update lean-toolchain for testing leanprover/lean4#11584

e35bc2c

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Dec 10, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 10, 2025

Update lean-toolchain for testing leanprover/lean4#11584

d634514

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 10, 2025

Update lean-toolchain for testing leanprover/lean4#11584

823e3f2

leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Dec 10, 2025

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 10, 2025

kim-em added the awaiting-author Waiting for PR author to address issues label Dec 11, 2025

chore: remove a test not particularly wanted

47373a4

pirapira mentioned this pull request Dec 11, 2025

RFC: disjunction of guard conditions for grind_pattern #11602

Open

pirapira marked this pull request as ready for review December 11, 2025 06:19

pirapira marked this pull request as draft December 11, 2025 06:42

pirapira added 3 commits December 11, 2025 07:45

fix: supress too concrete instances

1410cd8

fix: revert test expectation

b5074f0

fix: cheaper test first

5be60e5

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 11, 2025

Update lean-toolchain for leanprover/lean4#11584

f8a3a97

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 11, 2025

Update lean-toolchain for leanprover/lean4#11584

6f32604

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 11, 2025

Update lean-toolchain for leanprover/lean4#11584

72cd949

This comment was marked as outdated.

Sign in to view

pirapira marked this pull request as ready for review December 11, 2025 06:53

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 11, 2025

Update lean-toolchain for leanprover/lean4#11584

05f2ff0

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 11, 2025

Update lean-toolchain for leanprover/lean4#11584

b9f4790

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 11, 2025

Update lean-toolchain for leanprover/lean4#11584

4f657a4

pirapira commented Dec 11, 2025

View reviewed changes

src/Init/Data/Nat/Div/Basic.lean Show resolved Hide resolved

pirapira added 2 commits December 11, 2025 15:16

fix: more precise grind_pattern condition on mod_eq_of_lt

d4d9078

fix: prevent overlapping work

b09926b

github-actions bot added the changelog-library Library label Dec 12, 2025

style: comment style

b77d971

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 12, 2025

Update lean-toolchain for leanprover/lean4#11584

2fa11f0

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 12, 2025

Update lean-toolchain for leanprover/lean4#11584

931ceb2

leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 12, 2025

Update lean-toolchain for leanprover/lean4#11584

052ef07

This comment was marked as off-topic.

Sign in to view

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: grind_pattern mod_eq_of_lt #11584

feat: grind_pattern mod_eq_of_lt #11584

pirapira commented Dec 10, 2025 •

edited

Loading

Uh oh!

leanprover-community-bot commented Dec 10, 2025 •

edited

Loading

Uh oh!

leanprover-bot commented Dec 10, 2025 •

edited

Loading

Uh oh!

kim-em commented Dec 11, 2025

Uh oh!

pirapira commented Dec 11, 2025 •

edited

Loading

Uh oh!

This comment was marked as outdated.

Uh oh!

pirapira commented Dec 12, 2025

Uh oh!

This comment was marked as off-topic.

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

feat: grind_pattern mod_eq_of_lt #11584

Are you sure you want to change the base?

feat: grind_pattern mod_eq_of_lt #11584

Conversation

pirapira commented Dec 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-community-bot commented Dec 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Dec 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Dec 11, 2025

Uh oh!

pirapira commented Dec 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

This comment was marked as outdated.

Uh oh!

pirapira commented Dec 12, 2025

Uh oh!

This comment was marked as off-topic.

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

pirapira commented Dec 10, 2025 •

edited

Loading

leanprover-community-bot commented Dec 10, 2025 •

edited

Loading

leanprover-bot commented Dec 10, 2025 •

edited

Loading

pirapira commented Dec 11, 2025 •

edited

Loading