Type Theory And Formal Proof.

TYPE THEORY AND FORMAL PROOFAn IntroductionROB N E DERPELTEindhoven University of Technology,The NetherlllndsH E RMAN G E UVERSRlldboud University Nijmegen.andEindhoven University l!f Tech nology,The NetherlandsUCAMBRIDGE'iU NIVERSITY PRESS

ContentsForeword, by Henk BarendregtPrefaceAcknowledgementsGreek alphabetpage xiiixvXXVllxxviii1Untyped lambda calculus1.1 Input -output behaviour of functions1.2 The essence of fu nctions1.3 Lambda-terms1.4 Free and bound variables1.5 Alpha conversion1.6 Substitution1.7 Lambda-terms modulo a-equivalence1.8 Beta reduction1.9 Normal forms and confluence1.10 Fixed Point Theorem1.11 Conclusions1.12 Furt her readingExercises11248911141619242627292Simply typed lambda calculus2.1 Adding types2.2 Simple types2.3 Church-typing and Curry-typing2.4 Derivation rules for Church 's A-t2.5 Different form ats for a derivation in A-t2.6 Kinds of problems to be solved in type theory2.7 Well-typedness in A-t2.8 Type Checking in A-t2.9 Term Finding in A-t33333436394446475051

VlllContents2.10 General properties of ).--- 2.11 Reduction and ).--- 2.12 Consequences2.13 Conclusions2.14 Further readingExercises5359636465663Second order typed lambda calculus3.1 Type-abstraction and type-application3.2 II-types3.3 Second order abstraction and application rules3.4 The system ),23.5 Example of a derivation in ),23.6 Properties of ),23.7 Conclusions3.8 Further readingExercises696971727376788080824Types dependent on types4.1 Type constructors4.2 Sort-rule and var-rule in ). 4.3 The weakening rule in ). 4.4 The formation rule in ). 4.5 Application and abstraction rules in4.6 Shortened derivations4.7 The conversion rule4.8 Properties of ). 4.9 Conclusions4.10 Further readingExercises). 8585889093949597991001001015Types dependent on terms5.1 The missing extension5.2 Derivation rules of ).P5.3 An example derivation in ).P5.4 Minimal predicate logic in ).P5.5 Example of a logical derivation in ).P5.6 Conclusions5.7 Further readingExercises1031031051071091151181191216The Calculus of Constructions6.1 The system )'C6.2 The ).-cube123123125

Contents6.36.46.5Properties of ACConclusionsFurther readingExercises7T he encoding of logical not ions in AC7.1 Absurdity and negation in type t heory7.2 Conjunction and disjunction in type theory7.3 An example of propositional logic in AC7.4 Classical logic in AC7.5 Predicate logic in AC7.6 An example of predicate logic in AC7.7 Conclusions7.8 Further readingExercises8D efini tionsThe nature of definitionsInductive and recursive definitionsThe format of definitionsInstantiations of definitionsA formal format for definitionsDefinitions depending on assumptionsGiving names to proofsA general proof and a specialised versionMathematical statements as formal definitionsConclusionsFurther 19Extension of AC w ith definit ions9.1 Extension of AC to the system ADo9.2 Judgements extended with definitions9.3 The rule for adding a definition9.4 The rule for instantiating a defin ition9.5 Definition unfolding and 5-conversion9.6 Examples of 5-conversion9.7 The conversion rule extended with 9.8 The derivation rules for ADo9.9 A closer look at the derivation rules of ADo9.10 Conclusions9.11 Further 89189190192193197200202203204206207208

xContents10Rules and properties of AD10.1 Descriptive versus primitive definitions10.2 Axioms and axiomatic notions10.3 Rules for primitive definitions10.4 Properties of AD10.5 Normalisation and confluence in AD10.6 Conclusions10.7 Further style natural deduction in AD11.1 Formal derivations in AD11 .2 Comparing formal and flag-style AD11.3 Conventions about fl ag-style proofs in AD11 .4 Introduction and elimination rules11.5 Rules for constructive propositional logic11.6 Examples of logical derivations in AD11 .7 Suppressing unaltered parameter lists11.8 Rules for classical propositional logic11.9 Alternative natural deduction rules for V11.10 Rules for constructive predicate logic11.11 Rules for classical predicate logic11.12 Conclusions11.13 Further 4925225325412Mathematics in AD: a first attempt12.1 An example to start with12.2 Equality12.3 The congruence property of equality12.4 Orders12.5 A proof about orders12.6 Unique existence12.7 The descriptor L12.8 Conclusions12.9 Further 3Sets13.113 .213.313.4279279282287288and subsetsDealing with subsets in ADBasic set-theoretic notionsSpecial subsetsRelations

Contentsxi13.5 Maps13.6 Representation of mathematical notions13.7 Conclusions13.8 Further readingExercises29129529629730214N umbers and arithmetic in AD14.1 The Peano axioms for natural numbers14.2 Introducing integers the axiomatic way14.3 Basic properties of the 'new' N14.4 In teger addition14.5 An example of a basic computation in AD14.6 Arithmetical laws for addition14.7 Closure under addition for natural and negative numbers14.8 Integer subtraction14.9 The opposite of an integer14.10 Inequality relations on Z14.11 Multiplication of integers14.12 Divisibility14.13 Irrelevance of proof14.14 Conclusions14.15 Further 3533834034134334415An elaborated example15.1 Formalising a proof of Bezout's Lemma15.2 Preparatory work15.3 P art I of the proof of Bezout 's Lemma15.4 Part II of the proof15.5 Part III of the proof15.6 The holes in the proof of Bezout's Lemma15.7 The Minimum Theorem for Z15.8 The Division Theorem15.9 Conclusions15.10 Further 7616Further perspectives16.1 Useful applications of AD16.2 Proof assistants based OIl type theory16.3 Future of the field16.4 Conclusions16.5 Further reading379379380384386387

ContentsXliAppendixA.1A.2A.3A.4A Logic in ADConstructive propositional logicClassical propositional logicConstructive predicate logicClassical predicate logicAppendix BArithmetical axioms, definitions and lemmas391391393395396397Appendix C Two complete example proofs in ADC.1 Closure under addition in NC.2 The Minimum Theorem403403405Derivation rules for AD409Appendix DReferencesIndex of namesIndex of definitionsIndex of symbolsIndex of subjects411419421423425

8.2 Inductive and recursive definitions 167 8.3 The format of definitions 168 8.4 Instantiations of definitions 170 8.5 A formal format for definitions 172 8.6 Definitions depending on assumptions 174 8.7 Giving names to proofs 175 8.8 A general proof and a specialised version 178 8.9 Mathematical statements as formal definitions 180