Symbols: Special symbols
Preface
Basics: Functional Programming in Coq
- Introduction
- Enumerated Types
- Proof By Simplification
- The intros Tactic
- Proof by Rewriting
- Proof by Case Analysis
- More Exercises
- Optional Material
Induction: Proof by Induction
Lists: Working with Structured Data
Poly: Polymorphism and Higher-Order Functions
Gen: Generalizing Induction Hypotheses
Prop: Propositions and Evidence
- Inductively Defined Propositions
- Proof Objects
- Programming with Propositions
- Induction Principles
- Optional Material
- Additional Exercises
Logic: Logic in Coq
- Quantification and Implication
- Conjunction
- Disjunction
- Falsehood
- Negation
- Existential Quantification
- Equality
- Relations as Propositions
- Informal Proofs
- Optional Material
SfLib: Software Foundations Library
- From the Coq Standard Library
- From Basics.v
- From Props.v
- From Logic.v
- From Later Files
- Some useful tactics
Imp: Simple Imperative Programs
- Arithmetic and Boolean Expressions
- Coq Automation
- Evaluation as a Relation
- Expressions With Variables
- Commands
- Evaluation
- Reasoning About Programs
- Additional Exercises
ImpParser: Lexing and Parsing in Coq
ImpCEvalFun: Evaluation Function for Imp
Extraction: Extracting ML from Coq
Equiv: Program Equivalence
- Behavioral Equivalence
- Properties of Behavioral Equivalence
- Case Study: Constant Folding
- Proving That Programs Are Not Equivalent
- Extended exercise: Non-deterministic Imp
- Doing Without Extensionality (Optional)
- Additional Exercises
Hoare: Hoare Logic
- Hoare Logic
- Review of Hoare Logic
- Decorated Programs
- Sample Hoare Logic Proofs
- Formalizing Decorated Programs (Optional)
HoareList: Hoare Logic with Lists
HoareAsLogic: Hoare Logic as a Logic
Rel: Properties of Relations
Smallstep: Small-step Operational Semantics
Types: Type Systems
Stlc: The Simply Typed Lambda-Calculus
Typechecking
MoreStlc: More on the Simply Typed Lambda-Calculus
Records: Adding Records to STLC
References: Typing Mutable References
- Pragmatics
- Operational Semantics
- Typing
- Properties
- References and Nontermination
- Additional Exercises
Sub: Subtyping
RecordSub: Subtyping with Records
Norm: Normalization of STLC
LibTactics: A Collection of Handy General-Purpose Tactics
- Additional notations for Coq
- 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
- Introduction and generalization
- Rewriting
- Inversion
- Induction
- Decidable equality
- Equivalence
- N-ary Conjunctions and Disjunctions
- Tactics to prove typeclass instances
- Tactics to invoke automation
- Tactics to sort out the proof context
- Tactics for development purposes
- Compatibility with standard library
UseTactics: Tactic Library for Coq: A Gentle Introduction
- Tactics for introduction and case analysis
- Tactics for n-ary connectives
- Tactics for working with equality
- Some convenient shorthands
- Tactics for advanced lemma instantiation
- Summary
UseAuto: Theory and Practice of Automation in Coq Proofs
- Basic Features of Proof Search
- How Proof Search Works
- Examples of Use of Automation
- Advanced Topics in Proof Search
- Decision Procedures
- Summary
PE: Partial Evaluation
- Generalizing Constant Folding
- Partial Evaluation of Commands, Without Loops
- Partial Evaluation of Loops
- Partial Evaluation of Flowchart Programs
Postscript
Extraction2: Extracting ML from Coq, Part 2
NormInType: Alternate Version of Normalization, for Extraction
This page has been generated by coqdoc