The Hitchhiker’s Guide to Logical Verification

Contents
Preface
I Basics
1 Definitions and Statements
1.1 Types and Terms
1.1.1 Types
1.1.2 Terms
1.1.3 Type Checking and Type Inference
1.1.4 Type Inhabitation
1.2 Type Definitions
1.2.1 Natural Numbers
1.2.2 Arithmetic Expressions
1.2.3 Comparison with Java
1.2.4 Comparison with C
1.2.5 Lists
1.3 Function Definitions
1.4 Lemma Statements
1.5 Summary of New Lean Constructs
2 Backward Proofs
2.1 Tactic Mode
2.2 Basic Tactics
2.3 Reasoning about Connectives and Quantifiers
2.4 Reasoning about Equality
2.5 Rewriting Tactics
2.6 Proofs by Mathematical Induction
2.7 Induction Tactic
2.8 Cleanup Tactics
2.9 Summary of New Lean Constructs
3 Forward Proofs
3.1 Structured Proofs
3.2 Structured Constructs
3.3 Forward Reasoning about Connectives and Quantifiers
3.4 Calculational Proofs
3.5 Forward Reasoning with Tactics
3.6 Dependent Types
3.7 The PAT Principle
3.8 Induction by Pattern Matching
3.9 Summary of New Lean Constructs
II Functional–Logic Programming
4 Functional Programming
4.1 Inductive Types
4.2 Structural Induction
4.3 Structural Recursion
4.4 Pattern Matching Expressions
4.5 Structures
4.6 Type Classes
4.7 Lists
4.8 Binary Trees
4.9 Case Distinction and Induction Tactics
4.10 Dependent Inductive Types
4.11 Summary of New Lean Constructs
5 Inductive Predicates
5.1 Introductory Examples
5.1.1 Even Numbers
5.1.2 Tennis Games
5.1.3 Reflexive Transitive Closure
5.1.4 A Nonexample
5.2 Logical Symbols
5.3 Rule Induction
5.4 Linear Arithmetic Tactic
5.5 Elimination
5.6 Further Examples
5.6.1 Sorted Lists
5.6.2 Palindromes
5.6.3 Full Binary Trees
5.6.4 First-Order Terms
5.7 Summary of New Lean Constructs
6 Monads
6.1 Introductory Example
6.2 Two Operations and Three Laws
6.3 A Type Class
6.4 No Effects
6.5 Basic Exceptions
6.6 Mutable State
6.7 Nondeterminism
6.8 Tautology Tactic
6.9 A Generic Algorithm: Iteration over a List
6.10 Summary of New Lean Constructs
7 Metaprogramming
7.1 Tactics and Tactic Combinators
7.2 The Metaprogramming Monad
7.3 Names, Expressions, Declarations, and Environments
7.4 First Example: A Conjunction-Destructing Tactic
7.5 Second Example: A Provability Advisor
7.6 A Look at Two Predefined Tactics
7.7 Miscellaneous Tactics
7.8 Summary of New Lean Constructs
III Program Semantics
8 Operational Semantics
8.1 Formal Semantics
8.2 A Minimalistic Imperative Language
8.3 Big-Step Semantics
8.4 Properties of the Big-Step Semantics
8.5 Small-Step Semantics
8.6 Properties of the Small-Step Semantics
8.7 Parallelism
9 Hoare Logic
9.1 Hoare Triples
9.2 Hoare Rules
9.3 A Semantic Approach to Hoare Logic
9.4 First Program: Exchanging Two Variables
9.5 Second Program: Adding Two Numbers
9.6 Finish Tactic
9.7 A Verification Condition Generator
9.8 Second Program Revisited: Adding Two Numbers
9.9 Hoare Triples for Total Correctness
9.10 Summary of New Lean Constructs
10 Denotational Semantics
10.1 Compositionality
10.2 A Relational Denotational Semantics
10.3 Fixpoints
10.4 Monotone Functions
10.5 Complete Lattices
10.6 Least Fixpoint
10.7 A Relational Denotational Semantics, Continued
10.8 Application to Program Equivalence
10.9 A Simpler Approach Based on an Inductive Predicate
IV Mathematics
11 Logical Foundations of Mathematics
11.1 Universes
11.2 The Peculiarities of Prop
11.2.1 Impredicativity
11.2.2 Proof Irrelevance
11.2.3 No Large Elimination
11.3 The Axiom of Choice
11.4 Subtypes
11.4.1 First Example: Full Binary Trees
11.4.2 Second Example: Vectors
11.5 Quotient Types
11.5.1 First Example: Integers
11.5.2 Second Example: Unordered Pairs
11.5.3 Alternative Definitions via Normalization and Subtyping
11.6 Summary of New Lean Constructs
12 Basic Mathematical Structures
12.1 Type Classes over a Single Binary Operator
12.2 Type Classes over Two Binary Operators
12.3 Coercions
12.4 Normalization Tactics
12.5 Lists, Multisets, and Finite Sets
12.6 Order Type Classes
12.7 Summary of New Lean Constructs
13 Rational and Real Numbers
13.1 Rational Numbers
13.2 Real Numbers
13.3 Final Exhortation
13.4 Summary of New Lean Constructs
Bibliography