Interactive Theorem Proving and Program Development

Frontmatter

1. A Brief Overview

Abstract

Coq [37] is a proof assistant with which students, researchers, or engineers can express specifications and develop programs that fulfill these specifications. This tool is well adapted to develop programs for which absolute trust is required: for example, in telecommunication, transportation, energy, banking, etc. In these domains the need for programs that rigorously conform to specifications justifies the effort required to verify these programs formally. We shall see in this book how a proof assistant like Coq can make this work easier.

Yves Bertot, Pierre Castéran

2. Types and Expressions

Abstract

One of the main use of Coq is to certify and, more generally, to reason about programs We must show how the Gallina language represents these programs. The formalism used in this chapter is a simply typed λ-calculus [24], akin to a purely functional programming language without polymorphism. This simple formalism is introduced in a way that makes forthcoming extensions natural. With these extensions we can not only reason logically, but also build complex program specifications. To this end, classical notions like environments, contexts, expressions and types will be introduced, but we shall also see more complex notions like sorts and universes.

Yves Bertot, Pierre Castéran

3. Propositions and Proofs

Abstract

In this chapter we introduce the reasoning techniques used in Coq, start­ing with a very reduced fragment of logic, minimal propositional logic, where formulas are exclusively constructed using propositional variables and implication.

Yves Bertot, Pierre Castéran

4. Dependent Products or Pandora’s Box

Abstract

Until now we have restricted our study to simply typed λ-calculus and this considerably limited the expressive power of the specifications and propositions. This limitation disappears with the introduction of a new type construct, called the dependent product. This construct generalizes the arrow A → B which represents functional types or implications depending on the sort of A and B. With dependent products we can build functions where the result type depends on the argument.

Yves Bertot, Pierre Castéran

5. Everyday Logic

Abstract

The previous chapters show that the Calculus of Constructions is powerful enough as a type system for the representation of logical formulas and theorems. Interpreting types as formulas and terms as proofs works well and makes it possible to reduce the problem of verifying formal proofs to the problem of verifying that some terms are well-typed. This chapter takes a more pragmatic point of view and shows how we can use tactics to make the logical reasoning easier.

Yves Bertot, Pierre Castéran

6. Inductive Data Types

Abstract

The inductive types of Coq extend the various notions of type definitions provided in conventional programming languages. They can be compared to the recursive type definitions found in most functional programming languages. However, the possibility of mixing recursive types and dependent products makes the inductive types of Coq much more precise and expressive, up to the point where they can also be used to describe pure logic programming, in other words the primitive kernel of Prolog.

Yves Bertot, Pierre Castéran

7. Tactics and Automation

Abstract

There are two parts to this chapter. The first part presents several collections of tactics specialized in various domains of logic and mathematics: tactics specialized in reasoning about inductive types, the main automatic tactics, which rely on a Prolog-like proof search mechanism, the tactics for equality and rewriting, the tactics for numerical proofs, and the automatic decision procedures for restricted fragments of logic.

Yves Bertot, Pierre Castéran

8. Inductive Predicates

Abstract

The strength of inductive types in the Calculus of Constructions is mostly a consequence of their interaction with the dependent product. With the extra expressive power we can formulate a large variety of properties on data and programs, simply by using type expressions. Dependent inductive types easily cover the usual aspects of logic: namely, connectives, existential quantification, equality, natural numbers. All these concepts are uniformly described and handled as inductive types. The expressive power of inductive types also covers logic programming, in other words the languages of the Prolog family.

Yves Bertot, Pierre Castéran

9. * Functions and Their Specifications

Abstract

We gave an informal presentation of certified programs in Chap. 1. Given a relation R of A→B→Prop, we want to produce a function that maps any a in A to a value b in B together with a proof of “R a b” (a certificate).

Yves Bertot, Pierre Castéran

10. * Extraction and Imperative Programming

Abstract

We can use the Coq system to model programs, by describing them as functions in a purely functional programming language. However, the Coq system does not provide an efficient environment to execute them. It is better to rely on the usual programming tools (compilers, abstract machines, and so on) to provide this environment. The Coq system simply provides ways to translate formal developments into conventional programming languages.

Yves Bertot, Pierre Castéran

11. * A Case Study

Abstract

In Chap. 10, we described succinctly the principle of the extraction mechanism. This chapter contains a simple case study to illustrate the subtle links between the sorts Prop and Set. In particular, we can develop and extract certified programs that provide reasonable efficiency, thanks to our knowledge of the extraction process.

Yves Bertot, Pierre Castéran

12. * The Module System

Abstract

Most modern programming languages provide ways to structure programs in large units called modules.When modules are adequately designed, they can be reused in very different application contexts.

Yves Bertot, Pierre Castéran

13. ** Infinite Objects and Proofs

Abstract

Reasoning about infinite objects while staying in the finite world of a computer is one of the most fascinating uses of proof tools.

Yves Bertot, Pierre Castéran

14. ** Foundations of Inductive Types

Abstract

There is a lot of freedom in inductive definitions. A type may be a constant whose type is one of the sorts in the system, it may also be a function, this function may have a dependent type, and some of its arguments may be parameters. The constructors may be constants or functions, possibly with a dependent type, their arguments may or may not be in the inductive type, and these arguments may themselves be functions. In this section, we want to study the limits of this freedom.

Yves Bertot, Pierre Castéran

15. * General Recursion

Abstract

Structural recursion is powerful, especially in combination with higher-order definitions, as we have seen in the example of Ackermann’s function. Nevertheless, it is not always adapted to describe algorithms where termination is difficult to express as structural recursion with respect to one of the arguments.

Yves Bertot, Pierre Castéran

16. * Proof by Reflection

Abstract

Proof by reflection is a characteristic feature of proving in type theory. There is a programming language embedded inside the logical language and it can be used to describe decision procedures or systematic reasoning methods. We already know that programming in Coq is a costly task and this approach is only worth the effort because the proof process is made much more efficient. In some cases, dozens of rewrite operations can be replaced with a few theorem applications and a convertibility test of the Calculus of Inductive Constructions. Since the computations of this programming language do not appear in the proof terms, we obtain proofs that are smaller and often quicker to check.

Yves Bertot, Pierre Castéran

Backmatter