1.3 The Vernacular

1.3 The Vernacular

Figure 1.3 describes The Vernacular which is the language of commands of Gallina. A sentence of the vernacular language, like in many natural languages, begins with a capital letter and ends with a dot.
sentence ::= declaration
  | definition
  | statement
  | inductive
  | fixpoint
  | statement proof
     
params ::= typed_idents ; ... ; typed_idents
     
declaration ::= Axiom ident : term .
  | declaration_keyword params .
     
declaration_keyword ::= Parameter | Parameters
  | Variable | Variables
  | Hypothesis | Hypotheses
     


definition		 ::= Definition ident [: term] := term .
  | Local ident [: term] := term .
     


inductive		 ::= [Mutual] Inductive ind_body with ... with ind_body .
  | [Mutual] CoInductive ind_body with ... with ind_body .
     
ind_body ::= ident [[ params ]] : term := [constructor | ... | constructor]
     
constructor ::= ident : term
     


fixpoint		 ::= Fixpoint fix_body with ... with fix_body .
  | CoFixpoint cofix_body with ... with cofix_body .
     


statement		 ::= Theorem ident : term .
  | Lemma ident : term .
  | Definition ident : term .
     


proof		 ::= Proof . ... Qed .
  | Proof . ... Defined .


Figure 1.2:Syntax of sentences
The different kinds of command are described hereafter. They all suppose that the terms occurring in the sentences are well-typed.

1.3.1 Declarations

The declaration mechanism allows the user to specify his own basic objects. Declared objects play the role of axioms or parameters in mathematics. A declared object is an ident associated to a term. A declaration is accepted by Coq iff this term is a well-typed specification in the current context of the declaration and ident was not previously defined in the same module. This term is considered to be the type, or specification, of the ident.

Axiom ident : term.

This command links term to the name ident as its specification in the global context. The fact asserted by term is thus assumed as a postulate.


Error messages:
  1. Clash with previous constant ident



Variants:
  1. Parameter ident : term.
    Is equivalent to Axiom ident : term
  2. Parameter ident , ... , ident : term ; ... ; ident , ... , ident : term .
    Links the term's to the names comprising the lists ident , ... , ident : term ; ... ; ident , ... , ident : term.


Remark: It is possible to replace Parameter by Parameters when more than one parameter are given.

Variable ident : term.

This command links term to the name ident in the context of the current section. The name ident will be unknown when the current section will be closed. One says that the variable is discharged. Using the Variable command out of any section is equivalent to Axiom.


Error messages:
  1. Clash with previous constant ident



Variants:
  1. Variable ident , ... , ident:term ; ... ; ident , ... , ident:term .
    Links term to the names comprising the list ident , ... , ident:term ; ... ; ident , ... , ident:term
  2. Hypothesis ident , ... , ident  :  term ; ... ; ident , ... , ident  :  term .
    Hypothsis is a synonymous of Variable


Remark: It is possible to replace Variable by Variables and Hypothesis by Hypotheses when more than one variable or one hypothesis are given.


See also: section 2.5

It is advised to use the keywords Axiom and Hypothesis for logical postulates (i.e. when the assertion term is of sort Prop), and to use the keywords Parameter and Variable in other cases (corresponding to the declaration of an abstract mathematical entity).

1.3.2 Definitions

Definitions differ from declarations since they allow to give a name to a term whereas declarations were just giving a type to a name. That is to say that the name of a defined object can be replaced at any time by its definition. This replacement is called d-conversion(see section 4.3). A defined object is accepted by the system iff the defining term is well-typed in the current context of the definition. Then the type of the name is the type of term. The defined name is called a constantand one says that the constant is added to the environment.

A formal presentation of constants and environments is given in section 4.4.

Definition ident := term.

This command binds the value term to the name ident in the environment, provided that term is well-typed.


Error messages:
  1. Clash with previous constant ident



Variants:
  1. Definition ident : term1 := term2. It checks that the type of term2 is definitionally equal to term1, and registers ident as being of type term1, and bound to value term2.



Error messages:
  1. In environment the term: term2 does not have type term1.
    Actually, it has type     term3.



See also: sections 5.2.5, 7.5.6

Local ident := term.

