Preface

• Welcome
• Overview
  • Logic
  • Proof Assistants
  • Functional Programming
  • Program Verification
  • Type Systems
  • Further Reading
• Practicalities
  • Chapter Dependencies
  • System Requirements
  • Exercises
  • Downloading the Coq Files
• Note for Instructors
• Translations

Basics: Functional Programming in Coq

• Introduction
• Enumerated Types
  • Days of the Week
  • Homework Submission Guidelines
  • Booleans
  • Function Types
  • Modules
  • Numbers
• Proof by Simplification
• Proof by Rewriting
• Proof by Case Analysis
  • More on Notation (Optional)
  • Fixpoints and Structural Recursion (Optional)
• More Exercises

Induction: Proof by Induction

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

Lists: Working with Structured Data

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

Poly: Polymorphism and Higher-Order Functions

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

Tactics: More Basic Tactics

• The apply Tactic
• The apply ... with ... Tactic
• The inversion Tactic
• Using Tactics on Hypotheses
• Varying the Induction Hypothesis
• Unfolding Definitions
• Using destruct on Compound Expressions
• Review
• Additional Exercises

Logic: Logic in Coq

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

IndProp: Inductively Defined Propositions

• Inductively Defined Propositions
• 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

Maps: Total and Partial Maps

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

ProofObjects: The Curry-Howard Correspondence

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

IndPrinciples: Induction Principles

• 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

Rel: Properties of Relations

• Basic Properties
• Reflexive, Transitive Closure

Imp: Simple Imperative Programs

• 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
  • Evaluation
• Commands
  • Syntax
  • More Examples
• Evaluating Commands
  • Evaluation as a Function (Failed Attempt)
  • Evaluation as a Relation
  • Determinism of Evaluation
• Reasoning About Imp Programs
• Additional Exercises

ImpParser: Lexing and Parsing in Coq

• Internals
  • Lexical Analysis
  • Parsing
• Examples

ImpCEvalFun: Evaluation Function for Imp

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

Extraction: Extracting ML from Coq

• Basic Extraction
• Controlling Extraction of Specific Types
• A Complete Example
• Discussion

Equiv: Program Equivalence

• Behavioral Equivalence
  • Definitions
  • Simple Examples
• Properties of Behavioral Equivalence
  • Behavioral Equivalence Is an Equivalence
  • Behavioral Equivalence Is a Congruence
• Program Transformations
  • The Constant-Folding Transformation
  • Soundness of Constant Folding
• Proving That Programs Are Not Equivalent
• Extended Exercise: Nondeterministic Imp
• Additional Exercises

Hoare: Hoare Logic, Part I

• Assertions
• Hoare Triples
• Proof Rules
  • Assignment
  • Consequence
  • Digression: The eapply Tactic
  • Skip
  • Sequencing
  • Conditionals
  • Loops
• Summary
• Additional Exercises

Hoare2: Hoare Logic, Part II

• Decorated Programs
  • Example: Swapping Using Addition and Subtraction
  • Example: Simple Conditionals
  • Example: Reduce to Zero
  • Example: Division
• Finding Loop Invariants
  • Example: Slow Subtraction
  • Exercise: Slow Assignment
  • Exercise: Slow Addition
  • Example: Parity
  • Example: Finding Square Roots
  • Example: Squaring
  • Exercise: Factorial
  • Exercise: Min
  • Exercise: Power Series
• Weakest Preconditions (Optional)
• Formal Decorated Programs (Optional)
  • Syntax
  • Extracting Verification Conditions
  • Automation
  • Examples

HoareAsLogic: Hoare Logic as a Logic

• Definitions
• Properties

Smallstep: Small-step Operational Semantics

• A Toy Language
• Relations
  • Values
  • Strong Progress and Normal Forms
• Multi-Step Reduction
  • Examples
  • Normal Forms Again
  • Equivalence of Big-Step and Small-Step
  • Additional Exercises
• Small-Step Imp
• Concurrent Imp
• A Small-Step Stack Machine

Auto: More Automation

• The auto Tactic
• Searching For Hypotheses

Types: Type Systems

• Typed Arithmetic Expressions
  • Syntax
  • Operational Semantics
  • Normal Forms and Values
  • Typing
  • Progress
  • Type Preservation
  • Type Soundness
• Aside: the normalize Tactic
  • Additional Exercises

Stlc: The Simply Typed Lambda-Calculus

• The Simply Typed Lambda-Calculus
  • Overview
  • Syntax
  • Operational Semantics
  • Typing

StlcProp: Properties of STLC

• Canonical Forms
• Progress
• Preservation
  • Free Occurrences
  • Substitution
  • Main Theorem
• Type Soundness
• Uniqueness of Types
• Additional Exercises
  • Exercise: STLC with Arithmetic

MoreStlc: More on the Simply Typed Lambda-Calculus

• Simple Extensions to STLC
  • Numbers
  • Let Bindings
  • Pairs
  • Unit
  • Sums
  • Lists
  • General Recursion
  • Records
• Exercise: Formalizing the Extensions
  • Examples
  • Properties of Typing

Sub: Subtyping

• Concepts
  • A Motivating Example
  • Subtyping and Object-Oriented Languages
  • The Subsumption Rule
  • The Subtype Relation
  • Exercises
• Formal Definitions
  • Core Definitions
  • Subtyping
  • Typing
• Properties
  • Inversion Lemmas for Subtyping
  • Canonical Forms
  • Progress
  • Inversion Lemmas for Typing
  • Context Invariance
  • Substitution
  • Preservation
  • Records, via Products and Top
  • Exercises
• Exercise: Adding Products

Typechecking: A Typechecker for STLC

