\[\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}\]

Definitions

Let-in definitions

term_let::=let name : type? := term in term|let name binder+ : type? := term in term|destructuring_let

let ident := term1 in term2 represents the local binding of the variable ident to the value term1 in term2.

let ident binder+ := term1 in term2 is an abbreviation for let ident := fun binder+ => term1 in term2.

See also

Extensions of the let ... in ... syntax are described in Irrefutable patterns: the destructuring let variants.

Type cast

term_cast::=term10 <: type|term10 <<: type|term10 : type|term10 :>

The expression term10 : type is a type cast expression. It enforces the type of term10 to be type.

term10 <: type locally sets up the virtual machine for checking that term10 has type type.

term10 <<: type uses native compilation for checking that term10 has type type.

Top-level definitions

Definitions extend the global environment with associations of names to terms. A definition can be seen as a way to give a meaning to a name or as a way to abbreviate a term. In any case, the name can later be replaced at any time by its definition.

The operation of unfolding a name into its definition is called \(\delta\)-conversion (see Section δ-reduction). A definition is accepted by the system if and only if the defined term is well-typed in the current context of the definition and if the name is not already used. The name defined by the definition is called a constant and the term it refers to is its body. A definition has a type which is the type of its body.

A formal presentation of constants and environments is given in Section Typing rules.

Command Definition​Example ident_decl def_body

def_body::=binder* : type? := reduce? term|binder* : typereduce::=Eval red_expr in

These commands bind term to the name ident in the global environment, provided that term is well-typed. They can take the local attribute, which makes the defined ident accessible by Import and its variants only through their fully qualified names. If reduce is present then ident is bound to the result of the specified computation on term.

These commands also support the universes(polymorphic), program (see Program Definition), canonical, bypass_check(universes), bypass_check(guard), and using attributes.

If term is omitted, type is required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on the refine tactic. In this case, the proof should be terminated with Defined in order to define a constant for which the computational behavior is relevant. See Entering and exiting proof mode.

The form Definition ident : type := term checks that the type of term is definitionally equal to type, and registers ident as being of type type, and bound to value term.

The form Definition ident binder* : type := term is equivalent to Definition ident : forall binder*, type := fun binder* => term.

See also

Opaque, Transparent, unfold.

Error ident already exists.

Error The term term has type type while it is expected to have type type'.

Assertions and proofs

An assertion states a proposition (or a type) for which the proof (or an inhabitant of the type) is interactively built using tactics. Assertions cause Coq to enter proof mode (see Proof mode). Common tactics are described in the Basic proof writing chapter. The basic assertion command is:

Command thm_token ident_decl binder* : type with ident_decl binder* : type*

thm_token::=Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property

After the statement is asserted, Coq needs a proof. Once a proof of type under the assumptions represented by binders is given and validated, the proof is generalized into a proof of forall binder*, type and the theorem is bound to the name ident in the global environment.

These commands accept the program attribute. See Program Lemma.

Forms using the with clause are useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent statements in some mutual co-inductive type. It is equivalent to Fixpoint or CoFixpoint but using tactics to build the proof of the statements (or the body of the specification, depending on the point of view). The inductive or co-inductive types on which the induction or coinduction has to be done is assumed to be non ambiguous and is guessed by the system.

Like in a Fixpoint or CoFixpoint definition, the induction hypotheses have to be used on structurally smaller arguments (for a Fixpoint) or be guarded by a constructor (for a CoFixpoint). The verification that recursive proof arguments are correct is done only at the time of registering the lemma in the global environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command Guarded.

This command accepts the bypass_check(universes), bypass_check(guard), and using attributes.

Error The term term has type type which should be Set, Prop or Type.

Error ident already exists.

The name you provided is already defined. You have then to choose another name.

Error Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.

You are asserting a new statement when you're already in proof mode. This feature, called nested proofs, is disabled by default. To activate it, turn the Nested Proofs Allowed flag on.

Proofs start with the keyword Proof. Then Coq enters the proof mode until the proof is completed. In proof mode, the user primarily enters tactics (see Basic proof writing). The user may also enter commands to manage the proof mode (see Proof mode).

When the proof is complete, use the Qed command so the kernel verifies the proof and adds it to the global environment.

Note

1. Several statements can be simultaneously asserted provided the Nested Proofs Allowed flag was turned on.

2. Not only other assertions but any command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the statements still to be proved. Nonetheless, this practice is discouraged and may stop working in future versions.

3. Proofs ended by Qed are declared opaque. Their content cannot be unfolded (see Performing computations), thus realizing some form of proof-irrelevance. To be able to unfold a proof, the proof should be ended by Defined.

4. Proof is recommended but can currently be omitted. On the opposite side, Qed (or Defined) is mandatory to validate a proof.

5. One can also use Admitted in place of Qed to turn the current asserted statement into an axiom and exit proof mode.