This command binds the value term to the name ident in the environment of the current section. The name ident will be unknown when the current section will be closed and all occurrences of ident in persistent objects (such as theorems) defined within the section will be replaced by term. One can say that the Local definition is a kind of macro.


Error messages:
  1. Clash with previous constant ident



Variants:
  1. Local ident : term1 := term2.
    Checks that the type of term2 is definitionally equal to term1, and registers ident as being of type term1, and bound to value term2.



See also: sections 2.5, 5.2.5, 7.5.6

1.3.3 Inductive definitions

We gradually explain simple inductive types, simple annotated inductive types, simple parametric inductive types, mutually inductive types. We explain also co-inductive types.

Simple inductive types

A simple inductive type is defined by the following restricted grammar rule:

Inductive ident : term := | ident1 : term1 | .. | identn : termn.

The name ident is the name of the inductively defined object and term is its type. The names ident1, ..., identn are the names of its constructors and term1, ..., termn their respective types. The types of the constructors have to satisfy a positivity condition (see section 4.5.3) for ident. This condition ensures the soundness of the inductive definition. If this is the case, the constants ident, ident1, ..., identn are added to the environment with their respective types. Accordingly to the arity of the aimed inductive type (e.g. the type of term), Coq provides a number of destructors for ident. Destructors are named ident_ind, ident_rec or ident_rect which respectively correspond to elimination principles on Prop, Set and Type. The type of the destructors expresses structural induction/recursion principles over objects of ident. We give below two examples of the use of the Inductive definitions.

The set of natural numbers is defined as:
Coq < Inductive nat : Set := O : nat | S : nat -> nat.
nat_ind is defined
nat_rec is defined
nat_rect is defined
nat is defined


The type nat is defined as the least Set containing O and closed by the S constructor. The constants nat, O and S are added to the environment.

Now let us have a look at the elimination principles. They are three : nat_ind, nat_rec and nat_rect. The type of nat_ind is:
Coq < Check nat_ind.
nat_ind
     : (P:nat->Prop)(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)


This is the well known structural induction principle over natural numbers, i.e. the second-order form of Peano's induction principle. It allows to prove some universal property of natural numbers ((n:nat)(P n)) by induction on n. Recall that (n:nat)(P n) is Gallina's syntax for the universal quantification " n:nat× P(n).
The types of nat_rec and nat_rect are similar, except that they pertain to (P:nat->Set) and (P:nat->Type) respectively . They correspond to primitive induction principles (allowing dependent types) respectively over sorts Set and Type. The constant ident_ind is always provided, whereas ident_rec and ident_rect can be impossible to derive (for example, when ident is a proposition).

Simple annotated inductive types

As a second example of annotated inductive types, let us define the even predicate:

Coq < Inductive even : nat->Prop :=
Coq < | even_0 : (even O)
Coq < | even_SS : (n:nat)(even n)->(even (S (S n))).
even_ind is defined
even is defined


The type nat->Prop means that even is a unary predicate (inductively defined) over natural numbers. The type of its two constructors are the defining clauses of the predicate even. The type of even_ind is:

Coq < Check even_ind.
even_ind
     : (P:nat->Prop)
        (P O)
         ->((n:nat)(even n)->(P n)->(P (S (S n))))
            ->(n:nat)(even n)->(P n)


From a mathematical point of vue it asserts that the natural numbers satisfying the predicate even are exactly the naturals satisfying the clauses even_0 or even_SS. This is why, when we want to prove any predicate P over elements of even, it is enough to prove it for O and to prove that if any natural number n satisfies P its double successor (S (S n)) satisfies also P. This is indeed analogous to the structural induction principle we got for nat.


Error messages:
  1. Non positive Occurrence in termi
  2. Type of Constructor not well-formed



