Sections¶
Sections are naming scopes that permit creating section-local declarations that can
be used by other declarations in the section. Declarations made
with Variable, Hypothesis, Context,
Let, Let Fixpoint and
Let CoFixpoint (or the plural variants of the first two) within sections
are local to the section.
In proofs done within the section, section-local declarations
are included in the local context of the initial goal of the proof.
They are also accessible in definitions made with the Definition command.
Sections are opened by the Section command, and closed by End.
Sections can be nested.
When a section is closed, its local declarations are no longer available.
Global declarations that refer to them will be adjusted so they're still
usable outside the section as shown in this example.
- Command End ident¶
Closes the section or module named
ident. See Terminating an interactive module or module type definition for a description of its use with modules.After closing the section, the section-local declarations (variables and section-local definitions, see
Variable) are discharged, meaning that they stop being visible and that all global objects defined in the section are generalized with respect to the variables and local definitions they each depended on in the section.- Error There is nothing to end.¶
Note
Most commands, such as the Hint commands,
Notation and option management commands that
appear inside a section are canceled when the section is closed.
- Command Let ident_decl def_body¶
- Command Let Fixpoint fix_definition with fix_definition*¶
- Command Let CoFixpoint cofix_definition with cofix_definition*¶
These are similar to
Definition,FixpointandCoFixpoint, except that the declared constant is local to the current section. When the section is closed, all persistent definitions and theorems within it that depend on the constant will be wrapped with aterm_letwith the same declaration.As for
Definition,FixpointandCoFixpoint, iftermis omitted,typeis required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on therefinetactic. See Entering and exiting proof mode. The proof should be terminated withDefined. UsingQedin Let is deprecated. To get the same effect (hiding the body of the proof), add theclearbodyattribute to the Let.
- Attribute clearbody¶
When used with
Letin a section, clears the body of the definition in the proof context of following proofs. The kernel will still use the body when checking.
- Warning ident is declared opaque but this is not fully respected inside the section and not at all outside the section.¶
Terminating the proof for a
LetwithQedis deprecated. It has the same behavior asclearbodywithDefined.
- Command Context binder+¶
Declare variables in the context of the current section, like
Variable, but also allowing implicit variables, Implicit generalization, and let-binders.Context {A : Type} (a b : A). Context `{EqDec A}. Context (b' := b).
See also
Section Binders. Section Sections and contexts in chapter Typeclasses.
Example: Section-local declarations
- Section s1.
- Variables x y : nat.
- x is declared y is declared
The command Let introduces section-wide Let-in definitions. These definitions
won't persist when the section is closed, and all persistent definitions which
depend on y' will be prefixed with let y' := y in.
- Let y' := y.
- y' is defined
- Definition x' := S x.
- x' is defined
- Definition x'' := x' + y'.
- x'' is defined
- Print x'.
- x' = S x : nat x' uses section variable x.
- Print x''.
- x'' = x' + y' : nat x'' uses section variables x y.
- End s1.
- Print x'.
- x' = fun x : nat => S x : nat -> nat Arguments x' x%nat_scope
- Print x''.
- x'' = fun x y : nat => let y' := y in x' x + y' : nat -> nat -> nat Arguments x'' (x y)%nat_scope
Notice the difference between the value of x' and x'' inside section
s1 and outside.
Typing rules used at the end of a section¶
From the original rules of the type system, one can show the admissibility of rules which change the local context of definition of objects in the global environment. We show here the admissible rules that are used in the discharge mechanism at the end of a section.
Abstraction. One can modify a global declaration by generalizing it over a previously assumed constant \(c\). For doing that, we need to modify the reference to the global declaration in the subsequent global environment and local context by explicitly applying this constant to the constant \(c\).
Below, if \(Γ\) is a context of the form \([y_1 :A_1 ;~…;~y_n :A_n]\), we write \(∀x:U,~\subst{Γ}{c}{x}\) to mean \([y_1 :∀ x:U,~\subst{A_1}{c}{x};~…;~y_n :∀ x:U,~\subst{A_n}{c}{x}]\) and \(\subst{E}{|Γ|}{|Γ|c}\) to mean the parallel substitution \(E\{y_1 /(y_1~c)\}…\{y_n/(y_n~c)\}\).
First abstracting property:
One can similarly modify a global declaration by generalizing it over a previously defined constant \(c\). Below, if \(Γ\) is a context of the form \([y_1 :A_1 ;~…;~y_n :A_n]\), we write \(\subst{Γ}{c}{u}\) to mean \([y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]\).
Second abstracting property:
Pruning the local context. If one abstracts or substitutes constants with the above rules then it may happen that some declared or defined constant does not occur any more in the subsequent global environment and in the local context. One can consequently derive the following property.
- First pruning property:
- \[\frac{% \WF{E;~c:U;~E′}{Γ}% \hspace{3em}% c~\kw{does not occur in}~E′~\kw{and}~Γ% }{% \WF{E;E′}{Γ}% }\]
- Second pruning property:
- \[\frac{% \WF{E;~c:=u:U;~E′}{Γ}% \hspace{3em}% c~\kw{does not occur in}~E′~\kw{and}~Γ% }{% \WF{E;E′}{Γ}% }\]