4.4 Definitions in environments
We now give the rules for manipulating objects in the environment. Because a constant can depend on previously introduced constants, the environment will be an ordered list of declarations. When specifying an inductive definition, several objects will be introduced at the same time. So any object in the environment will define one or more constants.In this presentation we introduce two different sorts of objects in the environment. The first one is ordinary definitions which give a name to a particular well-formed term, the second one is inductive definitions which introduce new inductive objects.
4.4.1 Rules for definitions
Adding a new definition.
The simplest objects in the environment are definitions which can be seen as one possible mechanism for abbreviation.A definition will be represented in the environment as Def(G)(c:=t:T) which means that c is a constant which is valid in the context G whose value is t and type is T.
d-reduction.
If Def(G)(c:=t:T) is in the environment E then in this environment the d-reduction c |>d t is introduced.The rule for adding a new definition is simple:
- Def
-
WF (E; Def (G)(c:=t:T) )[G]
4.4.2 Derived rules
From the original rules of the type system, one can derive new rules which change the context of definition of objects in the 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.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 a variable in a term, one can define the substitution of a term for a constant. One easily extends this substitution to contexts and environments.Substitution Property:
|
Abstraction.
One can modify the 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 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 variable x is available at each stage where c is mentioned.Abstracting property:
|
Pruning the context.
We said the judgment WF(E)[G] means that the defining contexts of constants in E are included in G. If one abstracts or substitutes the constants with the above rules then it may happen that the context G 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 is the same as the one for the last constant. One can consequently derive the following property.Pruning property:
|