Definitions¶
Letin definitions¶
term_let::=
let name : type? := term in term

let name binder+ : type? := term in term

destructuring_let
let ident := term_{1} in term_{2}
represents the local binding of
the variable ident
to the value term_{1}
in term_{2}
.
let ident binder+ := term_{1} in term_{2}
is an abbreviation
for let ident := fun binder+ => term_{1} in term_{2}
.
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 :> type
The expression term10 : type
is a type cast expression. It enforces
the type of term10
to be type
.
term10 <: type
specifies that the virtual machine will be used
to type check that term10
has type type
(see vm_compute
).
term10 <<: type
specifies that compilation to OCaml will be used
to type check that term10
has type type
(see native_compute
).
term10 :> type
enforces the type of term10
to be
type
without leaving a trace in the produced value.
This is a volatile cast.
Toplevel definitions¶
Definitions extend the global environment by associating 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 deltareduction. A definition is accepted by the system if and only if the defined term is welltyped 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 DefinitionExample ident_decl def_body¶
 def_body
::=
binder* : type? := reduce? term
binder* : typereduce
::=
Eval red_expr inThese commands bind
term
to the nameident
in the global environment, provided thatterm
is welltyped. They can take thelocal
attribute, which makes the definedident
accessible byImport
and its variants only through their fully qualified names. Ifreduce
is present thenident
is bound to the result of the specified computation onterm
.These commands also support the
universes(polymorphic)
,program
(see Program Definition),canonical
,bypass_check(universes)
,bypass_check(guard)
,deprecated
andusing
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 therefine
tactic. In this case, the proof should be terminated withDefined
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 ofterm
is definitionally equal totype
, and registersident
as being of typetype
, and bound to valueterm
.The form
Definition ident binder* : type := term
is equivalent toDefinition ident : forall binder*, type := fun binder* => term
.See also
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
PropertyAfter the statement is asserted, Coq needs a proof. Once a proof of
type
under the assumptions represented bybinder
s is given and validated, the proof is generalized into a proof offorall binder*, type
and the theorem is bound to the nameident
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 coinductive type. It is equivalent toFixpoint
orCoFixpoint
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 coinductive types on which the induction or coinduction has to be done is assumed to be unambiguous and is guessed by the system.Like in a
Fixpoint
orCoFixpoint
definition, the induction hypotheses have to be used on structurally smaller arguments (for aFixpoint
) or be guarded by a constructor (for aCoFixpoint
). 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 commandGuarded
.This command accepts the
bypass_check(universes)
,bypass_check(guard)
,deprecated
, andusing
attributes. 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
Several statements can be simultaneously asserted provided the
Nested Proofs Allowed
flag was turned on.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.
Proofs ended by
Qed
are declared opaque. Their content cannot be unfolded (see Applying conversion rules), thus realizing some form of proofirrelevance. Proofs that end withDefined
can be unfolded.Proof
is recommended but can currently be omitted. On the opposite side,Qed
(orDefined
) is mandatory to validate a proof.One can also use
Admitted
in place ofQed
to turn the current asserted statement into an axiom and exit proof mode.