Variants:
  1. Inductive ident [ params ] : term := ident1:term1 | ... | identn:termn.
    Allows to define parameterized inductive types.
    For instance, one can define parameterized lists as:
    Coq < Inductive list [X:Set] : Set :=
    Coq < Nil : (list X) | Cons : X->(list X)->(list X).
    Note that, in the type of Nil and Cons, we write (list X) and not just list.
    The constants Nil and Cons will have respectively types:

    Coq < Check Nil.
    Nil
         : (X:Set)(list X)
    and

    Coq < Check Cons.
    Cons
         : (X:Set)X->(list X)->(list X)


    Types of destructors will be also quantified with (X:Set).
  2. Inductive sort ident := ident1:term1 | ... | identn:termn.
    with sort being one of Prop, Type, Set is equivalent to
    Inductive ident : sort := ident1:term1 | ... | identn:termn.
  3. Inductive sort ident [ params ]:= ident1:term1 | ... | identn:termn.
    Same as before but with parameters.



See also: sections 4.5, 7.7.1

Mutually inductive types

This command allows to define mutually recursive inductive types. Its syntax is:


Inductive ident1 : term1 :=
  ident11 : term11
| ...    
| identn11 : termn11
with
 ...
with identm : termm :=
  ident1m : term1m
| ...
| identnmm : termnmm.



Remark: The word Mutual can be optionally inserted in front of Inductive.

It has the same semantics as the above Inductive definition for each ident1, ..., identm. All names ident1, ..., identm and ident11, ..., identnmm are simultaneously added to the environment. Then well-typing of constructors can be checked. Each one of the ident1, ..., identm can be used on its own.

It is also possible to parameterize these inductive definitions. However, parameters correspond to a local context in which the whole set of inductive declarations is done. For this reason, the parameters must be strictly the same for each inductive types The extented syntax is:


Inductive ident1 [params ] : term1 :=
  ident11 : term11
 | ..
 | identn11 : termn11
with
  ..
with identm [params ] : termm :=
 ident1m : term1m
 | ..
 | identnmm : termnmm.



Example: The typical example of a mutual inductive data type is the one for trees and forests. We assume given two types A and B as variables. It can be declared the following way.

Coq < Variables A,B:Set.

Coq < Inductive tree : Set := node : A -> forest -> tree
Coq < with forest : Set :=
Coq < | leaf : B -> forest
Coq < | cons : tree -> forest -> forest.


This declaration generates automatically six induction principles. They are respectively called tree_rec, tree_ind, tree_rect, forest_rec, forest_ind, forest_rect. These ones are not the most general ones but are just the induction principles corresponding to each inductive part seen as a single inductive definition.

To illustrate this point on our example, we give the types of tree_rec and forest_rec.

Coq < Check tree_rec.
tree_rec
     : (P:tree->Set)((a:A)(f:forest)(P (node a f)))->(t:tree)(P t)

Coq < Check forest_rec.
forest_rec
     : (P:forest->Set)
        ((b:B)(P (leaf b)))
         ->((t:tree)(f:forest)(P f)->(P (cons t f)))->(f:forest)(P f)


Assume we want to parameterize our mutual inductive definitions with the two type variables A and B, the declaration should be done the following way:

Coq < Inductive
Coq < tree [A,B:Set] : Set := node : A -> (forest A B) -> (tree A B)
Coq < with forest [A,B:Set] : Set := leaf : B -> (forest A B)
Coq < | cons : (tree A B) -> (forest A B) -> (forest A B).


Assume we define an inductive definition inside a section. When the section is closed, the variables declared in the section and occurring free in the declaration are added as parameters to the inductive definition.

Co-inductive types

The objects of an inductive type are well-founded with respect to the constructors of the type. In other words, such objects contain only a finite number constructors. Co-inductive types arise from relaxing this condition, and admitting types whose objects contain an infinity of constructors. Infinite objects are introduced by a non-ending (but effective) process of construction, defined in terms of the constructors of the type.

An example of a co-inductive type is the type of infinite sequences of natural numbers, usually called streams. It can be introduced in Coq using the CoInductive command:
Coq < CoInductive Set Stream := Seq : nat->Stream->Stream.
Stream is defined


The syntax of this command is the same as the command Inductive (cf. section 1.3.3). Notice that no principle of induction is derived from the definition of a co-inductive type, since such principles only make sense for inductive ones. For co-inductive ones, the only elimination principle is case analysis. For example, the usual destructors on streams hd:Stream->nat and tl:Str->Str can be defined as follows:
Coq < Definition hd := [x:Stream]Cases x of (Seq a s) => a end.
hd is defined

