Certainty by Construction

Dedication
Quote
Contents
Preface
The Co-blub Paradox
	A World Without Execution?
A Gentle Introduction to Agda
	The Longevity of Knowledge
	Modules and Imports
	A Note on Interaction
	Importing Code
	Semantic Highlighting
	Types and Values
	Your First Function
	Normalization
	Unit Testing
	Dealing with Unicode
	Expressions and Functions
	Operators
	Agda\'s Computational Model
	Stuckness
	Records and Tuples
	Copatterns and Constructors
	Fixities
	Coproduct Types
	Function Types
	The Curry/Uncurry Isomorphism
	Implicit Arguments
	Wrapping Up
An Exploration of Numbers
	Natural Numbers
	Brief Notes on Data and Record Types
	Playing with Naturals
	Induction
	Two Notions of Evenness
	Constructing Evidence
	Addition
	Termination Checking
	Multiplication and Exponentiation
	Semi-subtraction
	Inconvenient Integers
	Difference Integers
	Unique Integer Representations
	Pattern Synonyms
	Integer Addition
	Wrapping Up
Proof Objects
	Constructivism
	Statements are Types; Programs are Proofs
	Hard to Prove or Simply False?
	The Equality Type
	Congruence
	Identity and Zero Elements
	Symmetry and Involutivity
	Transitivity
	Mixfix Parsing
	Equational Reasoning
	Ergonomics, Associativity and Commutativity
	Exercises in Proof
	Wrapping Up
Relations
	Universe Levels
	Dependent Pairs
	Heterogeneous Binary Relations
	The Relationship Between Functions and Relations
	Homogeneous Relations
	Standard Properties of Relations
	Attempting to Order the Naturals
	Substitution
	Unification
	Overconstrained by Dot Patterns
	Ordering the Natural Numbers
	Preorders
	Preorder Reasoning
	Reasoning over ≤
	Graph Reachability
	Free Preorders in the Wild
	Antisymmetry
	Equivalence Relations and Posets
	Strictly Less Than
	Wrapping Up
Modular Arithmetic
	Instance Arguments
	The Ring of Natural Numbers Modulo N
	Deriving Transitivity
	Congruence of Addition
	Congruence of Multiplication
	Automating Proofs
	Wrapping Up
Decidability
	Negation
	Bottom
	Inequality
	Negation Considered as a Callback
	Intransitivity of Inequality
	No Monus Left-Identity Exists
	Decidability
	Transforming Decisions
	Binary Trees
	Proving Things about Binary Trees
	Decidability of Tree Membership
	The All Predicate
	Binary Search Trees
	Trichotomy
	Insertion into BSTs
	Intrinsic vs Extrinsic Proofs
	An Intrinsic BST
	Wrapping Up
Monoids and Setoids
	Structured Sets
	Monoids
	Examples of Monoids
	Monoids as Queries
	More Monoids
	Monoidal Origami
	Composition of Monoids
	Function Extensionality
	Setoid Hell
	A Setoid for Extensionality
	The Pointwise Monoid
	Monoid Homomorphisms
	Finding Equivalent Computations
	Wrapping Up
Isomorphisms
	Finite Numbers
	Vectors and Finite Bounds
	Characteristic Functions
	Isomorphisms
	Equivalence on Isomorphisms
	Finite Types
	Algebraic Data Types
	The Algebra of Algebraic Data Types
	Monoids on Types
	Functions as Exponents
	Wrapping Up
Program Optimization
	Why Can This Be Done?
	Shaping the Cache
	Building the Tries
	Memoizing Functions
	Inspecting Memoized Tries
	Updating the Trie
	Wrapping It All Up
Appendix: Ring Solving
	Rings
	Agda\'s Ring Solver
	Tactical Solving
	The Pen and Paper Algorithm
	Horner Normal Form
	Multivariate Polynomials
	Building a Semiring over HNF
	Semantics
	Syntax
	Solving the Ring
	Ergonomics
Bibliography
Acknowledgments
About the Author
Books by Sandy Maguire