Prove closed-form sorting bounds

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.

https://jonsterling.github.io/agda-calf/

Apache License 2.0

55 stars 2 forks source link

Closed HarrisonGrodin closed 3 years ago

HarrisonGrodin commented 3 years ago

That wasn't so bad! Toughest part was noticing the theorem statement:

sort/recurrence≡* : ∀ k n → sort/recurrence k n ≡ k * n

which conveniently ended up being very clean (and ⌈log₂_⌉-free!).

HarrisonGrodin commented 3 years ago

Actually, huh, realization - the analysis for merge sort might as well be ≡, not Nat.≤.

HarrisonGrodin commented 3 years ago

(Rephrased analysis accordingly.)