Skip to content

chore: upstream Nat.binaryRec#3756

Open
astrainfinita wants to merge 7 commits intoleanprover:masterfrom
astrainfinita:binaryRec
Open

chore: upstream Nat.binaryRec#3756
astrainfinita wants to merge 7 commits intoleanprover:masterfrom
astrainfinita:binaryRec

Conversation

@astrainfinita
Copy link
Copy Markdown
Contributor

@astrainfinita astrainfinita commented Mar 24, 2024 •
edited
Loading

This was a PR for Std, but everything in Std.Data.Nat.Bitwise has been moved to Init.

Nat.binaryRec, Nat.binaryRec' and Nat.binaryRecFromOne replace Nat.div2Induction, which is noncomputable and more difficult to use. These definitions have been modified to be simpler and faster than the current version in Mathlib.

We also need Nat.bit because it is part of the type of Nat.binaryRec and we need some lemmas about it in this PR. If we do not introduce this definition, we'll have to use cond b everywhere. We cannot use Bool.toNat here because we have the import chain Init.Data.Nat.Bitwise.Basic -> Init.Data.Fin.Basic -> Init.Data.Array.Basic -> Init.Data.Array.Basic -> Init.Data.Array.Subarray -> Init.NotationExtra -> Init.BinderPredicates -> Init.Data.Bool.

Was leanprover-community/batteries#314.

Zulip

mathlib adaptations: leanprover-community/mathlib4#12419

@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 Mar 24, 2024
@ghost
Copy link
Copy Markdown

ghost commented Mar 24, 2024 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-03-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-03-24 12:54:47)
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but linting failed. (2024-03-26 05:31:32) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but linting failed. (2024-03-26 05:51:24) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but linting failed. (2024-04-24 06:48:15) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but linting failed. (2024-04-24 12:53:46) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but linting failed. (2024-04-24 15:59:50) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but linting failed. (2024-04-24 16:19:18) View Log
  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-04-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-04-24 17:44:21)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1630d9b803164bb522f4a40fbc8fbf104cca425e --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-25 04:55:04)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3990a9b3be9bd8d33b25bdf26a8a7821cb1a741c --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-25 05:59:13)
  • 💥 Mathlib branch lean-pr-testing-3756 build failed against this PR. (2024-04-25 07:06:37) View Log
  • 💥 Mathlib branch lean-pr-testing-3756 build failed against this PR. (2024-04-25 11:31:58) View Log
  • 💥 Mathlib branch lean-pr-testing-3756 build failed against this PR. (2024-04-25 16:03:32) View Log
  • 💥 Mathlib branch lean-pr-testing-3756 build failed against this PR. (2024-04-25 16:32:41) View Log
  • 💥 Mathlib branch lean-pr-testing-3756 build failed against this PR. (2024-05-07 23:31:19) View Log
  • 💥 Mathlib branch lean-pr-testing-3756 build failed against this PR. (2024-05-10 01:59:22) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but lean4checker failed. (2024-05-13 06:11:05) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but lean4checker failed. (2024-05-13 06:24:34) View Log
  • ❌ Mathlib branch lean-pr-testing-3756 built against this PR, but lean4checker failed. (2024-05-27 08:25:30) View Log

kim-em
kim-em reviewed Mar 26, 2024
View reviewed changes
kim-em
kim-em reviewed Mar 26, 2024
View reviewed changes
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Mar 26, 2024

