Volume 0: Discrete Math in Coq (alpha)
Table of Contents
Index
Roadmap
Preface
Welcome
Overview
Logic
Proof Assistants
Functional Programming
Further Reading
Practicalities
Chapter Dependencies
System Requirements
Exercises
Downloading the Coq Files
Lecture Videos
Note for Instructors
Recommended Citation Format
Translations
Thanks
Functional Programming in Coq (
Intro
)
Introduction
What is functional programming?
Getting the tools in order
Data and Functions
Enumerated Types
Days of the Week
Homework Submission Guidelines
Booleans
Function Types
Case study: DNA nucleotides
How to succeed in this course
Types
Separate Compilation
Compound Types
Modules
Numbers
Comparisons
Functions as Data
Higher-Order Functions
Functions That Construct Functions
Recursion
Fixpoints and Structural Recursion
Anonymous functions and fixpoints
Case study: binary and trinary numbers
What's happening here?
Structures
Lists
Polymorphic Pairs
Polymorphic Options
More Polymorphic Functions
Lists
Case study: DNA strands and amino acids
Combine and split
Higher-order predicates: forallb and existsb
Higherorder
Higher-Order List Functions
Higher-order Functions and Anonymous Functions: Together Forever
Map
Sorting
Insertion sort
What makes a sort correct?
Identifying sortedness
Trees
Binary trees
Traversals
Binary search trees (BSTs)
Sets
Sets from lists
Set operations
Sets from sorted lists
Sets from BSTs
Sets from functions
Expressions
Arithmetic and Boolean Expressions
Syntax
Evaluation
Optimization
Expressions With Variables
States
Syntax
Evaluation
Encodings
Compilation
Formal proof
Propositions
Simple proofs
Proof by Simplification
The
intros
and
apply
Tactics
Logical connectives
Conjunction
Disjunction
Truth
Proof by Rewriting
The
apply
Tactic, Revisited
Propositions so far
Tactics so far
What's happening here?
Cases
Proofs Within Proofs
Unfolding Definitions
Proof by Case Analysis
Logical Connectives
Conjunction
Disjunction
Falsehood and Negation
More Exercises
The
injection
and
discriminate
Tactics
Logical Equivalence
Using Tactics on Hypotheses
Using
destruct
on Compound Expressions
Induction
Overview
Applying Theorems to Arguments
Structural induction
More Exercises
One last hard one
Induction2
Varying the Induction Hypothesis
When to Vary
Generalizing the IH Explicitly
To vary or not to vary
Exists
Existential Quantification
Propositions and Booleans
Classical vs. Constructive Logic
Indprop
Inductive propositions
Evenness
Using Evidence in Proofs
Inversion on Evidence
Induction on Evidence
Inductive Relations
Indprop2
Reasoning about minima
In and All
Case study: getting
natset
right
Sorting2
Permutations
A computational interpretation
Sortedness
Proofs with Sortedness
Proof of Correctness
Making Sure the Specification is Right
Proving Correctness from the Alternate Spec
The Moral of This Story
Postscript
Looking Back
Looking Forward
Other sources
