RefMan, ch. 4: Consistent use of the terms local context and global environment.

1 files changed, 85 insertions, 82 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index a5471ac14a..9d79f7cac3 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -238,33 +238,33 @@ is written $\subst{u}{x}{t}$.
 \section[Typed terms]{Typed terms\label{Typed-terms}}
 
 As objects of type theory, terms are subjected to {\em type
-discipline}. The well typing of a term depends on an environment which
-consists in a global environment (see below) and a local context.
+discipline}. The well typing of a term depends on
+a global environment (see below) and a local context.
 
 \paragraph{Local context.}
-A {\em local context} (or shortly context) is an ordered list of
+A {\em local context} is an ordered list of
 declarations of variables. The declaration of some variable $x$ is
-either an assumption, written $x:T$ ($T$ is a type) or a definition,
-written $x:=t:T$.  We use brackets to write contexts. A
+either a local assumption, written $x:T$ ($T$ is a type) or a local definition,
+written $x:=t:T$.  We use brackets to write local contexts. A
 typical example is $[x:T;y:=u:U;z:V]$.  Notice that the variables
-declared in a context must be distinct. If $\Gamma$ declares some $x$,
+declared in a local context must be distinct. If $\Gamma$ declares some $x$,
 we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that
 either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such
 that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some
-$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.  Contexts must be
-themselves {\em well formed}.  For the rest of the chapter, the
-notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context
+$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.
+For the rest of the chapter, the
+notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the local context
 $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
-notation $[]$ denotes the empty context.  \index{Context}
+notation $[]$ denotes the empty local context.  \index{Local context}
 
 % Does not seem to be used further...
 % Si dans l'explication WF(E)[Gamma] concernant les constantes
 % definies ds un contexte
 
-We define the inclusion of two contexts $\Gamma$ and $\Delta$ (written
-as $\Gamma \subset \Delta$) as the property, for all variable $x$,
-type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
-and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.  
+%We define the inclusion of two local contexts $\Gamma$ and $\Delta$ (written
+%as $\Gamma \subset \Delta$) as the property, for all variable $x$,
+%type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
+%and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.
 %We write
 % $|\Delta|$ for the length of the context $\Delta$, that is for the number
 % of declarations (assumptions or definitions) in $\Delta$.
@@ -272,22 +272,20 @@ and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.
 A variable $x$ is said to be free in $\Gamma$ if $\Gamma$ contains a
 declaration $y:T$ such that $x$ is free in $T$.
 
-\paragraph[Environment.]{Environment.\index{Environment}}
-Because we are manipulating global declarations (constants and global
-assumptions), we also need to consider a global environment $E$.
+\paragraph[Global environment.]{Global environment.\index{Global environment}}
+%Because we are manipulating global declarations (global constants and global
+%assumptions), we also need to consider a global environment $E$.
 
-An environment is an ordered list of declarations of global
-names. Declarations are either assumptions or ``standard''
-definitions, that is abbreviations for well-formed terms
-but also definitions of inductive objects. In the latter
-case, an object in the environment will define one or more constants
-(that is types and constructors, see Section~\ref{Cic-inductive-definitions}).
+A {\em global environment} is an ordered list of global declarations.
+Global declarations are either global assumptions or global
+definitions, but also declarations of inductive objects. Inductive objects themselves declares both inductive or coinductive types and constructors
+(see Section~\ref{Cic-inductive-definitions}).
 
-An assumption will be represented in the environment as
+A global assumption will be represented in the global environment as
 \Assum{\Gamma}{c}{T} which means that $c$ is assumed of some type $T$
-well-defined in some context $\Gamma$. An (ordinary) definition will
-be represented in the environment as \Def{\Gamma}{c}{t}{T} which means
-that $c$ is a constant which is valid in some context $\Gamma$ whose
+well-defined in some local context $\Gamma$. A global definition will
+be represented in the global environment as \Def{\Gamma}{c}{t}{T} which means
+that $c$ is a constant which is valid in some local context $\Gamma$ whose
 value is $t$ and type is $T$.
 
 The rules for inductive definitions (see section
@@ -297,23 +295,27 @@ declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is
 declared in $E$, we write $(c : T) \in E$.
 
 \paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}}
-In the following, we assume $E$ is a valid environment w.r.t.
-inductive definitions.  We define simultaneously two
+In the following, we define simultaneously two
 judgments.  The first one \WTEG{t}{T} means the term $t$ is well-typed
