Skip to content

[Merged by Bors] - chore: redefine Nat.bit#19666

Closed
astrainfinita wants to merge 4 commits intomasterfrom
FR_binrec_bit
Closed

[Merged by Bors] - chore: redefine Nat.bit#19666
astrainfinita wants to merge 4 commits intomasterfrom
FR_binrec_bit

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Dec 1, 2024

split from #13649

Open in Gitpod

@astrainfinita astrainfinita added the t-data Data (lists, quotients, numbers, etc) label Dec 1, 2024
@astrainfinita astrainfinita mentioned this pull request Dec 1, 2024
Closed
2 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 1, 2024 •
edited
Loading

please_merge_master.md

@astrainfinita astrainfinita mentioned this pull request Dec 1, 2024
Closed
1 task
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 12, 2024

Could you please explain why you want to do this? I've never seen a @[csimp] lemma proved by rfl, which makes me a bit skeptical.

Could you include some form of benchmark showing the csimp lemma has a meaningful effect?

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Dec 13, 2024 

def bit (b : Bool) (n : Nat) : Nat :=
  cond b (2 * n + 1) (2 * n)

def bitImpl (b : Bool) (n : Nat) : Nat :=
  cond b (n <<< 1 + 1) (n <<< 1)

def run_bit (n : Nat) (x : Nat) : IO Unit := do
  let mut t := 0
  for _ in [0 : n] do
    t := bit false x

def run_bitImpl (n : Nat) (x : Nat) : IO Unit := do
  let mut t := 0
  for _ in [0 : n] do
    t := bitImpl false x

def n := 10^4
def x := 11^1000000

#eval timeit "bit" (run_bit n x) -- bit 620ms
#eval timeit "bitImpl" (run_bitImpl n x) -- bitImpl 433ms

@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jan 28, 2025

Although I'm by no means an expert here (and never use #eval in my own Lean work) I am by default suspicious of adding csimp lemmas which show only marginal improvement and in such niche cases. Are there any places in the library where the speedup is by e.g. a factor of 2 or more? Is it possible to give a lake exe benchmark which shows improvement? Are there other users who can see advantages here? e.g. @TwoFX or @girving ? Otherwise I am inclined to close as too niche. We've seen something get 30% better in one extreme case. How do we know, for example, that things don't get 30% slower for more reasonable values of n and x? We don't really have enough evidence to merge this change, in my opinion, but I'm open to changing my mind if more evidence is accumulated. With no more evidence I'm minded to close as "too risky to fiddle with".

@girving
Copy link
Copy Markdown
Collaborator

girving commented Jan 29, 2025

I don’t have a strong take here, but it does seem marginal. For one thing the code is branching, but my guess is that there’s some other even faster version.

@TwoFX
Copy link
Copy Markdown
Member

TwoFX commented Jan 30, 2025

@FR-vdash-bot, could you say a bit more about why you want this? Do you have a performance-critical compiled application that calls Nat.bit a lot?

@kbuzzard kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 3, 2025
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Apr 2, 2025

Then let's remove csimp from this PR..

@astrainfinita astrainfinita changed the title chore: redefine Nat.bit and csimp lemma for Nat.bit chore: redefine Nat.bit Apr 2, 2025
@astrainfinita astrainfinita removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2025
YaelDillies
YaelDillies reviewed Apr 6, 2025
View reviewed changes
YaelDillies
YaelDillies approved these changes Apr 6, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

I am happy to merge this since it makes two proofs easier, but really it's all quite marginal. Does your next PR #13649 really need to depend on this one?

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 6, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 6, 2025
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Apr 6, 2025

I'm not sure. I just split this part from #13649. It might simplify some other proofs.

@astrainfinita @YaelDillies
suggestion
c085779 
Co-authored-by: Yaël Dillies <[email protected]>
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 6, 2025

please_merge_master.md

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 7, 2025

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 7, 2025
mathlib-bors bot pushed a commit that referenced this pull request Apr 7, 2025
@astrainfinita
chore: redefine Nat.bit (#19666)
e943fd9
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: redefine Nat.bit [Merged by Bors] - chore: redefine Nat.bit Apr 7, 2025
@mathlib-bors mathlib-bors bot closed this Apr 7, 2025
@mathlib-bors mathlib-bors bot deleted the FR_binrec_bit branch April 7, 2025 01:19
tannerduve pushed a commit that referenced this pull request May 13, 2025
@astrainfinita @tannerduve
chore: redefine Nat.bit (#19666)
9cf47e4
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@astrainfinita @kim-em @kbuzzard @girving @TwoFX @YaelDillies