\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Functions and assumptions

Binders

open_binders::=name+ : term|binder+name::=_|identbinder::=name|( name+ : type )|( name : type? := term )|implicit_binders|generalizing_binder|( name : type | term )|' pattern0

Various constructions such as fun, forall, fix and cofix bind variables. A binding is represented by an identifier. If the binding variable is not used in the expression, the identifier can be replaced by the symbol _. When the type of a bound variable cannot be synthesized by the system, it can be specified with the notation (ident : type). There is also a notation for a sequence of binding variables sharing the same type: (ident+ : type). A binder can also be any pattern prefixed by a quote, e.g. '(x,y).

Some constructions allow the binding of a variable to value. This is called a “let-binder”. The entry binder of the grammar accepts either an assumption binder as defined above or a let-binder. The notation in the latter case is (ident := term). In a let-binder, only one variable can be introduced at the same time. It is also possible to give the type of the variable as follows: (ident : type := term).

Lists of binders are allowed. In the case of fun and forall, it is intended that at least one binder of the list is an assumption otherwise fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: fun (x y z : A) => t can be shortened in fun x y z : A => t).

Functions (fun) and function types (forall)

term_forall_or_fun::=forall open_binders , term|fun open_binders => term

The expression fun ident : type => term defines the abstraction of the variable ident, of type type, over the term term. It denotes a function of the variable ident that evaluates to the expression term (e.g. fun x : A => x denotes the identity function on type A). The keyword fun can be followed by several binders as given in Section Binders. Functions over several variables are equivalent to an iteration of one-variable functions. For instance the expression fun identi+ : type => term denotes the same function as fun identi : type =>+ term. If a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section Let-in definitions).

The expression forall ident : type, term denotes the product of the variable ident of type type, over the term term. As for abstractions, forall is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable products. Note that term is intended to be a type.

If the variable ident occurs in term, the product is called dependent product. The intention behind a dependent product forall x : A, B is twofold. It denotes either the universal quantification of the variable x of type A in the proposition B or the functional dependent product from A to B (a construction usually written \(\Pi_{x:A}.B\) in set theory).

Non dependent product types have a special notation: A -> B stands for forall _ : A, B. The non dependent product is used both to denote the propositional implication and function types.

Function application

term_application::=term1 arg+|@ qualid_annotated term1+arg::=( ident := term )|term1

termfun term denotes applying the function termfun to term.

termfun termi+ denotes applying termfun to the arguments termi. It is equivalent to ( … ( termfun term1 ) … ) termn: associativity is to the left.

The notation (ident := term) for arguments is used for making explicit the value of implicit arguments (see Section Explicit applications).

Assumptions

Assumptions extend the environment with axioms, parameters, hypotheses or variables. An assumption binds an ident to a type. It is accepted by Coq if and only if this type is a correct type in the environment preexisting the declaration and if ident was not previously defined in the same module. This type is considered to be the type (or specification, or statement) assumed by ident and we say that ident has type type.

Command assumption_token Inline ( num )?? ( assumpt )+​assumpt

assumption_token::=Axiom​Axioms|Conjecture​Conjectures|Parameter​Parameters|Hypothesis​Hypotheses|Variable​Variablesassumpt::=ident_decl+ of_typeident_decl::=ident univ_decl?of_type::=:​:>​:>> type

These commands bind one or more ident(s) to specified type(s) as their specifications in the global context. The fact asserted by the type (or, equivalently, the existence of an object of this type) is accepted as a postulate.

Axiom, Conjecture, Parameter and their plural forms are equivalent. They can take the local attribute, which makes the defined idents accessible by Import and its variants only through their fully qualified names.

Similarly, Hypothesis, Variable and their plural forms are equivalent. Outside of a section, these are equivalent to Local Parameter. Inside a section, the idents defined are only accessible within the section. When the current section is closed, the ident(s) become undefined and every object depending on them will be explicitly parameterized (i.e., the variables are discharged). See Section Section mechanism.

The Inline clause is only relevant inside functors. See Module.

Example: Simple assumptions

Parameter X Y : Set.

X is declared Y is declared

Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop).

R is declared S is declared

Axiom R_S_inv : forall x y, R x y <-> S y x.

R_S_inv is declared

Error ident already exists.

Warning ident is declared as a local axiom

Warning generated when using Variable or its equivalent instead of Local Parameter or its equivalent.

Note

We advise using the commands Axiom, Conjecture and Hypothesis (and their plural forms) for logical postulates (i.e. when the assertion type is of sort Prop), and to use the commands Parameter and Variable (and their plural forms) in other cases (corresponding to the declaration of an abstract object of the given type).