Coq < Definition tl := [x:Stream]Cases x of (Seq a s) => s end.
tl is defined


Definition of co-inductive predicates and blocks of mutually co-inductive definitions are also allowed. An example of a co-inductive predicate is the extensional equality on streams:

Coq < CoInductive EqSt : Stream->Stream->Prop :=
Coq < eqst : (s1,s2:Stream)
Coq < (hd s1)=(hd s2)->
Coq < (EqSt (tl s1) (tl s2))->(EqSt s1 s2).
EqSt is defined


In order to prove the extensionally equality of two streams s1 and s2 we have to construct and infinite proof of equality, that is, an infinite object of type ( EqSt s1 s2). We will see how to introduce infinite objects in section 1.3.4.

1.3.4 Definition of recursive functions

Fixpoint ident [ ident1 : term1 ] : term2 := term3

This command allows to define inductive objects using a fixed point construction. The meaning of this declaration is to define ident a recursive function with one argument ident1 of type term1 such that (ident ident1) has type term2 and is equivalent to the expression term3. The type of the ident is consequently (ident1 : term1)term2 and the value is equivalent to [ident1 : term1]term3. The argument ident1 (of type term1) is called the recursive variable of ident. Its type should be an inductive definition.

To be accepted, a Fixpoint definition has to satisfy some syntactical constraints on this recursive variable. They are needed to ensure that the Fixpoint definition always terminates. For instance, one can define the addition function as :

Coq < Fixpoint add [n:nat] : nat->nat
Coq < := [m:nat]Cases n of O => m | (S p) => (S (add p m)) end.
add is recursively defined


The Cases operator matches a value (here n) with the various constructors of its (inductive) type. The remaining arguments give the respective values to be returned, as functions of the parameters of the corresponding constructor. Thus here when n equals O we return m, and when n equals (S p) we return (S (add p m)).

The Cases operator is formally described in detail in section 4.5.4. The system recognizes that in the inductive call (add p m) the first argument actually decreases because it is a pattern variable coming from Cases n of.


Variants:
  1. Fixpoint ident [ params ] : term1 := term2.
    It declares a list of identifiers with their type usable in the type term1 and the definition body term2 and the last identifier in ident0 is the recursion variable.
  2. Fixpoint ident1 [ params1 ] : term1 := term1'
    with     ...
    with     identm [ paramsm ] : termm := termm'
    Allows to define simultaneously ident1, ..., identm.



Example: The following definition is not correct and generates an error message:

Coq < Fixpoint wrongplus [n:nat] : nat->nat
Coq < := [m:nat]Cases m of O => n | (S p) => (S (wrongplus n p)) end.
Error during interpretation of command:
Fixpoint wrongplus [n:nat] : nat->nat 
   := [m:nat]Cases m of O => n | (S p) => (S (wrongplus n p)) end.
Error: Recursive call applied to an illegal term
 The recursive definition
 [n:nat][m:nat]Cases m of
                 O => n
               | (S p) => (S (wrongplus n p))
               end is not well-formed


because the declared decreasing argument n actually does not decrease in the recursive call. The function computing the addition over the second argument should rather be written:

Coq < Fixpoint plus [n,m:nat] : nat
Coq < := Cases m of O => n | (S p) => (S (plus n p)) end.


The ordinary match operation on natural numbers can be mimicked in the following way.
Coq < Fixpoint nat_match [C:Set;f0:C;fS:nat->C->C;n:nat] : C
Coq < := Cases n of O => f0 | (S p) => (fS p (nat_match C f0 fS p)) end.
The recursive call may not only be on direct subterms of the recursive variable n but also on a deeper subterm and we can directly write the function mod2 which gives the remainder modulo 2 of a natural number.
Coq < Fixpoint mod2 [n:nat] : nat
Coq < := Cases n of
Coq < O => O
Coq < | (S p) => Cases p of O => (S O) | (S q) => (mod2 q) end
Coq < end.
In order to keep the strong normalisation property, the fixed point reduction will only be performed when the argument in position of the recursive variable (whose type should be in an inductive definition) starts with a constructor.

The Fixpoint construction enjoys also the with extension to define functions over mutually defined inductive types or more generally any mutually recursive definitions.


