Symbols

Preface

• Overview
• Practicalities
  • Chapter Dependencies
  • Required Background
• Coq
  • System Requirements
  • Access to the Coq files
• Exercises
• Recommended Reading
• For Instructors

Basics: Functional Programming and Reasoning About Programs

• Enumerated Types
  • Days of the Week
  • Booleans
  • Function Types
  • Numbers
• Proof By Simplification
• The intros Tactic
• Proof by Rewriting
• Case Analysis
• Naming Cases
• Induction
• Formal vs. Informal Proof
• Proofs Within Proofs
• More Exercises

Lists: Products, Lists and Options

• Pairs of Numbers
• Lists of Numbers
  • Bags via Lists
• Reasoning About Lists
  • Micro-Sermon
  • Induction on Lists
  • SearchAbout
  • List Exercises, Part 1
  • List Exercises, Part 2
• Options
• The apply Tactic
• Varying the Induction Hypothesis
• Exercise: Dictionaries

Poly: Polymorphism and Higher-Order Functions

• Polymorphism
  • Polymorphic Lists
  • Polymorphic Pairs
  • Polymorphic Options
• Functions as Data
  • Higher-Order Functions
  • Partial Application
  • Digression: Currying
  • Filter
  • Anonymous Functions
  • Map
  • Fold
  • Functions For Constructing Functions
• More About Coq
  • The unfold Tactic
  • Inversion
  • Using Tactics on Hypotheses
  • Using destruct on Compound Expressions
  • The remember Tactic
  • The apply ... with ... Tactic
• Review
• Additional Exercises

Gen: Generalizing Induction Hypotheses

Prop: Propositions and Evidence

• Programming with Propositions
• Evidence
  • Inductively Defined Propositions
  • Proof Objects
  • The Curry-Howard Correspondence
  • Implication
  • Induction Principles for Inductively Defined Types
  • Induction Hypotheses
  • Evenness Again
  • Reasoning by Induction Over Evidence
  • Why Define Propositions Inductively?
• The Big Picture: Coq's Two Universes
  • Values
  • Inductive Definitions
  • Types and Kinds
  • Propositions vs. Booleans
  • Functions vs. Quantifiers
  • Functions vs. Implications
• Informal Proofs
  • Informal Proofs by Induction
• Optional Material
  • More on the induction Tactic
  • Induction Principles in Prop
• Additional Exercises

Logic: Logic in Coq

• Quantification and Implication
• Conjunction
  • Iff
• Disjunction
  • Relating ∧ and ∨ with andb and orb
• Falsehood
  • Truth
• Negation
  • Inequality
• Existential Quantification
• Equality
  • Inversion, Again
• Relations as Propositions
  • Digression: More Facts about <= and <
• Optional Material
  • Induction Principles for ∧ and ∨
  • Explicit Proof Objects for Induction
  • The Coq Trusted Computing Base

Rel: Properties of Relations

• Basic Properties of Relations
• Reflexive, Transitive Closure

SfLib: Software Foundations Library

• From the Coq Standard Library
• From Basics.v
• From Props.v
• From Logic.v
• Some useful tactics

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
• Expressions With Variables
  • Identifiers
  • States
  • Syntax
  • Evaluation
• Commands
  • Syntax
  • Examples
• Evaluation
  • Evaluation Function
  • Evaluation as a Relation
  • Equivalence of Relational and Step-Indexed Evaluation
  • Determinacy of Evaluation
• Reasoning About Programs
  • Basic Examples
  • Proving a Program Correct (Optional)
• Additional Exercises

ImpParser: Lexing and Parsing in Coq

• Internals
  • Lexical Analysis
  • Parsing
• Examples

Equiv: Program Equivalence

• Behavioral Equivalence
  • Definitions
  • Examples
• Properties of Behavioral Equivalence
  • Behavioral Equivalence is an Equivalence
  • Behavioral Equivalence is a Congruence
• Case Study: Constant Folding
  • Soundness of Program Transformations
  • The Constant-Folding Transformation
  • Soundness of Constant Folding
• Proving That Programs Are Not Equivalent
• Doing Without Extensionality (Optional)
• Additional Exercises

