feat: analysis of binary search on a sorted array #237
Conversation
There was a problem hiding this comment.
Basically all the definitions as well as a monadic version of binary search already exists docs. Why reinvent Finvecs which already have good API and notation support?
| intentionally left unconstrained, eliminating out-of-bounds concerns. | ||
| This design substantially reduces index-related proof obligations, | ||
| leading to cleaner and more modular algorithmic analysis. -/ | ||
| structure SortedArray (α : Type) [LinearOrder α] (n : ℕ) where |
There was a problem hiding this comment.
This is extraneous. Lean core and mathlib already provide a bunch of API for various containers and allow to convert to and from so-called Finvecs which are maps of the form Fin n -> \alpa
| /-- Scoped notation for accessing elements of a `SortedArray`. | ||
| Writing `a[i]` abbreviates `SortedArray.get a i`, avoiding explicit projections | ||
| and improving readability in algorithm definitions such as `binarySearch`. -/ | ||
| scoped notation a "[" i "]" => SortedArray.get a i |
There was a problem hiding this comment.
The notation is unnecessary. This notation works for any container type with an instance of GetElem docs
| leading to cleaner and more modular algorithmic analysis. -/ | ||
| structure SortedArray (α : Type) [LinearOrder α] (n : ℕ) where | ||
| /-- Total access function for the array. | ||
| The value at indices `i ≥ n` is arbitrary and irrelevant to correctness. -/ |
There was a problem hiding this comment.
Additionally, Core already has a binary search on arrays
| namespace Cslib.Algorithms.Lean.TimeM | ||
|
|
||
| set_option autoImplicit false | ||
| set_option tactic.hygienic false |
There was a problem hiding this comment.
As addressed in your last PR, please do not unset tactic hygiene. It appears you have done so mostly to use inaccessible names after induction. The standard method here is to provide names to each branch using either with or cases.
|
|
||
| -/ | ||
|
|
||
| namespace Cslib.Algorithms.Lean.TimeM |
There was a problem hiding this comment.
I am again not sure about naming here. I would expect the TimeM namespace to be used only for the definition and utilities directly related to the monad, and this file to fall under a namespace corresponding to the file name. This is currently Cslib.Algorithms.Lean.Searching.BinarySearch, but if this is going to be nested and have multiple search procedures, maybe Cslib.Algorithms.Lean.Search.Binary is a bit more compact.
| scoped notation a "[" i "]" => SortedArray.get a i | ||
|
|
||
|
|
||
| variable {α : Type} [LinearOrder α] |
There was a problem hiding this comment.
This is duplicated from above.
| if q = arr_a then return (some a) | ||
| else return none |
There was a problem hiding this comment.
I'd use the same indenting for if/else as you did below for readability.
| intentionally left unconstrained, eliminating out-of-bounds concerns. | ||
| This design substantially reduces index-related proof obligations, | ||
| leading to cleaner and more modular algorithmic analysis. -/ | ||
| structure SortedArray (α : Type) [LinearOrder α] (n : ℕ) where |
There was a problem hiding this comment.
Before I review proofs carefully, we should discuss the design of this. I am going continue this discussion on Zulip.
3 participants
We introduce an analysis of binary search on a sorted array. We model a sorted array as a function from Nat to a type equipped with a size and a sortedness property. This representation eliminates concerns about out-of-bounds indexing. With fewer proof obligations related to array indices, the analysis becomes significantly cleaner and more modular.