\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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+ : type|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 , type|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 : type1, type2 denotes the product type (or product) of the variable ident of type type1 over the type type2. If ident is used in type2, then we say the expression is a dependent product, and otherwise a non-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. Non-dependent product is used to denote both propositional implication and function types.

These terms are also useful:

• n : nat is a dependent premise of forall n:nat, n + 0 = n because n appears both in the binder of the forall and in the quantified statement n + 0 = n. Note that if n isn't used in the statement, Coq considers it a non-dependent premise. Similarly, let n := ... in term is a dependent premise only if n is used in term.

• A and B are non-dependent premises (or, often, just "premises") of A -> B -> C because they don't appear in a forall binder. C is the conclusion of the type, which is a second meaning for the term conclusion. (As noted, A -> B is notation for the term forall _ : A, B; the wildcard _ can't be referred to in the quantified statement.)

As for abstractions, forall is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable products.

Function application

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

term1fun term1 denotes applying the function term1fun to term1.

term1fun term1i+ denotes applying term1fun to the arguments term1i. It is equivalent to ( … ( term1fun term11 ) … ) term1n: associativity is to the left.

The @ qualid_annotated term1+ form requires specifying all arguments, including implicit ones. Otherwise, implicit arguments need not be given. See Implicit arguments.

The notations (ident := term) and (natural := term) for arguments are used for making explicit the value of implicit arguments. See Explicit applications.

Assumptions

Assumptions extend the global environment with axioms, parameters, hypotheses or variables. An assumption binds an ident to a type. It is accepted by Coq only if type is a correct type in the global environment before 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 ( natural )?? ( 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 environment. The fact asserted by type (or, equivalently, the existence of an object of this type) is accepted as a postulate. They accept the program and deprecated attributes.

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

:>

If specified, ident_decl is automatically declared as a coercion to the class of its type. See Implicit Coercions.

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