- Coq
Start training on this collection. Each time you skip or complete a kata you will be taken to the next kata in the series. Once you cycle through the items in the collection you will revert back to your normal training routine.
DescriptionEdit
Verified Sorting Algorithms
"Verified Sorting Algorithms" is a collection of exercises on verifying the correctness of selected sorting algorithms. Though by no means necessary, it is best completed alongside Volume 3: Verified Functional Algorithms (VFA) of Software Foundations.
General Prerequisites
Before attempting a Kata in this Collection, you may wish to read the following chapters in VFA:
- Basic Techniques for Permutations and Ordering (Perm)
- Insertion Sort (Sort)
- Insertion Sort With Multisets (Multiset)
- Selection Sort, With Specification and Proof of Correctness (Selection)
Permitted Axioms
You are allowed to assume functional extensionality (or rather, its dependent counterpart functional_extensionality_dep) in case you decide to use the multiset method; otherwise, you are not allowed to assume any additional axioms (unless otherwise stated by the Kata Description).