-and has type $T$ in the environment $E$ and context $\Gamma$.  The
-second judgment \WFE{\Gamma} means that the environment $E$ is
-well-formed and the context $\Gamma$ is a valid context in this
-environment.  It also means a third property which makes sure that any
-constant in $E$ was defined in an environment which is included in
-$\Gamma$
-\footnote{This requirement could be relaxed if we instead introduced
-  an explicit mechanism for instantiating constants. At the external
-  level, the Coq engine works accordingly to this view that all the
-  definitions in the environment were built in a sub-context of the
-  current context.}.
-
-A term $t$ is well typed in an environment $E$ iff there exists a
-context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
+and has type $T$ in the global environment $E$ and local context $\Gamma$.  The
+second judgment \WFE{\Gamma} means that the global environment $E$ is
+well-formed and the local context $\Gamma$ is a valid local context in this
+global environment.
+% HH: This looks to me complicated. I think it would be better to talk
+% about ``discharge'' as a transformation of global environments,
+% rather than as keeping a local context next to global constants.
+%
+%%  It also means a third property which makes sure that any
+%%constant in $E$ was defined in an environment which is included in
+%%$\Gamma$
+%%\footnote{This requirement could be relaxed if we instead introduced
+%%  an explicit mechanism for instantiating constants. At the external
+%%  level, the Coq engine works accordingly to this view that all the
+%%  definitions in the environment were built in a local sub-context of the
+%%  current local context.}.
+
+A term $t$ is well typed in a global environment $E$ iff there exists a
+local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can
 be derived from the following rules.
 \begin{description}
 \item[W-E] \inference{\WF{[]}{[]}}
@@ -370,7 +372,7 @@ may be used in a conversion rule (see Section~\ref{conv-rules}).
 We want to be able to identify some terms as we can identify the
 application of a function to a given argument with its result. For
 instance the identity function over a given type $T$ can be written
-$\lb x:T\mto x$. In any environment $E$ and context $\Gamma$, we want to identify any object $a$ (of type $T$) with the
+$\lb x:T\mto x$. In any global environment $E$ and local context $\Gamma$, we want to identify any object $a$ (of type $T$) with the
 application $((\lb x:T\mto x)~a)$. We define for this a {\em reduction} (or a
 {\em conversion}) rule we call $\beta$:
 \[ \WTEGRED{((\lb x:T\mto
@@ -387,7 +389,7 @@ refer the interested reader to \cite{Coq85}.
 
 \paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}}
 A specific conversion rule is associated to the inductive objects in
-the environment.  We shall give later on (see Section~\ref{iotared}) the
+the global environment.  We shall give later on (see Section~\ref{iotared}) the
 precise rules but it just says that a destructor applied to an object
 built from a constructor behaves as expected.  This reduction is
 called $\iota$-reduction and is more precisely studied in
@@ -396,7 +398,7 @@ called $\iota$-reduction and is more precisely studied in
 
 \paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}}
 
-We may have defined variables in contexts or constants in the global
+We may have defined variables in local contexts or constants in the global
 environment. It is legal to identify such a reference with its value,
 that is to expand (or unfold) it into its value. This
 reduction is called $\delta$-reduction and shows as follows.
@@ -435,12 +437,12 @@ the type. However, $\eta$ can be used as a conversion rule.
 \paragraph[Convertibility.]{Convertibility.\label{convertibility}
 \index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}}
 
-Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the environment $E$ and context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
+Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the global environment $E$ and local context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$.
 
 We say that two terms $t_1$ and $t_2$ are {\em
   $\beta\iota\delta\zeta\eta$-convertible}, or simply {\em
-  convertible}, or {\em equivalent}, in the environment $E$ and
-context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that
+  convertible}, or {\em equivalent}, in the global environment $E$ and
+local context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that
 $\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u_1}$ and
 $\WTEGRED{t_2}{\triangleright \ldots \triangleright}{u_2}$ and either
 $u_1$ and $u_2$ are identical, or they are convertible up to
@@ -503,10 +505,10 @@ $u_i$ can be reducible.
 Similar notions of head-normal forms involving $\delta$, $\iota$ and $\zeta$
 reductions or any combination of those can also be defined.
 
-\section{Derived rules for environments}
+\section{Derived rules for global environments}
 
 From the original rules of the type system, one can derive new rules
-which change the context of definition of objects in the environment.
+which change the local context of definition of objects in the global environment.
 Because these rules correspond to elementary operations in the \Coq\ 
 engine used in the discharge mechanism at the end of a section, we
 state them explicitly.