ImpList: Imp Extended with Lists

• Imp Programs with Lists
  • Repeated Definitions
  • Extensions
  • Repeated Definitions

Hoare: Hoare Logic

• Hoare Logic
  • Assertions
  • Hoare Triples
  • Weakest Preconditions
  • Proof Rules
  • Decorated Programs
• Reasoning About Programs with Hoare Logic
  • Example: Slow Subtraction
  • Exercise: Reduce to Zero
  • Exercise: Slow Addition
  • Example: Parity
  • Example: Finding Square Roots
  • Exercise: Factorial
  • Reasoning About Programs with Lists
  • Formalizing Decorated Programs
  • Syntax
  • Extracting Verification Conditions
  • Examples

HoareAsLogic: Hoare Logic as a Logic

Smallstep: Small-step Operational Semantics

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

Types: Type Systems

• More Automation
  • The auto and eauto Tactics
  • The Proof with Tactic
  • The solve by inversion Tactic
  • The try solve Tactic
  • The f_equal Tactic
  • The normalize Tactic
• Typed Arithmetic Expressions
  • Syntax
  • Small-Step Reduction
  • Normal Forms and Values
  • Typing
  • Progress
  • Type Preservation
  • Type Soundness
  • Additional Exercises

Stlc: The Simply Typed Lambda-Calculus

• The Simply Typed Lambda-Calculus
  • Overview
  • Syntax
  • Operational Semantics
  • Typing
  • Properties
  • Additional Exercises
• Exercise: STLC with Arithmetic
  • Syntax and Operational Semantics

Typechecking

• MoreStlc: A Typechecker for STLC
  • Comparing Types
  • The Typechecker
  • Properties

MoreStlc: More on the Simply Typed Lambda-Calculus

• Simple Extensions to STLC
  • Records and Variants (Optional)
• Formalizing the Extensions
  • Examples
  • Properties of Typing

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

Subtyping

• Concepts
  • A Motivating Example
  • Subtyping and Object-Oriented Languages
  • The Subsumption Rule
  • The Subtype Relation
• Core definitions
  • Definition
  • Subtyping Examples and Exercises
• Typing
  • Typing examples
• Properties
  • Inversion Lemmas for Subtyping
  • Canonical Forms
  • Progress
  • Inversion Lemmas for Typing
  • Context Invariance
  • Substitution
  • Preservation
  • Exercises on Typing
• Exercise: Adding Products

RecordSub: Subtyping with Records

• Core Definitions
• Subtyping
  • Definition
  • Subtyping Examples and Exercises
  • Properties of Subtyping
• Typing
  • Typing Examples
  • Properties of Typing
  • Exercises on Typing

Norm: Normalization of STLC

• Language
• Normalization
  • Membership in R_T is invariant under evaluation
  • Closed instances of terms of type T belong to R_T

UseTactics: Tactic Library for Coq: a gentle introduction

• Tactics for introduction and case analysis
  • The tactic introv
  • The tactic inverts
  • The tactics cases and cases_if
• 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

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
  • Determinacy
  • 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

LibTactics: A Collection of Handy General-Purpose Tactics

• Additional notations for Coq
  • N-ary Existentials
• 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
  • Tagging of hypotheses
  • Tagging of hypotheses
  • Deconstructing terms
  • Action at occurence and action not at occurence
  • An alias for eq
• Backward and forward chaining
  • Application
  • Assertions
  • Instantiation and forward-chaining
  • Experimental tactics for application
  • Adding assumptions
  • Application of tautologies
  • Application modulo equalities
• Introduction and generalization
  • Introduction
  • Generalization
  • Naming
• Rewriting
  • Rewriting
  • Replace
  • Renaming
  • Unfolding
  • Simplification
  • Evaluation
  • 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
• Decidable equality
• Equivalence
• N-ary Conjunctions and Disjunctions
• Tactics to prove typeclass instances
• Tactics to invoke automation
  • jauto, a new automation tactics
  • Definitions of automation tactics
  • Definitions for parsing compatibility
  • 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

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...
• Further Reading