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

Section mechanism¶

Sections create local contexts which can be shared across multiple definitions.

Example

Sections are opened by the Section command, and closed by End.

Section s1.

Inside a section, local parameters can be introduced using Variable, Hypothesis, or Context (there are also plural variants for the first two).

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
Print x''.: x'' = x' + y' : nat
End s1.
Print x'.: x' = fun x : nat => S x : nat -> nat Arguments x' _%nat_scope
Print x''.: x'' = fun x y : nat => let y' := y in x' x + y' : nat -> nat -> nat Arguments x'' (_ _)%nat_scope

Notice the difference between the value of x' and x'' inside section s1 and outside.

Command Section ident¶: This command is used to open a section named ident. Section names do not need to be unique.

Command End ident¶

This command 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 local declarations (variables and 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, like Hint, Notation, option management, … which 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 commands behave like 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 editing 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 leaving proof editing mode.

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