|
|
|
|
|
|
by jacobparker
1717 days ago
|
|
|
I highly recommend SF. The trick is you must use the books via coqIDE or something equivalent; viewing the rendered HTML is almost pointless at best, but probably counter-productive. Binary search would be a good exercise. I think SF volume 1 would be more than enough, with the exception of deciding how to model arrays (you'd probably want to look up Coq's persistent arrays/PArray system for this.) SF volume 3 does binary search _trees_ which is similar but avoids the array problem (as is customary in functional languages.) However, Coq (by default) also uses infinite precision numbers. This works very well for proofs but isn't necessarily realistic. This is where some extra fun comes in: fixed precision arithmetic is a very common source of bugs for binary search: https://ai.googleblog.com/2006/06/extra-extra-read-all-about... |
|
|