• Comparing Types
• The Typechecker
• Properties
• Exercises

Records: Adding Records to STLC

• Adding Records
• Formalizing Records
  • Examples
  • Properties of Typing

References: Typing Mutable References

• Definitions
• Syntax
• Pragmatics
  • Side Effects and Sequencing
  • References and Aliasing
  • Shared State
  • Objects
  • References to Compound Types
  • Null References
  • Garbage Collection
• Operational Semantics
  • Locations
  • Stores
  • Reduction
• Typing
  • Store typings
  • The Typing Relation
• Properties
  • Well-Typed Stores
  • Extending Store Typings
  • Preservation, Finally
  • Substitution Lemma
  • Assignment Preserves Store Typing
  • Weakening for Stores
  • Preservation!
  • Progress
• References and Nontermination
• Additional Exercises

RecordSub: Subtyping with Records

• Core Definitions
• Subtyping
  • Definition
  • Examples
  • Properties of Subtyping
• Typing
  • Typing Examples
  • Properties of Typing

Norm: Normalization of STLC

• Language
• Normalization
  • Membership in R_T Is Invariant Under Reduction
  • Closed Instances of Terms of Type t Belong to R_T

LibTactics: A Collection of Handy General-Purpose Tactics

• Tools for Programming with Ltac
  • Identity Continuation
  • Untyped Arguments for Tactics
  • Optional Arguments for Tactics
  • Wildcard Arguments for Tactics
  • Position Markers
  • List of Arguments for Tactics
  • Databases of Lemmas
  • On-the-Fly Removal of Hypotheses
  • Numbers as Arguments
  • Testing Tactics
  • Check No Evar in Goal
  • Helper Function for Introducing Evars
  • Tagging of Hypotheses
  • More Tagging of Hypotheses
  • Deconstructing Terms
  • Action at Occurence and Action Not at Occurence
  • An Alias for eq
• Common Tactics for Simplifying Goals Like intuition
• Backward and Forward Chaining
  • Application
  • Assertions
  • Instantiation and Forward-Chaining
  • Experimental Tactics for Application
  • Adding Assumptions
  • Application of Tautologies
  • Application Modulo Equalities
  • Absurd Goals
• Introduction and Generalization
  • Introduction
  • Generalization
  • Naming
• Rewriting
  • Replace
  • Change
  • Renaming
  • Unfolding
  • Simplification
  • Reduction
  • Substitution
  • Tactics to Work with Proof Irrelevance
  • Proving Equalities
• Inversion
  • Basic Inversion
  • Inversion with Substitution
  • Injection with Substitution
  • Inversion and Injection with Substitution —rough implementation
  • Case Analysis
• Induction
• Coinduction
• Decidable Equality
• Equivalence
• N-ary Conjunctions and Disjunctions
• Tactics to Prove Typeclass Instances
• Tactics to Invoke Automation
  • Definitions for Parsing Compatibility
  • hint to Add Hints Local to a Lemma
  • jauto, a New Automation Tactic
  • Definitions of Automation Tactics
  • Parsing for Light Automation
  • Parsing for Strong Automation
• Tactics to Sort Out the Proof Context
  • Hiding Hypotheses
  • Sorting Hypotheses
  • Clearing Hypotheses
• Tactics for Development Purposes
  • Skipping Subgoals
• Compatibility with Standard Library

UseTactics: Tactic Library for Coq: A Gentle Introduction

• Tactics for Introduction and Case Analysis
  • The Tactic introv
  • The Tactic inverts
• Tactics for N-ary Connectives
  • The Tactic splits
  • The Tactic branch
  • The Tactic ∃
• Tactics for Working with Equality
  • The Tactics asserts_rewrite and cuts_rewrite
  • The Tactic substs
  • The Tactic fequals
  • The Tactic applys_eq
• Some Convenient Shorthands
  • The Tactic unfolds
  • The Tactics false and tryfalse
  • The Tactic gen
  • The Tactics skip, skip_rewrite and skip_goal
  • The Tactic sort
• Tactics for Advanced Lemma Instantiation
  • Working of lets
  • Working of applys, forwards and specializes
  • Example of Instantiations
• Summary

UseAuto: Theory and Practice of Automation in Coq Proofs

• Basic Features of Proof Search
  • Strength of Proof Search
  • Basics
  • Conjunctions
  • Disjunctions
  • Existentials
  • Negation
  • Equalities
• How Proof Search Works
  • Search Depth
  • Backtracking
  • Adding Hints
  • Integration of Automation in Tactics
• Examples of Use of Automation
  • Determinism
  • Preservation for STLC
  • Progress for STLC
  • BigStep and SmallStep
  • Preservation for STLCRef
  • Progress for STLCRef
  • Subtyping
• Advanced Topics in Proof Search
  • Stating Lemmas in the Right Way
  • Unfolding of Definitions During Proof-Search
  • Automation for Proving Absurd Goals
  • Automation for Transitivity Lemmas
• Decision Procedures
  • Omega
  • Ring
  • Congruence
• Summary

PE: Partial Evaluation

• Generalizing Constant Folding
  • Partial States
  • Arithmetic Expressions
  • Boolean Expressions
• Partial Evaluation of Commands, Without Loops
  • Assignment
  • Conditional
  • The Partial Evaluation Relation
  • Examples
  • Correctness of Partial Evaluation
• Partial Evaluation of Loops
  • Examples
  • Correctness
• Partial Evaluation of Flowchart Programs
  • Basic blocks
  • Flowchart programs
  • Partial Evaluation of Basic Blocks and Flowchart Programs

Postscript

• Looking Back
• Looking Around
• Looking Forward

Bib: Bibliography