Skip to main content
PRL Project

The Book

Implementing Mathematics with The Nuprl Proof Development System

See title page for important information about this reference

next up previous contents
Next: The Metalanguage Up: Index Previous: System Description   Contents

The Rules


Semantics

The Nuprl semantics is a variation on that given by Martin-Löf for his type theory [Martin-Löf 82]. There are three stages in the semantic specification: the computation system, the type system and the so-called judgement forms. Here is how we shall proceed. We shall specify a computation system consisting of terms, divided into canonical and noncanonical, and a procedure for evaluating terms which for a given term $t$ returns at most one canonical term, called the value of $t$. In Nuprl whether a term is canonical depends only on the outermost form of the term, and there are terms which have no value. We shall write $t \mbox{$\leftarrow$}{} s$ to mean that $s$ has value $t$.

Next we shall specify a system of types. A type is a term $T$ (of the computation system) with which is associated a transitive, symmetric relation, $t = s \in T$, which respects evaluation in $t$ and $s$; that is, if $T$ is a type and $t'\mbox{$\leftarrow$}{} t$ and $s'\mbox{$\leftarrow$}{} s$, then $t'=s'\in T$ if and only if $t = s \in T$. We shall sometimes say ``$T$ type'' to mean that $T$ is a type. We say $t$ is a member of $T$, or $t \in T$, if $t=t\in T$. Note that $t = s \in T$ is an equivalence relation (in $t$ and $s$) when restricted to members of $T$.8.1Actually, $t = s \in T$ is a three-place relation on terms which respects evaluation in all three places. We also use a transitive, symmetric relation on terms, $T = S$, called type equality, which $t = s \in T$ respects in $T$; that is, if $T = S$ then $t = s \in T$ if and only if $t=s\in S$. The relation $T = S$ respects evaluation in $T$ and $S$, and $T$ is a type if and only if $T=T$. The restriction of $T = S$ to types is an equivalence relation.

For our purposes, then, a type system for a given computation system consists of a two-place relation $T = S$ and a three-place relation $t = s \in T$ on terms such that

$T = S$ is transitive and symmetric;
$T = S$ if and only if $\exists T'.\,\, T'\mbox{$\leftarrow$}{} T$ & $T'=S$;
$t = s \in T$ is transitive and symmetric in $t$ and $s$;
$t = s \in T$ if and only if $\exists t'.\,\, t'\mbox{$\leftarrow$}{} t$ & $t'=s\in T$;
$T=T$ if $t = s \in T$;
$t = s \in T$ if $T = S$ & $t=s\in S$.
We define ``$T$ type'' and ``$t \in T$'' by
$T$ type if and only if $T=T$;
$t \in T$ if and only if $t=t\in T$.

Finally, so-called judgements will be explained. This requires consideration of terms with free variables because substitution of closed terms for free variables is central to judgements as presented here. In the description of semantics given so far ``term'' has meant a closed term, i.e., a term with no free variables. There is only one form of judgement in Nuprl, $x_1$:$T_1$,$\dots$,$x_n$:$T_n$ » $S$ [ext $s$], which in the case that $n$ is $0$ means $s\in S$. The explanation of the cases in which $n$ is not $0$ must wait.

Substitution

For the purposes of giving the procedure for evaluation and explaining the semantics of judgements, we would only need to consider substitution of closed terms for free variables and hence would not need to consider simultaneous substitution or capture. However, for the purpose of specifying inference rules later we shall want to have simultaneous substitution of terms with free variables for free variables. The result of such a substitution is indicated thus:

\begin{displaymath}t[t_1,\dots, t_n/x_1,\dots,x_n] \end{displaymath}

where $0\le n$, $x_1,\dots,x_n$ are variables (not necessarily distinct) and $t_1,\dots,t_n$ are terms. It is handy to permit multiple occurrences of the same variable among the targets for replacements, all but the last of which are ignored. $t[t_1,\dots, t_n/x_1,\dots,x_n]$ is the result of replacing each free occurrence of $x_i$ in $t$ by $s_i$ for $1\le i\le n$, where $s_i$ is $t_j$ with $j$ the greatest $k$ such that $x_i$ is $x_k$.

The Computation System

Figure 8.1 shows the terms of Nuprl. Variables are terms, although since they are not closed they are not executable. Variables are written as identifiers, with distinct identifiers indicating distinct variables.8.2Nonnegative integers are written in standard decimal notation. There is no way to write a negative integer in Nuprl; the best one can do is to write a noncanonical term, such as -5, which evaluates to a negative integer. Atom constants are written as character strings enclosed in double quotes, with distinct strings indicating distinct atom constants.


Term Table

Term Table

Figure 8.1: Terms

The free occurrences of a variable $x$ in a term $t$ are the occurrences of $x$ which either are $t$ or are free in the immediate subterms of $t$, excepting those occurrences of $x$ which become bound in $t$. In figure 8.1 the variables written below the terms indicate which variable occurrences become bound; some examples are explained below.

  • In $x$:$A$#$B$ the $x$ in front of the colon becomes bound and any free occurrences of $x$ in $B$ become bound. The free occurrences of variables in $x$:$A$#$B$ are all the free occurrences of variables in $A$ and all the free occurrences of variables in $B$ except for $x$.
  • In <$a$,$b$> no variable occurrences become bound; hence, the free occurrences of variables in <$a$,$b$> are those of $a$ and those of $b$.
  • In spread($s$;$x$,$y$.$t$) the $x$ and $y$ in front of the dot and any free occurrences of $x$ or $y$ in $t$ become bound.

Parentheses may be used freely around terms and often must be used to resolve ambiguous notations correctly. Figure 8.2 gives the relative precedences and associativities of Nuprl operators.

Figure 8.2: Operator Precedence
\begin{figure}\hrule {} \vspace{2ex} \begin{center} \begin{tabular}{ll} \multico... ...Higher Precedence} \end{tabular}\end{center} \vspace{2pt} \hrule {} \end{figure}

The closed terms above the dotted line in figure 8.1 are the canonical terms, while the closed terms below it are the noncanonical terms. Note that carets appear below most of the noncanonical forms; these indicate the principal argument places of those terms. This notion is used in the evaluation procedure below. Certain terms are designated as redices, and each redex has a unique contractum. Figure 8.3 shows all redices and their contracta.

Figure 8.3: Redices and Contracta
\begin{figure}\hrule {} \begin{center} \begin{tabular}{lp{2.5in}} {\bf Redex} & ... ...range over atom constants. \end{tabular} }\vspace{2pt} \hrule {} \end{figure}

The evaluation procedure is as follows. Given a (closed) term $t$,

If $t$ is canonical then the procedure terminates with result $t$.
Otherwise, execute the evaluation procedure on each principal argument of $t$, and if each has a value, replace the principal arguments of $t$ by their respective values; call this term $s$.
If $s$ is a redex then the procedure for evaluating $t$ is continued by evaluating the contractum of $s$.
If $s$ is not a redex then the procedure is terminated without result; $t$ has no value.

The Type System

For convenience we shall extend the relation $t \mbox{$\leftarrow$}{} s$ to possibly open terms. If $s$ or $t$ contain free variables then $t \mbox{$\leftarrow$}{} s$ does not hold; otherwise, it is true if and only if $s$ has value $t$. Also, define $t\mbox{$\leftarrow$}{}s,r$ to mean that $t \mbox{$\leftarrow$}{} s$ and $t\mbox{$\leftarrow$}{}r$.

Recall that the members of a type are its canonical members and the terms which have those members as values. The integers are the canonical members of the type int. The denumerably many atom constants are the canonical members of the type atom. The type void is empty. The type $A$|$B$ is like a disjoint union of types $A$ and $B$. The terms inl($a$) and inr($b$) are canonical members so long as $a\in A$ and $b\in B$; $a$ and $b$ need not be canonical. (The operator names inl and inr are mnemonic for ``inject left'' and ``inject right''.) The canonical members of $x$:$A$#$B$ are the terms <$a$,$b$> with $a\in A$ and $b\in B[a/x]$, $a$ and $b$ not necessarily canonical. Note that the type from which the second component is selected may depend on the value of the first component. The canonical members of the type $A$ list represent lists of members of $A$. The empty list is represented by nil. A nonempty list with head $a$ is represented by $a$.$b$, where $b$ evaluates to a member of the type $A$ list and represents the tail.

A term of the form $t$($a$) is called an application of $t$ to $a$, and $a$ is called its argument. The members of $x$:$A$->$B$ are called functions, and each canonical member is a lambda term, \$x$.$b$, whose application to any $a\in A$ is a member of $B[a/x]$. It is required that applications to equal members of type $A$ be equal. Clearly, $t$($a$)$\in B[a/x]$ if $t\in$ $x$:$A$->$B$ and $a\in A$.

The significance of some constructors derives from the representation of propositions as types. A proposition represented by a type is true if and only if the type is inhabited. The type $a$<$b$ is inhabited if and only if the value of $a$ is less than the value of $b$. The type ($a$=$b$ in $A$) is inhabited if and only if $a=b\in A$. Obviously, the type ($a$=$a$ in $A$) is inhabited if and only if $a\in A$, so ``$a$ in $A$'' has been adopted as a notation for this type. The members of {$x$:$A$|$B$} are the members $a$ of $A$ such that $B[a/x]$ is inhabited. Types of the form {$x$:$A$|$B$} are called set types. The set constructor provides a device for specifying subtypes; for example, {x:int|0<x} has just the positive integers as canonical members.

The members of $x$,$y$:$A$//$B$ are the members of $A$. The difference between this type and $A$ is equality. $a=a'\in$ $x$,$y$:$A$//$B$ if and only if $a$ and $a'$ are members of $A$ and $B[a,a'/x,y]$ is inhabited. Types of this form are called quotient types. The relation $\exists b. b\in B[a,a'/x,y]$ is an equivalence relation over $A$ in $a$ and $a'$; this is built into the criteria for $x$,$y$:$A$//$B$ being a type.

