The Coq Proof Assistant A Tutorial.pdf-资料库

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第1页.png

第1页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第2页.png

第2页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第3页.png

第3页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第4页.png

第4页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第5页.png

第5页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第6页.png

第6页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第7页.png

第7页 / 共53页

54282aa6-7517-482e-84f4-fb2e55b92398.pdf-第8页.png

第8页 / 共53页

The Coq Proof Assistant A Tutorial April 19, 2011 Version 8.3pl2 Gérard Huet, Gilles Kahn and Christine Paulin-Mohring The Coq Development Team

V8.3pl2, April 19, 2011 cINRIA 1999-2004 (COQ versions 7.x) cINRIA 2004-2010 (COQ versions 8.x)

Getting started COQ is a Proof Assistant for a Logical Framework known as the Calculus of Induc- tive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their speciﬁcations. It runs as a computer program on many architectures. It is available with a variety of user interfaces. The present document does not attempt to present a comprehensive view of all the possibilities of COQ, but rather to present in the most elementary manner a tutorial on the basic speciﬁcation language, called Gallina, in which for- mal axiomatisations may be developed, and on the main proof tools. For more advanced information, the reader could refer to the COQ Reference Manual or the Coq’Art, a new book by Y. Bertot and P. Castéran on practical uses of the COQ system. Coq can be used from a standard teletype-like shell window but preferably through the graphical user interface CoqIde1. Instructions on installation procedures, as well as more comprehensive docu- mentation, may be found in the standard distribution of COQ, which may be ob- tained from COQ web site http://coq.inria.fr. In the following, we assume that COQ is called from a standard teletype-like shell window. All examples preceded by the prompting sequence Coq < represent user input, terminated by a period. The following lines usually show COQ’s answer as it appears on the users screen. When used from a graphical user interface such as CoqIde, the prompt is not displayed: user input is given in one window and COQ’s answers are displayed in a different window. The sequence of such examples is a valid COQ session, unless otherwise spec- iﬁed. This version of the tutorial has been prepared on a PC workstation running Linux. The standard invocation of COQ delivers a message such as: unix:~> coqtop Welcome to Coq 8.3 (October 2010) Coq < The ﬁrst line gives a banner stating the precise version of COQ used. You 1Alternative graphical interfaces exist: Proof General and Pcoq. 3

4 should always return this banner when you report an anomaly to our bug-tracking system http://coq.inria.fr/bugs

Chapter 1 Basic Predicate Calculus 1.1 An overview of the speciﬁcation language Gallina A formal development in Gallina consists in a sequence of declarations and deﬁni- tions. You may also send COQ commands which are not really part of the formal development, but correspond to information requests, or service routine invoca- tions. For instance, the command: Coq < Quit. terminates the current session. 1.1.1 Declarations A declaration associates a name with a speciﬁcation. A name corresponds roughly to an identiﬁer in a programming language, i.e. to a string of letters, digits, and a few ASCII symbols like underscore (_) and prime (’), starting with a letter. We use case distinction, so that the names A and a are distinct. Certain strings are reserved as key-words of COQ, and thus are forbidden as user identiﬁers. A speciﬁcation is a formal expression which classiﬁes the notion which is being declared. There are basically three kinds of speciﬁcations: logical propositions, mathematical collections, and abstract types. They are classiﬁed by the three basic sorts of the system, called respectively Prop, Set, and Type, which are themselves atomic abstract types. Every valid expression e in Gallina is associated with a speciﬁcation, itself a valid expression, called its type τ(E). We write e : τ(E) for the judgment that e is of type E. You may request COQ to return to you the type of a valid expression by using the command Check: Coq < Check O. 0 : nat 5

6 CHAPTER 1. BASIC PREDICATE CALCULUS Thus we know that the identiﬁer O (the name ‘O’, not to be confused with the numeral ‘0’ which is not a proper identiﬁer!) is known in the current context, and that its type is the speciﬁcation nat. This speciﬁcation is itself classiﬁed as a mathematical collection, as we may readily check: Coq < Check nat. nat : Set The speciﬁcation Set is an abstract type, one of the basic sorts of the Gal- lina language, whereas the notions nat and O are notions which are deﬁned in the arithmetic prelude, automatically loaded when running the COQ system. We start by introducing a so-called section name. The role of sections is to structure the modelisation by limiting the scope of parameters, hypotheses and deﬁnitions. It will also give a convenient way to reset part of the development. Coq < Section Declaration. With what we already know, we may now enter in the system a declaration, corre- sponding to the informal mathematics let n be a natural number. Coq < Variable n : nat. n is assumed If we want to translate a more precise statement, such as let n be a positive natural number, we have to add another declaration, which will declare explicitly the hypothesis Pos_n, with speciﬁcation the proper logical proposition: Coq < Hypothesis Pos_n : (gt n 0). Pos_n is assumed Indeed we may check that the relation gt is known with the right type in the current context: Coq < Check gt. gt : nat -> nat -> Prop which tells us that gt is a function expecting two arguments of type nat in order to build a logical proposition. What happens here is similar to what we are used to in a functional programming language: we may compose the (speciﬁcation) type nat with the (abstract) type Prop of logical propositions through the arrow function constructor, in order to get a functional type nat->Prop: Coq < Check (nat -> Prop). nat -> Prop : Type

