The Hitchhiker's Guide to Logical Verification - Brown University

Anne Baanen Alexander Bentkamp Jasmin Blanchette Johannes H?lzl Jannis Limperg

The Hitchhiker's Guide to Logical Verification

Standard Edition

(October , )

lean-forward.github.io/ logical-verification/

ii

Contents

Contents

iii

Preface

vii

I Basics

Definitions and Statements . Types and Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Type Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Function Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Lemma Statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Backward Proofs . Tactic Mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Basic Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Reasoning about Connectives and Quantifiers . . . . . . . . . . . . . . . Reasoning about Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . Rewriting Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Proofs by Mathematical Induction . . . . . . . . . . . . . . . . . . . . . . Induction Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Cleanup Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Forward Proofs . Structured Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Structured Constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Forward Reasoning about Connectives and Quantifiers . . . . . . . . . Calculational Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Forward Reasoning with Tactics . . . . . . . . . . . . . . . . . . . . . . . Dependent Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . The PAT Principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Induction by Pattern Matching . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

iii

II Functional?Logic Programming

Functional Programming . Inductive Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Structural Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Structural Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Pattern Matching Expressions . . . . . . . . . . . . . . . . . . . . . . . . Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Type Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Binary Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Case Distinction and Induction Tactics . . . . . . . . . . . . . . . . . . . Dependent Inductive Types . . . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Inductive Predicates . Introductory Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Logical Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Rule Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Linear Arithmetic Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Further Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Monads . Introductory Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Two Operations and Three Laws . . . . . . . . . . . . . . . . . . . . . . . A Type Class . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . No E ects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Basic Exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Mutable State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Nondeterminism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Tautology Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A Generic Algorithm: Iteration over a List . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Metaprogramming . Tactics and Tactic Combinators . . . . . . . . . . . . . . . . . . . . . . . . The Metaprogramming Monad . . . . . . . . . . . . . . . . . . . . . . . . Names, Expressions, Declarations, and Environments . . . . . . . . . . First Example: A Conjunction-Destructing Tactic . . . . . . . . . . . . . . Second Example: A Provability Advisor . . . . . . . . . . . . . . . . . . . A Look at Two Predefined Tactics . . . . . . . . . . . . . . . . . . . . . . . Miscellaneous Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

III Program Semantics

Operational Semantics

iv

. Formal Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A Minimalistic Imperative Language . . . . . . . . . . . . . . . . . . . . . Big-Step Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Properties of the Big-Step Semantics . . . . . . . . . . . . . . . . . . . . Small-Step Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Properties of the Small-Step Semantics . . . . . . . . . . . . . . . . . . Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Hoare Logic . Hoare Triples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Hoare Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A Semantic Approach to Hoare Logic . . . . . . . . . . . . . . . . . . . . First Program: Exchanging Two Variables . . . . . . . . . . . . . . . . . . Second Program: Adding Two Numbers . . . . . . . . . . . . . . . . . . . Finish Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A Verification Condition Generator . . . . . . . . . . . . . . . . . . . . . . Second Program Revisited: Adding Two Numbers . . . . . . . . . . . . . Hoare Triples for Total Correctness . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Denotational Semantics . Compositionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A Relational Denotational Semantics . . . . . . . . . . . . . . . . . . . . Fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Monotone Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Complete Lattices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Least Fixpoint . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . A Relational Denotational Semantics, Continued . . . . . . . . . . . . . Application to Program Equivalence . . . . . . . . . . . . . . . . . . . . . A Simpler Approach Based on an Inductive Predicate . . . . . . . . .

IV Mathematics

Logical Foundations of Mathematics . Universes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . The Peculiarities of Prop . . . . . . . . . . . . . . . . . . . . . . . . . . . The Axiom of Choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Quotient Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Summary of New Lean Constructs . . . . . . . . . . . . . . . . . . . . .

Basic Mathematical Structures . Type Classes over a Single Binary Operator . . . . . . . . . . . . . . . . Type Classes over Two Binary Operators . . . . . . . . . . . . . . . . . . Coercions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Normalization Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Lists, Multisets, and Finite Sets . . . . . . . . . . . . . . . . . . . . . . . . Order Type Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

v

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download