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.

1.2.3 Sorts

There are three sorts Set, Prop and Type.

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 ``[ ident : type] term'' denotes the abstraction of the variable ident of type type, over the term term.

One can abstract several variables successively: the notation [ ident1 , ... , identn : type] term stands for [ ident1 : type]( ... ([ identn : type] term ) ...) and the notation [ typed_idents1 ; ... ; typed_identsm ] term is a shorthand for [ typed_idents1 ]( ... ([ typed_identsm ] term )
[ ident1 , ... , identn : type] term.

Remark: The types of variables may be omitted in an abstraction when they can be synthetized by the system.

1.2.6 Products

The expression ``( ident : type) term'' denotes the product of the variable ident of type type, over the term term.

Similarly, the expression ( ident1 , ... , identn : type) term is equivalent to ( ident1 : type)( ... (( identn : type) term ) ...) and the expression ( typed_idents1 ; ... ; typed_identsm ) term is a equivalent to ( typed_idents1 )( ... (( typed_identsm ) term ) ...)

1.2.7 Applications

(term0 term1) denotes the application of term term0 to term1.

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 case analysis

In a simple pattern ( ident ... ident ), the first ident is intended to be a constructor.

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).

The annotation is the resulting type of the whole Cases expression. Most of the time, when this type is the same as the types of all the termi, the annotation is not needed2. The annotation has to be given when the resulting type of the whole Cases depends on the actual term0 matched.

1.2.9 Recursive functions

The expression Fix identi { ident1 [ bindings1 ] : type1 := term1 with ... with identn [ bindingsn ] : typen := termn } denotes the ith component of a block of functions defined by mutual well-founded recursion.

The expression CoFix identi { ident1 : type1 with ... with identn [ bindingsn ] : typen } denotes the ith component of a block of terms defined by a mutual guarded recursion.