lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

refactor: simplify `Array.findIdx?` code

Open michelsol opened this issue 11 months ago • 1 comments

This shortens Array.findIdx? code, by using termination_by (and well-founded recursion) instead of a structural recursion trick, with the intent to make it more proof friendly.

One motivation is that it makes it easier to write a proof that Array.findIdx? and List.findIdx? are equivalent. Furthermore, this will be useful to prove that more complex functions are equivalent.

Closes #3646

michelsol avatar Mar 10 '24 22:03 michelsol

Mathlib CI status (docs):

  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-10 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-03-10 22:28:12)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1388f6bc83b5ea085fe14faa1db213e745c3e398 --onto 32dcc6eb895b58df3d3241a2521963e64995b621. (2024-03-11 18:02:13)
  • ✅ Mathlib branch lean-pr-testing-3648 has successfully built against this PR. (2024-03-12 15:19:49) View Log
  • ✅ Mathlib branch lean-pr-testing-3648 has successfully built against this PR. (2024-03-12 15:58:41) View Log

leanprover-community-mathlib4-bot avatar Mar 10 '24 22:03 leanprover-community-mathlib4-bot

@michelsol, we would need to see convincing evidence there is no possible performance regression from this.

kim-em avatar Mar 22 '24 00:03 kim-em

!bench

kim-em avatar Mar 22 '24 00:03 kim-em

I would expect the new version to perform better than the original one, because it had an unnecessary fuel parameter which will be there in the compiled code. It has the look of something that was written either before a good well founded recursion mechanism was available, or in order to avoid well founded recursion for other reasons (e.g. defeq reduction in the kernel), but I think we have since decided not to worry about this in Array functions given the proliferation of well founded recursive definitions.

digama0 avatar Mar 22 '24 00:03 digama0

Here are the benchmark results for commit 93e8169a10b54ddfc6fda1cefcfdf5768a7fd597. There were no significant changes against commit ae492265fec103aa834d897bf9f68c94d10f0785.

leanprover-bot avatar Mar 22 '24 00:03 leanprover-bot

Sorry I wasn't aware of the bench command. Is the benchmark report good enough or is there something else I'm expected to do?

michelsol avatar Mar 22 '24 12:03 michelsol