@@ -514,9 +516,9 @@ state them explicitly.
 \paragraph{Mechanism of substitution.}
 
 One rule which can be proved valid, is to replace a term $c$ by its
-value in the environment. As we defined the substitution of a term for
+value in the global environment. As we defined the substitution of a term for
 a variable in a term, one can define the substitution of a term for a
-constant. One easily extends this substitution to contexts and
+constant. One easily extends this substitution to local contexts and global
 environments.
 
 \paragraph{Substitution Property:} 
@@ -526,13 +528,13 @@ environments.
 
 \paragraph{Abstraction.}
 
-One can modify the context of definition of a constant $c$ by
+One can modify the local context of definition of a constant $c$ by
 abstracting a constant with respect to the last variable $x$ of its
-defining context. For doing that, we need to check that the constants
+defining local context. For doing that, we need to check that the constants
 appearing in the body of the declaration do not depend on $x$, we need
-also to modify the reference to the constant $c$ in the environment
-and context by explicitly applying this constant to the variable $x$.
-Because of the rules for building environments and terms we know the
+also to modify the reference to the constant $c$ in the global environment
+and local context by explicitly applying this constant to the variable $x$.
+Because of the rules for building global environments and terms we know the
 variable $x$ is available at each stage where $c$ is mentioned.
 
 \paragraph{Abstracting property:} 
@@ -541,13 +543,13 @@ variable $x$ is available at each stage where $c$ is mentioned.
            {\WF{E;\Def{\Gamma}{c}{\lb x:U\mto t}{\forall~x:U,T};
   \subst{F}{c}{(c~x)}}{\subst{\Delta}{c}{(c~x)}}}}
 
-\paragraph{Pruning the context.} 
-We said the judgment \WFE{\Gamma} means that the defining contexts of
+\paragraph{Pruning the local context.}
+We said the judgment \WFE{\Gamma} means that the defining local contexts of
 constants in $E$ are included in $\Gamma$. If one abstracts or
 substitutes the constants with the above rules then it may happen
-that the context $\Gamma$ is now bigger than the one needed for
-defining the constants in $E$. Because defining contexts are growing
-in $E$, the minimum context needed for defining the constants in $E$
+that the local context $\Gamma$ is now bigger than the one needed for
+defining the constants in $E$. Because defining local contexts are growing
+in $E$, the minimum local context needed for defining the constants in $E$
 is the same as the one for the last constant. One can consequently
 derive the following property.
 
@@ -561,8 +563,8 @@ derive the following property.
 A (possibly mutual) inductive definition is specified by giving the
 names and the type of the inductive sets or families to be
 defined and the names and types of the constructors of the inductive
-predicates.  An inductive declaration in the environment can
-consequently be represented with two contexts (one for inductive
+predicates.  An inductive declaration in the global environment can
+consequently be represented with two local contexts (one for inductive
 definitions, one for constructors).
 
 Stating the rules for inductive definitions in their general form
@@ -576,15 +578,15 @@ forests.
 \subsection{Representing an inductive definition}
 \subsubsection{Inductive definitions without parameters}
 As for constants, inductive definitions can be defined in a non-empty
-context. \\
+local context. \\
 We write \NInd{\Gamma}{\Gamma_I}{\Gamma_C} an inductive
-definition valid in a context $\Gamma$, a
-context of definitions $\Gamma_I$ and a context of constructors
+definition valid in a local context $\Gamma$, a
+context of type definitions $\Gamma_I$ and a context of constructors
 $\Gamma_C$.
 \paragraph{Examples.}
 The inductive declaration for the type of natural numbers will be:
 \[\NInd{}{\nat:\Set}{\nO:\nat,\nS:\nat\ra\nat}\]
-In a context with a variable $A:\Set$, the lists of elements in $A$ are
+In a local context with a variable $A:\Set$, the lists of elements in $A$ are
 represented by:
 \[\NInd{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra
   \List}\]
@@ -603,7 +605,7 @@ represented by:
 We have to slightly complicate the representation above in order to handle
 the delicate problem of parameters. 
 Let us explain that on the example of \List. With the above definition,
-the type \List\ can only be used in an environment where we
+the type \List\ can only be used in a global environment where we
 have a variable $A:\Set$. Generally one want to consider lists of
 elements in different types. For constants this is easily done by abstracting
 the value over the parameter. In the case of inductive definitions we
@@ -630,11 +632,11 @@ We say that $q$ is the number of real arguments of the constructor
 $c$. 
 \paragraph{Context of parameters.}
 If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
-$r$ inductive parameters, then there exists a context $\Gamma_P$ of
+$r$ inductive parameters, then there exists a local context $\Gamma_P$ of
 size $r$, such that $\Gamma_P=[p_1:P_1;\ldots;p_r:P_r]$ and 
 if $(t:A) \in \Gamma_I,\Gamma_C$ then $A$ can be written as 
 $\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. 
-We call $\Gamma_P$ the context of parameters of the inductive
+We call $\Gamma_P$ the local context of parameters of the inductive
 definition and use the notation $\forall \Gamma_P,A'$ for the term $A$.
 \paragraph{Remark.}
 If we have a term $t$ in an instance of an
@@ -662,7 +664,7 @@ But the following definition has $0$ parameters:
 %$\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
 %  \ra (\List~A\ra A) \ra (\List~A)}$.}
 \paragraph{Concrete syntax.}
