let ident := term in term’
denotes the local binding of
term to the variable
term’. There is a syntactic sugar for let-in
definition of functions:
let ident binder+ := term in term’
let ident := fun binder+ => term in term’.
Definitions extend the 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.
DefinitionExample ident_decl def_body¶
These commands bind
termto the name
identin the environment, provided that
termis well-typed. They can take the
localattribute, which makes the defined
Importand its variants only through their fully qualified names. If
reduceis present then
identis bound to the result of the specified computation on
typeis required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the
refinetactic. In this case, the proof should be terminated with
Definedin order to define a constant for which the computational behavior is relevant. See Entering and leaving proof editing mode.
Assertions and proofs¶
An assertion states a proposition (or a type) of which the proof (or an inhabitant of the type) is interactively built using tactics. The interactive proof mode is described in Chapter Proof handling and the tactics in Chapter Tactics. The basic assertion command is:
thm_token ident_decl binder* : type with ident_decl binder* : type*¶
After the statement is asserted, Coq needs a proof. Once a proof of
typeunder the assumptions represented by
binders is given and validated, the proof is generalized into a proof of
forall binder*, typeand the theorem is bound to the name
identin the environment.
Forms using the
withclause 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
CoFixpointbut 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
CoFixpointdefinition, 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 environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command
ident already exists.¶
The name you provided is already defined. You have then to choose another name.
Proofs start with the keyword
Proof. Then Coq enters the proof editing mode
until the proof is completed. In proof editing mode, the user primarily enters
tactics, which are described in chapter Tactics. The user may also enter
commands to manage the proof editing mode. They are described in Chapter
When the proof is complete, use the
Qed command so the kernel verifies
the proof and adds it to the environment.
Several statements can be simultaneously asserted provided the
Nested Proofs Allowedflag was turned on.
Not only other assertions but any vernacular 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
Qedare 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