Preface
Program Equivalence (Equiv)
Hoare Logic, Part I (Hoare)
Hoare Logic, Part II (Hoare2)
Hoare Logic as a Logic (HoareAsLogic)
Small-step Operational Semantics (Smallstep)
Type Systems (Types)
The Simply Typed Lambda-Calculus (Stlc)
Properties of STLC (StlcProp)
More on the Simply Typed Lambda-Calculus (MoreStlc)
Subtyping (Sub)
A Typechecker for STLC (Typechecking)
Adding Records to STLC (Records)
Typing Mutable References (References)
Subtyping with Records (RecordSub)
Normalization of STLC (Norm)
A Collection of Handy General-Purpose Tactics (LibTactics)
- Fixing Stdlib
- 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
- Testing evars and non-evars
- 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
- Introduction and Generalization
- Rewriting
- Inversion
- Induction
- Coinduction
- 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