The Hitchhiker’s Guide to Logical Verification

Description

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