1.2 Terms

1.2 Terms

1.2.1 Syntax of terms

Figure 1.1 describes the basic set of terms which form the Calculus of Inductive Constructions (also called Cic). The formal presentation of Cic is given in chapter 4. Extensions of this syntax are given in chapter 2. How to customize the syntax is described in chapter 9.

term ::= ident
  | sort
  | term -> term
  | ( typed_idents ; ... ; typed_idents ) term
  | [ idents ; ... ; idents ] term
  | ( term ... term )
  | [annotation] Cases term of [equation | ... | equation] end
  | Fix ident { fix_body with ... with fix_body }
  | CoFix ident { cofix_body with ... with cofix_body }
     
sort ::= Prop
  | Set
  | Type
     
annotation ::= < term >
     
typed_idents ::= ident , ... , ident : term
idents ::= ident , ... , ident [: term]
     
fix_body ::= ident [ typed_idents ; ... ; typed_idents ]: term := term
cofix_body ::= ident : term := term
     
simple_pattern ::= ident
  | ( ident ... ident )
equation ::= simple_pattern  =>  term


Figure 1.1:Syntax of terms

1.2.2 Identifiers

Identifiers denotes either variables, constants, inductive types or constructors of inductive types. In a simple pattern ( ident ... ident ), the first ident is intended to be a constructor.

1.2.3 Sorts

There are three sorts Set, Prop and Type.
Prop
is the universe of logical propositions. The logical propositions themselves are typing the proofs. We denote propositions by form. This constitutes a semantic subclass of the syntactic class term.
Set
is the universe of program types or specifications. The specifications themselves are typing the programs. We denote specifications by specif. This constitutes a semantic subclass of the syntactic class term.
Type
is the type of Set and Prop.


More on sorts can be found in section 4.1.1.

1.2.4 Types

Coq terms are typed. Coq types are recognized by the same syntactic class as term. We denote by type the semantic subclass of types inside the syntactic class term.

1.2.5 Abstractions

The expression ``[ typed_idents1 ; ... ; typed_identsm ] term'' is equivalent to the expression ``[ typed_idents1 ]( ... ([ typed_identsm ] term ) ...)''. An expression of the form ``[ ident1 , ... , identn : type] term'' is itself equivalent to the expression ``[ ident1 : type]( ... ([ identn : type] term ) ...)''. At the end, the expression ``[ ident : type] term'' denotes the abstraction of the variable ident of type type, over the term term. Going back to the notation ``[ idents1 ; ... ; identsm ] term'', this stands for the successive abstractions of a sequence of sequence of variables.

Remark: The types of variables may be omitted.

1.2.6 Products

Similarly, the expression ``( typed_idents1 ; ... ; typed_identsm ) term'' is equivalent to the expression ``( typed_idents1 )( ... (( typed_identsm ) term ) ...)''. An expression of the form ``( ident1 , ... , identn : type) term'' is itself equivalent to the expression ``( ident1 : type)( ... (( identn : type) term ) ...)''. At the end, the expression ``( ident : type) term'' denotes the product of the variable ident of type type, over the term term. Going back to the notation ``( idents1 ; ... ; identsm ) term'', this stands for the successive products of a sequence of sequence of variables.

1.2.7 Applications

The expression (term0 term1 ... termn) denotes the application of the term term0 to the arguments term1 ... then termn. It is equivalent to ( ... ( term0 term1 ) ... termn ): associativity is to the left.

1.2.8 Definition by cases

The expression [annotation] Cases term0 of pattern1 => term1 | ... | patternn => termn end, denotes a pattern-matching over the term term0 (expected to be of an inductive type). When no equation is given in the Cases expression, the annotation is mandatory.

1.2.9 Recursive functions

The expression Fix identi { ident1 [ bindings1 ] : type1 := term1 with ... with identn [ bindingsn ] : typen := termn } denotes a function defined by well-founded recursion. The expression CoFix identi { ident1 : type1 with ... with identn [ bindingsn ] : typen } denotes a term defined by a guarded recursion.

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