$\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}$

# 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 (or the plural variants of the first two) and definitions made with Let, Let Fixpoint and Let CoFixpoint 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.

## Using sections¶

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 Section ident

Opens the section named ident. Section names do not need to be unique.

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.
Error Last block to end has name ident.

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. In some cases, this behaviour can be tuned with locality attributes. See this table.

Command
Command Let Fixpoint fix_definition with fix_definition*
Command Let CoFixpoint cofix_definition with cofix_definition*

These are similar to Definition, Fixpoint and CoFixpoint, 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 a term_let with the same declaration.

As for Definition, Fixpoint and CoFixpoint, 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. See Entering and exiting proof mode.

Attribute clearbody

When used with Let in a section, clears the body of the definition in the proof context of following proofs. The kernel will still use the body when checking.

Note

Terminating the proof for a Let with Qed produces an opaque side definition. Let foo : T. Proof. tactics. Qed. is equivalent to

Lemma foo_subproof : T. Proof. tactics. Qed. #[clearbody] Let foo := foo_subproof.
Command Context

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

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.

## Summary of locality attributes in a section¶

This table sums up the effect of locality attributes on the scope of vernacular commands in a Section, when outside the Section where they were entered. In the following table:

A similar table for Module can be found here.

Command

no attribute

local

export

global

available 1

module 1

Ltac

local

not available

Ltac2

local

not available

Notation (abbreviation)

local

not available

Notation

local

not available

Tactic Notation

local

not available

Ltac2 Notation

local

not available

Coercion

global

not available

module 2

Canonical Structure

global

not available

module 2

Hints (and Instance)

local

not available

Set or Unset a flag

available 3

not available

module 3

module 3

1(1,2)

For Definition, Lemma, ... the default visibility is to be available outside the section and available with a short name when the current Module is imported (with Import or cmd:Export) outside the current Module. The local attribute make the corresponding identifiers available in the current Module but only with a fully qualified name outside the current Module.

2(1,2)

For Coercion and Canonical Structure, the global visibility, which is the default, makes them available outside the section, in the current Module, and outside the current Module when it is imported (with Import or cmd:Export).

3(1,2,3)

For Set and Unset, the export and global attributes both make the command's effects persist outside the current section, in the current Module. It will also persist outside the current Module with the global attribute, or with the export attribute, when the Module is imported (with Import or cmd:Export). The default behaviour (no attribute) is to make the setting persist outside the section in the current Module, but not outside the current Module`.

## 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:

$\frac{\WF{E;~c:U;~E′;~c′:=t:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} {\subst{Γ}{c′}{(c′~c)}}}$
$\frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}}$
$\frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ \subst{E″}{|Γ_I ;Γ_C |}{|Γ_I ;Γ_C | c}} {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}}$

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:

$\frac{\WF{E;~c:=u:U;~E′;~c′:=t:T;~E″}{Γ}} {\WF{E;~c:=u:U;~E′;~c′:=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};~E″}{Γ}}$
$\frac{\WF{E;~c:=u:U;~E′;~c′:T;~E″}{Γ}} {\WF{E;~c:=u:U;~E′;~c′:\subst{T}{c}{u};~E″}{Γ}}$
$\frac{\WF{E;~c:=u:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} {\WF{E;~c:=u:U;~E′;~\ind{p}{\subst{Γ_I}{c}{u}}{\subst{Γ_C}{c}{u}};~E″}{Γ}}$

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′}{Γ}% }$