Now consider equality on the other types already discussed. (Recall that terms are equal in a given type if and only if they evaluate to canonical terms equal in that type. Recall also that $a=a'\in A$ is an equivalence relation in $a$ and $a'$ when restricted to members of $A$.) Members of int are equal (in int) if and only if they have the same value. The same goes for type atom. Canonical members of $A$|$B$ ($x$:$A$#$B$, $A$ list) are equal if and only if they have the same outermost operator and their corresponding immediate subterms are equal (in the corresponding types). Members of $x$:$A$->$B$ are equal if and only if their applications to any member $a$ of $A$ are equal in $B[a/x]$. We say equality on $x$:$A$->$B$ is extensional. The types $a$<$b$ and ($a$=$b$ in $A$) have at most one canonical member, axiom. Equality in {$x$:$A$|$B$} is just the restriction of equality in $A$ to {$x$:$A$|$B$}.

We must now consider the notion of functionality. A term $B$ is type-functional in $x:A$ if and only if $A$ is a type and $B[a/x]=B[a'/x]$ for any $a$ and $a'$ such that $a=a'\in A$. A term $b$ is $B$-functional in $x:A$ if and only if $B$ is type-functional in $x:A$ and $b[a/x]=b[a'/x]\in B[a/x]$ for any $a$ and $a'$ such that $a=a'\in A$. There are restrictions on type formation involving type-functionality. These can be seen in the type formation clauses of section 8.2 for $x$:$A$#$B$, $x$:$A$->$B$, and {$x$:$A$|$B$}. In each of these $B$ must be type-functional in $x$:$A$.8.3We may now say that the members of $x$:$A$->$B$ are the lambda terms \$x$.$b$ such that $b$ is $B$-functional in $x:A$. In the type $x$,$y$:$A$//$B$, that $B$ must be type-functional in both $x$,$y$:$A$ follows from the fact that $x$:$A$->$y$:$A$->$B$->$B$ must be a type. There are also constraints on the typehood of $x$,$y$:$A$//$B$ which guarantee that the relation $\exists b. b\in B[a,a'/x,y]$ is an equivalence relation on members of $A$ and respects equality in $A$. It should be noted that if $A$ is empty then every term is type-functional in its free variables over $A$. Hence, $x$:void#3 is a type (with no members) even though 3 is not a type.

Equal types have the same membership and equality, but not conversely. Type equality in Nuprl is not extensional; that is, it is not enough for type equality that two types should have the same membership and equality. In Nuprl equal canonical types always have the same outermost type constructor.8.4The relations that must hold between the respective immediate subterms are seen easily enough in the definition of type equality given in section 8.2 on page [*]. It should be noted that in contrast to equality between types of the form $x$:$A$#$B$ or $x$:$A$->$B$, much less is required for {$x$:$A$|$B$}$=${$x$:$A$|$B'$} than type-functional equality of $B$ and $B'$ in $x$:$A$. All that is required is the existence of functions which for each $a\in A$ evaluate to functions mapping back and forth between $B[a/x]$ and $B'[a/x]$. Equality between quotient types is defined similarly. If $x$ does not occur free in $B$ then $A$#$B$$=$$x$:$A$#$B$, $A$->$B$$=$$x$:$A$->$B$, and {$A$|$B$}$=${$x$:$A$|$B$}; if $x$ and $y$ do not occur free in $B$ then $A$//$B$$=$$x$,$y$:$A$//$B$. As a result there is no need for clauses in the type system description giving the criteria for $t=t'\in$ $A$#$B$ and the others explicitly.

Now consider the so-called universes, $U_k$ ($k$ positive). The members of $U_k$ are types. The universes are cumulative; that is, if $j$ is less than $k$ then membership and equality in $U_j$ are just restrictions of membership and equality in $U_k$. Universe $U_k$ is closed under all the type-forming operations except formation of $U_i$ for $i$ greater than or equal to $k$. Equality (hence membership) in $U_k$ is similar to type equality as defined previously except that equality (membership) in $U_k$ is required wherever type equality (typehood) was formerly required, and although all universes are types, only those U$i$ such that $i$ is less than $k$ are in $U_k$. Equality in $U_k$ is the restriction of type equality to members of $U_k$.

So far the only noncanonical form explicitly mentioned in connection with the type system is application. We shall elaborate here on a couple of forms, and it should then be easy to see how to treat the others. The spread form is used for computational analysis of pairs. The pair of components is spread apart so that the components can be used separately.

spread($e$;$x$,$y$.$t$)$\in T[e/z]$ if
\( e\in\mbox{\tt$x$:$A$\char93 $B$} \)
& $T$ is type functional in $z$:($x$:$A$#$B$)
& $\forall a,b. t[a,b/x,y]\in T[$<$a$,$b$>$/z]$
if $a\in A$ and $b\in B[a/x]$

Since \( e\in\mbox{\tt$x$:$A$\char93 $B$},\) then for some $a$ and $b$ \( \mbox{\tt <$a$,$b$>} \mbox{$\leftarrow$}{} e\) where $a\in A$, and $b\in B[a/x]$. Hence \( \mbox{\tt spread($e$;$x$,$y$.$t$)} \) and \( t[a,b/x,y] \) have the same value, so it is enough that \( t[a,b/x,y]\in T[e/z]. \) But from our hypotheses it follows that \( t[a,b/x,y]\in T[\mbox{\tt <$a$,$b$>}/z], \) so it is enough that \( T[e/z]=T[\mbox{\tt <$a$,$b$>}/z]. \) Now \( e=\mbox{\tt <$a$,$b$>}\in \mbox{\tt$x$:$A$\char93 $B$} \) since $e\in$ $x$:$A$#$B$ and equality respects evaluation; therefore \( T[e/z]=T[\mbox{\tt <$a$,$b$>}/z] \) in light of $T$'s functionality in $z$:($x$:$A$#$B$).8.5

The list induction form allows one to perform inductive analysis of lists. list_ind($e$;$s$;$x$,$y$.$t$) is a function (in $e$) which halts on all members of $A$ list. It is the function (in $e$) defined by primitive recursion, where $s$ is the result for the base case of $e=$nil (in $A$ list) and $t$ shows how to build the value for $e=$$x$.$y$ (in $A$ list) from $x$, $y$ and the value of the function being defined on $y$, this value being passed through $u$ during evaluation.
\( \mbox{\tt list\_ind($e$;$s$;$x$,$y$,$u$.$t$)}\in T[e/z] \) if
$e\in$ $A$ list
& $T$ is type functional in $z$:($A$ list)
& $s\in T[$nil$/z]$
& \( \forall a,b,c. t[a,b,c/x,y,u]\in T[\mbox{\tt$a$.$b$}/z] \)
if $a\in A$ & $b\in \mbox{\tt$A$ list}$ & $c\in T[b/z].$

Let us prove this by induction on the length of the list represented by $e$, all other variables universally quantified. Suppose ${\tt nil}\mbox{$\leftarrow$}{}e$. By definition we know that list_ind($e$;$s$;$x$,$y$,$u$.$t$) and $s$ have the same value, so it is enough for the base case that $s\in T[e/z]$; this is true since $T$ is functional in $z:$$A$ list, ${\tt nil}=e\in A\;{\tt list}$, and $s\in T[{\tt nil}/z]$. Now suppose that for some $a$ and $b$, $a$.$b$ $\mbox{$\leftarrow$}{}e$ , $a\in A$ , and $b\in A\;{\tt list}$. Now

\begin{displaymath}{\tt list\_ind(}e;s;x,y,u.t{\tt )}\end{displaymath}

and

\begin{displaymath}t[a,b,\mbox{{\tt list\_ind(}b;s;x,y,u.t{\tt )}}/\mbox{x,y,u}\end{displaymath}

have the same value, so it is enough that the substitution into $t$ is in $T[e/z]$. $b\in A\;{\tt list}$ and $b$ represents a shorter list than $e$; therefore, by inductive hypothesis

\begin{displaymath}\mbox{\tt list\_ind($b$;$s$;$x$,$y$,$u$.$t$)}\in T[b/z]. \end{displaymath}

It follows that the substitution into $t$ is in $T[\mbox{\tt$a$.$b$}/z]$, so it is enough that $T[\mbox{\tt$a$.$b$}/z]=T[e/z]$; this holds because of $T$'s functionality and the equality of $a$.$b$ and $e$ (in $A$ list).

The decide form is used to discern a left from a right injection, and to permit computation on the injected term. The ind form is used to define functions recursively on integers.8.6The reader is referred to chapter 2 or to the exposition of the rules for further elaboration of the use of noncanonical forms.

Judgements

The significance of the so-called judgements lies in the fact that they constitute the claims of a Nuprl proof. They are the units of assertion; they are the objects of inference. The judgements of Nuprl have the form

\begin{displaymath}\mbox{\tt$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ » $S$ [ext $s$]} \end{displaymath}

where $x_1,\dots,x_n$ are distinct variables and $T_1,\dots,T_n,S,s$ are terms ($n$ may be $0$), every free variable of $T_i$ is one of $x_1,\dots,x_{i-1}$, and every free variable of $S$ or of $s$ is one of $x_1,\dots,x_n$. The list \( \mbox{\tt$x_1$:$T_1$,\dots,$x_n$:$T_n$} \) is called the hypothesis list or assumption list, each $x_i$:$T_i$ is called a declaration (of $x_i$), each $T_i$ is called a hypothesis or assumption, $S$ is called the consequent or conclusion, $s$ the extract term (the reason will be seen later), and the whole thing is called a sequent.

Before explaining the conditions which make a Nuprl sequent true we shall define a relation $H @ l$, where $H$ is a hypothesis list and $l$ is a list of terms, and we shall define what it is for a sequent to be true at a list of terms.

$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ $@$ $t_1,\dots,t_n$ if and only if
\(\forall j < n. t_{j+1} \in T_{j+1}[t_1,\dots,t_j/x_1,\dots,x_j]\)
& \( \forall t_1',\dots,t_j'.\,\, T_{j+1}[t_1,\dots,t_j/x_1,\dots,x_j]=\\ * \hspace*{1em}\hspace*{4em}\hspace*{4em} T_{j+1}[t_1',\dots,t_j'/x_1,\dots,x_j] \)
if \( \forall i < j. t_{i+1}=t_{i+1}'\in T_{i+1}[t_1,\dots,t_i/x_1,\dots,x_i] \)

We can also express this relation by saying that every $t_i$ is a member of

\begin{displaymath}T_i[t_1,\dots,t_{i-1}/x_1,\dots,x_{i-1}] \end{displaymath}

and every $T_i$ is type-functional in $x_1:\hat{T}_1,\dots,x_{i-1}:\hat{T}_{i-1}$, where $\hat{T}_j$ means the set type

\begin{displaymath} \{ x_j:T_j[t_1,\dots,t_{j-1}/x_1,\dots,x_{j-1}] \vert x_j=t_j \: {\tt in } \: T_j[t_1,\dots,t_{j-1}/x_1,\dots,x_{j-1}] \} . \end{displaymath}

The sequent

\( \mbox{\tt$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ » $S$ [ext $s$]} \)
is true at $t_1,\dots,t_n$ if and only if
\( \forall t_1',\dots,t_n'. \) ( \(S[t_1,\dots,t_n/x_1,\dots,x_n]=S[t_1',\dots,t_n'/x_1,\dots,x_n] \)
& \( s[t_1,\dots,t_n/x_1,\dots,x_n]=\)
\(s[t_1',\dots,t_n'/x_1,\dots,x_n]\in S[t_1,\dots,t_n/x_1,\dots,x_n] \) )
if $x_1$:$T_1$,$\dots$,$x_n$:$T_n$ $@$ $t_1,\dots,t_n$
& \( \forall i < n. t_{i+1}=t_{i+1}'\in T_{i+1}[t_1,\dots,t_i/x_1,\dots,x_i] \)

Equivalently, we can say that $s$ is $S$-functional in $x_1:\hat{T}_1,\dots,x_n:\hat{T}_n$ if
$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ $@$ $t_1,\dots,t_n$. The sequent

\( \mbox{\tt$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ » $S$ [ext $s$]} \) is true if and only if
\(\forall t_1,\dots,t_n. \mbox{\tt$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ » $S$ [ext $s$]} \) is true at $t_1,\dots,t_n$

The connection between functionality and the truth of sequents lies in the fact that $S$ is type-functional (or $s$ is $S$-functional) in $x:T$ if and only if $T$ is a type and for each member $t$ of $T$, $S$ is type-functional ($s$ is $S$-functional) in $x:${$x$:$T$| $x$=$t$ in $T$}. Therefore, $s$ is $S$-functional in $x:T$ if and only if $T$ is a type and the sequent $x$:$T$ » $S$ [ext $s$] is true.8.7

It is not always necessary to declare a variable with every hypothesis in a hypothesis list. If a declared variable does not occur free in the conclusion, extract term or any hypothesis, then the variable (and the colon following it) may be omitted.

In Nuprl it is not possible for the user to enter a complete sequent directly; the extract term must be omitted. In fact, a sequent is never displayed with its extract term. The system has been designed so that upon completion of a proof, the system automatically provides, or extracts, the extract term. This is because in what is anticipated to be the standard mode of use, the user tries to prove that a certain type is inhabited without regard to the identity of any member. One expects that in this mode the user thinks of the type (that is to be shown inhabited) as a proposition, and that it is merely the truth of this proposition that the user wants to show. When one does wish to show explicitly that $a=b\in A$ or that $a\in A$, one instead shows the type ($a$ = $b$ in $A$) or the type ($a$ in $A$) to be inhabited.8.8

Also, the system can often extract a term from an incomplete proof when the extraction is independent of the extract terms of any unproven claims within the proof body. Of course, such unproven claims may still contribute to the truth of the proof's main claim. For example, it is possible to provide an incomplete proof of the untrue sequent » 1<1 [ext axiom], the extract term axiom being provided automatically.

Although the term extracted from a proof of a sequent is not displayed in the sequent, the term is accessible by other means through the name assigned to the proof in the user's library. It should be noted that in the current system proofs named in the user's library cannot be proofs of sequents with hypotheses.

The Type System in Detail

This section may be skipped on the first reading, as the informal description of the type system given in section 8.1 should meet the needs of most readers.

This section consists of two parts. First, we give the formal definition of Nuprl's type system by means of a recursive definition of the necessary predicates. Then, for ease of understanding and reference, from the definition we extract criteria for typehood and membership. Those who do read this section may benefit by reading the latter part first.


Formal Definition of Equality

What follows is a recursive definition of four predicates-- $T$ type, $t \in T$, $T = S$ and $t = s \in T$--on possibly open terms. When restricted to closed terms these are just the predicates which constitute the Nuprl type system.8.9 In the clauses below,

$T,T',A,A',B,B',a,a',b,b',e,e',t,t',f,g,h$ range over possibly open terms,

$x,x',y,y',u,u',v,w$ range over variables;

$k,j$ range over positive integers;

$m,n$ range over integers;

$i$ ranges over atom constants.
$T$ type iff $T=T$
$t \in T$ iff $t=t\in T$
$T=T'$ iff void $\mbox{$\leftarrow$}{}T,T'$ or atom $\mbox{$\leftarrow$}{}T,T'$ or int $\mbox{$\leftarrow$}{}T,T'$
or $\exists A,A',a,a',b,b'. $($a$=$b$ in $A$) $\mbox{$\leftarrow$}{}T$ & ($a'$=$b'$ in $A'$) $\mbox{$\leftarrow$}{}T'$
& $A=A'$ & $a=a'\in A$ & $b=b'\in A$
or $\exists a,a',b,b'. $($a$<$b$) $\mbox{$\leftarrow$}{}T$ & ($a'$<$b'$) $\mbox{$\leftarrow$}{}T'$ & $a=a'\in $int & $b=b'\in $int
or $\exists A,A'. $$A$ list $\mbox{$\leftarrow$}{}T$ & $A'$ list $\mbox{$\leftarrow$}{}T'$ & $A=A'$
or $\exists A,A',B,B'. $$A$|$B$ $\mbox{$\leftarrow$}{}T$ & $A'$|$B'$ $\mbox{$\leftarrow$}{}T'$ & $A=A'$ & $B=B'$
or $\exists A,A',x,x',B,B'.\,\, \\ * \hspace*{3em}\hspace*{4em} $( $x$:$A$#$B$ $\mbox{$\leftarrow$}{}T$ or $A$#$B$ $\mbox{$\leftarrow$}{}T$ )
& ( $x'$:$A'$#$B'$ $\mbox{$\leftarrow$}{}T'$ or $A'$#$B'$ $\mbox{$\leftarrow$}{}T'$ )
& $A=A'$ & $\forall a,a'. B[a/x]=B'[a'/x']$ if $a=a'\in A$
or $\exists A,A',x,x',B,B'.\,\, \\ * \hspace*{3em}\hspace*{4em} $( $x$:$A$->$B$ $\mbox{$\leftarrow$}{}T$ or $A$->$B$ $\mbox{$\leftarrow$}{}T$ )
& ( $x'$:$A'$->$B'$ $\mbox{$\leftarrow$}{}T'$ or $A'$->$B'$ $\mbox{$\leftarrow$}{}T'$ )
& $A=A'$ & $\forall a,a'. B[a/x]=B'[a'/x']$ if $a=a'\in A$
or $\exists A,A',x,x',B,B',e,e',u. $
( {$x$:$A$|$B$} $\mbox{$\leftarrow$}{}T$ or {$A$|$B$} $\mbox{$\leftarrow$}{}T$ )
& ( {$x'$:$A'$|$B'$} $\mbox{$\leftarrow$}{}T'$ or {$A'$|$B'$} $\mbox{$\leftarrow$}{}T'$ )
& $A=A'$ & $u$ occurs in neither $B$ nor $B'$
& $e\in$ $u$:$A$->$B[u/x]$->$B'[u/x']$
& $e'\in$ $u$:$A$->$B'[u/x']$->$B[u/x]$
or $\exists A,A',x,x',y,y',B,B',e,e',f,g,h,u,v,w. $
( $x$,$y$:$A$//$B$ $\mbox{$\leftarrow$}{}T$ or $A$//$B$ $\mbox{$\leftarrow$}{}T$ )
& ( $x'$,$y'$:$A'$//$B'$ $\mbox{$\leftarrow$}{}T'$ or $A'$//$B'$ $\mbox{$\leftarrow$}{}T'$ )
& $A=A'$
& $u,v,w$ are distinct and occur in neither $B$ nor $B'$
& $e\in$ $u$:$A$->$v$:$A$->$B[u,v/x,y]$->$B'[u,v/x',y']$
& $e'\in$ $u$:$A$->$v$:$A$->$B'[u,v/x',y']$->$B[u,v/x,y]$
& $f\in$ $u$:$A$->$B[u,u/x,y]$
& $g\in$ $u$:$A$->$v$:$A$->$B[u,v/x,y]$->$B[v,u/x,y]$
& $h\in$ $u$:$A$->$v$:$A$->$w$:$A$->$B[u,v/x,y]$->$B[v,w/x,y]$->
$B[u,w/x,y]$
or $\exists k. $U$k$ $\mbox{$\leftarrow$}{}T,T'$
$t=t'\in T$ if $T=T'$ & $t=t'\in T'$
not $t\in$ void
$t=t'\in$ atom iff $\exists i.\,\, i\mbox{$\leftarrow$}{}t,t'$
$t=t'\in$ int iff $\exists n.\,\, n\mbox{$\leftarrow$}{}t,t'$
$t\in$ ($a$=$b$ in $A$) iff axiom $\mbox{$\leftarrow$}{}t$ & $a=b\in A$
$t\in$ $a$<$b$ iff axiom $\mbox{$\leftarrow$}{}t$ & $\exists m,n.\,\, m\mbox{$\leftarrow$}{}a$ & $n\mbox{$\leftarrow$}{}b$ & $m$ is less than $n$
$t=t'\in$ $A$ list iff $A$ list type
& nil $\mbox{$\leftarrow$}{}t,t'$ or $\exists a,a',b,b'. $($a$.$b$) $\mbox{$\leftarrow$}{}t$ & ($a'$.$b'$) $\mbox{$\leftarrow$}{}t'$
& $a=a'\in A$ & $b=b'\in$ $A$ list
$t=t'\in$ $A$|$B$ iff $A$|$B$ type
& ( $\exists a,a'. $inl($a$) $\mbox{$\leftarrow$}{}t$ & inl($a'$) $\mbox{$\leftarrow$}{}t'$ & $a=a'\in A$ )
or $\exists b,b'. $inr($b$) $\mbox{$\leftarrow$}{}t$ & inr($b'$) $\mbox{$\leftarrow$}{}t'$ & $b=b'\in B$
$t=t'\in$ $x$:$A$#$B$ iff $x$:$A$#$B$ type
& $\exists a,a',b,b'. $<$a$,$b$> $\mbox{$\leftarrow$}{}t$ & <$a'$,$b'$> $\mbox{$\leftarrow$}{}t'$
& $a=a'\in A$ & $b=b'\in B[a/x]$
$t=t'\in$ $x$:$A$->$B$ iff $x$:$A$->$B$ type
& $\exists u,u',b,b'. $\$u$.$b$ $\mbox{$\leftarrow$}{}t$ & \$u'$.$b'$ $\mbox{$\leftarrow$}{}t'$
& $\forall a,a'. b[a/u]=b'[a'/u']\in B[a/x]$
if $a=a'\in A$
$t=t'\in$ {$x$:$A$|$B$} iff {$x$:$A$|$B$} type & $t=t'\in A$ & $\exists b. b\in B[t/x]$
$t=t'\in$ $x$,$y$:$A$//$B$ iff $x$,$y$:$A$//$B$ type & $t\in A$ & $t'\in A$
& $\exists b. b\in B[t,t'/x,y]$
$T=T'\in$ U$k$ iff void $\mbox{$\leftarrow$}{}T,T'$ or atom $\mbox{$\leftarrow$}{}T,T'$ or int $\mbox{$\leftarrow$}{}T,T'$
or $\exists A,A',a,a',b,b'. $($a$=$b$ in $A$) $\mbox{$\leftarrow$}{}T$ & ($a'$=$b'$ in $A'$) $\mbox{$\leftarrow$}{}T'$
& $A=A'\in$ U$k$ & $a=a'\in A$ & $b=b'\in A$
or $\exists a,a',b,b'. $($a$<$b$) $\mbox{$\leftarrow$}{}T$ & ($a'$<$b'$) $\mbox{$\leftarrow$}{}T'$
& $a=a'\in$ int & $b=b'\in$ int
or $\exists A,A'. $$A$ list $\mbox{$\leftarrow$}{}T$ & $A'$ list $\mbox{$\leftarrow$}{}T'$ & $A=A'\in$ U$k$
or $\exists A,A',B,B'. $$A$|$B$ $\mbox{$\leftarrow$}{}T$ & $A'$|$B'$ $\mbox{$\leftarrow$}{}T'$
& $A=A'\in$ U$k$ & $B=B'\in$ U$k$
or $\exists A,A',x,x',B,B'.\,\, \\ * \hspace*{3em}\hspace*{4em} $( $x$:$A$#$B$ $\mbox{$\leftarrow$}{}T$ or $A$#$B$ $\mbox{$\leftarrow$}{}T$ )
& ( $x'$:$A'$#$B'$ $\mbox{$\leftarrow$}{}T'$ or $A'$#$B'$ $\mbox{$\leftarrow$}{}T'$ )
& $A=A'\in$ U$k$
& $\forall a,a'. B[a/x]=B'[a'/x']\in$ U$k$ if $a=a'\in A$
or $\exists A,A',x,x',B,B'.\,\, \\ * \hspace*{3em}\hspace*{4em} $( $x$:$A$->$B$ $\mbox{$\leftarrow$}{}T$ or $A$->$B$ $\mbox{$\leftarrow$}{}T$ )
& ( $x'$:$A'$->$B'$ $\mbox{$\leftarrow$}{}T'$ or $A'$->$B'$ $\mbox{$\leftarrow$}{}T'$ )
& $A=A'\in$ U$k$
& $\forall a,a'. B[a/x]=B'[a'/x']\in$ U$k$ if $a=a'\in A$
or $\exists A,A',x,x',B,B',e,e',u. $
( {$x$:$A$|$B$} $\mbox{$\leftarrow$}{}T$ or {$A$|$B$} $\mbox{$\leftarrow$}{}T$ )
& ( {$x'$:$A'$|$B'$} $\mbox{$\leftarrow$}{}T'$ or {$A'$|$B'$} $\mbox{$\leftarrow$}{}T'$ )
& $A=A'\in$ U$k$
& $\forall a. B[a/x]\in$ U$k$ if $a\in A$
& $\forall a. B'[a/x']\in$ U$k$ if $a\in A$
& $u$ occurs in neither $B$ nor $B'$
& $e\in$ $u$:$A$->$B[u/x]$->$B'[u/x']$
& $e'\in$ $u$:$A$->$B'[u/x']$->$B[u/x]$
or $\exists A,A',x,x',y,y',B,B',e,e',f,g,h,u,v,w. $
( $x$,$y$:$A$//$B$ $\mbox{$\leftarrow$}{}T$ or $A$//$B$ $\mbox{$\leftarrow$}{}T$ )
& ( $x'$,$y'$:$A'$//$B'$ $\mbox{$\leftarrow$}{}T'$ or $A'$//$B'$ $\mbox{$\leftarrow$}{}T'$ )
& $A=A'\in$ U$k$
& $\forall a,b. B[a,b/x,y]\in$ U$k$ if $a\in A$ & $b\in A$
& $\forall a,b. B'[a,b/x',y']\in$ U$k$ if $a\in A$ & $b\in A$
& $u,v,w$ are distinct and occur in neither $B$ nor $B'$
& $e\in$ $u$:$A$->$v$:$A$->$B[u,v/x,y]$->$B'[u,v/x',y']$
& $e'\in$ $u$:$A$->$v$:$A$->$B'[u,v/x',y']$->$B[u,v/x,y]$
& $f\in$ $u$:$A$->$B[u,u/x,y]$
& $g\in$ $u$:$A$->$v$:$A$->$B[u,v/x,y]$->$B[v,u/x,y]$
& $h\in$ $u$:$A$->$v$:$A$->$w$:$A$->$B[u,v/x,y]$->$B[v,w/x,y]$->
$B[u,w/x,y]$
or $\exists j. $U$j$ $\mbox{$\leftarrow$}{}T,T'$ & $j$ is less than $k$

Typehood and Membership

What follows is not a definition but a body of facts easily derived from the definition above.

$T$ type iff void $\mbox{$\leftarrow$}{}T$ or atom $\mbox{$\leftarrow$}{}T$ or int $\mbox{$\leftarrow$}{}T$
or $\exists A,a,b. $($a$=$b$ in $A$) $\mbox{$\leftarrow$}{}T$ & $a\in A$ & $b\in A$
or $\exists a,b. $($a$<$b$) $\mbox{$\leftarrow$}{}T$ & $a\in$ int & $b\in$ int
or $\exists A. $$A$ list $\mbox{$\leftarrow$}{}T$ & $A$ type
or $\exists A,B. $$A$|$B$ $\mbox{$\leftarrow$}{}T$ & $A$ type & $B$ type
or $\exists A,x,B. $( $x$:$A$#$B$ $\mbox{$\leftarrow$}{}T$ or $A$#$B$ $\mbox{$\leftarrow$}{}T$ )
& $A$ type & $\forall a,a'. B[a/x]=B[a'/x]$ if $a=a'\in A$
or $\exists A,x,B. $( $x$:$A$->$B$ $\mbox{$\leftarrow$}{}T$ or $A$->$B$ $\mbox{$\leftarrow$}{}T$ )
& $A$ type & $\forall a,a'. B[a/x]=B[a'/x]$ if $a=a'\in A$
or $\exists A,x,B. $( {$x$:$A$|$B$} $\mbox{$\leftarrow$}{}T$ or {$A$|$B$} $\mbox{$\leftarrow$}{}T$ )
& $A$ type & $\forall a,a'. B[a/x]=B[a'/x]$ if $a=a'\in A$
or $\exists A,x,y,B,f,g,h,u,v,w. $
( $x$,$y$:$A$//$B$ $\mbox{$\leftarrow$}{}T$ or $A$//$B$ $\mbox{$\leftarrow$}{}T$ )
& $A$ type
& $u,v,w$ are distinct and don't occur in $B$
& $f\in$ $u$:$A$->$B[u,u/x,y]$
& $g\in$ $u$:$A$->$v$:$A$->$B[u,v/x,y]$->$B[v,u/x,y]$
& $h\in$ $u$:$A$->$v$:$A$->$w$:$A$->$B[u,v/x,y]$->$B[v,w/x,y]$->
$B[u,w/x,y]$
or $\exists k. $U$k$ $\mbox{$\leftarrow$}{}T$
$t \in T$ if $T=T'$ & $t\in T'$
not $t\in$ void
$t\in$ atom iff $\exists i.\,\, i\mbox{$\leftarrow$}{}t$
$t\in$ int iff $\exists n.\,\, n\mbox{$\leftarrow$}{}t$
$t\in$ ($a$=$b$ in $A$) iff axiom $\mbox{$\leftarrow$}{}t$ & $a=b\in A$
$t\in$ $a$<$b$ iff axiom $\mbox{$\leftarrow$}{}t$ & $\exists m,n.\,\, m\mbox{$\leftarrow$}{}a$ & $n\mbox{$\leftarrow$}{}b$ & $m$ is less than $n$
$t\in$ $A$ list iff $A$ list type
& nil $\mbox{$\leftarrow$}{}t$ or $\exists a,b. $($a$.$b$) $\mbox{$\leftarrow$}{}t$ & $a\in A$ & $b\in$ $A$ list
$t\in$ $A$|$B$ iff $A$|$B$ type
& ( $\exists a. $inl($a$) $\mbox{$\leftarrow$}{}t$ & $a\in A$ ) or $\exists b. $inr($b$) $\mbox{$\leftarrow$}{}t$ & $b\in B$
$t\in$ $x$:$A$#$B$ iff $x$:$A$#$B$ type & $\exists a,b. $<$a$,$b$> $\mbox{$\leftarrow$}{}t$ & $a\in A$ & $b\in B[a/x]$
$t\in$ $x$:$A$->$B$ iff $x$:$A$->$B$ type
& $\exists u,b. $\$u$.$b$ $\mbox{$\leftarrow$}{}t$
& $\forall a,a'. b[a/u]=b[a'/u]\in B[a/x]$
if $a=a'\in A$
$t\in$ {$x$:$A$|$B$} iff {$x$:$A$|$B$} type & $t\in A$ & $\exists b. b\in B[t/x]$
$t\in$ $x$,$y$:$A$//$B$ iff $x$,$y$:$A$//$B$ type & $t\in A$
$T\in$ U$k$ iff void $\mbox{$\leftarrow$}{}T$ or atom $\mbox{$\leftarrow$}{}T$ or int $\mbox{$\leftarrow$}{}T$
or $\exists A,a,b. $($a$=$b$ in $A$) $\mbox{$\leftarrow$}{}T$ & $A\in$ U$k$ & $a\in A$ & $b\in A$
or $\exists a,b. $($a$<$b$) $\mbox{$\leftarrow$}{}T$ & $a\in$ int & $b\in$ int
or $\exists A. $$A$ list $\mbox{$\leftarrow$}{}T$ & $A\in$ U$k$
or $\exists A,B. $$A$|$B$ $\mbox{$\leftarrow$}{}T$ & $A\in$ U$k$ & $B\in$ U$k$
or $\exists A,x,B. $( $x$:$A$#$B$ $\mbox{$\leftarrow$}{}T$ or $A$#$B$ $\mbox{$\leftarrow$}{}T$ )
& $A\in$ U$k$ & $\forall a,a'. B[a/x]=B[a'/x]\in$ U$k$ if $a=a'\in A$
or $\exists A,x,B. $( $x$:$A$->$B$ $\mbox{$\leftarrow$}{}T$ or $A$->$B$ $\mbox{$\leftarrow$}{}T$ )
& $A\in$ U$k$ & $\forall a,a'. B[a/x]=B[a'/x]\in$ U$k$ if $a=a'\in A$
or $\exists A,x,B. $( {$x$:$A$|$B$} $\mbox{$\leftarrow$}{}T$ or {$A$|$B$} $\mbox{$\leftarrow$}{}T$ )
& $A\in$ U$k$ & $\forall a,a'. B[a/x]=B[a'/x]\in$ U$k$ if $a=a'\in A$
or $\exists A,x,y,B,f,g,h,u,v,w. $
( $x$,$y$:$A$//$B$ $\mbox{$\leftarrow$}{}T$ or $A$//$B$ $\mbox{$\leftarrow$}{}T$ )
& $A\in$ U$k$
& $\forall a,a',b,b'. B[a,b/x,y]=B[a',b'/x,y]\in$ U$k$
if $a=a'\in A$ & $b=b'\in A$
& $u,v,w$ are distinct and don't occur in $B$
& $f\in$ $u$:$A$->$B[u,u/x,y]$
& $g\in$ $u$:$A$->$v$:$A$->$B[u,v/x,y]$->$B[v,u/x,y]$
& $h\in$ $u$:$A$->$v$:$A$->$w$:$A$->$B[u,v/x,y]$->$B[v,w/x,y]$->
$B[u,w/x,y]$
or $\exists j. $U$j$ $\mbox{$\leftarrow$}{}T$ & $j$ is less than $k$

The Rules

The Nuprl system has been designed to accommodate the top-down construction of proofs by refinement. In this style one proves a judgement (i.e., a goal) by applying a refinement rule, thereby obtaining a set of judgements called subgoals, and then proving each of the subgoals. The mechanics of using the proof-editing system were discussed in chapter 7. In this section we will describe the refinement rules themselves. First we give some general comments regarding the rules and then proceed to give a description of each rule.

The Form of a Rule

To accommodate the top-down style of the Nuprl system the rules of the logic are presented in the following refinement style. $H$ » $T$ ext $t$ by $rule$
$H_1$ » $T_1$ ext $t_1$
                 $\left.\vdots\right.$
$H_k$ » $T_k$ ext $t_k$
The goal is shown at the top, and each subgoal is shown indented underneath. The rules are defined so that if every subgoal is true then one can show the truth of the goal, where the truth of a judgement is to be understood as defined in section 8.1. If there are no subgoals ($k=0$) then the truth of the goal is axiomatic.

One of the features of the proof editor is that the extraction terms are not displayed and indeed are not immediately available. The idea is that one can judge a term $T$ to be a type and $T$ to be inhabited without explicitly presenting the inhabiting object. When one is viewing $T$ as a proposition this is convenient, as a proposition is true if it is inhabited. If $T$ is being viewed as a specification this allows one to implicitly build a program which is guaranteed to be correct for the specification. The extraction term for a goal is built as a function of the extraction terms of the subgoals and thus in general cannot be built until each of the subgoals have been proved. If one has a specific term, $t$, in mind as the inhabiting object and wants it displayed, one can use the explicit intro rule and then show that the type $t$ in $T$ is inhabited. The rules have the property that each subgoal can be constructed from the information in the rule and from the goal, exclusive of the extraction term. As a result some of the more complicated rules require certain terms as parameters.

Implicit in showing a judgement to be true is showing that the conclusion of the judgement is in fact a type. We cannot directly judge a term to be a type; rather, we show that it inhabits a universe. An examination of the semantic definition will reveal that this is sufficient for our purposes. Due to the rich type structure of the system it is not possible in general to decide algorithmically if a given term denotes an element of a universe, so this is something which will require proof. The logic has been arranged so the proof that the conclusion of a goal is a type can be conducted simultaneously with the proof that the type is inhabited. In many cases this causes no great overhead, but some rules have subgoals whose only purpose is to establish that the goal is a type, that is, that it is well-formed. These subgoals all have the form $H$ » $T$ in ${\tt U}{i}$ and are referred to as well-formedness subgoals.

Organization of the Rules

The rules for reasoning about each type and objects of the type will be presented in separate sections. Recall from above that for each judgement of the form $H$ » $T$ ext $t$ where the inhabiting object $t$ is left implicit, there is a corresponding explicit judgement $H$ » $t$ in $T$ ext axiom. As the content of these judgements is essentially the same, the rules for reasoning about them will be presented together. In the preceding chapters, the rules have been classified mainly as introduction or elimination rules, where the introduction rules break down the form of the conclusion of a goal, and the elimination rules use a hypothesis. This is too coarse a classification for the purposes of this section, as the large majority of the rules are introduction rules. Here we will use different criteria for classifying the rules which will hopefully be more illuminating. For each type we will have the following categories of rules:
  • Formation
    These rules give the conditions under which a canonical type may be judged to inhabit a universe, thus verifying that it is indeed a type.
  • Canonical
    These rules give the conditions under which a canonical object (implicitly or explicitly presented) may be judged to inhabit a canonical type. Note that the formation rules are all actually canonical rules, but it is convenient to separate them.
  • Noncanonical
    These rules give the conditions under which a noncanonical object may be judged to inhabit a type. The elimination rules all fall in this category, as the extract term for an elimination rule is a noncanonical term.
  • Equality
    These rules give the conditions under which objects having the same outer form may be judged to be equal. Recall that the rules are being presented in implicit/explicit pairs, $H$ » $T$ ext $t$ and $H$ » $t$ in $T$. The explicit judgement $H$ » $t$ in $T$ is simply the reflexive instance of the general equality judgement $H$ » $t$ = $t'$ in $T$, and in most cases the rule for the general form is an obvious generalization of the rule for the reflexive form, and thus will be omitted. As the rules for the reflexive judgement are given in one of the other categories, there will be no equality rules presented for some types.
  • Computation
    These rules allow one to make judgements of equalities resulting from computation.

Rules such as the sequence, hypothesis and lemma rules which are not associated with one particular type are grouped together under the heading "miscellaneous".

Specifying a Rule

In the context of a particular goal a rule is specified by giving a name and, possibly, certain parameters. As there are a large number of rules it would be unfortunate to have to remember a unique name for each one. Instead, there are small number of generic names, and the proof editor infers the specific rule desired from the form of the goal. In fact, for the rules dealing with specific types or objects of specific types, there are only the names intro, elim and reduce. The intro rules are those which break down the conclusion of the goal, and the elim rules are those which use a hypothesis. Accordingly, the first parameter of any elim rule is the declared variable or number of the hypothesis to be used. The reduce rules are the computation rules. The first parameter of a reduce rule is a number that specifies which term of the equality is to be reduced. Among the parameters of some rules are keyword parameters which have the following form:
  • new $x_1,\cdots,x_n$
    This parameter is used to give new names for hypotheses in the subgoals. In most cases the defaults, which are derived from subterms of the conclusion of the goal, suffice. For technical reasons the same variable can be declared at most once in a hypothesis list, so if a default name is already declared a new name will have to be given. Whenever this parameter is used it must be the case that the names given are all distinct and do not occur in the hypothesis list of the goal.
  • using $T$, over $z.T$
    These parameters are used when judging the equality of noncanonical forms in types dependent on the principal argument of the noncanonical form. The using parameter specifies the type of the principal argument of the noncanonical form. The value should be a canonical type which is appropriate for the particular noncanonical form. The over parameter specifies the dependence of the type over which the equality is being judged on the principal argument of the form. Each occurrence of $z$ in $T$ indicates such a dependency. The proof editor always checks that the term obtained by substituting the principal argument for $z$ in $T$ is $\alpha$-convertible to the type of the equality judgement.
  • at $\mbox{${\tt U}{i}$}$
    The value of this parameter is the universe level at which any type judgements in the subgoals are to be made. The default is $\mbox{${\tt U}{1}$}$.

Optional Parameters and Defaults

Each rule will be presented in its most general form. However, some of the parameters of a rule may be optional, in which case they will be enclosed by square brackets ([]). If a new hypothesis in a subgoal depends on an optional parameter, and in a particular instance of the rule the optional parameter is not given, that new hypothesis will not be added. Such a dependence is usually in the form of a hypothesis specifically referring to an optional new name. The over parameter discussed above is almost always optional. If it is not given, it is assumed that the type of the equality has no dependence on the principal argument of the noncanonical form.

The issue of default values for variable names arises when the main term of a goal's conclusion contains binding variables. In general, the default values are taken to be those binding variables. For example, the rule for explicitly showing a product to be in a universe is



$H$ » $x$:$A$#$B$ in ${\tt U}{i}$ by intro [new y]
» $A$ in ${\tt U}{i}$
$y$:$A$ » $B$ in ${\tt U}{i}$
The rule is presented as if a new name is given, but the default is to use $x$. All the dependent types follow this general pattern.

For judging the equality of terms containing binding variables the binding variables of the first term are in general the default values for the ``appropriate'' new hypotheses. Consider the rule for showing that a spread term is in a type:



$H$ » spread($e$;$x,y.t$) in $T$[$e$/$z$]
by intro [over $z.T$] using $w$:$A$#$B$ [new $u,v$]
$H$ » $e$ in $w$:$A$#$B$
$H$,$u$:$A$,$v$:$B$[$u$/$w$] » $t$[$u,v$/$x,y$] in $T$[<$u$,$v$>/$z$]
Here the new variables default to $x,y$. If no new names are given and $x$ and $y$ don't appear in $H$, then the second subgoal will be




$H$,$x$:$A$,$y$:$B$ » $t$ in $T$[<$x$,$y$>/$z$]
Again this is the general pattern for rules of this type.

Hidden Assumptions

For certain rules, we need to be able to control the free variables occuring in the extract term. The mechanism used to achieve this is that of hidden hypotheses. A hypothesis is hidden when it is displayed enclosed in square brackets. At the moment the only place where such hypotheses are added is in a subgoal of the set elim rule. The intended meaning of a hypothesis being hidden is that the name of the hypothesis cannot appear free in the extracted term; that is, that it cannot be used computationally. Accordingly, a hidden hypothesis cannot be the object of an elim or hyp rule. For the rules for which the extract term is the trivial term axiom, the extract term contains no free variable references and so all restrictions on the use of hidden hypotheses can be removed. The editor will remove the brackets from any hidden hypotheses in displaying a goal of this form.

Shortcuts in the Presentation

With the exception of one of the direct computation rules, each of the rules has the property that the list of hypotheses in a subgoal is an extension of the hypothesis list of the goal. To highlight the new hypotheses and to save space, we will show only the new hypotheses in the subgoals. Also, we will not explicitly display trivial extraction terms, that is, extraction terms which are just axiom.

ATOM

formation

1.$H$ » ${\tt U}{i}$ ext atom by intro atom

2.$H$ » atom in ${\tt U}{i}$ by intro

canonical

3.$H$ » atom ext "$\cdots$" by intro "$\cdots$"

4.$H$ » "$\cdots$" in atom by intro

where `$\cdots$' is any sequence of prl characters.



5.$H$ » atom_eq($a$;$b$;$t$;$t'$) in $T$ by intro
» $a$ in atom
» $b$ in atom
$a$=$b$ in atom » $t$ in $T$
($a$=$b$ in atom)->void » $t'$ in $T$

computation

6a.$H$ » atom_eq($a$;$a$;$t$;$t'$)=$t''$ in $T$ by reduce 1
» $t$=$t''$ in $T$
where $a$ is a canonical token term.

6b.$H$ » atom_eq($a$;$b$;$t$;$t'$)=$t''$ in $T$ by reduce 1
» $t'$=$t''$ in $T$

where $a$ and $b$ are different canonical token terms.

VOID

formation

1.$H$ » ${\tt U}{i}$ ext void by intro void

2.$H$ » void in ${\tt U}{i}$ by intro

noncanonical

3.$H$,$z$:void » $T$ ext any($z$) by elim $z$

4.$H$ » any($e$) in $T$ by intro
» $e$ in void

INT

formation

1.$H$ » ${\tt U}{i}$ ext int by intro int

2.$H$ » int in ${\tt U}{i}$ by intro

canonical

3.$H$ » int ext $c$ by intro $c$

4.$H$ » $c$ in int by intro

where $c$ must be an integer constant.

noncanonical

5.$H$ » -$t$ in int
» $t$ in int

6.$H$ » int ext $m op n$ by intro $op$
» int ext $m$
» int ext $n$

7.$H$ » $m op n$ in int by intro
» $m$ in int
» $n$ in int

where $op$ must be one of +,-,*,/, or mod.

8.$H$,$x$:int,$H'$ » $T$ ext ind($x$;$y,z$.$t_d$;$t_b$;$y,z$.$t_u$) by elim $x$ new $z$[,$y$]
$y$:int,$y$<0,$z$:$T$[$y$+1/$x$] » $T$[$y$/$x$] ext $t_d$
» $T$[0/$x$] ext $t_b$
$y$:int,0<$y$,$z$:$T$[$y$-1/$x$] » $T$[$y$/$x$] ext $t_u$

The optional new name must be given if $x$ occurs free in $H'$.

9.$H$ » ind($e$;$x$,$y$.$t_d$;$t_b$;$x$,$y$.$t_u$) in $T[e/z]$
by intro [over $z$.$T$] [new $u$,$v$]
» $e$ in int
$u$:int,$u$<0,$v$: $T[u{\tt +1}/z]$ » $t_d[u,v/x,y]$ in $T[u/z]$
» $t_b$ in $T[{\tt0}/z]$
$u$:int,0<$u$,$v$: $T[u{\tt -1}/z]$ » $t_u[u,v/x,y]$ in $T[u/z]$

10.$H$ » int_eq($a$;$b$;$t$;$t'$) in $T$ by intro
» $a$ in int
» $b$ in int
$a$=$b$ in int » $t$ in $T$
($a$=$b$ in int)->void » $t'$ in $T$

11.$H$ » less($a$;$b$;$t$;$t'$) in $T$ by intro
» $a$ in int
» $b$ in int
$a$<$b$ » $t$ in $T$
($a$<$b$)->void » $t'$ in $T$

computation

12a.$H$ » ind($nt$;$x$,$y$.$t_d$;$t_b$;$x$,$y$.$t_u$) = $t$ in $T$ by reduce 1 down
» $t_d$[$nt$,(ind($nt$+1;$x$,$y$.$t_d$;$t_b$;$x$,$y$.$t_u$))/$x$,$y$] = $t$ in $T$
» $nt$<0

12b.$H$ » ind($zt$;$x$,$y$./$t_d$;$t_b$;$x$,$y$.$t_u$) = $t$ in $T$ by reduce 1 base
» $t_b$ = $t$ in $T$
» $zt$ = 0 in int

12c.$H$ » ind($nt$;$x$,$y$.$t_d$;$t_b$;$x$,$y$.$t_u$) = $t$ in $T$ by reduce 1 up
» $t_u$[$nt$,(ind($nt$-1;$x$,$y$.$t_d$;$t_b$;$x$,$y$.$t_u$))/$x$,$y$] = $t$ in $T$
» 0<$nt$

13a.$H$ » int_eq($a$;$a$;$t$;$t'$) = $t''$ in $T$ by reduce 1
» $t$=$t''$ in $T$

13b.$H$ » int_eq($a$;$b$;$t$;$t'$) = $t''$ in $T$ by reduce 1
» $t'$ = $t''$ in $T$

where $a$ and $b$ are canonical int terms, and $a \neq b$.

14a.$H$ » less($a$;$b$;$t$;$t'$) = $t''$ in $T$ by reduce 1
» $t$=$t''$ in $T$

where $a$ and $b$ are canonical int terms such that $a<b$.

14b.$H$ » less($a$;$b$;$t$;$t'$) = $t''$ in $T$ by reduce 1
» $t'$=$t''$ in $T$

where $a$ and $b$ are canonical int terms such that $a \geq b$.

LESS

formation

1.$H$ » ${\tt U}{i}$ ext $a$<$b$ by intro less
$H$ » int ext $a$
$H$ » int ext $b$

2.$H$ » $a$<$b$ in ${\tt U}{i}$ by intro
$H$ » $a$ in int
$H$ » $b$ in int

equality

3.$H$ » axiom in $a$<$b$
$H$ » $a$<$b$

LIST

formation

1.$H$ » ${\tt U}{i}$ ext $A$ list by intro list
» ${\tt U}{i}$ ext $A$

2.$H$ » $A$ list in ${\tt U}{i}$ by intro
» $A$ in ${\tt U}{i}$

canonical

3.$H$ » $A$ list ext nil by intro nil at ${\tt U}{i}$
» $A$ in ${\tt U}{i}$

4.$H$ » nil in $A$ list by intro at ${\tt U}{i}$
» $A$ in ${\tt U}{i}$

5.$H$ » $A$ list ext $h$.$t$ by intro .
» $A$ ext $h$
» $A$ list ext $t$

6.$H$ » $a.b$ in $A$ list by intro
» $a$ in $A$
» $b$ in $A$ list

noncanonical

7.$H$,$x$:$A$ list,$H'$ » T ext list_ind($x$;$t_b$;$u,v,w$.$t_u$)
by elim $x$ new $w$,$u$[,$v$]
» $T$[nil/$x$] ext $t_b$
$u$:$A$,$v$:$A$ list,$w$:$T$[$v$/$x$] » $T$[$u.v$/$x$] ext $t_u$

8.$H$ » list_ind($e$;$t_b$;$x,y,z.t_u$) in $T$[$e$/$z$]
by intro [over $z.T$] using $A$ list [new u,v,w]
» $e$ in $A$ list
» $t_b$ in $T$[nil/$z$]
$u$:$A$,$v$:$A$ list,$w$:$T$[$v$/$z$]
» $t_u$[$u,v,w$/$x,y,z$] in $T$[$u$.$v$/$z$]

computation

9a.$H$ » list_ind(nil;$t_b$;$u,v,w.t_u$) = $t$ in $T$ by reduce 1
» $t_b$ = $t$ in $T$

9b.$H$ » list_ind($a.b$;$t_b$;$u,v,w.t_u$) = $t$ in $T$ by reduce 1
» $t_u$[$a,b,$list_ind($b$;$t_b$;$u,v,w.t_u$)/$u,v,w$] = $t$ in $T$

UNION

formation

1.$H$ » ${\tt U}{i}$ ext $A$|$B$ by intro union
» ${\tt U}{i}$ ext $A$
» ${\tt U}{i}$ ext $B$

2.$H$ » $A$|$B$ in ${\tt U}{i}$ by intro
» $A$ in ${\tt U}{i}$
» $B$ in ${\tt U}{i}$

canonical

3.$H$ » $A$|$B$ ext inl($a$) by intro at ${\tt U}{i}$ left
» $A$ ext $a$
» $B$ in ${\tt U}{i}$

4.$H$ » inl($a$) in $A$|$B$ by intro at ${\tt U}{i}$
» $a$ in $A$
» $B$ in ${\tt U}{i}$

5.$H$ » $A$|$B$ ext inr($b$) by intro at ${\tt U}{i}$ right
» $B$ ext $b$
» $A$ in ${\tt U}{i}$

6.$H$ » inr($b$) in $A$|$B$ by intro at ${\tt U}{i}$
» $b$ in $B$
» $A$ in ${\tt U}{i}$

noncanonical

7.$H$,$z$:$A$|$B$,$H'$ » $T$ ext decide($z$;$x$.$t_l$;$y$.$t_r$) by elim $z$ [new $x$,$y$] $x$:$A$,$z$=inl($x$) in $A$|$B$ » $T$[inl($x$)/$z$] ext $t_l$
$y$:$B$,$z$=inr($y$) in $A$|$B$ » $T$[inr($y$)/$z$] ext $t_r$

8.$H$ » decide($e$;$x$.$t_l$;$y$.$t_r$) in $T$[$e$/$z$]
by intro [over $z$.$T$] using $A$|$B$ [new u,v]
» $e$ in $A$|$B$
$u$:$A$, $e$=inl($u$) in $A$|$B$ » $t_l$[$u$/$x$] in $T$[inl($u$)/$z$]
$v$:$B$, $e$=inr($v$) in $A$|$B$ » $t_r$[$v$/$y$] in $T$[inr($v$)/$z$]

computation

9a.$H$ » decide(inl($a$);$x$.$t_l$;$y$.$t_r$) = $t$ in $T$ by reduce 1
» $t_l$[$a$/$x$] = $t$ in $T$

9b.$H$ » decide(inr($b$);$x$.$t_l$;$y$.$t_r$) = $t$ in $T$ by reduce 1
» $t_r$[$b$/$y$] = $t$ in $T$

FUNCTION

formation

1.$H$ » ${\tt U}{i}$ ext $x$:$A$->$B$ by intro function $A$ new $x$
» $A$ in ${\tt U}{i}$
$x$:$A$ » ${\tt U}{i}$ ext $B$

2.$H$ » $x$:$A$->$B$ in ${\tt U}{i}$ by intro [new $y$]
» $A$ in ${\tt U}{i}$
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

3.$H$ » ${\tt U}{i}$ ext $A$->$B$ by intro function
» ${\tt U}{i}$ ext $A$
» ${\tt U}{i}$ ext $B$

4.$H$ » $A$->$B$ in ${\tt U}{i}$ by intro
» $A$ in ${\tt U}{i}$
» $B$ in ${\tt U}{i}$

canonical

5.$H$ » $x$:$A$->$B$ ext $\backslash$$y$.$b$ by intro at ${\tt U}{i}$ [new $y$]
$y$:$A$ » $B$[$y$/$x$] ext $b$
» $A$ in ${\tt U}{i}$

6.$H$ » $\backslash$$x$.$b$ in $y$:$A$->$B$ by intro at ${\tt U}{i}$ [new $z$]
$z$:$A$ » $b$[$z$/$x$] in $B$[$z$/$y$]
» $A$ in ${\tt U}{i}$

noncanonical

7.$H$,$f$:($x$:$A$->$B$),$H'$ » $T$ ext $t$[$f$($a$)/$y$] by elim $f$ on $a$ [new $y$] » $a$ in $A$
$y$:$B$[$a$/$x$], $y$=$f$($a$) in $B$[$a$/$x$] » $T$ ext $t$

8.$H$,$f$:($x$:$A$->$B$),$H'$ » $T$ ext $t$[$f$($a$)/$y$] by elim $f$ [new $y$]
» $A$ ext $a$
$y$:$B$ » $T$ ext $t$

The first form is used when $x$ occurs free in $B$, the second when it doesn't.

9.$H$ » $f$($a$) in $B$[$a$/$x$] by intro using $x$:$A$->$B$
» $f$ in $x$:$A$->$B$
» $a$ in $A$

equality

10.$H$ » $f$ = $g$ in $x$:$A$->$B$ by extensionality [new $y$]
$y$:$A$ » $f$($y$) = $g$($y$) in $B$[$y$/$x$]
» $f$ in $x$:$A$->$B$
» $g$ in $x$:$A$->$B$

computation

11.$H$ » ($\backslash$$x$.$b$)($a$) = $t$ in $B$ by reduce 1
» $b$[$a$/$x$] = $t$ in $B$

PRODUCT

formation

1.$H$ » ${\tt U}{i}$ ext $x$:$A$#$B$ by intro product $A$ new $x$
» $A$ in ${\tt U}{i}$
$x$:$A$ » ${\tt U}{i}$ ext $B$

2.$H$ » $x$:$A$#$B$ in ${\tt U}{i}$ by intro [new $y$]
» $A$ in ${\tt U}{i}$
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

3.$H$ » ${\tt U}{i}$ ext $A$#$B$ by intro product
» ${\tt U}{i}$ ext $A$
» ${\tt U}{i}$ ext $B$

4.$H$ » $A$#$B$ in ${\tt U}{i}$ by intro
» $A$ in ${\tt U}{i}$
» $B$ in ${\tt U}{i}$

canonical

5.$H$ » $x$:$A$#$B$ ext <$a$,$b$> by intro at ${\tt U}{i}$ $a$ [new $y$]
» $a$ in $A$
» $B$[$a$/$x$] ext $b$
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

6.$H$ » <$a$,$b$> in $x$:$A$#$B$ by intro at ${\tt U}{i}$ [new $y$]
» $a$ in $A$
» $b$ in $B$[$a$/$x$]
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

7.$H$ » $A$#$B$ ext <$a$,$b$> by intro
» $A$ ext $a$
» $B$ ext $b$

8.$H$ » <$a$,$b$> in $A$#$B$ by intro
» $a$ in $A$
» $b$ in $B$

noncanonical

9.$H$,$z$:($x$:$A$#$B$),$H'$ » $T$ ext spread($z$;$u,v$.$t$) by elim $z$ new $u,v$
$u$:$A$,$v$:$B$[$u$/$x$],$z$=<$u$,$v$> in $x$:$A$#$B$ » $T$[<$u$,$v$>/$z$] ext $t$

10.$H$ » spread($e$;$x,y.t$) in $T$[$e$/$z$]
by intro [over $z.T$] using $w$:$A$#$B$ [new $u,v$]
» $e$ in $w$:$A$#$B$
$u$:$A$,$v$:$B$[$u$/$w$],$e$=<$u$,$v$> in $w$:$A$#$B$ » $t$[$u,v$/$x,y$] in $T$[<$u$,$v$>/$z$]

computation

11.$H$ » spread(<$a$,$b$>;$x,y.t$) = $s$ in $T$ by reduce 1
» $t$[$a,b$/$x,y$] = $s$ in $T$

QUOTIENT

formation

1.$H$ » ${\tt U}{i}$ ext ($x$,$y$):$A$//$E$ by intro quotient $A$,$E$ new $x$,$y$,$z$
» $A$ in ${\tt U}{i}$
$x$:$A$,$y$:$A$ » $E$ in ${\tt U}{i}$
$x$:$A$ » $E$[$x,x$/$x,y$]
$x$:$A$,$y$:$A$,$E$[$x,y$/$x,y$] » $E$[$y,x$/$x,y$]
$x$:$A$,$y$:$A$,$z$:$A$,$E$[$x,y$/$x,y$], $E$[$y,z$/$x,y$] » $E$[$x,z$/$x,y$]

2.$H$ » ($u,v$):$A$//$E$ in ${\tt U}{i}$ by intro new $x$,$y$,$z$
» $A$ in ${\tt U}{i}$
$x$:$A$,$y$:$A$ » $E$[$x,y$/$u,v$] in ${\tt U}{i}$
$x$:$A$ » $E$[$x,x$/$u,v$]
$x$:$A$,$y$:$A$,$E$[$x,y$/$u,v$] » $E$[$y,x$/$u,v$]
$x$:$A$,$y$:$A$,$z$:$A$,$E$[$x,y$/$u,v$], $E$[$y,z$/$u,v$] » $E$[$x,z$/$u,v$]

canonical

3.$H$ » ($x,y$):$A$//$E$ ext $a$ by intro at ${\tt U}{i}$
» ($x,y$):$A$//$E$ in ${\tt U}{i}$
» $A$ ext $a$

4.$H$ » $a$ in ($x,y$):$A$//$E$ by intro at ${\tt U}{i}$
» ($x,y$):$A$//$E$ in ${\tt U}{i}$
» $a$ in $A$

noncanonical

5.$H$,$u$:($x,y$):$A$//$E$,$H'$ » $t$=$t'$ in $T$ by elim $u$ at ${\tt U}{i}$ [new $v,w$]
$v$:$A$,$w$:$A$ » $E$[$v,w$/$x,y$] in ${\tt U}{i}$
» $T$ in ${\tt U}{i}$
$v$:$A$,$w$:$A$,$E$[$v,w$/$x,y$] »
$t$[$v$/$u$] = $t'$[$w$/$u$] in $T$[$v$/$u$]

equality

6.$H$ » ($x,y$):$A$//$E$ = ($u,v$):$B$//$F$ in ${\tt U}{i}$ by intro [new $r,s$]
» ($x,y$):$A$//$E$ in ${\tt U}{i}$
» ($u,v$):$B$//$F$ in ${\tt U}{i}$
» $A$ = $B$ in ${\tt U}{i}$
$A$=$B$ in ${\tt U}{i}$,$r$:$A$,$s$:$A$ » $E$[$r,s$/$x,y$] -> $F$[$r,s$/$u,v$]
$A$=$B$ in ${\tt U}{i}$,$r$:$A$,$s$:$A$ » $F$[$r,s$/$u,v$] -> $E$[$r,s$/$x,y$]

7.$H$ » $t$ = $t'$ in ($x,y$):$A$//$E$ by intro at ${\tt U}{i}$
» ($x,y$):$A$//$E$ in ${\tt U}{i}$
» $t$ in $A$
» $t'$ in $A$
» $E$[$t,t'$/$x,y$]

SET

formation

< 1.$H$ » ${\tt U}{i}$ ext $\{$$x$:$A$|$B$$\}$ by intro set $A$ new $x$
» $A$ in ${\tt U}{i}$
$x$:$A$ » ${\tt U}{i}$ ext $B$

2.$H$ » $\{$$x$:$A$|$B$$\}$ in ${\tt U}{i}$ by intro [new y]
» $A$ in ${\tt U}{i}$
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

3.$H$ » ${\tt U}{i}$ ext $\{$$A$|$B$$\}$ by intro set
» ${\tt U}{i}$ ext $A$
» ${\tt U}{i}$ ext $B$

4.$H$ » $\{$$A$|$B$$\}$ in ${\tt U}{i}$ by intro
» $A$ in ${\tt U}{i}$
» $B$ in ${\tt U}{i}$

canonical

5.$H$ » $\{$$x$:$A$|$B$$\}$ ext $a$ by intro at ${\tt U}{i}$ $a$ [new $y$]
» $a$ in $A$
» $B$[$a$/$x$] ext $b$
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

All hidden hypothesis in $H$ become unhidden in the second subgoal.

6.$H$ » $a$ in $\{$$x$:$A$|$B$$\}$ by intro at ${\tt U}{i}$ [new $y$]
» $a$ in $A$
» $B$[$a$/$x$]
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$

7.$H$ » $\{$$A$|$B$$\}$ ext $a$ by intro
» $A$ ext $a$
» $B$ ext $b$

All hidden hypotheses in $H$ become unhidden in the second subgoal.

8.$H$ » $a$ in $\{$$A$|$B$$\}$ by intro
» $a$ in $A$
» $B$ ext $b$

noncanonical

9.$H$,$u$:$\{$$x$:$A$|$B$$\}$,$H'$ » $T$ ext ($\backslash$$y$.$t$)($u$) by elim $u$ at ${\tt U}{i}$ [new $y$]
$y$:$A$ » $B$[$y$/$x$] in ${\tt U}{i}$
$y$:$A$,[$B$[$y$/$x$]],$u$=$y$ in $A$ » $T$[$y$/$u$] ext $t$

Note that the second new hypotheses of the second subgoal is hidden.

equality

10.$H$ » $\{$$x$:$A$|$B$$\}$ = $\{$$y$:$A'$|$B'$$\}$ in ${\tt U}{i}$ by intro [new $z$]
» $A$ = $A'$ in ${\tt U}{i}$
$z$:$A$ » $B$[$z$/$x$] -> $B'$[$z$/$y$]
$z$:$A$ » $B'$[$z$/$y$] -> $B$[$z$/$x$]

EQUALITY

formation

1.$H$ » ${\tt U}{i}$ ext $a_1$=$\cdots$=$a_n$ in $A$ by intro equality $A$ $n$
» $A$ in ${\tt U}{i}$
» $A$ ext $a_1$
         $\left.\vdots\right.$
» $A$ ext $a_n$

The default for $n$ is 1.

2.$H$ » ($a_1$=$\cdots$=$a_n$ in $A$) in ${\tt U}{i}$ by intro
» $A$ in ${\tt U}{i}$
» $a_1$ in $A$
         $\left.\vdots\right.$
» $a_n$ in $A$

canonical

3.$H$ » axiom in ($a$ in $A$) by intro
» $a$ in $A$

4.$H$,$x$:$T$,$H'$ » $x$ in $T$ by intro

This rule doesn't work when T is a set or quotient term, since intro will invoke the equality rule for the set or quotient type, respectively. In any case, the equality rule can be used.

UNIVERSE

canonical

1.$H$ » ${\tt U}{i}$ ext ${\tt U}{j}$ by intro universe ${\tt U}{j}$

2.$H$ » ${\tt U}{j}$ in ${\tt U}{i}$ by intro

where $j<i$. Note that all the formation rules are intro rules for a universe type.

noncanonical

Currently there are no rules in the system for analyzing universes. At some later date such rules may be added.

MISCELLANEOUS

hypothesis

1.$H$,$x$:$A$,$H'$ » $A'$ ext $x$ by hyp $x$

where $A'$ is $\alpha$-convertible to $A$

sequence

2.$H$ » $T$ ext ($\backslash$$x_1$.$\cdots$($\backslash$$x_n$.$t$)($t_n$))$\cdots$)($t_1$)
by seq $T_1,\dots,T_n$ [new $x_1,\dots,x_n$]
» $T_1$ ext $t_1$
$x_1$:$T_1$ » $T_2$ ext $t_2$
         $\left.\vdots\right.$
$x_1$:$T_1$,$\dots$,$x_n$:$T_n$ » $T$ ext $t$

lemma

3.$H$ » $T$ ext $t$[term_of($theorem$)/$x$] by lemma $theorem$ [new $x$]
$x$:$C$ » $T$ ext $t$

where $C$ is the conclusion of the complete theorem $theorem$.

def

4.$H$ » $T$ ext $t$ by def ${theorem}$ [new $x$]
$x$:term_of(${theorem}$) = ${ext}$-${term}$ in $C$ » $T$ ext $t$

where $C$ is the conclusion of the complete theorem, ${theorem}$, and ${ext}$-${term}$ is the term extracted from that theorem. 8.10

explicit intro

5.$H$ » $T$ ext $t$ by explicit intro $t$
» $t$ in $T$

cumulativity

6.$H$ » $T$ in ${\tt U}{i}$ by cumulativity at ${\tt U}{j}$
» $T$ in ${\tt U}{j}$

where $j<i$

substitution

7.$H$ » $T$[$t$/$x$] ext $s$ by subst at ${\tt U}{i}$ $t$=$t'$ in $T'$ over $x.T$
» $t$ = $t'$ in $T'$
» $T$[$t'$/$x$] ext $s$
$x$:$T'$ » $T$ in ${\tt U}{i}$

direct computation

8.$H$ » $T$ ext $t$ by compute using $S$
» $T'$ ext $t$

9.$H$, $x$:$T$, $H'$ » $T''$ ext $t$ by compute hyp i using $S$
$H$, $x$:$T'$, $H'$» $T''$ ext $t$

where $x$:$T$ is the $i^{th}$ hypothesis, where $S$ is obtained from $T$ by ``tagging'' some of its subterms, and where $T'$ is generated by the system by performing some computation steps on subterms of $T$, as indicated by the tags. A subterm $t$ is tagged by replacing it by [[*;$t$]] or [[$n$;$t$]], where $n$ is a positive integer constant. The latter tag causes $t$ to be computed for $n$ steps, and the former causes computation to proceed as far as possible. There are some somewhat complicated restrictions on what subterms of $A$ may be tagged, but most users will likely find it sufficient to know that any subterm of $T$ may be tagged that does not occur within the scope of a binding variable occurrence in $T$. An application of one of these rules will fail if the tagging is illegal, or if removing the tags from $S$ does not yield a term equal to $T$. For a more complete description of this rule, see appendix C. Note that many of the computation rules, such as the one for product, are instances of direct computation.

equality

10.$H$ » $t$ = $t'$ in $T$ by equality

where the equality of $t$ and $t'$ can be deduced from assumptions that are equalities over $T$ (or equalities over $T'$ where $T=T'$ is deducible using only reflexivity, commutativity and transitivity) .

arith

11.$H$ » $C$ by arith at ${\tt U}{i}$

The arith rule is used to justify conclusions which follow from hypotheses by a restricted form of arithmetic reasoning. Roughly speaking, arith knows about the ring axioms for integer multiplication and addition, the total order axioms of $<$, the reflexivity, symmetry and transitivity of equality, and a limited form of substitutivity of equality. We will describe the class of problems decidable by arith by giving an informal account of the procedure which arith uses to decide whether or not $C$ follows from $H$.

The terms that arith understands are those denoting arithmetic relations, namely terms of the form $s$<$t$, $s$=$t$ in int or the negation of a term of this form. As the only equalities arith concerns itself with are those of the form $s$=$t$ in int, we will drop the in int and write only $s$=$t$ in the rest of this description. For arith the negation of an arithmetic relation $s \theta t$ where $\theta$ is one of $<$ or $=$ is of the form ($s \theta t$)->void, which we will write as $\neg s \theta t$. As integer equality and less-than are decidable relations, $s \theta t$ and $\neg \neg s \theta t$ denote the same relation and will be treated identically by arith.

The arith rule may be used to justify goals of the form

$H_1$, $\ldots$, $H_n$ » $C_1$ | $\ldots$ | $C_m$ ,

where each $H_i$ and $C_i$ is a term denoting an arithmetic relation. If arith can justify the goal it will produce subgoals requiring the user to show that the left- and right-hand sides of each $C_i$ denote integer terms. As a convenience arith will attempt to prove goals in which not all of the $C_i$ are arithmetic relations; it simply ignores such disjuncts. If it is successful on such a goal, it will produce subgoals requiring the user to prove that each such disjunct is a type at the level given in the invocation of the rule.

Arith begins by normalizing the relevant formulas of the goal according to the following conventions:

  1. Rewrite each relation of the form $\neg s=t$ as the equivalent $s<t$|$t<s$. A conclusion $C$ follows from such an assumption if it follows from either $s<t$ or $t<s$; hence arith tries both cases. Henceforth, we assume that all negations of equalities have been eliminated from consideration.
  2. Replace all occurrences of terms which are not addition, subtraction or multiplication by a new variable. Multiple occurrences of the same term are replaced by the same variable. Arith uses only facts about addition, subtraction and multiplication, so it treats all other terms as atomic. At this point all terms are built from integer constants and integer variables using $+$, $-$ and $\ast$.
  3. Rewrite all terms as polynomials in canonical form. The exact nature of the canonical form is irrelevant (the reader may think of it as the form used in high school algebra texts) but has the important property that any two equal terms are identical. Each term now has the form $p+c \theta p'+c'$, where $p$ and $p'$ are nonconstant polynomials in canonical form, $c$ and $c'$ are constants, and $\theta$ is one of $<$, $=$ or $\geq$ ($s \geq t$ is equivalent to $\neg t < s$).
  4. Replace each nonconstant polynomial $p$ by a new variable, with each occurrence of $p$ being replaced by the same variable. This amounts to treating each nonconstant polynomial as an atom. Now each formula is of the form $z+c \theta z'+c'$. Arith now decides whether or not the conclusion follows from the hypotheses by using the total order axioms of $<$, the reflexivity, symmetry, transitivity and substitutivity of $=$, and the following so-called trivial monotonicity axioms ($c$ and $d$ are constants).
    • $x \geq y, c \geq d \Rightarrow x+c \geq y+d$
    • $x \geq y, c \leq d \Rightarrow x-c \geq y-d$
    These rules capture all of the acceptable forms of reasoning which may be applied to formulas in canonical form.

For a detailed account of the arith rule and a proof of its correctness, see the article by Tat-hung Chan in [Constable, Johnson, & Eichenlaub 82].

ML Constructors

One of the features of the Nuprl system is that it comes with its own formal metalanguage, implemented in ML. Accordingly, ML needs access to the rules of the system. Following is a list of the ML rule constructors. The constructors are categorized and numbered in the same manner as the rules. For example, the constructor numbered 4 in the atom section corresponds to the rule numbered 4 in the atom section. Each constructor is presented in the form constructor_name(parameter names): type. The parameter names are never actually used but appear here solely for documentation purposes. Following are some conventions regarding the parameter names which we give with their types:

  • hyp:int is used to indicate a hypothesis.
  • where:int is used to indicate which equand of an equality should be reduced in a computation rule.
  • level:int is used to give a universe level.
  • using:term is used to indicate a using term.
  • over_id:tok, over:term are used to indicate an over term. If the over_id is the token `nil`, the over term is ignored.
All parameters corresponding to new identifiers have the same names as the new names given in the corresponding rule, and should be ML tokens. To specify the default identifier for an optional new identifier, give the token `nil`.

Unlike the rules, each constructor needs a unique name. The general form of the names is base-type_kind_qualifier, where base-type is a prl type and kind is one of intro, elim, equality, formation or computation. So, for example, list_equality_nil is the name of the constructor for the rule which specifies how to show two nil terms are the same in a list type, and int_elim is the name of the constructor for the elim rule for integers. There are some exceptions to this general pattern, the main one being that the name of the constructor for the rule for showing two canonical type terms to be equal in some universe is type_equality rather than universe_equality_type.

ATOM

formation universe_intro_atom: rule.

atom_equality: rule.

canonical

atom_intro(token): term $\rightarrow$ rule.

atom_equality_token: rule.

quality

atom_eq_equality: rule.

computation

atom_eq_computation(where): int $\rightarrow$ rule.

VOID

formation

universe_intro_void: rule.

void_equality: rule.

noncanonical

void_elim(hyp): int $\rightarrow$ rule.

void_equality_any: rule.

INT

formation

universe_intro_integer: rule.

int_equality: rule.

canonical

integer_intro_integer(c): int $\rightarrow$ rule.

integer_equality_natural_number: rule.

noncanonical

integer_equality_minus: rule.



integer_intro_addition: rule.

integer_intro_subtraction: rule.

integer_intro_multiplication: rule.

integer_intro_division: rule.

integer_intro_modulo: rule.



integer_equality_addition: rule.

integer_equality_subtraction: rule.

integer_equality_multiplication: rule.

integer_equality_division: rule.

integer_equality_modulo: rule.



integer_elim(hyp y z): int $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

integer_equality_induction(over_id over u v): tok $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

equality

int_eq_equality: rule.

int_less_equality: rule.

computation

integer_computation(kind where): tok $\rightarrow$ int $\rightarrow$ rule.where kind should be one of `UP`, `BASE` or `DOWN`.

int_eq_computation(where): int $\rightarrow$ rule.

int_less_computation(where): int $\rightarrow$ rule.

LESS

formation

universe_intro_less: rule.

less_equality: rule.

equality

axiom_equality_less: rule.

LIST

formation

universe_intro_list: rule.

list_equality(level): int $\rightarrow$ rule.

canonical

list_intro_nil(level): int $\rightarrow$ rule.

list_equality_nil(level): int $\rightarrow$ rule.



list_intro_cons: rule.

list_equality_cons: rule.

noncanonical

list_elim (hyp u v w): int $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

list_equality_induction (over_id over using u v w): tok $\rightarrow$ term $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

computation

list_computation(where): int $\rightarrow$ rule.

UNION

formation

universe_intro_union: rule.

union_equality: rule.

canonical

union_intro_left(level): int $\rightarrow$ rule.

union_equality_inl(level): int $\rightarrow$ rule.



union_intro_right(level): int $\rightarrow$ rule.

union_equality_inr(level): int $\rightarrow$ rule.

noncanonical

union_elim(hyp x y): int $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

union_equality_decide(over_id over using u v): tok $\rightarrow$ term $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

computation

union_computation(where): int $\rightarrow$ rule.

FUNCTION

formation

universe_intro_function(x term): tok $\rightarrow$ term $\rightarrow$ rule.

function_equality(y): tok $\rightarrow$ rule.

universe_intro_function_independent: rule.

function_equality_independent: rule.

canonical

function_intro(level y): int $\rightarrow$ tok $\rightarrow$ rule.

function_equality_lambda(level z): int $\rightarrow$ tok $\rightarrow$ rule.

noncanonical

function_elim(hyp on y): int $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ rule.

function_elim_independent(hyp y): int $\rightarrow$ tok $\rightarrow$ rule.

function_equality_apply(using): term $\rightarrow$ rule.

equality

extensionality(y): tok $\rightarrow$ rule.

computation

function_computation(where): int $\rightarrow$ rule.

PRODUCT

formation

universe_intro_product(x left_term): tok $\rightarrow$ term $\rightarrow$ rule.

product_equality(y): tok $\rightarrow$ rule.

universe_intro_product_independent: rule.

product_equality_independent: rule.

canonical

product_intro_dependent(left_term level y): term $\rightarrow$ int $\rightarrow$ tok $\rightarrow$ rule.

product_equality_pair(level y): int $\rightarrow$ tok $\rightarrow$ rule.

product_intro: rule.

product_equality_pair_independent: rule.

noncanonical

product_elim(hyp u v): int $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

product_equality_spread(over_id over using u v): tok $\rightarrow$ term $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

computation

product_computation(where): int $\rightarrow$ rule.

QUOTIENT

formation

universe_intro_quotient(A E x y z): term $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

quotient_formation(x y z): tok $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

canonical

quotient_intro(level): int $\rightarrow$ rule.

quotient_equality_element(level): int $\rightarrow$ rule.

noncanonical

quotient_elim (hyp level v w): int $\rightarrow$ int $\rightarrow$ tok $\rightarrow$ tok $\rightarrow$ rule.

equality

quotient_equality(r s): tok $\rightarrow$ tok $\rightarrow$ rule.

quotient_equality_element(level): int $\rightarrow$ rule.

SET

formation

universe_intro_set(x type): tok $\rightarrow$ term $\rightarrow$ rule.

set_formation(y): tok $\rightarrow$ rule.

universe_intro_set_independent: rule.

set_formation_independent: rule.

canonical

set_intro(level left_term y): int $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ rule.

set_equality_element(level y): int $\rightarrow$ tok $\rightarrow$ rule.

set_intro_independent: rule.

set_equality_element: rule.

noncanonical

set_elim(hyp level y): int $\rightarrow$ int $\rightarrow$ tok $\rightarrow$ rule.

equality

set_equality(z): tok $\rightarrow$ rule.

EQUALITY

formation

universe_intro_equality(type number_terms): term $\rightarrow$ int $\rightarrow$ rule.

equal_equality: rule.

canonical

axiom_equality_equal: rule.

equal_equality_variable: rule.

UNIVERSE

canonical

universe_intro_universe (level): int $\rightarrow$ rule.

universe_equality: rule.

MISCELLANEOUS

hypothesis

hyp(hyp): int $\rightarrow$ rule.

sequence

seq(term_list id_list): (term list) $\rightarrow$ (tok list) $\rightarrow$ rule.where the length of the token list should match the length of the term list.

lemma

lemma(lemma_name x): tok $\rightarrow$ tok $\rightarrow$ rule.

def

def(theorem x): tok $\rightarrow$ tok $\rightarrow$ rule.

explicit intro

explicit_intro(term): term $\rightarrow$ rule.

cumulativity

cumulativity(level): int $\rightarrow$ rule.

substitution

substitution(level equality_term over_id over): int $\rightarrow$ term $\rightarrow$ tok $\rightarrow$ term $\rightarrow$ rule.

direct computation

direct_computation(tagged_term): term $\rightarrow$ rule.

direct_computation_hyp(hyp tagged_term): int $\rightarrow$ term $\rightarrow$ rule.

equality

equality: rule.

arith

arith(level): int $\rightarrow$ rule.

Footnotes

....8.1
There is a similarity between a type and Bishop's notion of set. Bishop [Bishop 67] says that to give a set, one gives a way to construct its members and gives an equivalence relation, called the equality on that set, on the members.
... variables.8.2
An identifier is any string of letters, digits, underscores or at-signs that starts with a letter. The only identifiers which cannot be used for variables are term_of and those which serve as operator names, such as int or spread.
....8.3
In the formation of these as members of $U_k$, $B$ must be $U_k$-functional in $x$:$A$.
... constructor.8.4
modulo the difference between $A$#$B$ and $x$:$A$#$B$, etc.
... CLASS="MATH">$B$).8.5
If the reader finds this a bit difficult to follow, perhaps it would help to consider first the case in which $x$ is not free in $B$ and $z$ is not free in $T$ and then the more general cases afterward.
... integers.8.6
This is defined by primitive recursion with 0 as the base case and an induction step for each direction out (positive and negative). Of course, in a higher-order system such as Nuprl, where functions can take functions as arguments and have functions as values, one can define by primitive recursion functions in int->int which are not primitive recursive.
... true.8.7
If we were to give a similar semantic account of the judgements of [Martin-Löf 82], the plainest difference between the truth conditions for those judgements and Nuprl judgements would be that the truth of the former requires type-functionality of each assumption in all its variables.
... inhabited.8.8
Recall that the term ($a$ = $b$ in $A$) is a type whenever $a\in A$ and $b\in A$ and is inhabited just when $a=b\in A$. As a special case, the term ($a$ in $A$) is a type and is inhabited just when $a\in A$.
... system.8.9
It turns out that these predicates will hold only for closed terms.
... theorem.8.10
This rule introduces very strong interproof dependencies. A proof using this rule depends not only on $C$ but also on the way $C$ is proved.
next up previous contents
Next: The Metalanguage Up: Index Previous: System Description   Contents
PRL Home
Introduction
The Nuprl book
Origins of the PRL Project
Goals
Dynamics of the Project
Mathematical Expression in Nuprl
Cross Links to Math & CS Fields
Knowledge Base
Math Library
Publications
Projects
CRASH
Nuprl/FDL System
EventML Software
Seminar
People
Wiki
The Book
Lectures
Other Groups


Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library