Volume 1: Logical Foundations
Table of Contents
Index
Roadmap
Preface
Welcome
Overview
Logic
Proof Assistants
Functional Programming
Further Reading
Practicalities
System Requirements
Exercises
Downloading the Coq Files
Chapter Dependencies
Recommended Citation Format
Resources
Sample Exams
Lecture Videos
Note for Instructors and Contributors
Translations
Thanks
Functional Programming in Coq (
Basics
)
Homework Submission Guidelines
Testing Your Solutions
Introduction
Data and Functions
Enumerated Types
Days of the Week
Booleans
Types
New Types from Old
Modules
Tuples
Numbers
Proof by Simplification
Proof by Rewriting
Proof by Case Analysis
More on Notation (Optional)
Fixpoints and Structural Recursion (Optional)
More Exercises
Warmups
Course Late Policies Formalized
Binary Numerals
Proof by Induction (
Induction
)
Separate Compilation
Proof by Induction
Proofs Within Proofs
Formal vs. Informal Proof
More Exercises
Nat to Bin and Back to Nat
Bin to Nat and Back to Bin (Advanced)
Working with Structured Data (
Lists
)
Pairs of Numbers
Lists of Numbers
Reasoning About Lists
Induction on Lists
Search
List Exercises, Part 1
List Exercises, Part 2
Options
Partial Maps
Labeled Trees
Polymorphism and Higher-Order Functions (
Poly
)
Polymorphism
Polymorphic Lists
Polymorphic Pairs
Polymorphic Options
Functions as Data
Higher-Order Functions
Filter
Anonymous Functions
Map
Fold
Functions That Construct Functions
Additional Exercises
Church Numerals (Advanced)
More Basic Tactics (
Tactics
)
The
apply
Tactic
The
apply
with
Tactic
The
injection
and
discriminate
Tactics
Using Tactics on Hypotheses
Varying the Induction Hypothesis
Unfolding Definitions
Using
destruct
on Compound Expressions
Review
Additional Exercises
Logic in Coq: part 1 (
Logic1
)
Logical Connectives
Conjunction
Disjunction
Falsehood and Negation
Truth
Logical Equivalence
Setoids and Logical Equivalence
Logic in Coq: part 2 (
Logic
)
Existential Quantification
Programming with Propositions
Applying Theorems to Arguments
Coq vs. Set Theory
Functional Extensionality
Propositions vs. Booleans
Working with Decidable Properties
Classical vs. Constructive Logic
Inductively Defined Propositions: part 1 (
IndProp1
)
Inductively Defined Propositions
The Collatz Conjecture
Binary relations
Reflexive and Transitive Closure
Permutations
Evenness (yet again)
Constructing Evidence for Permutations
Using Evidence in Proofs
Destructing and Inverting Evidence
Induction on Evidence
Inductive Relations
Inductively Defined Propositions: part 2 (
IndProp
)
Case Study: Regular Expressions
The
remember
Tactic
Case Study: Improving Reflection
Additional Exercises
Extended Exercise: A Verified Regular-Expression Matcher
Total and Partial Maps (
Maps
)
The Coq Standard Library
Identifiers
Total Maps
Partial maps
The Curry-Howard Correspondence (
ProofTerms
)
Proof Scripts
Quantifiers, Implications, Functions
Programming with Tactics
Logical Connectives as Inductive Types
Conjunction
Disjunction
Existential Quantification
True
and
False
Equality
Inversion, Again
Coq's Trusted Computing Base
More Exercises
Proof Irrelevance (Advanced, Optional)
Induction Principles (
IndPrinciples
)
Basics
Polymorphism
Induction Hypotheses
More on the
induction
Tactic
Induction Principles for Propositions
Another Form of Induction Principles on Propositions (Optional)
Formal vs. Informal Proofs by Induction
Induction Over an Inductively Defined Set
Induction Over an Inductively Defined Proposition
Explicit Proof Terms for Induction (Optional)
Properties of Relations (
Rel
)
Relations
Basic Properties
Reflexive, Transitive Closure
Simple Imperative Programs (
Imp
)
Arithmetic and Boolean Expressions
Syntax
Evaluation
Optimization
Coq Automation
Tacticals
Defining New Tactics
The
lia
Tactic
A Few More Handy Tactics
Evaluation as a Relation
Inference Rule Notation
Equivalence of the Definitions
Computational vs. Relational Definitions
Expressions With Variables
States
Syntax
Notations
Evaluation
Commands
Syntax
Desugaring Notations
Locate
Again
More Examples
Evaluating Commands
Evaluation as a Function (Failed Attempt)
Evaluation as a Relation
Determinism of Evaluation
Reasoning About Imp Programs
Additional Exercises
Defining Secrecy and Secure Multi-Execution (
Noninterference
)
Noninterference for pure functions
Secure Multi-Execution (SME)
Noninterference for state transformers
SME for state transformers
Noninterference and SME for Imp programs without loops
Noninterference and SME for Imp programs with loops
Termination-Sensitive Noninterference
Lexing and Parsing in Coq (
ImpParser
)
Internals
Lexical Analysis
Parsing
Examples
An Evaluation Function for Imp (
ImpCEvalFun
)
A Broken Evaluator
A Step-Indexed Evaluator
Relational vs. Step-Indexed Evaluation
Determinism of Evaluation Again
Extracting OCaml from Coq (
Extraction
)
Basic Extraction
Controlling Extraction of Specific Types
A Complete Example
Discussion
Going Further
More Automation (
Auto
)
The
auto
Tactic
Searching For Hypotheses
Tactics
eapply
and
eauto
Constraints on Existential Variables
A Streamlined Treatment of Automation (
AltAuto
)
Tacticals
The
try
Tactical
The Sequence Tactical
;
(Simple Form)
The Sequence Tactical
;
(Local Form)
The
repeat
Tactical
An Optimization Exercise
Tactics that Make Mentioning Names Unnecessary
The
assumption
tactic
The
contradiction
tactic
The
subst
tactic
The
constructor
tactic
Automatic Solvers
Linear Integer Arithmetic: The
lia
Tactic
Equalities: The
congruence
Tactic
Propositions: The
intuition
Tactic
Exercises with Automatic Solvers
Search Tactics
The
auto
Tactic
The
eauto
variant
Ltac: The Tactic Language
Ltac Functions
Ltac Pattern Matching
Using
match
goal
to Prove Tautologies
Review
Postscript
Looking Back
Looking Forward
Resources
Bibliography (
Bib
)
Resources cited in this volume
