Preface

• Top
• Welcome
• Overview
  • Logic
  • Proof Assistants
  • Functional Programming
  • Further Reading
• Practicalities
  • Chapter Dependencies
  • System Requirements
  • Exercises
  • Downloading the Coq Files
• Resources
  • Sample Exams
  • Lecture Videos
• Note for Instructors
• Translations
• Thanks

Functional Programming in Coq    (Basics)

• Top
• Introduction
• Data and Functions
  • Enumerated Types
  • Days of the Week
  • Homework Submission Guidelines
  • Booleans
  • Types
  • New Types from Old
  • Tuples
  • Modules
  • Numbers
• Proof by Simplification
• Proof by Rewriting
• Proof by Case Analysis
  • More on Notation (Optional)
  • Fixpoints and Structural Recursion (Optional)
• More Exercises

Proof by Induction    (Induction)

• Top
• Proof by Induction
• Proofs Within Proofs
• Formal vs. Informal Proof
• More Exercises

Working with Structured Data    (Lists)

• Top
• Pairs of Numbers
• Lists of Numbers
• Reasoning About Lists
  • Induction on Lists
  • Search
  • List Exercises, Part 1
  • List Exercises, Part 2
• Options
• Partial Maps

Polymorphism and Higher-Order Functions    (Poly)

• Top
• Polymorphism
  • Polymorphic Lists
  • Polymorphic Pairs
  • Polymorphic Options
• Functions as Data
  • Higher-Order Functions
  • Filter
  • Anonymous Functions
  • Map
  • Fold
  • Functions That Construct Functions
• Additional Exercises

More Basic Tactics    (Tactics)

• Top
• 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    (Logic)

• Top
• Logical Connectives
  • Conjunction
  • Disjunction
  • Falsehood and Negation
  • Truth
  • Logical Equivalence
  • Setoids and Logical Equivalence
  • Existential Quantification
• Programming with Propositions
• Applying Theorems to Arguments
• Coq vs. Set Theory
  • Functional Extensionality
  • Propositions and Booleans
  • Classical vs. Constructive Logic

Inductively Defined Propositions    (IndProp)

• Top
• Inductively Defined Propositions
  • Inductive Definition of Evenness
• Using Evidence in Proofs
  • Inversion on Evidence
  • Induction on Evidence
• Inductive Relations
• 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)

• Top
• The Coq Standard Library
• Identifiers
• Total Maps
• Partial maps

The Curry-Howard Correspondence    (ProofObjects)

• Top
• Proof Scripts
• Quantifiers, Implications, Functions
• Programming with Tactics
• Logical Connectives as Inductive Types
  • Conjunction
  • Disjunction
  • Existential Quantification
  • True and False
• Equality
  • Inversion, Again

Induction Principles    (IndPrinciples)

• Top
• Basics
• Polymorphism
• Induction Hypotheses
• More on the induction Tactic
• Induction Principles in Prop
• Formal vs. Informal Proofs by Induction
  • Induction Over an Inductively Defined Set
  • Induction Over an Inductively Defined Proposition
• Explicit Proof Objects for Induction (Optional)
• The Coq Trusted Computing Base

Properties of Relations    (Rel)

• Top
• Relations
• Basic Properties
• Reflexive, Transitive Closure

Simple Imperative Programs    (Imp)

• Top
• Arithmetic and Boolean Expressions
  • Syntax
  • Evaluation
  • Optimization
• Coq Automation
  • Tacticals
  • Defining New Tactic Notations
  • The omega 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
  • The Locate command
  • More Examples
• Evaluating Commands
  • Evaluation as a Function (Failed Attempt)
  • Evaluation as a Relation
  • Determinism of Evaluation
• Reasoning About Imp Programs
• Additional Exercises

Lexing and Parsing in Coq    (ImpParser)

• Top
• Internals
  • Lexical Analysis
  • Parsing
• Examples

An Evaluation Function for Imp    (ImpCEvalFun)

• Top
• A Broken Evaluator
• A Step-Indexed Evaluator
• Relational vs. Step-Indexed Evaluation
• Determinism of Evaluation Again

Extracting ML from Coq    (Extraction)

• Top
• Basic Extraction
• Controlling Extraction of Specific Types
• A Complete Example
• Discussion
• Going Further

More Automation    (Auto)

• Top
• The auto Tactic
• Searching For Hypotheses
  • The eapply and eauto variants

More Automation    (AltAuto)

• Top
• Coq Automation
• Tacticals
  • A Few More Handy Tactics
  • Defining New Tactics
• Decision Procedures
  • The Omega Tactic
• Search Tactics
  • The constructor tactic.
  • The auto Tactic
  • The eapply and eauto variants

Postscript

• Top
• Looking Back
• Looking Forward
• Other sources

Bibliography    (Bib)

• Top
• Resources cited in this volume