Please include in the PR description an explanation of why this should be moved to Lean. (Not just a link to zulip, which doesn't really explain either.)

@kim-em kim-em added the awaiting-author Waiting for PR author to address issues label Mar 26, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 26, 2024
Update lean-toolchain for testing leanprover/lean4#3756
4f8c88c
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 26, 2024
Update lean-toolchain for testing leanprover/lean4#3756
5707b4e
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 26, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 26, 2024
Trigger CI for leanprover/lean4#3756
f054431
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 26, 2024
Trigger CI for leanprover/lean4#3756
4205f70
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
9d943ce
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
1d2e926
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
3dd3482
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
8b92f8f
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
73b94f6
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
e8dd65a
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
67d65c6
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 24, 2024
Trigger CI for leanprover/lean4#3756
4771753
@astrainfinita
Copy link
Copy Markdown
Contributor Author

astrainfinita commented Apr 24, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 24, 2024
astrainfinita added a commit to astrainfinita/std4 that referenced this pull request Apr 24, 2024
@astrainfinita
chore: adaptations for leanprover/lean4#3756
3837547
astrainfinita added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 25, 2024
@astrainfinita
chore: adaptations for leanprover/lean4#3756
d351718
@astrainfinita
Copy link
Copy Markdown
Contributor Author

astrainfinita commented Apr 25, 2024 •
edited
Loading

!bench

(Looks like I can't trigger lean4 benchmark. The CI of my mathlib4 testing PR is very slow. Maybe I got something wrong.)

Let me rebase to v4.7.0 nightly-2024-04-21.

@astrainfinita astrainfinita force-pushed the binaryRec branch 3 times, most recently from 7db39b9 to c751e82 Compare April 25, 2024 06:18
kim-em
kim-em reviewed May 10, 2024
View reviewed changes
src/Init/Data/Nat/Bitwise/Lemmas.lean
rw [Nat.testBit_to_div_mod]
rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all

theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
Copy link
Copy Markdown
Collaborator

@kim-em kim-em May 10, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

exists_testBit_eq_true_of_ne_zero? or just exists_testBit?

kim-em
kim-em reviewed May 10, 2024
View reviewed changes
src/Init/Data/Nat/Bitwise/Lemmas.lean
refine ⟨i + 1, ?_⟩
rwa [Nat.add_le_add_iff_right, testBit_succ, bit_div_two]

theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
Copy link
Copy Markdown
Collaborator

@kim-em kim-em May 10, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, all these implies in the names are bad. They predate this PR of course. Maybe we should deal with them separately.

@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented May 10, 2024

I'm still uncertain about whether it is a good idea to move bit up to Lean, just for the sake of removing div2induction.

Would you consider splitting this into a PR that does all the cleanup that you do here without adding bit and Nat.binaryRec, and then once we have a more minimal PR we can try to get some other opinions?

@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented May 10, 2024

(This is not urgent at this point while we're still deciding what to do, but certainly for this PR to be merged we'll need a successful mathlib build, which I think hasn't occurred yet.)

@kim-em kim-em self-assigned this May 10, 2024
@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels May 10, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 10, 2024
Trigger CI for leanprover/lean4#3756
41f43d8
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2024
Trigger CI for leanprover/lean4#3756
248930b
@astrainfinita
Copy link
Copy Markdown
Contributor Author

astrainfinita commented May 10, 2024

We had leanprover-community/mathlib4#12419 2 weeks ago. Should I force-push to lean-pr-testing-3756?

@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented May 13, 2024

We had leanprover-community/mathlib4#12419 2 weeks ago. Should I force-push to lean-pr-testing-3756?

Yes, you can keep pushing commits to lean-pr-testing-3756 to get it working.

@kim-em kim-em added the full-ci label May 13, 2024
@astrainfinita
Copy link
Copy Markdown
Contributor Author

astrainfinita commented May 18, 2024

Would you consider splitting this into a PR that does all the cleanup that you do here without adding bit and Nat.binaryRec, and then once we have a more minimal PR we can try to get some other opinions?

I split the change of Nat.testBit to #4188, could you give some comments?

@Kha Kha added release-ci Enable all CI checks for a PR, like is done for releases and removed full-ci labels May 24, 2024
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 27, 2024
Trigger CI for leanprover/lean4#3756
2201661
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 27, 2024
Trigger CI for leanprover/lean4#3756
73dde1d
@astrainfinita astrainfinita mentioned this pull request Jun 9, 2024
Closed
2 tasks
@github-actions github-actions bot added stale and removed stale labels Jun 29, 2024
@fgdorais fgdorais mentioned this pull request Jul 23, 2024
Closed
2 tasks
@astrainfinita astrainfinita mentioned this pull request Aug 6, 2024
Closed
1 task
@github-actions github-actions bot added the stale label Aug 20, 2024
@github-actions github-actions bot removed the stale label Sep 6, 2024
@github-actions github-actions bot added the stale label Oct 30, 2024
@github-actions github-actions bot removed the stale label Jun 6, 2025
@github-actions github-actions bot added the stale label Jul 28, 2025
@github-actions github-actions bot removed the stale label Aug 27, 2025
@github-actions github-actions bot added the stale label Sep 27, 2025
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

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees

@kim-em kim-em

Labels

awaiting-author Waiting for PR author to address issues breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases stale 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.

3 participants

@astrainfinita @kim-em @Kha