-In the Coq system, the context of parameters is given explicitly
+In the Coq system, the local context of parameters is given explicitly
 after the name of the inductive definitions and is shared between the
 arities and the type of constructors.
 % The vernacular declaration of polymorphic trees and forests will be:\\
@@ -685,7 +687,7 @@ parameters.
 Formally the representation of an inductive declaration
 will be 
 \Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} for an inductive
-definition valid in a context $\Gamma$ with $p$ parameters, a
+definition valid in a local context $\Gamma$ with $p$ parameters, a
 context of definitions $\Gamma_I$ and a context of constructors
 $\Gamma_C$.
 
@@ -763,7 +765,7 @@ Inductive list' (A:Set) : Set :=
 
 
 \subsection{Types of inductive objects}
-We have to give the type of constants in an environment $E$ which
+We have to give the type of constants in a global environment $E$ which
 contains an inductive declaration.
 
 \begin{description}
@@ -881,7 +883,7 @@ We shall now describe the rules allowing the introduction of a new
 inductive definition.
 
 \begin{description}
-\item[W-Ind] Let $E$ be an environment and
+\item[W-Ind] Let $E$ be a global environment and
   $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
   $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall
   \Gamma_P,A_k]$ and $\Gamma_C$ is 
@@ -941,20 +943,21 @@ Inductive exType (P:Type->Prop) : Type
 %a recursive argument and $(x:_P T)C$ if the argument is not recursive.
 
 \paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}}
+\label{Sort-polymorphism-inductive}
 
 From {\Coq} version 8.1, inductive families declared in {\Type} are
 polymorphic over their arguments in {\Type}.
 
 If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity
 obtained from $A$ by replacing its sort with $s$. Especially, if $A$
-is well-typed in some environment and context, then $A_{/s}$ is typable
+is well-typed in some global environment and local context, then $A_{/s}$ is typable
 by typability of all products in the Calculus of Inductive Constructions.
 The following typing rule is added to the theory.
 
 \begin{description}
 \item[Ind-Family] Let $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ be an
   inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$
-  be its context of parameters, $\Gamma_I = [I_1:\forall
+  be its local context of parameters, $\Gamma_I = [I_1:\forall
     \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of
   definitions and $\Gamma_C = [c_1:\forall
     \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of
@@ -1105,7 +1108,7 @@ a strongly normalizing reduction, we cannot accept any sort of
 recursion (even terminating). So the basic idea is to restrict
 ourselves to primitive recursive functions and functionals.
 
-For instance, assuming a parameter $A:\Set$ exists in the context, we
+For instance, assuming a parameter $A:\Set$ exists in the local context, we
 want to build a function \length\ of type $\ListA\ra \nat$ which
 computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$
 and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$.  We want these
@@ -1364,7 +1367,7 @@ constructor have type \Prop. In that case, there is a canonical
 way to interpret the informative extraction on an object in that type,
 such that the elimination on any sort $s$ is legal.  Typical examples are
 the conjunction of non-informative propositions and the equality. 
-If there is an hypothesis $h:a=b$ in the context, it can be used for
+If there is an hypothesis $h:a=b$ in the local context, it can be used for
 rewriting not only in logical propositions but also in any type.
 % In that case, the term \verb!eq_rec! which was defined as an axiom, is
 % now a term of the calculus.
@@ -1438,8 +1441,8 @@ only constructors of $I$.
 
 \paragraph{Example.}
 For \List\ and \Length\ the typing rules for the {\tt match} expression
-are (writing just $t:M$ instead of \WTEG{t}{M}, the environment and
-context being the same in all the judgments).
+are (writing just $t:M$ instead of \WTEG{t}{M}, the global environment and
+local context being the same in all the judgments).
 
 \[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~
       f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))}