1.1. AN OVERVIEW OF THE SPECIFICATION LANGUAGE GALLINA 7 which may be composed one more times with nat in order to obtain the type nat->nat->Prop of binary relations over natural numbers. Actually the type nat->nat->Prop is an abbreviation for nat->(nat->Prop). Functional notions may be composed in the usual way. An expression f of type A → B may be applied to an expression e of type A in order to form the ex- pression ( f e) of type B. Here we get that the expression (gt n) is well-formed of type nat->Prop, and thus that the expression (gt n O), which abbreviates ((gt n) O), is a well-formed proposition. Coq < Check gt n O. n > 0 : Prop 1.1.2 Deﬁnitions The initial prelude contains a few arithmetic deﬁnitions: nat is deﬁned as a math- ematical collection (type Set), constants O, S, plus, are deﬁned as objects of types respectively nat, nat->nat, and nat->nat->nat. You may introduce new deﬁni- tions, which link a name to a well-typed value. For instance, we may introduce the constant one as being deﬁned to be equal to the successor of zero: Coq < Definition one := (S O). one is defined We may optionally indicate the required type: Coq < Definition two : nat := S one. two is defined Actually COQ allows several possible syntaxes: Coq < Definition three : nat := S two. three is defined Here is a way to deﬁne the doubling function, which expects an argument m of type nat in order to build its result as (plus m m): Coq < Definition double (m:nat) := plus m m. double is defined This introduces the constant double deﬁned as the expression fun m:nat => plus m m. The abstraction introduced by fun is explained as follows. The ex- pression fun x:A => e is well formed of type A->B in a context whenever the expression e is well-formed of type B in the given context to which we add the declaration that x is of type A. Here x is a bound, or dummy variable in the ex- pression fun x:A => e. For instance we could as well have deﬁned double as fun n:nat => (plus n n). Bound (local) variables and free (global) variables may be mixed. For instance, we may deﬁne the function which adds the constant n to its argument as

8 CHAPTER 1. BASIC PREDICATE CALCULUS Coq < Definition add_n (m:nat) := plus m n. add_n is defined However, note that here we may not rename the formal argument m into n without capturing the free occurrence of n, and thus changing the meaning of the deﬁned notion. Binding operations are well known for instance in logic, where they are called quantiﬁers. Thus we may universally quantify a proposition such as m > 0 in order to get a universal proposition ∀m· m > 0. Indeed this operator is available in COQ, with the following syntax: forall m:nat, gt m O. Similarly to the case of the functional abstraction binding, we are obliged to declare explicitly the type of the quantiﬁed variable. We check: Coq < Check (forall m:nat, gt m 0). forall m : nat, m > 0 : Prop We may clean-up the development by removing the contents of the current section: Coq < Reset Declaration. 1.2 Introduction to the proof engine: Minimal Logic In the following, we are going to consider various propositions, built from atomic propositions A,B,C. This may be done easily, by introducing these atoms as global variables declared of type Prop. It is easy to declare several names with the same speciﬁcation: Coq < Section Minimal_Logic. Coq < Variables A B C : Prop. A is assumed B is assumed C is assumed We shall consider simple implications, such as A → B, read as “A implies B”. Remark that we overload the arrow symbol, which has been used above as the functionality type constructor, and which may be used as well as propositional connective: Coq < Check (A -> B). A -> B : Prop Let us now embark on a simple proof. We want to prove the easy tautology ((A → (B → C)) → (A → B) → (A → C). We enter the proof engine by the com- mand Goal, followed by the conjecture we want to verify: Coq < Goal (A -> B -> C) -> (A -> B) -> A -> C. 1 subgoal

资料库

The Coq Proof Assistant A Tutorial.pdf

相关推荐

开发技术

热门标签

最新资料