第1页 / 共791页
第2页 / 共791页
第3页 / 共791页
第4页 / 共791页
第5页 / 共791页
第6页 / 共791页
第7页 / 共791页
第8页 / 共791页
software foundations.pdf
Library Top.Preface
Preface
Welcome
Overview
Logic
Proof Assistants
Functional Programming
Program Verification
Type Systems
Further Reading
Practicalities
Chapter Dependencies
System Requirements
Exercises
Downloading the Coq Files
Note for Instructors
Translations
Library Top.Basics
Basics: Functional Programming in Coq
Introduction
Enumerated Types
Days of the Week
Homework Submission Guidelines
Booleans
Function Types
Modules
Numbers
Proof by Simplification
Proof by Rewriting
Proof by Case Analysis
More on Notation (Optional)
Fixpoints and Structural Recursion (Optional)
More Exercises
Library Top.Induction
Induction: Proof by Induction
Proof by Induction
Proofs Within Proofs
Formal vs. Informal Proof
More Exercises
Library Top.Lists
Lists: Working with Structured Data
Pairs of Numbers
Lists of Numbers
Reasoning About Lists
Induction on Lists
Search
List Exercises, Part 1
List Exercises, Part 2
Options
Partial Maps
Library Top.Poly
Poly: Polymorphism and Higher-Order Functions
Polymorphism
Polymorphic Lists
Polymorphic Pairs
Polymorphic Options
Functions as Data
Higher-Order Functions
Filter
Anonymous Functions
Map
Fold
Functions That Construct Functions
Additional Exercises
Library Top.Tactics
Tactics: More Basic Tactics
The apply Tactic
The apply ... with ... Tactic
The inversion Tactic
Using Tactics on Hypotheses
Varying the Induction Hypothesis
Unfolding Definitions
Using destruct on Compound Expressions
Review
Additional Exercises
Library Top.Logic
Logic: Logic in Coq
Logical Connectives
Conjunction
Disjunction
Falsehood and Negation
Truth
Logical Equivalence
Existential Quantification
Programming with Propositions
Applying Theorems to Arguments
Coq vs. Set Theory
Functional Extensionality
Propositions and Booleans
Classical vs. Constructive Logic
Library Top.IndProp
IndProp: Inductively Defined Propositions
Inductively Defined Propositions
Using Evidence in Proofs
Inversion on Evidence
Induction on Evidence
Inductive Relations
Case Study: Regular Expressions
The rememberremember Tactic
Case Study: Improving Reflection
Additional Exercises
Library Top.Maps
Maps: Total and Partial Maps
The Coq Standard Library
Identifiers
Total Maps
Partial maps
Library Top.ProofObjects
ProofObjects: The Curry-Howard Correspondence
Proof Scripts
Quantifiers, Implications, Functions
Programming with Tactics
Logical Connectives as Inductive Types
Conjunction
Disjunction
Existential Quantification
True and False
Equality
Inversion, Again
Library Top.IndPrinciples
IndPrinciples: Induction Principles
Basics
Polymorphism
Induction Hypotheses
More on the induction Tactic
Induction Principles in Prop
Formal vs. Informal Proofs by Induction
Induction Over an Inductively Defined Set
Induction Over an Inductively Defined Proposition
Library Top.Rel
Rel: Properties of Relations
Basic Properties
Reflexive, Transitive Closure
Library Top.Imp
Imp: Simple Imperative Programs
Arithmetic and Boolean Expressions
Syntax
Evaluation
Optimization
Coq Automation
Tacticals
Defining New Tactic Notations
The omega Tactic
A Few More Handy Tactics
Evaluation as a Relation
Inference Rule Notation
Equivalence of the Definitions
Computational vs. Relational Definitions
Expressions With Variables
States
Syntax
Evaluation
Commands
Syntax
More Examples
Evaluating Commands
Evaluation as a Function (Failed Attempt)
Evaluation as a Relation
Determinism of Evaluation
Reasoning About Imp Programs
Additional Exercises
Library Top.ImpParser
ImpParser: Lexing and Parsing in Coq
Internals
Lexical Analysis
Parsing
Examples
Library Top.ImpCEvalFun
ImpCEvalFun: Evaluation Function for Imp
A Broken Evaluator
A Step-Indexed Evaluator
Relational vs. Step-Indexed Evaluation
Determinism of Evaluation Again
Library Top.Extraction
Extraction: Extracting ML from Coq
Basic Extraction
Controlling Extraction of Specific Types
A Complete Example
Discussion
Library Top.Equiv
Equiv: Program Equivalence
Behavioral Equivalence
Definitions
Simple Examples
Properties of Behavioral Equivalence
Behavioral Equivalence Is an Equivalence
Behavioral Equivalence Is a Congruence
Program Transformations
The Constant-Folding Transformation
Soundness of Constant Folding
Proving That Programs Are Not Equivalent
Extended Exercise: Nondeterministic Imp
Additional Exercises
Library Top.Hoare
Hoare: Hoare Logic, Part I
Assertions
Hoare Triples
Proof Rules
Assignment
Consequence
Digression: The eapply Tactic
Skip
Sequencing
Conditionals
Loops
Summary
Additional Exercises
Library Top.Hoare2
Hoare2: Hoare Logic, Part II
Decorated Programs
Example: Swapping Using Addition and Subtraction
Example: Simple Conditionals
Example: Reduce to Zero
Example: Division
Finding Loop Invariants
Example: Slow Subtraction
Exercise: Slow Assignment
Exercise: Slow Addition
Example: Parity
Example: Finding Square Roots
Example: Squaring
Exercise: Factorial
Exercise: Min
Exercise: Power Series
Weakest Preconditions (Optional)
Formal Decorated Programs (Optional)
Syntax
Extracting Verification Conditions
Automation
Examples
Library Top.HoareAsLogic
HoareAsLogic: Hoare Logic as a Logic
Definitions
Properties
Library Top.Smallstep
Smallstep: Small-step Operational Semantics
A Toy Language
Relations
Values
Strong Progress and Normal Forms
Multi-Step Reduction
Examples
Normal Forms Again
Equivalence of Big-Step and Small-Step
Additional Exercises
Small-Step Imp
Concurrent Imp
A Small-Step Stack Machine
Library Top.Auto
Auto: More Automation
The auto Tactic
Searching For Hypotheses
Library Top.Types
Types: Type Systems
Typed Arithmetic Expressions
Syntax
Operational Semantics
Normal Forms and Values
Typing
Progress
Type Preservation
Type Soundness
Aside: the normalizenormalize Tactic
Additional Exercises
Library Top.Stlc
Stlc: The Simply Typed Lambda-Calculus
The Simply Typed Lambda-Calculus
Overview
Syntax
Operational Semantics
Typing
Library Top.StlcProp
StlcProp: Properties of STLC
Canonical Forms
Progress
Preservation
Free Occurrences
Substitution
Main Theorem
Type Soundness
Uniqueness of Types
Additional Exercises
Exercise: STLC with Arithmetic
Library Top.MoreStlc
MoreStlc: More on the Simply Typed Lambda-Calculus
Simple Extensions to STLC
Numbers
Let Bindings
Pairs
Unit
Sums
Lists
General Recursion
Records
Exercise: Formalizing the Extensions
Examples
Properties of Typing
Library Top.Sub
Sub: Subtyping
Concepts
A Motivating Example
Subtyping and Object-Oriented Languages
The Subsumption Rule
The Subtype Relation
Exercises
Formal Definitions
Core Definitions
Subtyping
Typing
Properties
Inversion Lemmas for Subtyping
Canonical Forms
Progress
Inversion Lemmas for Typing
Context Invariance
Substitution
Preservation
Records, via Products and Top
Exercises
Exercise: Adding Products
Library Top.Typechecking
Typechecking: A Typechecker for STLC
Comparing Types
The Typechecker
Properties
Exercises
Library Top.Records
Records: Adding Records to STLC
Adding Records
Formalizing Records
Examples
Properties of Typing
Library Top.References
References: Typing Mutable References
Definitions
Syntax
Pragmatics
Side Effects and Sequencing
References and Aliasing
Shared State
Objects
References to Compound Types
Null References
Garbage Collection
Operational Semantics
Locations
Stores
Reduction
Typing
Store typings
The Typing Relation
Properties
Well-Typed Stores
Extending Store Typings
Preservation, Finally
Substitution Lemma
Assignment Preserves Store Typing
Weakening for Stores
Preservation!
Progress
References and Nontermination
Additional Exercises
Library Top.RecordSub
RecordSub: Subtyping with Records
Core Definitions
Subtyping
Definition
Examples
Properties of Subtyping
Typing
Typing Examples
Properties of Typing
Library Top.Norm
Norm: Normalization of STLC
Language
Normalization
Membership in R_TR_T Is Invariant Under Reduction
Closed Instances of Terms of Type t Belong to R_TR_T
Library Top.LibTactics
LibTactics: A Collection of Handy General-Purpose Tactics
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
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
Application
Assertions
Instantiation and Forward-Chaining
Experimental Tactics for Application
Adding Assumptions
Application of Tautologies
Application Modulo Equalities
Absurd Goals
Introduction and Generalization
Introduction
Generalization
Naming
Rewriting
Replace
Change
Renaming
Unfolding
Simplification
Reduction
Substitution
Tactics to Work with Proof Irrelevance
Proving Equalities
Inversion
Basic Inversion
Inversion with Substitution
Injection with Substitution
Inversion and Injection with Substitution –rough implementation
Case Analysis
Induction
Coinduction
Decidable Equality
Equivalence
N-ary Conjunctions and Disjunctions
Tactics to Prove Typeclass Instances
Tactics to Invoke Automation
Definitions for Parsing Compatibility
hinthint to Add Hints Local to a Lemma
jautojauto, a New Automation Tactic
Definitions of Automation Tactics
Parsing for Light Automation
Parsing for Strong Automation
Tactics to Sort Out the Proof Context
Hiding Hypotheses
Sorting Hypotheses
Clearing Hypotheses
Tactics for Development Purposes
Skipping Subgoals
Compatibility with Standard Library
Library Top.UseTactics
UseTactics: Tactic Library for Coq: A Gentle Introduction
Tactics for Introduction and Case Analysis
The Tactic introvintrov
The Tactic invertsinverts
Tactics for N-ary Connectives
The Tactic splitssplits
The Tactic branchbranch
The Tactic
Tactics for Working with Equality
The Tactics asserts_rewriteasserts_rewrite and cuts_rewritecuts_rewrite
The Tactic substssubsts
The Tactic fequalsfequals
The Tactic applys_eqapplys_eq
Some Convenient Shorthands
The Tactic unfoldsunfolds
The Tactics false and tryfalsetryfalse
The Tactic gengen
The Tactics skipskip, skip_rewriteskip_rewrite and skip_goalskip_goal
The Tactic sortsort
Tactics for Advanced Lemma Instantiation
Working of letslets
Working of applysapplys, forwardsforwards and specializesspecializes
Example of Instantiations
Summary
Library Top.UseAuto
UseAuto: Theory and Practice of Automation in Coq Proofs
Basic Features of Proof Search
Strength of Proof Search
Basics
Conjunctions
Disjunctions
Existentials
Negation
Equalities
How Proof Search Works
Search Depth
Backtracking
Adding Hints
Integration of Automation in Tactics
Examples of Use of Automation
Determinism
Preservation for STLC
Progress for STLC
BigStep and SmallStep
Preservation for STLCRef
Progress for STLCRef
Subtyping
Advanced Topics in Proof Search
Stating Lemmas in the Right Way
Unfolding of Definitions During Proof-Search
Automation for Proving Absurd Goals
Automation for Transitivity Lemmas
Decision Procedures
Omega
Ring
Congruence
Summary
Library Top.PE
PE: Partial Evaluation
Generalizing Constant Folding
Partial States
Arithmetic Expressions
Boolean Expressions
Partial Evaluation of Commands, Without Loops
Assignment
Conditional
The Partial Evaluation Relation
Examples
Correctness of Partial Evaluation
Partial Evaluation of Loops
Examples
Correctness
Partial Evaluation of Flowchart Programs
Basic blocks
Flowchart programs
Partial Evaluation of Basic Blocks and Flowchart Programs
Library Top.Postscript
Postscript
Looking Back
Looking Around
Looking Forward
Library Top.Bib
Bib: Bibliography
Contents
1 Library Top.Preface
1.1 Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Welcome . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.1 Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.2 Proof Assistants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.3 Functional Programming . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.4 Program Verification . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.5 Type Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3.6 Further Reading
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . .
1.4.1 Chapter Dependencies
1.4.2
System Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4.3 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4.4 Downloading the Coq Files . . . . . . . . . . . . . . . . . . . . . . . .
1.5 Note for Instructors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.6 Translations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4 Practicalities
2 Library Top.Basics
2.1 Basics: Functional Programming in Coq . . . . . . . . . . . . . . . . . . . .
2.2
Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 Enumerated Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.1 Days of the Week . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.2 Homework Submission Guidelines . . . . . . . . . . . . . . . . . . . .
2.3.3 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.4 Function Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.5 Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3.6 Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4 Proof by Simplification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.5 Proof by Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.6 Proof by Case Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.6.1 More on Notation (Optional)
. . . . . . . . . . . . . . . . . . . . . .
2.6.2 Fixpoints and Structural Recursion (Optional) . . . . . . . . . . . . .
1
2
2
2
2
3
4
5
6
7
7
7
7
7
8
8
9
9
10
10
10
10
11
12
13
15
15
15
20
22
24
27
28
2.7 More Exercises
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3 Library Top.Induction
3.1
Induction: Proof by Induction . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Proof by Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3 Proofs Within Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4 Formal vs. Informal Proof
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.5 More Exercises
4 Library Top.Lists
4.1 Lists: Working with Structured Data . . . . . . . . . . . . . . . . . . . . . .
4.2 Pairs of Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Lists of Numbers
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4 Reasoning About Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
Induction on Lists
4.4.1
4.4.2
Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4.3 List Exercises, Part 1 . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4.4 List Exercises, Part 2 . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.5 Options
4.6 Partial Maps
5 Library Top.Poly
5.1 Poly: Polymorphism and Higher-Order Functions
. . . . . . . . . . . . . . .
5.2 Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.1 Polymorphic Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.2 Polymorphic Pairs
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.2.3 Polymorphic Options . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3 Functions as Data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . .
5.3.1 Higher-Order Functions
5.3.2 Filter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.3 Anonymous Functions
. . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.4 Map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.5 Fold . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . .
5.3.6 Functions That Construct Functions
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4 Additional Exercises
6 Library Top.Tactics
6.1 Tactics: More Basic Tactics
. . . . . . . . . . . . . . . . . . . . . . . . . . .
6.2 The apply Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.3 The apply ... with ... Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.4 The inversion Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.5 Using Tactics on Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.6 Varying the Induction Hypothesis . . . . . . . . . . . . . . . . . . . . . . . .
2
29
31
31
31
34
35
38
41
41
41
43
49
50
53
54
55
56
58
60
60
60
60
67
68
69
70
70
71
72
74
74
75
80
80
80
82
83
86
87
6.7 Unfolding Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.8 Using destruct on Compound Expressions . . . . . . . . . . . . . . . . . . .
6.9 Review . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6.10 Additional Exercises
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
92
94
96
97
7 Library Top.Logic
100
7.1 Logic: Logic in Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
7.2 Logical Connectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
7.2.1 Conjunction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
7.2.2 Disjunction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
7.2.3 Falsehood and Negation . . . . . . . . . . . . . . . . . . . . . . . . . 105
7.2.4 Truth . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
7.2.5 Logical Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
7.2.6 Existential Quantification . . . . . . . . . . . . . . . . . . . . . . . . 111
7.3 Programming with Propositions . . . . . . . . . . . . . . . . . . . . . . . . . 112
7.4 Applying Theorems to Arguments . . . . . . . . . . . . . . . . . . . . . . . . 115
7.5 Coq vs. Set Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
7.5.1 Functional Extensionality . . . . . . . . . . . . . . . . . . . . . . . . 117
7.5.2 Propositions and Booleans . . . . . . . . . . . . . . . . . . . . . . . . 118
7.5.3 Classical vs. Constructive Logic . . . . . . . . . . . . . . . . . . . . . 122
8 Library Top.IndProp
126
IndProp: Inductively Defined Propositions . . . . . . . . . . . . . . . . . . . 126
8.1
8.2
Inductively Defined Propositions . . . . . . . . . . . . . . . . . . . . . . . . . 126
8.3 Using Evidence in Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
Inversion on Evidence
. . . . . . . . . . . . . . . . . . . . . . . . . . 128
8.3.1
8.3.2
Induction on Evidence . . . . . . . . . . . . . . . . . . . . . . . . . . 132
Inductive Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
. . . . . . . . . . . . . . . . . . . . . . . . 138
8.5.1 The remember Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
8.6 Case Study: Improving Reflection . . . . . . . . . . . . . . . . . . . . . . . . 148
8.7 Additional Exercises
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
8.4
8.5 Case Study: Regular Expressions
9 Library Top.Maps
155
9.1 Maps: Total and Partial Maps . . . . . . . . . . . . . . . . . . . . . . . . . . 155
9.2 The Coq Standard Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156
9.3
9.4 Total Maps
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
9.5 Partial maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160
Identifiers
10 Library Top.ProofObjects
162
10.1 ProofObjects: The Curry-Howard Correspondence . . . . . . . . . . . . . . . 162
10.2 Proof Scripts
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
3
10.3 Quantifiers, Implications, Functions . . . . . . . . . . . . . . . . . . . . . . . 165
10.4 Programming with Tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
10.5 Logical Connectives as Inductive Types . . . . . . . . . . . . . . . . . . . . . 167
10.5.1 Conjunction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167
10.5.2 Disjunction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168
10.5.3 Existential Quantification . . . . . . . . . . . . . . . . . . . . . . . . 168
10.5.4 True and False . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
10.6 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
10.6.1 Inversion, Again . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170
11 Library Top.IndPrinciples
172
. . . . . . . . . . . . . . . . . . . . . . . 172
11.1 IndPrinciples: Induction Principles
11.2 Basics
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172
11.3 Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
11.4 Induction Hypotheses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176
11.5 More on the induction Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . 177
11.6 Induction Principles in Prop . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
11.7 Formal vs. Informal Proofs by Induction . . . . . . . . . . . . . . . . . . . . 180
11.7.1 Induction Over an Inductively Defined Set . . . . . . . . . . . . . . . 181
11.7.2 Induction Over an Inductively Defined Proposition . . . . . . . . . . 181
12 Library Top.Rel
183
12.1 Rel: Properties of Relations
. . . . . . . . . . . . . . . . . . . . . . . . . . . 183
12.2 Basic Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
12.3 Reflexive, Transitive Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . 188
13 Library Top.Imp
191
13.1 Imp: Simple Imperative Programs . . . . . . . . . . . . . . . . . . . . . . . . 191
13.2 Arithmetic and Boolean Expressions
. . . . . . . . . . . . . . . . . . . . . . 191
13.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
13.2.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
13.2.3 Optimization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
13.3 Coq Automation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195
13.3.1 Tacticals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195
13.3.2 Defining New Tactic Notations
. . . . . . . . . . . . . . . . . . . . . 199
13.3.3 The omega Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199
. . . . . . . . . . . . . . . . . . . . . . . 200
13.3.4 A Few More Handy Tactics
13.4 Evaluation as a Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201
13.4.1 Inference Rule Notation . . . . . . . . . . . . . . . . . . . . . . . . . 202
13.4.2 Equivalence of the Definitions . . . . . . . . . . . . . . . . . . . . . . 203
13.4.3 Computational vs. Relational Definitions . . . . . . . . . . . . . . . . 204
. . . . . . . . . . . . . . . . . . . . . . . . . . . 206
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206
13.5 Expressions With Variables
13.5.1 States
4
13.6 Commands
13.5.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207
13.5.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
13.6.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
13.6.2 More Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209
13.7 Evaluating Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210
13.7.1 Evaluation as a Function (Failed Attempt) . . . . . . . . . . . . . . . 210
13.7.2 Evaluation as a Relation . . . . . . . . . . . . . . . . . . . . . . . . . 211
13.7.3 Determinism of Evaluation . . . . . . . . . . . . . . . . . . . . . . . . 214
13.8 Reasoning About Imp Programs . . . . . . . . . . . . . . . . . . . . . . . . . 215
13.9 Additional Exercises
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216
14 Library Top.ImpParser
222
14.1 ImpParser: Lexing and Parsing in Coq . . . . . . . . . . . . . . . . . . . . . 222
14.2 Internals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
14.2.1 Lexical Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
14.2.2 Parsing
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230
14.3 Examples
15 Library Top.ImpCEvalFun
231
15.1 ImpCEvalFun: Evaluation Function for Imp . . . . . . . . . . . . . . . . . . 231
15.2 A Broken Evaluator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
15.3 A Step-Indexed Evaluator
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 232
15.4 Relational vs. Step-Indexed Evaluation . . . . . . . . . . . . . . . . . . . . . 235
15.5 Determinism of Evaluation Again . . . . . . . . . . . . . . . . . . . . . . . . 238
16 Library Top.Extraction
239
16.1 Extraction: Extracting ML from Coq . . . . . . . . . . . . . . . . . . . . . . 239
16.2 Basic Extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239
16.3 Controlling Extraction of Specific Types
. . . . . . . . . . . . . . . . . . . . 239
16.4 A Complete Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240
16.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241
17 Library Top.Equiv
242
17.1 Equiv: Program Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . 242
17.2 Behavioral Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
17.2.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
17.2.2 Simple Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244
17.3 Properties of Behavioral Equivalence . . . . . . . . . . . . . . . . . . . . . . 251
17.3.1 Behavioral Equivalence Is an Equivalence . . . . . . . . . . . . . . . . 251
. . . . . . . . . . . . . . . . 252
17.3.2 Behavioral Equivalence Is a Congruence
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
17.4.1 The Constant-Folding Transformation . . . . . . . . . . . . . . . . . 256
17.4 Program Transformations
5
17.4.2 Soundness of Constant Folding
. . . . . . . . . . . . . . . . . . . . . 259
17.5 Proving That Programs Are Not Equivalent . . . . . . . . . . . . . . . . . . 263
17.6 Extended Exercise: Nondeterministic Imp . . . . . . . . . . . . . . . . . . . 266
17.7 Additional Exercises
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 270
18 Library Top.Hoare
273
18.1 Hoare: Hoare Logic, Part I . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273
18.2 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275
18.3 Hoare Triples
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 276
18.4 Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278
18.4.1 Assignment
18.4.2 Consequence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 282
18.4.3 Digression: The eapply Tactic . . . . . . . . . . . . . . . . . . . . . . 284
18.4.4 Skip . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 286
18.4.5 Sequencing
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287
18.4.6 Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289
18.4.7 Loops
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 294
18.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 298
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300
18.6 Additional Exercises
19 Library Top.Hoare2
19.3 Finding Loop Invariants
302
19.1 Hoare2: Hoare Logic, Part II . . . . . . . . . . . . . . . . . . . . . . . . . . . 302
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 302
19.2 Decorated Programs
19.2.1 Example: Swapping Using Addition and Subtraction . . . . . . . . . 304
19.2.2 Example: Simple Conditionals . . . . . . . . . . . . . . . . . . . . . . 305
19.2.3 Example: Reduce to Zero . . . . . . . . . . . . . . . . . . . . . . . . 306
19.2.4 Example: Division . . . . . . . . . . . . . . . . . . . . . . . . . . . . 307
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 308
19.3.1 Example: Slow Subtraction . . . . . . . . . . . . . . . . . . . . . . . 308
19.3.2 Exercise: Slow Assignment . . . . . . . . . . . . . . . . . . . . . . . . 310
19.3.3 Exercise: Slow Addition . . . . . . . . . . . . . . . . . . . . . . . . . 311
19.3.4 Example: Parity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311
19.3.5 Example: Finding Square Roots . . . . . . . . . . . . . . . . . . . . . 312
19.3.6 Example: Squaring . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313
19.3.7 Exercise: Factorial
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 314
19.3.8 Exercise: Min . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315
19.3.9 Exercise: Power Series . . . . . . . . . . . . . . . . . . . . . . . . . . 316
19.4 Weakest Preconditions (Optional) . . . . . . . . . . . . . . . . . . . . . . . . 316
19.5 Formal Decorated Programs (Optional) . . . . . . . . . . . . . . . . . . . . . 318
19.5.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 318
19.5.2 Extracting Verification Conditions . . . . . . . . . . . . . . . . . . . . 322
19.5.3 Automation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 324
19.5.4 Examples
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 326
6
20 Library Top.HoareAsLogic
339
20.1 HoareAsLogic: Hoare Logic as a Logic
. . . . . . . . . . . . . . . . . . . . . 339
20.2 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 339
20.3 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341
21 Library Top.Smallstep
345
21.1 Smallstep: Small-step Operational Semantics . . . . . . . . . . . . . . . . . . 345
21.2 A Toy Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 346
21.3 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 348
21.3.1 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 351
21.3.2 Strong Progress and Normal Forms . . . . . . . . . . . . . . . . . . . 353
21.4 Multi-Step Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 360
21.4.1 Examples
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 361
21.4.2 Normal Forms Again . . . . . . . . . . . . . . . . . . . . . . . . . . . 363
21.4.3 Equivalence of Big-Step and Small-Step . . . . . . . . . . . . . . . . . 365
. . . . . . . . . . . . . . . . . . . . . . . . . . . 367
21.4.4 Additional Exercises
21.5 Small-Step Imp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368
21.6 Concurrent Imp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 371
21.7 A Small-Step Stack Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . 375
22 Library Top.Auto
377
22.1 Auto: More Automation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377
22.2 The auto Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 378
22.3 Searching For Hypotheses
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 382
23 Library Top.Types
390
23.1 Types: Type Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 390
23.2 Typed Arithmetic Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 390
23.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 390
23.2.2 Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 391
23.2.3 Normal Forms and Values
. . . . . . . . . . . . . . . . . . . . . . . . 393
23.2.4 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 394
23.2.5 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 396
23.2.6 Type Preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 397
23.2.7 Type Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399
23.3 Aside: the normalize Tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . 399
. . . . . . . . . . . . . . . . . . . . . . . . . . . 401
23.3.1 Additional Exercises
24 Library Top.Stlc
404
24.1 Stlc: The Simply Typed Lambda-Calculus . . . . . . . . . . . . . . . . . . . 404
24.2 The Simply Typed Lambda-Calculus . . . . . . . . . . . . . . . . . . . . . . 404
24.2.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 404
24.2.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 406
7
24.2.3 Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 407
24.2.4 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 414
25 Library Top.StlcProp
418
25.1 StlcProp: Properties of STLC . . . . . . . . . . . . . . . . . . . . . . . . . . 418
25.2 Canonical Forms
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 418
25.3 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419
25.4 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421
25.4.1 Free Occurrences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421
25.4.2 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 422
25.4.3 Main Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427
25.5 Type Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 428
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 429
25.6 Uniqueness of Types
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 429
25.7 Additional Exercises
. . . . . . . . . . . . . . . . . . . . 432
25.7.1 Exercise: STLC with Arithmetic
26 Library Top.MoreStlc
433
26.1 MoreStlc: More on the Simply Typed Lambda-Calculus . . . . . . . . . . . . 433
26.2 Simple Extensions to STLC . . . . . . . . . . . . . . . . . . . . . . . . . . . 433
26.2.1 Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 433
26.2.2 Let Bindings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 433
26.2.3 Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 434
26.2.4 Unit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 436
26.2.5 Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 436
26.2.6 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 438
26.2.7 General Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 439
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442
26.2.8 Records
26.3 Exercise: Formalizing the Extensions . . . . . . . . . . . . . . . . . . . . . . 444
26.3.1 Examples
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 452
26.3.2 Properties of Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . 456
27 Library Top.Sub
467
27.1 Sub: Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 467
27.2 Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 467
27.2.1 A Motivating Example . . . . . . . . . . . . . . . . . . . . . . . . . . 467
27.2.2 Subtyping and Object-Oriented Languages . . . . . . . . . . . . . . . 468
27.2.3 The Subsumption Rule . . . . . . . . . . . . . . . . . . . . . . . . . . 468
27.2.4 The Subtype Relation . . . . . . . . . . . . . . . . . . . . . . . . . . 469
27.2.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 476
27.3.1 Core Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477
27.3.2 Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 479
27.3.3 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 480
27.3 Formal Definitions
8
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