Example: The size of trees and forests can be defined the following way:
Coq < Fixpoint tree_size [t:tree] : nat :=
Coq < Cases t of (node a f) => (S (forest_size f)) end
Coq < with forest_size [f:forest] : nat :=
Coq < Cases f of (leaf b) => (S O)
Coq < | (cons t f') => (plus (tree_size t) (forest_size f'))
Coq < end.
A generic command Scheme is useful to build automatically various mutual induction principles. It is described in section 7.15.

CoFixpoint ident : term2 := term3.

The CoFixpoint command introduces a method for constructing an infinite object of a coinductive type. For example, the stream containing all natural numbers can be introduced applying the following method to the number O:

Coq < CoFixpoint from : nat->Stream := [n:nat](Seq n (from (S n))).
from is corecursively defined


Oppositely to recursive ones, there is no decreasing argument in a co-recursive definition. To be admissible, a method of construction must provide at least one extra constructor of the infinite object for each iteration. A syntactical guardedness condition is imposed on co-recursive definitions in order to ensure this: each recursive call in the definition must be protected by at least one constructor, and only by constructors. That is the case in the former definition, where the single recursive call of from is guarded by an application of cons. On the contrary, the following recursive function does not satisfy the guardedness condition:

Coq < CoFixpoint filter : (nat->bool)->Stream->Stream :=
Coq < [p:nat->bool]
Coq < [s:Stream]
Coq < if (p (hd s)) then (Seq (hd s) (filter p (tl s)))
Coq < else (filter p (tl s)).


Notice that the definition contains an unguarded recursive call of filter on the else branch of the test.

The elimination of co-recursive definition is done lazily, i.e. the definition is expanded only when it occurs at the head of an application which is the argument of a case expression. Isolate, it is considered as a canonical expression which is completely evaluated. We can test this using the command Eval, which computes the normal forms of a term:
Coq < Eval Simpl in (from O).
     = (from O)
     : Stream

Coq < Eval Simpl in (hd (from O)).
     = O
     : nat

Coq < Eval Simpl in (tl (from O)).
     = (from (S O))
     : Stream


As in the Fixpoint command (cf. section 1.3.4), it is possible to introduce a block of mutually dependent methods. The general syntax for this case is:

CoFixpoint ident1 :term1 := term1'
with
  ...
with identm : termm := termm'

1.3.5 Statement and proofs

A statement claims a goal of which the proof is then interactively done using tactics. More on the proof editing mode, statements and proofs can be found in chapter 6.

Theorem ident : term.

This command binds term to the name ident in the environment, provided that a proof of term is next given.

After a statement, Coq needs a proof.


Variants:
  1. Lemma ident : term.
    Same as Theorem except that this statement is in a section then the name ident will be unknown when the current section (see section 2.5) will be closed. All proofs of persistent objects (such as theorems) referring to ident within the section will be replaced by the proof of ident.
  2. Definition ident : term.
    Allow to define a term of type term using the proof editing mode. It behaves as Theorem except the defined term will be transparent (see 5.2.5, 7.5.6).

Proof . ...Qed .

A proof starts by the keyword Proof. Then Coq enters the proof editing mode until the proof is completed. The proof editing mode essentially contains tactics that are described in chapter 7. Besides tactics, there are commands to manage the proof editing mode. They are described in chapter 6. When the proof is completed it should be validated and put in the environment using the keyword Qed.



Error message:
  1. Clash with previous constant ident



Remarks:
  1. Several statements can be simultaneously opened.
  2. Not only other statements but any vernacular command can be given within the proof editing mode. In this case, the command is understood as if it would have been given before the statements still to be proved.
  3. Proof is recommended but can currently be omitted. On the opposite, Qed is mandatory to validate a proof.



Variants:
  1. Proof . ...Defined .
    Same as Proof . ...Qed . but it is intended to surround a definition built using the proof-editing mode.
  2. Proof . ...Save.
    Same as Proof . ...Qed .
  3. Goal term...Save ident
    Same as Lemma ident: term...Save. This is intended to be used in the interactive mode. Conversely to named lemmas, anonymous goals cannot be nested.


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.0.0.2.html at 8/10/98