Preface

Functional Programming in Coq    (Basics)

Proof by Induction    (Induction)

Working with Structured Data    (Lists)

Polymorphism and Higher-Order Functions    (Poly)

More Basic Tactics    (Tactics)

Logic in Coq    (Logic)

Inductively Defined Propositions    (IndProp)

Total and Partial Maps    (Maps)

ProofObjects

Induction Principles    (IndPrinciples)

Properties of Relations    (Rel)

Simple Imperative Programs    (Imp)

Lexing and Parsing in Coq    (ImpParser)

An Evaluation Function for Imp    (ImpCEvalFun)

Extracting OCaml from Rocq    (Extraction)

More Automation    (Auto)

A Streamlined Treatment of Automation    (AltAuto)

Postscript

Bibliography    (Bib)