feat: query complexity model for algorithms#275
feat: query complexity model for algorithms#275Shreyas4991 wants to merge 128 commits intoleanprover:mainfrom
Conversation
Co-authored-by: Sorrachai Yingchareonthawornhcai <sorrachai@users.noreply.github.com>
Co-authored-by: Sorrachai Yingchareonthawornhcai <sorrachai@users.noreply.github.com>
…ity-freeM-shreyas
…ity-freeM-shreyas
…ity-freeM-shreyas
Shreyas4991
changed the title
| @[simps] | ||
| def add (soc₁ soc₂ : SortOpsCost) : SortOpsCost:= | ||
| ⟨soc₁.compares + soc₂.compares, soc₁.inserts + soc₂.inserts⟩ | ||
|
|
||
| /-- Component-wise scalar (natural number) multiplication operation on `SortOpsCost` -/ | ||
| @[simps] | ||
| def nsmul (n : ℕ) (soc : SortOpsCost) : SortOpsCost := ⟨n • soc.compares, n • soc.inserts⟩ | ||
|
|
||
| @[simps] | ||
| instance AddSortOps : Add SortOpsCost where | ||
| add := add |
There was a problem hiding this comment.
I would recommend you inline add directly here, which will save you from needing to simplify it every time.
| lemma SortModel_addComponents (m₁ m₂ m₃ : SortOpsCost) : | ||
| m₁ + m₂ = m₃ ↔ | ||
| m₁.compares + m₂.compares = m₃.compares ∧ | ||
| m₁.inserts + m₂.inserts = m₃.inserts := by | ||
| aesop |
There was a problem hiding this comment.
This lemma should probably be dropped, this is handled by the ext tactic already
| m₁.inserts + m₂.inserts = m₃.inserts := by | ||
| aesop | ||
|
|
||
| lemma SortModel_leComponents (m₁ m₂ : SortOpsCost) : |
There was a problem hiding this comment.
| lemma SortModel_leComponents (m₁ m₂ : SortOpsCost) : | |
| lemma SortOpsCost.le_def (m₁ m₂ : SortOpsCost) : |
but this lemma is now a duplicate of the one generated by @[simps] so you should either drop it or remove the attibute.
There was a problem hiding this comment.
It's removed now
| match P with | ||
| | .pure _ => 0 | ||
| | .liftBind op cont => | ||
| let t₁ := M.cost op | ||
| let qval := M.evalQuery op | ||
| t₁ + (time (cont qval) M) |
There was a problem hiding this comment.
| match P with | |
| | .pure _ => 0 | |
| | .liftBind op cont => | |
| let t₁ := M.cost op | |
| let qval := M.evalQuery op | |
| t₁ + (time (cont qval) M) | |
| (P.liftM fun x => do tick (M.cost x); return (M.evalQuery x)).time |
where you could quite reasonably define
abbrev Model.timeQuery (M : Model Q Cost) (x : Q i) : TimeM Cost ι := do tick (M.cost x); return (M.evalQuery x)
| have hleft : (mergeSort left).eval (sortModelNat α) = mergeSortNaive left := by grind | ||
| have hright : (mergeSort right).eval (sortModelNat α) = mergeSortNaive right := by grind | ||
| have hleft' : | ||
| FreeM.liftM (m := Id) (fun {ι} q => (sortModelNat α).evalQuery q) |
There was a problem hiding this comment.
Passing := Id is usually a code smell, this means you're missing an Id.run somewhere.
There was a problem hiding this comment.
No the Id.run would be simplified with Id.run_pure at this point.
| /-- | ||
| The vanilla-lean version of `merge` that merges two lists. When the two lists | ||
| are sorted, so is the merged list. | ||
| -/ | ||
| def mergeNaive [LinearOrder α] (x y : List α) : List α := | ||
| match x,y with | ||
| | [], ys => ys | ||
| | xs, [] => xs | ||
| | x :: xs', y :: ys' => | ||
| if x ≤ y then | ||
| let rest := mergeNaive xs' (y :: ys') | ||
| x :: rest | ||
| else | ||
| let rest := mergeNaive (x :: xs') ys' | ||
| y :: rest | ||
|
|
||
| lemma mergeNaive_length [LinearOrder α] (x y : List α) : | ||
| (mergeNaive x y).length = x.length + y.length := by | ||
| fun_induction mergeNaive <;> try grind |
There was a problem hiding this comment.
I think you should just drop this and use List.merge, which I think is defined identically up to lets anyway.
There was a problem hiding this comment.
I strongly prefer not to. List.merge doesn't even produce an induction principle with fun_induction.
| /-- | ||
| The vanilla-lean version of `mergeSortNaive` that is extensionally equal to `mergeSort` | ||
| -/ | ||
| def mergeSortNaive [LinearOrder α] (xs : List α) : List α := | ||
| if xs.length < 2 then xs | ||
| else | ||
| let sortedLeft := mergeSortNaive (xs.take (xs.length/2)) | ||
| let sortedRight := mergeSortNaive (xs.drop (xs.length/2)) | ||
| mergeNaive sortedLeft sortedRight |
There was a problem hiding this comment.
Ideally we'd drop this in favor of List.mergeSort
| let P : Nat → Prop := | ||
| fun n => ∀ xs, xs.length = n → (mergeSort xs).eval (sortModelNat α) = mergeSortNaive xs | ||
| have hP : P xs.length := by | ||
| refine Nat.strong_induction_on (n := xs.length) ?_ |
There was a problem hiding this comment.
I think the dance you're trying to do here is induction hlen : xs.length using Nat.strong_induction_on?
There was a problem hiding this comment.
induction hlen : xs.length using Nat.strong_induction_on generalizing xs with
There was a problem hiding this comment.
I changed the syntax, but I find the refine formulation shorter
…ity-freeM-shreyas
4 participants
Generalizing @tannerduve 's query complexity model. This model of algorithmic complexity provides a lightweight approach to complexity verification of algorithms, similar to #165
However it offers several improvements over #165 :
Update to the below drawback : The model requires users to choose a cost for each pure operation upfront by a typeclass instance for a given type of
Cost. This is a departure fromTimeMs model. But with custom Cost types with a specific field forpure, these costs can be separated from that of calls to queries.One drawback : It is still possible to sneak in free operations inside
pure. However this is unavoidable in any lightweight monadic approach. A deeply embedded DSL is the only foolproof way to avoid this. Nevertheless this approach removes annotation and review burden and ensures that any actual call to a query will be counted. Thus it is easy to notice when a monadic operation is not being called.Zulip Discussion Thread: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Query.20model.20for.20Algorithms.20complexity.20.3A.20updates/near/569606456