Volume 3: Verified Functional Algorithms
Table of Contents
Index
Roadmap
Preface
Welcome
Practicalities
Chapter Dependencies
System Requirements
Exercises
Downloading the Coq Files
Lecture Videos
For Instructors and Contributors
Recommended Citation Format
Thanks
Basic Techniques for Permutations and Ordering (
Perm
)
The Less-Than Order on the Natural Numbers
Relating
Prop
to
bool
A Tactic for Boolean destruction
Linear Integer Inequalities
Permutations
Summary: Comparisons and Permutations
Insertion Sort (
Sort
)
Recommended Reading
The Insertion-Sort Program
Specification of Correctness
Proof of Correctness
Making Sure the Specification is Right
Proving Correctness from the Alternative Spec
The Moral of This Story
Insertion Sort With Multisets (
Multiset
)
Correctness
Permutations and Multisets
The Main Theorem: Equivalence of Multisets and Permutations
Insertion Sort With Bags (
BagPerm
)
Correctness
Permutations and Multisets
The Main Theorem: Equivalence of Multisets and Permutations
Selection Sort, With Specification and Proof of Correctness (
Selection
)
The Selection-Sort Program
Proof of Correctness of Selection sort
Recursive Functions That are Not Structurally Recursive
Merge Sort, With Specification and Proof of Correctness (
Merge
)
Split and its properties
Defining Merge
Defining Mergesort
Correctness: Sortedness
Correctness: Permutation
Binary Search Trees (
SearchTree
)
Sections
Program for Binary Search Trees
Search Tree Examples
Properties of
lookup
and
insert
Derived Properties
Properties of
elements
Efficiency of Search Trees
Model-based specifications
Abstract Data Types (
ADT
)
A Brief Excursion into Dependent Types
Abstracting over invariants.
Module signatures for model-based Specification
Summary of Abstract Data Type Proofs
Exercise in Data Abstraction
Running Coq Programs in OCaml (
Extract
)
Utilities for OCaml Integer Comparisons
SearchTrees, Extracted
Trees, on
int
Instead of
nat
Performance Tests
Implementation and Proof of Red-Black Trees (
Redblack
)
Required Reading
Implementation
Proof Automation for Case-Analysis Proofs.
Proof Automation for Case-Analysis Proofs.
The BST Property
Proving fundamental laws relating
insert
and
lookup
.
Proving Efficiency
Extracting and Measuring Red-Black Trees
Success!
Number Representations and Efficient Lookup Tables (
Trie
)
LogN Penalties in Functional Programming
A Simple Program That's Waaaaay Too Slow.
Efficient Positive Numbers
Coq's Integer Type,
Z
From
N
×
N
×
N
to
N
×
N
×
logN
From
N
×
N
×
logN
to
N
×
logN
×
logN
Tries: Efficient Lookup Tables on Positive Binary Numbers
From
N
×
logN
×
logN
to
N
×
logN
Proving the Correctness of Trie Tables
Lemmas About the Relation Between
lookup
and
insert
Bijection Between
positive
and
nat
.
Proving That Tries are a "Table" ADT.
Sanity Check
Conclusion
Priority Queues (
Priqueue
)
Module Signature
Implementation
Some Preliminaries
The Program
Predicates on Priority Queues
The Representation Invariant
Sanity Checks on the Abstraction Relation
Characterizations of the Operations on Queues
Binomial Queues (
Binom
)
Required Reading
The Program
Characterization Predicates
Proof of Algorithm Correctness
Various Functions Preserve the Representation Invariant
The Abstraction Relation
Sanity Checks on the Abstraction Relation
Various Functions Preserve the Abstraction Relation
Optional Exercises
Measurement.
Programming with Decision Procedures (
Decide
)
Using
reflect
to characterize decision procedures
Using
sumbool
to Characterize Decision Procedures
sumbool
in the Coq Standard Library
Decidability and Computability
Opacity of
Qed
Advantages and Disadvantages of
reflect
Versus
sumbool
Graph Coloring (
Color
)
Preliminaries: Representing Graphs
Lemmas About Sets and Maps
equivlistA
SortA_equivlistA_eqlistA
S.remove and S.elements
Lists of (key,value) Pairs
Cardinality
Now Begins the Graph Coloring Program
Some Proofs in Support of Termination
The Rest of the Algorithm
Proof of Correctness of the Algorithm.
Trying Out the Algorithm on an Actual Test Case
