Skip to content

feat: Nat.lt_pow_self#6200

Merged
tydeu merged 2 commits intoleanprover:masterfrom
tydeu:nat-lt-pow-self
Nov 27, 2024
Merged

feat: Nat.lt_pow_self#6200
tydeu merged 2 commits intoleanprover:masterfrom
tydeu:nat-lt-pow-self

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Nov 24, 2024

This PR upstreams Nat.lt_pow_self and Nat.lt_two_pow from Mathlib and uses them to prove the simp theorem Nat.mod_two_pow.

This simplifies expressions like System.Platform.numBits % 2 ^ System.Platform.numBits = System.Platform.numBits, which is needed for #6188.

@tydeu tydeu added the changelog-library Library label Nov 24, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 24, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Nov 24, 2024
Update lean-toolchain for testing leanprover/lean4#6200
c7de4e5
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 24, 2024
Update lean-toolchain for testing leanprover/lean4#6200
835c294
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 24, 2024
@ghost
Copy link
Copy Markdown

ghost commented Nov 24, 2024 •
edited by ghost
Loading

Mathlib CI status (docs):

@tydeu tydeu added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Nov 24, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Nov 24, 2024
Trigger CI for leanprover/lean4#6200
a718748
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 24, 2024
Trigger CI for leanprover/lean4#6200
64cdba7
@tydeu tydeu added release-ci Enable all CI checks for a PR, like is done for releases and removed merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. labels Nov 24, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Nov 25, 2024
Trigger CI for leanprover/lean4#6200
4ab3974
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2024
Trigger CI for leanprover/lean4#6200
7dd730c
@tydeu tydeu mentioned this pull request Nov 25, 2024
Merged
tydeu added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2024
@tydeu
chore: adaptions for leanprover/lean4#6200
3f941d8
tydeu added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2024
@tydeu
chore: adaptions for leanprover/lean4#6200
bb8b98c
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 25, 2024
@tydeu tydeu marked this pull request as ready for review November 25, 2024 02:23
@tydeu tydeu requested a review from kim-em as a code owner November 25, 2024 02:23
kim-em
kim-em reviewed Nov 26, 2024
View reviewed changes
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Nov 26, 2024
Trigger CI for leanprover/lean4#6200
c8eca4f
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 26, 2024
Trigger CI for leanprover/lean4#6200
5e5178b
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Nov 26, 2024
tydeu added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 26, 2024
@tydeu
chore: review adaptions for leanprover/lean4#6200
c94e3c9
@ghost ghost removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 26, 2024
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 26, 2024
@tydeu tydeu added this pull request to the merge queue Nov 26, 2024
Merged via the queue into leanprover:master with commit 23bec25 Nov 27, 2024
@tydeu tydeu deleted the nat-lt-pow-self branch November 27, 2024 02:23
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@tydeu @JovanGerb
feat: Nat.lt_pow_self (leanprover#6200)
271adfc 
This PR upstreams `Nat.lt_pow_self` and `Nat.lt_two_pow` from Mathlib
and uses them to prove the simp theorem `Nat.mod_two_pow`.

This simplifies expressions like `System.Platform.numBits % 2 ^
System.Platform.numBits = System.Platform.numBits`, which is needed for
leanprover#6188.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@tydeu @kim-em