Certified Programming with Dependent Types - Adam Chlipala

Because Twelf is specialized to the domain of syntactic metatheory proofs about programming languages and logics, it is feasible to use it to write those kinds of ...
4MB Sizes 4 Downloads 445 Views
Certified Programming with Dependent Types Adam Chlipala July 12, 2017

A print version of this book is available from the MIT Press. For more information, see the book’s home page: http://adam.chlipala.net/cpdt/

Copyright Adam Chlipala 2008-2013, 2015, 2017. This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License. The license text is available at: http://creativecommons.org/licenses/by-nc-nd/3.0/

Contents 1 Introduction 1.1 Whence This Book? . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Why Coq? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.1 Based on a Higher-Order Functional Programming Language 1.2.2 Dependent Types . . . . . . . . . . . . . . . . . . . . . . . . 1.2.3 An Easy-to-Check Kernel Proof Language . . . . . . . . . . 1.2.4 Convenient Programmable Proof Automation . . . . . . . . 1.2.5 Proof by Reflection . . . . . . . . . . . . . . . . . . . . . . . 1.3 Why Not a Different Dependently Typed Language? . . . . . . . . 1.4 Engineering with a Proof Assistant . . . . . . . . . . . . . . . . . . 1.5 Prerequisites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.6 Using This Book . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.6.1 Reading This Book . . . . . . . . . . . . . . . . . . . . . . . 1.6.2 On the Tactic Library . . . . . . . . . . . . . . . . . . . . . 1.6.3 Installation and Emacs Set-Up . . . . . . . . . . . . . . . . . 1.7 Chapter Source Files . . . . . . . . . . . . . . . . . . . . . . . . . .

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

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

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

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

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

6 6 8 8 8 9 9 10 10 11 12 12 13 14 14 16

2 Some Quick Examples 2.1 Arithmetic Expressions Over Natural Numbers . 2.1.1 Source Language . . . . . . . . . . . . . 2.1.2 Target Language . . . . . . . . . . . . . 2.1.3 Translation . . . . . . . . . . . . . . . . 2.1.4 Translation Correctness . . . . . . . . . 2.2 Typed Expressions . . . . . . . . . . . . . . . . 2.2.1 Source Language . . . . . . . . . . . . . 2.2.2 Target Language . . . . . . . . . . . . . 2.2.3 Translation . . . . . . . . . . . . . . . . 2.2.4 Translation Correctness . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

17 17 18 20 21 22 30 30 32 35 36

I

Basic Programming and Proving

3 Introducing Inductive Types

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

39 40

2

3.1 3.2 3.3 3.4 3.5 3.6 3.7 3.8 3.9

Proof Terms . . . . . . . . . . . . . . Enumerations . . . . . . . . . . . . . Simple Recursive Types . . . . . . . Parameterized Types . . . . . . . . . Mutually Inductive Types . . . . . . Reflexive Types . . . . . . . . . . . . An Interlude on Induction Principles Nested Inductive Types . . . . . . . . Manual Proofs About Constructors .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

40 42 45 49 51 54 56 60 65

. . . . .

68 69 74 75 76 79

5 Infinite Data and Proofs 5.1 Computing with Infinite Data . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Infinite Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Simple Modeling of Non-Terminating Programs . . . . . . . . . . . . . . . .

86 87 90 98

4 Inductive Predicates 4.1 Propositional Logic . . . . . . . . . . . . 4.2 Wh