% -LaTeX-
\section
In the previous section we began our presentation of the
representation of proofs. In it we showed how primitive proofs
are represented. The class of primitive proofs is logically
adequate, but practically more is needed. Primitive rules
are too primitive. As a result, proofs constructed only
primitive rules rapidly become unmanageably large. Moreover,
because of the level of detail required in their construction,
they are unbelievably tedious to construct. In addition,
they are of little documentary value: the sheer mass of detail obscures
the logical thrust of an argument. For all these reasons, more
complex inference rules are required.
Nuprl follows LCF in its use of tactics to provide
more complex derived inference rules. A tactic is a program
which given a goal $g$ produces a sequence of subgoals $\sequence
$,
and a validation $v$. The validation $v$ provides evidence that
$g$ follows from $\sequence
$. Tactics allow users to treat
a collection of primitive inference rules as a single inference step.
Since they are written in a general purpose programming language,
tactics can construct a sequence of primitive inferences to fit
the goal $g$. This construction can be arbitrarily complicated.
For us, the validation object $v$ produced by a tactic $t$,
when it is used to refine $g$, is a possibly incomplete
proof. Let $\sequence
$ be the sequence containing the
sequents at each unjustified node of $v$, in order. For
$t$ to be a correct justification of $g$ from $\sequence
$,
$\sequence
$ and $\sequence
$ must be identical.
Note that $\sequence
$ can be generated from $v$ using an
in order tree traversal of $v$. This means that tactics need only
generate their validations; their subgoals can be produced
automatically from these validations. For this reason,
we often think of tactics as functions which map sequents $g$
to proofs $v$.
Most of the work done in the section on primitive proofs still
applies. We need only to make various minor changes.
First, we must change the definition of the type $\Justification$
so that it represents a class of objects which includes tactics.
We must also update the definition of the operators
$\IsApplicable$ and $\AreSubs$ to account for the new sort of justification.
Nothing else changes.
\section
First, we must decide exactly what we want to represent. The
simplest option is to treat tactics extensionally. By this we
mean that the evaluation of tactics to produce validations is treated
as an extra-theoretic convenience. It is the validations themselves
which actually serve as justifications. All tactics that produce the
same validation are treated as equivalent, since only the validation
has any theoretical significance. When they use a tactic to
refine a goal, users are really, at least in principal, providing
the validation, albeit in a much abbreviated form.
If we view tactics in this fashion, a justification
consists of either the unjustification, or a primitive rule, or a proof;
together with an indication of which of three it actually is.
Tactic justifications can be treated as subproofs of the proof
in which they occur. Moreover, in pre-proofs, we can allow arbitrary
sub-pre-proofs as tactic justifications of a given goal. When the
proofs are selected out, one of the things we check is that all the
tactic justification pre-proofs are actually proofs.
Recall that our definition of the representation of
pre-proofs relied on the fact that the height of any sub-pre-proof
of a given pre-proof is less than the height of the pre-proof itself.
Since we want to include tactic justifications
as sub-pre-proofs of the pre-proof in which they occur, we
must ensure that the height operation on pre-proofs is appropriately
defined. To this end, we define the height of a
justification $j$ to be $0$ if $j$ is either the unjustification or
a primitive rule, and to be the height of the pre-proof $j$, if $j$ is
a tactic. Then, the height of the pre-proof
$\langle g, \langle j,(s_1,\ldots,s_n)\rangle\rangle$ is
[
1 + \max(\height(j), \max\limits_
\height(s_i)).
]
That is, it is one more then the height of its tallest sub-pre-proof,
where this might be the height of $j$.
Recall that we defined a representation relation for pre-proofs of
each possible height. We must now also parameterize our representation
relation for justifications in the same fashion. We use the
representation relation for pre-proofs of height $i$ or less in our
definition of the representation relation for justifications of
height $i$ or less. Then we use the representation relation for
justifications of height $i$ or less in our definition of the representation
relation for pre-proofs of height $i+1$ or less. Thus, we simultaneously
define two families of relations $\repsrelfor
$ and
$\repsrelfor
$ each parameterized by natural numbers $i$.
\begin
For each natural number $i$,
$t \repsrelfor
p$ is a two place relation between closed
terms $t$ and pre-proofs $p$, and $t \repsrelfor
j$
is a two place relation between closed terms $t$ and justifications $j$.
These relations are defined by induction on $i$, as follows.
\begin
\item
The relation $t \repsrelfor
p$ is never satisfied.
\item
The relation $t \repsrelfor{\preproof_{i+1}} p$ is satisfied
if and only if $t \mathrel{{\repsrelfor{\sequentclass}}\times
({\repsrelfor{\justification_i}}
\times {\repsrelforseq{\preproof_i}})} p$.
\item
If the justification $j$ is the unjustification, then
the relation $t \repsrelfor
j$ is satisfied
if and only if there is a term $t'$ such that
$\evalsto
{\inlterm{t'}}$ and
$t' \repsrelfor
j$.
\item
If the justification $j$ is a primitive rule, then
the relation $t \repsrelfor
j$ is satisfied
if and only if there are terms $t'$ and $t''$ such that
$\evalsto
{\inrterm{t'}}$,
$\evalsto
{\inlterm{t''}}$ and
$t'' \repsrelfor
j$.
\item
If the justification $j$ is a tactic, then
the relation $t \repsrelfor
j$ is satisfied
if and only if there are terms $t'$ and $t''$ such that
$\evalsto
{\inrterm{t'}}$,
$\evalsto
{\inrterm{t''}}$ and
$t'' \repsrelfor
j$.
\end
\end
Using these relations, we can define representation relations
for the class of pre-proofs and the class of justifications.
\begin
The relation $t \repsrelfor
p$ is a two place relation
on closed terms $t$ and pre-proofs $p$. The relation
$t \repsrelfor
j$ is a two place relation on closed terms $t$ and justifications $j$. They are defined as follows:
\begin
{\repsrelfor{\preproof}}&=&\bigcup_
{\repsrelfor{\preproof_i}}.
{\repsrelfor{\justification}}&=&
\bigcup_
{\repsrelfor{\justification_i}}.
\end
\end
\begin
The relation $\repsrelfor
$ is a computationally closed
representation relation for the class of pre-proofs. The relation
$\repsrelfor
$ is a computationally closed
representation relation for the class of justifications.
\end
To prove this, we first show, by induction on $i$,
that $\repsrelfor
$ is a computationally closed
representation relation for the class of pre-proofs of height
$i$ or less, and that $\repsrelfor
$ is
a representation relation for the class of justifications of height $i$
or less.
Since there are are no pre-proofs of height $0$, if $p$ is
a pre-proof of height $0$, we can conclude anything at all. In particular
that there is a closed term $t$ such that $t \repsrelfor
p$.
Similarly, $\repsrelfor
$ is empty. Thus, if
$t \repsrelfor
p$ we can conclude anything. In particular,
if it is also the case that $t \repsrelfor
p'$ then
$p$ and $p'$ are identical, and if it is also the case that $\squiggle t'$
then $t' \repsrelfor
p$.
A pre-proof of height $i+1$ is an object consisting of a sequent,
together with a justification of height $i$ or less, and a sequence
of pre-proofs of height $i$ or less. By the induction hypothesis
that $\repsrelfor
$ is a computationally closed
representation relation for the class of pre-proofs of height
$i$ or less. Therefore, $\repsrelforseq
$ is a
computationally closed representation relation for the class of
sequences of such pre-proofs. Also by the induction
hypothesis $\repsrelfor
$ is a computationally
closed representation relation for the class of justifications of height $i$
or less. Thus,
${\repsrelfor{\justification_i}} \times {\repsrelforseq{\preproof_i}}$
is a computationally closed representation for the class of objects
consisting of a justification of height $i$ or less, together with a sequence
of pre-proofs of height $i$ or less. Then,
[
{\repsrelfor{\sequentclass}} \times
(\repsrelfor{\justification_i
\times {\repsrelforseq
}})
]
is a computationally closed representation for the class of objects
consisting of a sequent, together with a justification of height $i$ or less,
together with a sequence of pre-proofs of height $i$ or less.
That is, it is a computationally closed representation for the class of
pre-proofs of height $i+1$ or less. By definition, however, this
relation is $\repsrelfor{\preproof_{i+1}}$.
A justification $j$ of height $i$ or less is either the
unjustification, or a primitive rule, or a pre-proof of height $i$ or less. We
consider each case in turn. If $j$ is the unjustification, then since
$\repsrelfor
$ is a representation relation for the class of
unjustifications, there is a term $t$ such that $t
\repsrelfor
j$. Since $\inl$ is value producing,
$\inlterm
$ evaluates to itself, and so $\inlterm
\repsrelfor
j$. If $j$ is a primitive rule, then
since $\repsrelfor
$ is a representation relation for the
class of primitive rules, there is a term $t$ such that $t
\repsrelfor
j$. Since $\inl$ is value producing,
$\inlterm
$ evaluates to itself. Since $\inr$ is value producing,
$\inrterm{\inlterm{t}}$ also evaluates to itself. Thus,
$\inrterm{\inlterm{t}} \repsrelfor
j$. If $j$ is a
pre-proof of height $i$ or less, then
since $\repsrelfor
$ is a representation relation for the
class of pre-proofs of height $i$ or less, there is a term $t$ such that $t
\repsrelfor
j$. Since $\inr$ is value producing,
$\inrterm
$ evaluates to itself. Since $\inr$ is value producing,
$\inrterm{\inrterm{t}}$ also evaluates to itself. Thus,
$\inrterm{\inrterm{t}} \repsrelfor
j$.
Suppose that $t \repsrelfor
j$ and
$t \repsrelfor
j'$ both hold for some closed term $t$, and
justifications $j$ and $j'$ of height $i$ or less. $j$ is either the
unjustification, or a primitive rule, or a pre-proof of height $i$ or less.
Likewise, $j'$ is either the
unjustification, or a primitive rule, or a pre-proof of height $i$ or less.
Suppose that $j$ is the unjustification.
Then $\evalsto
{\inlterm{t'}}$
for some term $t'$. Since evaluation is single valued, this
means that $t$ does not evaluate to a term of the form $\inrterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be a primitive rule or tactic. It follows that
$j'$ must be the unjustification too.
Otherwise, $j$ is either a primitive rule or a tactic.
Then, $\evalsto
{\inrterm{t'}}$
for some term $t'$. Since evaluation is single valued, this
means that $t$ does not evaluate to a term of the form $\inlterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be the unjustification; it must be either a primitive rule
or a tactic.
If $j$ is a primitive rule, then $\evalsto
{\inlterm{t''}}$
for some term $t''$. Since evaluation is single valued, this
means that $t'$ does not evaluate to a term of the form $\inrterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be a tactic; it must be a primitive rule too.
Furthermore, $t'' \repsrelfor
j$ and
$t'' \repsrelfor
j'$ must both hold. Since
$\repsrelfor
$ is a representation relation for the class of
primitive rules, we can conclude that $j$ is $j'$.
If $j$ is a pre-proof of height $i$ or less, then
$\evalsto
{\inrterm{t''}}$
for some term $t''$. Since evaluation is single valued, this
means that $t'$ does not evaluate to a term of the form $\inlterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be a primitive rule; it must be a
pre-proof of height $i$ or less too.
Furthermore, $t'' \repsrelfor
j$ and
$t'' \repsrelfor
j'$ must both hold. Since
$\repsrelfor
$ is a representation relation for the class of
pre-proofs of height or less, we can conclude that $j$ is $j'$.
Thus, it must always be the case that whenever both
$t \repsrelfor
j$ and
$t \repsrelfor
j'$ hold, $j$ and $j'$ are identical.
Now suppose that $t \repsrelfor
j$ holds
and $t \squiggle t'$. If $j$ is the unjustification, then
$\evalsto
{\inlterm{s}}$. Since $t \squiggle t'$,
$\evalsto
{\inlterm{s'}}$ for some term $s'$ such that $s \squiggle s'$.
Also, $s \repsrelfor
j$. Therefore, since $\repsrelfor
$ is
computationally closed, $s' \repsrelfor
j$.
Therefore, $t' \repsrelfor
j$. If $j$ is a primitive rule,
then $\evalsto
{\inrterm{s}}$. Since $t \squiggle t'$,
$\evalsto
{\inrterm{s'}}$ for some term $s'$ such that $s \squiggle s'$.
Furthermore, $\evalsto
{\inlterm{r}}$, and so, since $s \squiggle s'$,
$\evalsto
{\inlterm{r'}}$ for some term $r'$ such that $r \squiggle r'$.
Also, $r \repsrelfor
j$. Therefore, since $\repsrelfor
$
is computationally closed, $r' \repsrelfor
j$.
Therefore, $t' \repsrelfor
j$. If $j$ is a
pre-proof of height $i$ or less, then $\evalsto
{\inrterm{s}}$.
Since $t \squiggle t'$, $\evalsto
{\inrterm{s'}}$ for some term $s'$
such that $s \squiggle s'$.
Furthermore, $\evalsto
{\inrterm{r}}$, and so, since $s \squiggle s'$,
$\evalsto
{\inrterm{r'}}$ for some term $r'$ such that $r \squiggle r'$.
Also, $r \repsrelfor
j$. Therefore, since
$\repsrelfor
$ is computationally closed,
$r' \repsrelfor
j$. Therefore,
$t' \repsrelfor
j$.
Now, we can show that if $p$ is a pre-proof of
height $i$, the relation $t \repsrelfor
p$ holds
if and only if $k \ge i$ and $t \repsrelfor
p$.
Likewise, we show that if $j$ is a justification of height $i$ or
less the relation $t \repsrelfor
p$ holds
if and only if $k \ge i$ and $t \repsrelfor
p$.
To do this, we introduce a relation which is the restriction of
$\repsrelfor
$ to pre-proofs of height
$l$ or less. We define the relation
$t \repsrelfor
p$ to hold if and only if $p$ is of
height $k$ or less, and $t \repsrelfor
p$.
Similarly, we define
$t \repsrelfor
j$ to hold if and only if $j$ is of
height $k$ or less, and $t \repsrelfor
j$.
We show that if $l \le k$ then $\repsrelfor
$
is $\repsrelfor
$, and $\repsrelfor
$
is $\repsrelfor
$.
Our proof is by induction on $l$. If $l$ is $0$, then
since there are no pre-proofs of height $0$,
$\repsrelfor
$ is empty for any $l$.
$\repsrelfor
$ is empty by definition.
We conclude that $\repsrelfor
$ and
$\repsrelfor
$ are identical.
Now suppose that $l = m + 1$. Since $k \ge l$,
let $k = n + 1$, with $n \ge m$. We must show that
$\repsrelfor{\preproof_
^{m+1}}$ is
$\repsrelfor{\preproof_{m+1}}$.
The relation $\repsrelfor{\preproof_
^{m}}$ is
the restriction of $\repsrelfor{\preproof_{n}}$ to
pre-proofs of height $m$ or less. Thus, by theorem~\ref{},
$\repsrelforseq{\preproof_
^m}$ to
$\repsrelforseq{\preproof_{n}}$ to
sequences of pre-proofs of height $m$ or less.
We also know that the relation $\repsrelfor{\justification_
^{m}}$ is
the restriction of $\repsrelfor{\justification_{n}}$ to
justifications of height $m$ or less.
Using theorem~\ref{}, we can conclude that
${\repsrelfor{\justification_n^m}} \times
{\repsrelforseq{\preproof_n^m}}$ is the restriction of
${\repsrelfor{\justification_n}} \times
{\repsrelforseq{\preproof_n}}$ to
objects consisting of a justification of height $m$ or less
together with a finite sequence of pre-proofs of height
$m$ or less. Using theorem~\ref{} again, we can conclude that
$\repsrelfor
\times
({\repsrelfor{\justification_n^m}} \times
{\repsrelforseq{\preproof_n^m}})$ is the restriction of
$\repsrelfor
\times ({\repsrelfor{\justification_n}} \times
{\repsrelforseq{\preproof_n}})$ to objects consisting of
a sequent together with an object consisting of
a justification of height $m$ or less
together with a finite sequence of pre-proofs of height
$m$ or less. That is, it is the restriction of
$\repsrelfor{\preproof_{n+1}}$ to pre-proofs of height $m+1$ or less,
which is the relation $\repsrelfor{\preproof_
^{m+1}}$.
But by the induction hypothesis
$\repsrelfor{\preproof_
^{m}}$ is $\repsrelfor{\preproof_{m}}$ and
$\repsrelfor{\justification_
^{m}}$ is $\repsrelfor{\justification_{m}}$.
This means that
$\repsrelfor
\times
({\repsrelfor{\justification_n^m}} \times
{\repsrelforseq{\preproof_n^m}})$ is
$\repsrelfor
\times ({\repsrelfor{\justification_m}} \times
{\repsrelforseq{\preproof_m}})$. That is, it is
$\repsrelfor{\preproof_{m+1}}$. Therefore, by transitivity,
$\repsrelfor{\preproof_
^{m+1}}$ is $\repsrelfor{\preproof_{m+1}}$.
If $j$ is the unjustification, it is of height $0$. Thus
since $l \ge 0$, the relation $t \repsrelfor
j$
holds if and only if $t \repsrelfor
j$ holds.
This holds if and only if $\evalsto
{\inlterm{t'}}$ and
$t' \repsrelfor
j$, since $j$ is the unjustification.
But then, $t \repsrelfor
j$ holds for any $l$.
If $j$ is a primitive rule, it is of height $0$. Thus
since $l \ge 0$, the relation $t \repsrelfor
j$
holds if and only if $t \repsrelfor
j$ holds.
This holds if and only if $\evalsto
{\inrterm{t'}}$,
$\evalsto
{\inlterm{t''}}$ and
$t'' \repsrelfor
j$, since $j$ is a primitive rule
But then, $t \repsrelfor
j$ holds for any $l$.
Finally, suppose $j$ is a pre-proof. The relation
$t \repsrelfor
j$ holds if and only if
$t \repsrelfor
j$ holds and $j$ is a pre-proof
of height $l$ or less. Thus, it holds if and only if
$\evalsto
{\inrterm{t'}}$,
$\evalsto
{\inrterm{t''}}$ and
$t'' \repsrelfor
j$,
and $j$ is of height $l$ or less.
We can combine the last two conditions as $t'' \repsrelfor
j$.
Since $l \le k$, this is equivalent to $t'' \repsrelfor
j$.
Therefore, $t \repsrelfor
j$.
Now if $p$ is of height $l$, and $k \ge l$, we
know that $t \repsrelfor
p$ holds if and only if
$t \repsrelfor
p$ holds, and that this holds if
and only if $t \repsrelfor
p$ holds. And if $k < l$,
then since $k \le k$, $t \repsrelfor
p$ holds if and only if
$t \repsrelfor
p$ holds. But since $p$ is of height $l > k$,
it does not. Therefore, for any $k$, $t \repsrelfor
p$ holds
if and only if $k \ge l$ and $t \repsrelfor
p$. Similarly,
for any $k$, $t \repsrelfor
p$ holds
if and only if $k \ge l$ and $t \repsrelfor
p$.
This allows us to conclude that if $p$ is a pre-proof of
height $i$, $t \repsrelfor
p$ holds
if and only if $t \repsrelfor
p$ does.
For suppose that $t \repsrelfor
p$ holds,
then it must be the case, by definition, that
$t \repsrelfor
p$ holds. But this can only be the case if
$j \ge i$ and $t \repsrelfor
p$. The converse is trivial.
In a similar fashion, we can conclude that if $j$ is a
justification of height $i$ or less, the relation
$t \repsrelfor
p$ holds
if and only if $t \repsrelfor
p$ does.
If $p$ is a pre-proof, then it is a pre-proof of some height $i$.
Since $\repsrelfor
$ is a representation relation for
pre-proofs of height $i$ or less, there is a closed term
$t$ such that $t \repsrelfor
p$. Then,
$t \repsrelfor
p$.
If $t \repsrelfor
p$ and
$t \repsrelfor
p'$ for pre-proofs $p$ and $p'$, let
$i$ be the height of $p$ and $i'$ be the height of $p'$.
We can conclude that $t \repsrelfor
p$ and
$t \repsrelfor{\preproof_{i'}} p'$. Let $k = \max(i, i')$.
Since $k \ge i$, $t \repsrelfor
p$ holds if and only if
$t \repsrelfor
p$ does. But by our discussion above,
$t \repsrelfor
p$ holds
if and only if $t \repsrelfor
p$ does.
Since the latter relation is satisfied, we conclude that
$t \repsrelfor
p$. Similarly,
$t \repsrelfor
p'$. But $\repsrelfor
$
is a representation relation for pre-proofs of height $k$ or less.
Both $p$ and $p'$ are pre-proofs height $k$ or less. We conclude that
$p$ is $p'$.
Suppose $t \repsrelfor
p$ and
$t \squiggle t'$. Let $i$ be the height of $p$.
Then $t \repsrelfor
p$. But then,
since $\repsrelfor
$ is computationally closed,
$t' \repsrelfor
p$. Therefore,
$t' \repsrelfor
p$. This completes our proof that
$\repsrelfor
$ is a computationally closed representation relation
for the class of pre-proofs.
In a similar fashion, we can show that $\repsrelfor
$
is a computationally closed representation relation for the class
of justifications. We could also show that
the relation $\repsrelfor
$ is the smallest relation $R$ such that
$t \mathrel
p$ if and only if
[
t \mathrel{{\repsrelfor{\sequentclass}} \times
({\repsrelfor{\justification}}
\times {\repsrelforseq
)}} p,
]
but doing so would lead us too far astray.
We can simultaneously define representation functions
for the classes of pre-proofs and of justifications.
\begin
The function $\repfunfor
(j)$ maps justifications $j$ to
terms. If $j$ is the unjustification,
[
\repfunfor
(j) =
\inlterm{\repfunfor
(j)}.
]
If $j$ is a primitive rule,
[
\repfunfor
(j) =
\inrterm{\inlterm{\repfunfor
(j)}}.
]
If $j$ is a tactic rule,
[
\repfunfor
(j) =
\inrterm{\inrterm{\repfunfor
(j)}}.
]
The function $\repfunfor
(p)$ maps pre-proofs $p$ to
terms. It is defined by
[
\repfunfor
(p) =
(\repfunfor
\times
(\repfunfor
\times
\repfunforseq
))(p)
]
\end
\begin
The function $\repfunfor
$ is a representation function
for the relation $\repsrelfor
$. The function
$\repfunfor
$ is a representation function
for the relation $\repsrelfor
$.
\end
First, we show by induction on $i$ that
$\repfunfor
$ is a representation function
for the relation $\repsrelfor
p$.
Likewise, we show that $\repfunfor
$
is a representation function for the relation $\repsrelfor
$
Since there are no pre-proofs of height $0$,
if $p$ is a pre-proof of height $0$,
$\repfunfor
(p) \repsrelfor
p$.
Thus, $\repfunfor
$ is a representation function for
the relation $\repsrelfor
$.
Now suppose $i = n + 1$.
By the induction hypothesis,
$\repfunfor
$ is a representation function
for the relation $\repsrelfor
$.
But then by theorem~\ref{},
$\repfunforseq
$ is a representation function
for the relation $\repsrelforseq
$.
Also by the induction hypothesis,
$\repfunfor
$ is a representation function
for the relation $\repsrelfor
$.
So by theorem~\ref{},
$\repfunfor
\times
\repfunforseq
$
is a representation function for the relation
${\repsrelfor{\justification_n}} \times
{\repsrelforseq{\preproof_n}}$.
Using theorem~\ref{} again, we conclude that
[
\repfunfor
(p) =
(\repfunfor
\times
(\repfunfor
\times
\repfunforseq
))
]
is a representation function for the relation
[
{\repsrelfor{\preproof_
}} =
{\repsrelfor{\sequentclass}} \times
({\repsrelfor{\justification_n}} \times
{\repsrelforseq{\preproof_n}}).
]
If $j$ is an unjustification,
$\repfunfor
(j) = \inlterm{\repfunfor
(j)}$.
But $\repfunfor
(j) \repsrelfor
j$. Therefore,
since $\inl$ is value producing,
$\repfunfor
(j) \repsrelfor
j$ for any
natural number $i$.
If $j$ is a primitive rule
$\repfunfor
(j) = \inrterm{\inlterm{\repfunfor
(j)}}$.
But $\repfunfor
(j) \repsrelfor
j$. Therefore,
since $\inl$ and $\inr$ are value producing,
$\repfunfor
(j) \repsrelfor
j$ for any
natural number $i$.
If $j$ is a tactic pre-proof of height $i$ or less,
$\repfunfor
(j) = \inrterm{\inrterm{\repfunfor
(j)}}$.
But $\repfunfor
(j) \repsrelfor
j$. Therefore,
since $\inr$ is value producing,
$\repfunfor
(j) \repsrelfor
j$.
Now suppose that $p$ is a pre-proof. let $n$ be the height of $p$.
We have shown that $\repfunfor
(p) \repsrelfor
p$.
But then, $\repfunfor
(p) \repsrelfor
p$.
Likewise, if $j$ is a justification, let $n$ be the height of $j$.
We have shown that
$\repfunfor
(j) \repsrelfor
j$.
But then, $\repfunfor
(j) \repsrelfor
j$.
The unjustification functions are similar.
\begin
The partial function $\unrepfunfor
(s)$ maps
closed terms $s$ to justifications.
If $\eval(s)$ is $\inlterm
$ then
[
\unrepfunfor
(s) =
\unrepfunfor
(s').
]
If $\eval(s)$ is $\inrterm
$ and
$\eval(s')$ is $\inlterm
$ then
[
\unrepfunfor
(s) =
\unrepfunfor
(s'')
]
If $\eval(s)$ is $\inrterm
$ and
$\eval(s')$ is $\inrterm
$ then
[
\unrepfunfor
(s) =
\unrepfunfor
(s'')
]
The partial function $\unrepfunfor
(t)$
maps terms $t$ to pre-proofs. It is defined by
[
\unrepfunfor
(t) =
(\unrepfunfor
\times
(\unrepfunfor
\times
\unrepfunforseq
))(t)
]
\end
\begin
The partial function $\unrepfunfor
$ is an `
unrepresentation function
for the relation $\repsrelfor
$. The partial function
$\unrepfunfor
$ is an unrepresentation function
for the relation $\repsrelfor
$.
\end
First, we show by induction on $i$ that
$\unrepfunfor
$ is an unjustification function for the relation
$\repsrelfor
$.
Likewise, we show that
$\unrepfunfor
$ is an unjustification function for the relation
$\repsrelfor
$.
Since $\repsrelfor
$ is empty, if
$t \repsrelfor
p$, then $\unrepfunfor
(t) = p$.
Now suppose $i = n + 1$.
By the induction hypothesis,
$\unrepfunfor
$ is a representation function
for the relation $\repsrelfor
$.
But then by theorem~\ref{},
$\unrepfunforseq
$ is a representation function
for the relation $\repsrelforseq
$.
Also by the induction hypothesis,
$\unrepfunfor
$ is a representation function
for the relation $\repsrelfor
$.
So by theorem~\ref{},
$\unrepfunfor
\times
\unrepfunforseq
$
is a representation function fro the relation
${\repsrelfor{\justification_n}} \times
{\repsrelforseq{\preproof_n}}$.
Using theorem~\ref{} again, we conclude that
[
\unrepfunfor
(p) =
(\unrepfunfor
\times
(\unrepfunfor
\times
\unrepfunforseq
))
]
is a representation function for the relation
[
{\repsrelfor{\preproof_
}} =
{\repsrelfor{\sequentclass}} \times
({\repsrelfor{\justification_n}} \times
{\repsrelforseq{\preproof_n}}).
]
Suppose that $s \repsrelfor
j$.
If $j$ is an unjustification, then
$\evalsto
{\inlterm{s'}}$, and $s' \repsrelfor
j$.
But then, by the definition of $\eval$, $\eval(s)$ is $\inlterm
$.
This means that $\unrepfunfor
(s)$ is
$\unrepfunfor
(s')$. But $\unrepfunfor
$ is an
unrepresentation function for the relation $\repsrelfor
$.
We conclude that $\unrepfunfor
(s') = j$.
If $j$ is a primitive rule, then
$\evalsto
{\inrterm{s'}}$, $\evalsto
{\inlterm{s''}}$,
and $s'' \repsrelfor
j$.
But then, by the definition of $\eval$, $\eval(s)$ is $\inrterm
$.
and $\eval(s')$ is $\inlterm
$.
This means that $\unrepfunfor
(s)$ is
$\unrepfunfor
(s'')$. But $\unrepfunfor
$ is an
unrepresentation function for the relation $\repsrelfor
$.
We conclude that $\unrepfunfor
(s'') = j$.
If $j$ is a tactic of height $i$ or less, then
$\evalsto
{\inrterm{s'}}$, $\evalsto
{\inrterm{s''}}$,
and $s'' \repsrelfor
j$.
But then, by the definition of $\eval$, $\eval(s)$ is $\inrterm
$.
and $\eval(s')$ is $\inrterm
$.
This means that $\unrepfunfor
(s)$ is
$\unrepfunfor
(s'')$. But $\unrepfunfor
$ is an
unrepresentation function for the relation $\repsrelfor
$.
We conclude that $\unrepfunfor
(s'') = j$.
Now suppose that $p$ is a pre-proof, and that
$t \repsrelfor
p$. Let $n$ be the height of $p$.
Then, $t \repsrelfor
p$. But then
$\unrepfunfor
(t) = p$. Similarly,
if $j$ is a justification, and $s \repsrelfor
j$,
then let $n$ be the height of $j$, conclude that
$s \repsrelfor
j$, and so that
$\unrepfunfor
(s) = j$.
As usual, we use the Nuprl $\rec$ type constructor to
define a type to represent a class of tree structured objects.
\begin
[
\PreProof \abstreq
\recterm
{\indepproducttype
{(\indepproducttype{\uniontype
{(\uniontype
)}}{\listtype{p}})}}
]
\end
\begin
The type $\PreProof$, as just defined, represents the class of
pre-proofs.
\end
To prove this theorem, we define two indexed families of types
$Q_i$ and $J_i$, each indexed by natural numbers $i$.
It can be shown that $t$ and $t'$ are equal members of $\PreProof$
if and only if they are equal members of $Q_n$, for some natural number $n$.
We show, by induction on $i$, that, for each natural number $i$,
the type $Q_i$ represents the class of pre-proofs of height $i$ or less
using the relation $\repsrelfor
$. In passing, we prove that
$J_i$ represents the class of justifications of height $i$ or less
using the relation $\repsrelfor
$.
\begin
Q_0 &=& \voidtype
Q_
&=& \indepproducttype
{(\indepproducttype
{\listtype{Q_i}})}
J_i &=& \uniontype
{(\uniontype
)}
\end
We show, by induction on $i$, that $Q_i$ represents the class
of pre-proofs of height $i$ or less, and, simultaneously, that $J_i$
represents the class of justifications of height $i$ or less.
If $i = 0$, then $Q_i$ is $\voidtype$. $\voidtype$ is empty, so
two terms are never equal in $Q_0$. Thus, if $t$ and $t'$ are equal members
of $Q_0$, there is a pre-proof $p$ such that $t \repsrelfor
p$ and
$t' \repsrelfor
p$. Conversely, $\repsrelfor
$ is
empty too. This means that it is never the case that
$t \repsrelfor
p$ for any closed term $t$. From
this we can conclude that if both $t \repsrelfor
p$ and
$t' \repsrelfor
p$ hold then $t$ and $t'$ are equal
members of $Q_0$.
If $i = n+1$, then $Q_i$ is
$\indepproducttype
{(\indepproducttype
{\listtype{Q_n}})}$.
By the induction hypothesis, $J_n$ represents the class of
justifications of height $n$ or less using the relation
$\repsrelfor
$, and $Q_n$ represents the class of
pre-proofs of height $n$ or less using the relation $\repsrelfor
$.
$\Sequent$ represents the class of sequents using the relation
$\repsrelfor
$.
Using theorem~\ref{} (twice) we conclude
that $Q_
$ represents the class of objects consisting of a sequent,
and an object consisting of a justification of height $n$ or less,
together with a finite sequence of pre-proofs of height $n$ or less.
$Q_i$ does so using the relation
$ {\repsrelfor{\sequentclass}} \times
({\repsrelfor{\justification_i}}\times{\repsrelfor{\preproof_i}})$.
That is to say, $Q_
$ represents the class of pre-proofs
of height $n+1$ or less using the relation $\repsrelfor{\preproof_{n+1}}$.
Suppose two terms $t$ and $t'$ are equal members of
$J_i$. Either both $\evalsto
{\inlterm{s}}$ and
$\evalsto
{\inlterm{s'}}$ hold for terms $s$ and $s'$ equal in
$\unittype$, or both $\evalsto
{\inrterm{s}}$ and
$\evalsto
{\inrterm{s'}}$ hold for terms $s$ and $s'$ equal in
$\uniontype
$.
In the first case, since
$\unittype$ represents the class of unjustifications
using the relation $\repsrelfor
$, we can conclude that
both $s$ and $s'$ represent the same unjustification $j$. But then
Both $t \repsrelfor
j$ and
$t' \repsrelfor
j$ hold.
In the second case, Either both $\evalsto
{\inlterm{r}}$ and
$\evalsto
{\inlterm{r'}}$ hold for terms $r$ and $r'$ equal in
$\PrimRule$, or both $\evalsto
{\inrterm{r}}$ and
$\evalsto
{\inrterm{r'}}$ hold for terms $r$ and $r'$ equal in
$Q_i$.
In the first subcase, since
$\PrimRule$ represents the class of primitive rules
using the relation $\repsrelfor
$, we can conclude that
both $r$ and $r'$ represent the same primitive rule $j$. But then
Both $t \repsrelfor
j$ and
$t' \repsrelfor
j$ hold.
In the second subcase, since
$Q_i$ represents the class of pre-proofs of height $i$ or less
using the relation $\repsrelfor
$, we can conclude that
both $r$ and $r'$ represent the same pre-proof $j$. But then
Both $t \repsrelfor
j$ and
$t' \repsrelfor
j$ hold.
Conversely, suppose that both $t \repsrelfor
j$ and
$t' \repsrelfor
j$ hold for some justification $j$ of
height $i$ or less.
If $j$ is the unjustification, then both
$\evalsto
{\inlterm{s}}$ and
$\evalsto
{\inlterm{s'}}$ hold for terms $s$ and $s'$
such that $s \repsrelfor
j$ and $s' \repsrelfor
j$.
Since
$\unittype$ represents the class of unjustifications
using the relation $\repsrelfor
$, we can conclude that
$s$ and $s'$ are equal members of $\unittype$. We conclude that
$t$ and $t'$ are equal members of $J_i$.
If $j$ is a primitive rule, then
$\evalsto
{\inrterm{s}}$ and
$\evalsto
{\inrterm{s'}}$ hold for terms $s$ and $s'$
such that
$\evalsto
{\inlterm{r}}$ and
$\evalsto
{\inlterm{r'}}$ hold for terms $r$ and $r'$
such that $r \repsrelfor
j$ and $r' \repsrelfor
j$.
Since $\PrimRule$ represents the class of primitive rules
using the relation $\repsrelfor
$, we can conclude that $r$ and $r'$
are equal members of $\PrimRule$. From this we deduce that
$s$ and $s'$ are equal members of $\uniontype
$, and so that
$t$ and $t'$ are equal members of $J_i$.
Otherwise, $j$ is a pre-proof of height $i$ or less.
$\evalsto
{\inrterm{s}}$ and
$\evalsto
{\inrterm{s'}}$ hold for terms $s$ and $s'$
such that
$\evalsto
{\inrterm{r}}$ and
$\evalsto
{\inrterm{r'}}$ hold for terms $r$ and $r'$
such that $r \repsrelfor
j$ and $r' \repsrelfor
j$.
Since $Q_i$ represents the class of pre-proofs of height $i$ or less
using the representation relation $\repsrelfor
$,
we can conclude that $r$ and $r'$ are equal members of $Q_i$.
From this we deduce that $t$ and $t'$ are equal members of $J_i$.
Now suppose that $t$ and $t'$ are equal members of
$\PreProof$. In chapter~\ref{} we show that this implies that they
are equal members of $Q_i$ for some $i$. Since $Q_i$ represents
the class of pre-proofs of height $i$ or less using the relation
$\repsrelfor
$, we can conclude that
$t \repsrelfor
p$ and $t' \repsrelfor
p$
for some pre-proof $p$ of height $i$ or less. But then $p$ is a pre-proof,
and then $t \repsrelfor
p$ and $t' \repsrelfor
p$
both hold.
Conversely, suppose that $t \repsrelfor
p$
and $t' \repsrelfor
p$ both hold for some pre-proof $p$.
Let $i$ be the height of $p$. Then $t \repsrelfor
p$
and $t' \repsrelfor
p$. Since $Q_i$ represents
the class of pre-proofs of height $i$ or less using the relation
$\repsrelfor
$, we can conclude that $t$ and $t'$ are equal members
of $Q_i$. In chapter~\ref{} we show that this implies that they are
equal members of $\PreProof$.
We now define an operator $\PPind$ to represent primitive
recursion on pre-proofs. For certain definitions, among them, the
definition of $\Foo$ we want to use the fact that tactic justifications
are sub-pre-proofs of the pre-proofs in which they appear. For this reason,
we modify the definition of $\PPind$ somewhat, so that it has four sub-terms:
one for the pre-proof argument, and one to tell what is to be done for
each sort of justification. The resulting abstraction definition
is large, but not terribly complex.
\begin
[
\begin
\PPindgen\argleft
\PPindtermb
\argsemi
\hphantom
\PPindtermc
\argsemi
\hphantom
\PPindtermd
\argright \abstreq {}
\qquad
\lambda f\argcomma p\argdot
\proglet{\pairterm
{\pairterm
}}
\progin{}
\qquad\qquad
\progcase
{\inlterm{u}}
\qquad\qquad\qquad
{t_u[g\argsemi u\argsemi\argsemi
\lengthterm
\argsemi\lambda n\argdot \nthterm
\argsemi
\lambda n\argdot f(\nthterm
)]}
\qquad\qquad
\orcase{\inrterm{\inlterm
}}
\qquad\qquad\qquad
{t_r[g\argsemi r\argsemi\argsemi
\lengthterm
\argsemi\lambda n\argdot \nthterm
\argsemi
\lambda n\argdot f(\nthterm
)]}
\qquad\qquad
\orcase{\inrterm{\inrterm
}}
\qquad\qquad\qquad
{t_t[g\argsemi t\argsemi\argsemi
\lengthterm
\argsemi\lambda n\argdot \nthterm
\argsemi
\lambda n\argdot f(\nthterm
)\argsemi f(t)]}
\PPind\argleft p\argsemi
\PPindtermb
\argsemi
\hphantom
\PPindtermc
\argsemi
\hphantom
\PPindtermd
\argright \abstreq {}
\qquad\ycomb
\PPindgen\argleft
\PPindtermb
\argsemi
\hphantom
\PPindtermc
\argsemi
\hphantom
\PPindtermd
\argright (p)
\end
]
\end
We can state the usual theorems characterizing this operator.
\begin
Let $
(p, a_1, \ldots, a_n)$ be an operation which maps
pre-proofs $p$, and objects $a_1$, \dots, $a_n$ chosen from classes
$
_1$, \dots, $
_n$ respectively to objects of $\cal B$.
Let $
_u(g, j, \sequence
, a_1, \ldots, a_n)$ be an
operation which maps sequents $g$, unjustifications $j$, sequences
$\sequence
$ of pre-proofs, and objects $a_1$, \dots, $a_n$ chosen
from classes $
_1$, \dots, $
_n$ respectively to objects
of $\cal B$.
Let $
_r(g, j, \sequence
, a_1, \ldots, a_n)$ be an
operation which maps sequents $g$, primitive rules $j$, sequences
$\sequence
$ of pre-proofs, and objects $a_1$, \dots, $a_n$ chosen
from classes $
_1$, \dots, $
_n$ respectively to objects
of $\cal B$.
Let $
_t(g, j, \sequence
, a_1, \ldots, a_n)$ be an
operation which maps sequents $g$, pre-proofs $j$, sequences
$\sequence
$ of pre-proofs, and objects $a_1$, \dots, $a_n$ chosen
from classes $
_1$, \dots, $
_n$ respectively to objects
of $\cal B$.
Suppose that for any pre-proof
$p = \langle g, \langle j, \sequence
\rangle\rangle$
in which $j$ is an unjustification,
$
(p, a_1, \ldots, a_n)
=
_u(g, j, \sequence
, a_1, \ldots, a_n)$.
Likewise, if $j$ is a primitive rule,
$
(p, a_1, \ldots, a_n)
=
_r(g, j, \sequence
, a_1, \ldots, a_n)$.
And if $j$ is a pre-proof,
$
(p, a_1, \ldots, a_n)
=
_t(g, j, \sequence
, a_1, \ldots, a_n)$.
Suppose that whenever each of the following conditions holds,
$\subst
(t_
)\ldots(t_
)$
represents $
_u(g, j, (s_1,\ldots,s_m), a_1,\ldots,a_n)$.
\begin
\item
$t_g$ represents the sequent $g$.
\item
$t_j$ represents the unjustification $j$.
\item
$t_m$ represents the natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ represents $i$ then $t_s(t_i)$ represents the pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ represents $i$, $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$t_h(t_i)(t_
)\ldots(t_
)$ represents
$
(s_i, a_1, \ldots, a_n)$.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
Likewise, suppose that whenever each of the following conditions holds,
$\subst
(t_
)\ldots(t_
)$
represents $
_r(g, j, (s_1,\ldots,s_m), a_1,\ldots,a_n)$.
\begin
\item
$t_g$ represents the sequent $g$.
\item
$t_j$ represents the primitive rule $j$.
\item
$t_m$ represents the natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ represents $i$ then $t_s(t_i)$ represents the pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ represents $i$, $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$t_h(t_i)(t_
)\ldots(t_
)$ represents
$
(s_i, a_1, \ldots, a_n)$.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
And suppose that whenever each of the following conditions holds,
$\subst
(t_
)\ldots(t_
)$
represents $
_t(g, j, (s_1,\ldots,s_m), a_1,\ldots,a_n)$.
\begin
\item
$t_g$ represents the sequent $g$.
\item
$t_j$ represents the pre-proof $j$.
\item
$t_m$ represents the natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ represents $i$ then $t_s(t_i)$ represents the pre-proof $s_i$.\
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ represents $i$, $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$t_h(t_i)(t_
)\ldots(t_
)$ represents
$
(s_i, a_1, \ldots, a_n)$.
\item
For all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$t_x(t_
)\ldots(t_
)$ represents
$
(j, a_1 \ldots, a_n)$.
\item
$t_
$ represents the object $a_1$ of $
_1$, \dots, and
$t_
$ represents the object $a_n$ of $
_n$.
\end
Then if $t_p$ represents the pre-proof $p$,
$t_
$ represents the object $a_1$ of $
_1$, \dots, and
$t_
$ represents the object $a_n$ of $
_n$, the term
[
\PPindtermx
{{g_u}
{t_u}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}(t_
)\ldots
(t_
)
]
represents $
(p, a_1, \ldots, a_n)$.
\end
\begin
Let $\Phi(p, a_1, \ldots, a_n)$ be a predicate on
pre-proofs $p$, and objects $a_1$, \dots, $a_n$ chosen from classes
$
_1$, \dots, $
_n$ respectively.
Let $\Phi_u(g, j, \sequence
, a_1, \ldots, a_n)$ be a predicate
on sequents $g$, unjustifications $j$, sequences
$\sequence
$ of pre-proofs, and objects $a_1$, \dots, $a_n$ chosen
from classes $
_1$, \dots, $
_n$ respectively.
Let $\Phi_r(g, j, \sequence
, a_1, \ldots, a_n)$ be a predicate
on sequents $g$, primitive rules $j$, sequences
$\sequence
$ of pre-proofs, and objects $a_1$, \dots, $a_n$ chosen
from classes $
_1$, \dots, $
_n$ respectively.
Let $\Phi_t(g, j, \sequence
, a_1, \ldots, a_n)$ be a predicate
on sequents $g$, pre-proofs $j$, sequences
$\sequence
$ of pre-proofs, and objects $a_1$, \dots, $a_n$ chosen
from classes $
_1$, \dots, $
_n$ respectively.
Suppose that for any pre-proof
$p = \langle g, \langle j, \sequence
\rangle\rangle$
in which $j$ is an unjustification,
$\Phi(p, a_1, \ldots, a_n)$ holds if and only if
$\Phi_u(g, j, \sequence
, a_1, \ldots, a_n)$ does.
Likewise, if $j$ is a primitive rule
$\Phi(p, a_1, \ldots, a_n)$ holds if and only if
$\Phi_r(g, j, \sequence
, a_1, \ldots, a_n)$ does.
And if $j$ is a pre-proof,
$\Phi(p, a_1, \ldots, a_n)$ holds if and only if
$\Phi_t(g, j, \sequence
, a_1, \ldots, a_n)$ does.
Suppose that whenever each of the following conditions holds,
the terms
$\subst
(t_
)\ldots(t_
)$
and $\subst
(t'_
)\ldots(t'_
)$
are equal types which are inhabited if and only if
$\Phi_u(g, j, (s_1,\ldots,s_m), a_1,\ldots,a_n)$ holds
\begin
\item
$t_g$ and $t'_g$ represent the same sequent $g$.
\item
$t_j$ and $t'_j$ represent the same unjustification $j$.
\item
$t_m$ and $t'_m$ represent the same natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ and $t'_i$ both represent $i$ then
both $t_s(t_i)$ and $t'_s(t'_i)$ represent the same pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ and $t'i$ both represent $i$, $t
$ and $t'_
$ both represent
$a_1$, \dots, and
$t_
$ and $t'_
$ both represent $a_n$, then
$t_h(t_i)(t_
)\ldots(t_
)$ and
$t'h(t'_i)(t'
)\ldots(t'_
)$ are
equal types which are inhabited if and only if
$\Phi(s_i, a_1, \ldots, a_n)$ holds.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
Likewise, suppose that whenever each of the following conditions holds,
the terms
$\subst
(t_
)\ldots(t_
)$
and $\subst
(t'_
)\ldots(t'_
)$
are equal types which are inhabited if and only if
$\Phi_r(g, j, (s_1,\ldots,s_m), a_1,\ldots,a_n)$ holds
\begin
\item
$t_g$ and $t'_g$ represent the same sequent $g$.
\item
$t_j$ and $t'_j$ represent the same primitive rule $j$.
\item
$t_m$ and $t'_m$ represent the same natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ and $t'_i$ both represent $i$ then
both $t_s(t_i)$ and $t'_s(t'_i)$ represent the same pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ and $t'i$ both represent $i$, $t
$ and $t'_
$ both represent
$a_1$, \dots, and
$t_
$ and $t'_
$ both represent $a_n$, then
$t_h(t_i)(t_
)\ldots(t_
)$ and
$t'h(t'_i)(t'
)\ldots(t'_
)$ are
equal types which are inhabited if and only if
$\Phi(s_i, a_1, \ldots, a_n)$ holds.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
And suppose that whenever each of the following conditions holds,
the terms
$\subst
(t_
)\ldots(t_
)$
and $\subst
(t'_
)\ldots(t'_
)$
are equal types which are inhabited if and only if
$\Phi_t(g, j, (s_1,\ldots,s_m), a_1,\ldots,a_n)$ holds
\begin
\item
$t_g$ and $t'_g$ represent the same sequent $g$.
\item
$t_j$ and $t'_j$ represent the same primitive rule $j$.
\item
$t_m$ and $t'_m$ represent the same natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ and $t'_i$ both represent $i$ then
both $t_s(t_i)$ and $t'_s(t'_i)$ represent the same pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ and $t'i$ both represent $i$, $t
$ and $t'_
$ both represent
$a_1$, \dots, and
$t_
$ and $t'_
$ both represent $a_n$, then
$t_h(t_i)(t_
)\ldots(t_
)$ and
$t'h(t'_i)(t'
)\ldots(t'_
)$ are
equal types which are inhabited if and only if
$\Phi(s_i, a_1, \ldots, a_n)$ holds.
\item
For all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_
$ and $t'_
$ both represent
$a_1$, \dots, and
$t_
$ and $t'_
$ both represent $a_n$, then
$t_x(t_
)\ldots(t_
)$ and
$t'x(t'
)\ldots(t'_
)$ are
equal types which are inhabited if and only if
$\Phi(j, a_1, \ldots, a_n)$ holds.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
Then if $t_p$ and $t'_p$ both represent the pre-proof $p$,
$t_
$ and $t'_
$ both represent the object $a_1$ of $
_1$,
\dots, and $t_
$ and $t'_
$ both represent the object $a_n$
of $
_n$, the terms
[
\PPindtermx
{{g_u}
{t_u}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}(t_
)\ldots
(t_
)
]
and
[
\PPindtermx
{{g'_u}
{t'_u}}
{{g'_r}
{t'_r}}
{{g'_t}
{t't}}(t'
)\ldots
(t'_
)
]
are equal types, and these types are inhabited if and only if
$\Phi(p, a_1, \ldots, a_n)$ holds.
\end
These two theorems are proved in roughly the same manner. The
proof of the second theorem is somewhat messier, since we have to carry
around two sets of terms which represent the various objects involved, but
isn't really any more difficult. For this reason, we prove only the first.
Our proof is by induction on the height of the pre-proof $p$. Since there
are no pre-proofs of height $0$, $t_p$ cannot represent a proof of height
$0$. Thus, the base case is vacuously true.
First, we note that the term
[
\PPindtermx
{{g_u}
{t_u}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}(t_
)\ldots
(t_
)
]
expands to the term
[
\ycomb \PPindgentermx{{g_u}
{t_u}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}(t_p)(t_
)\ldots
(t_
).
]
We replace terms of the form $\ycomb F$ with the computationally equivalent
$F(\ycomb F)$. We expand the first instance of $\PPindgen$ in the resulting
term. And we contract the resulting beta redices. IN this fashion,
we obtain the term
[
(\proglet{\pairterm
{\pairterm
}}
\progin{}
\progcase
{\inlterm{u}}
\subst
{g, u, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
)}
\orcase{\inrterm{\inlterm
}}
\subst
{g, r, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
)}
\orcase{\inrterm{\inrterm
}}
\subst
{g, t, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
), \ycomb F\; t}
)(t_
)\ldots(t_
).
]
Since $t_p$ represents a pre-proof it represents a pre-proof of
some height $k+ 1$. Thus, it represents an object
$\langle g, \langle j, (s_1, \ldots, s_m)\rangle\rangle$ for some sequent
$g$, justification $j$ and sequence of pre-proofs $(s_1, \ldots, s_m)$.
$j$ is of height $k$ or less, as are each of the pre-proofs $s_1$, \dots,
$s_m$. Thus, $t_p$ evaluates to a term $\pairterm
$ and
$t_y$ evaluates to a term $\pairterm
$ for some terms
$t_g$, $t_j$ and $t_s$ such that $t_g$ represents $g$,
$t_j$ represents the justification $j$, and $t_s$ represents
the sequence $(s_1, \ldots, s_n)$. For this reason a term of the form
$\proglet{\pairterm
{\pairterm
}}
\progin
$
is computationally equivalent to a term
$\subst
$.
If $j$ is an unjustification, $t_j$ evaluates to a term
$\inlterm
$ and $t'_j$ represents the unjustification $j$.
Then a term of the form $\progcase
{\inlterm{u}}
\mid\ldots$
is computationally equivalent to the term $\subst
$.
From this we conclude that the term displayed above is
computationally equivalent to the term
[
\subst
{t_g, t'_j, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
)}
(t_
)\ldots(t_
).
]
The term $\lengthterm
$ represents $m$, the length of the sequence
$(s_1, \ldots, s_m)$. Suppose $i$ is an integer between
$1$ and $m$, and that $t_i$ represents $i$. The term
$(\lambda n\argdot \nthterm
)(t_i)$, is computationally equivalent to
the corresponding beta contractum $\nthterm
$, which represents $s_i$
the $i$\/th element of the sequence $(s_1, \ldots, s_m)$.
Suppose too that $q_
$, \dots, $q_
$ represent
objects $a_1$, \dots, $a_n$ chosen from the classes
$
_1$, \dots, $
_n$. The term
$(\lambda n\argdot \ycomb F (\nthterm
))(t_i)(q_
)\ldots(q_
)$
is computationally equivalent to
$\ycomb F (\nthterm
)(q_
)\ldots(q_
)$.
But the term
[
\PPindtermx{\nthterm
{t_s}}{{g_u}
{t_u}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}
]
expands to the term $\ycomb F (\nthterm
)$.
Thus we can replace the latter term with the former.
This yields the term
[
\PPindtermx{\nthterm
{t_s}}{{g_u}
{t_u}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}(q_
)\ldots
(q_
).
]
Since $\nthterm
$ represents the pre-proof $s_i$ which is of height
$k$ or less, the induction hypothesis allows us to conclude that this term
represents $
(s_i, a_1, \ldots, a_n)$.
So we now know that the following conditions hold
\begin
\item $t_g$ represents the sequent $g$.
\item
$t'_j$ represents the unjustification $j$.
\item
$\lengthterm
$ represents the natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ represents $i$ then $(\lambda n\argdot\nthterm
)(t_i)$
represents the pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ represents $i$, $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$(\lambda n\argdot \ycomb F \nthterm
)(t_i)(t_
)\ldots(t_
)$ represents
$
(s_i, a_1, \ldots, a_n)$.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
Therefore,
[
\subst
{t_g, t'_j, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
)}
(t_
)\ldots(t_
).
]
represents $
_u(g, j, (s_1, \ldots, s_m), a_1, \ldots, a_n)$.
But $j$ is the unjustification, so
this is exactly $
(p, a_1, \ldots, a_n)$.
If $j$ is a primitive rule, $t_j$ evaluates to a term
$\inrterm
$, $t'_j$ evaluates to a term $\inlterm
$, and
$t''_j$ represents the primitive rule $j$.
Then a term of the form
$\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\mid\ldots$
is computationally equivalent to the term $\subst
$.
From this we conclude that the term displayed above is
computationally equivalent to the term
[
\subst
{t_g, t''_j, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
)}
(t_
)\ldots(t_
).
]
The term $\lengthterm
$ represents $m$, the length of the sequence
$(s_1, \ldots, s_m)$. Suppose $i$ is an integer between
$1$ and $m$, and that $t_i$ represents $i$. The term
$(\lambda n\argdot \nthterm
)(t_i)$, is computationally equivalent to
the corresponding beta contractum $\nthterm
$, which represents $s_i$
the $i$\/th element of the sequence $(s_1, \ldots, s_m)$.
Suppose too that $q_
$, \dots, $q_
$ represent
objects $a_1$, \dots, $a_n$ chosen from the classes
$
_1$, \dots, $
_n$. The term
$(\lambda n\argdot \ycomb F (\nthterm
))(t_i)(q_
)\ldots(q_
)$
is computationally equivalent to
$\ycomb F (\nthterm
)(q_
)\ldots(q_
)$.
But the term
[
\PPindtermx{\nthterm
{t_s}}{{g_r}
{t_r}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}
]
expands to the term $\ycomb F (\nthterm
)$.
Thus we can replace the latter term with the former.
This yields the term
[
\PPindtermx{\nthterm
{t_s}}{{g_r}
{t_r}}
{{g_r}
{t_r}}
{{g_t}
{t_t}}(q_
)\ldots
(q_
).
]
Since $\nthterm
$ represents the pre-proof $s_i$ which is of height
$k$ or less, the induction hypothesis allows us to conclude that this term
represents $
(s_i, a_1, \ldots, a_n)$.
So we now know that the following conditions hold
\begin
\item $t_g$ represents the sequent $g$.
\item
$t''_j$ represents the primitive rule $j$.
\item
$\lengthterm
$ represents the natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ represents $i$ then $(\lambda n\argdot\nthterm
)(t_i)$
represents the pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ represents $i$, $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$(\lambda n\argdot \ycomb F \nthterm
)(t_i)(t_
)\ldots(t_
)$ represents
$
(s_i, a_1, \ldots, a_n)$.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
Therefore,
[
\subst
{t_g, t''_j, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
)}
(t_
)\ldots(t_
).
]
represents $
_r(g, j, (s_1, \ldots, s_m), a_1, \ldots, a_n)$.
But $j$ is a primitive rule, so
this is exactly $
(p, a_1, \ldots, a_n)$.
Otherwise $j$ is a pre-proof. Then, $t_j$ evaluates to a term
$\inrterm
$, $t'_j$ evaluates to a term $\inrterm
$, and
$t''_j$ represents the pre-proof $j$. Note that since $j$ is
of height $k$ or less, so too is this pre-proof.
Then a term of the form
[
\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\orcase{\inrterm{\inrterm
}}
]
is computationally equivalent to the term $\subst
$.
From this we conclude that the term displayed above is
computationally equivalent to the term
[
\subst
{t_g, t''_j, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
),\ycomb F\;t''_j}
(t_
)\ldots(t_
).
]
The term $\lengthterm
$ represents $m$, the length of the sequence
$(s_1, \ldots, s_m)$. Suppose $i$ is an integer between
$1$ and $m$, and that $t_i$ represents $i$. The term
$(\lambda n\argdot \nthterm
)(t_i)$, is computationally equivalent to
the corresponding beta contractum $\nthterm
$, which represents $s_i$
the $i$\/th element of the sequence $(s_1, \ldots, s_m)$.
Suppose too that $q_
$, \dots, $q_
$ represent
objects $a_1$, \dots, $a_n$ chosen from the classes
$
_1$, \dots, $
_n$. The term
$(\lambda n\argdot \ycomb F (\nthterm
))(t_i)(q_
)\ldots(q_
)$
is computationally equivalent to
$\ycomb F (\nthterm
)(q_
)\ldots(q_
)$.
But the term
[
\PPindtermx{\nthterm
{t_s}}{{g_t}
{t_t}}
{{g_t}
{t_t}}
{{g_t}
{t_t}}
]
expands to the term $\ycomb F (\nthterm
)$.
Thus we can replace the latter term with the former.
This yields the term
[
\PPindtermx{\nthterm
{t_s}}{{g_t}
{t_t}}
{{g_t}
{t_t}}
{{g_t}
{t_t}}(q_
)\ldots
(q_
).
]
Since $\nthterm
$ represents the pre-proof $s_i$ which is of height
$k$ or less, the induction hypothesis allows us to conclude that this term
represents $
(s_i, a_1, \ldots, a_n)$.
Likewise, we can replace the term $\ycomb F\;t''_j$
with a term which expands to it:
[
\PPindtermx
{{g_t}
{t_t}}
{{g_t}
{t_t}}
{{g_t}
{t_t}}.
]
Doing so yields the term
[
\PPindtermx
{{g_t}
{t_t}}
{{g_t}
{t_t}}
{{g_t}
{t_t}}(q_
)\ldots
(q_
).
]
Since $t''_j$ represents the pre-proof $j$ which is of height
$k$ or less, the induction hypothesis allows to conclude that this
term represents $
(j, a_1, \ldots, a_n)$.
So we now know that the following conditions hold
\begin
\item $t_g$ represents the sequent $g$.
\item
$t''_j$ represents the pre-proof $j$
\item
$\lengthterm
$ represents the natural number $m$.
\item
For all integers $i$ such that $1\le i\le m$,
if $t_i$ represents $i$ then $(\lambda n\argdot\nthterm
)(t_i)$
represents the pre-proof $s_i$.
\item
For all integers $i$ such that $1\le i\le m$,
and for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_i$ represents $i$, $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$(\lambda n\argdot \ycomb F \nthterm
)(t_i)(t_
)\ldots(t_
)$ represents
$
(s_i, a_1, \ldots, a_n)$.
\item
for all elements $a_1$, \dots, $a_n$ of $
_1$, \dots, $
_n$,
if $t_
$ represents $a_1$, \dots, and
$t_
$ represents $a_n$, then
$\ycomb F (t''j)(t
)\ldots(t_
)$ represents
$
(j, a_1, \ldots, a_n)$.
\item
$a_1$ represents the object $a_1$ of $
_1$, \dots, and
$a_n$ represents the object $a_n$ of $
_n$.
\end
Therefore,
[
\subst
{t_g, t''_j, \lengthterm
, \lambda n\argdot \nthterm
,
\lambda n\argdot \ycomb F (\nthterm
),
\ycomb F\; t''_j}
(t_
)\ldots(t_
).
]
represents $
_t(g, j, (s_1, \ldots, s_m), a_1, \ldots, a_n)$.
But $j$ is a pre-proof, so
this is exactly $
(p, a_1, \ldots, a_n)$.
This completes our proof.
Using the new $\PPind$ operator, we can define an operator
$\PPHeight$ to represent the operation which maps pre-proofs to their height.
Note that this operation is different from the one we represented earlier,
because it must take into account the height of any tactic justifications.
\begin
[
\begin
\PPHeightterm
\abstreq {}
\qquad
\PPind\argleft p\argsemi
\PPindtermb
{1 + \maxterm
{h}}\argsemi
\qquad\qquad
\PPindtermc
{1 + \maxterm
{h}}\argsemi
\qquad\qquad
\PPindtermd
{1 + \maxtwoterm{\maxterm
{h}}{h'}}
\argright
\end
]
\end
\begin
The operator $\PPHeight$ represents the operation $\height$ on
pre-proofs.
\end
We must show that whenever $t$ represents the pre-proof $p$,
$\PPHeightterm
$ represents $\height(p)$. To do so, note that the
height of pre-proof $\langle g, \langle j, (s_1, \ldots, s_n)\rangle\rangle$
is $\max(0, \max_1\le i\le n \height(s_i)) = \max_1\le i\le n \height(s_i)$
if $j$ is either the unjustification or a primitive rule, and that
it is $\max(\height(j), \max_1\le i\le n \height(s_i))$ if $j$
is a pre-proof. We expand the definition
of $\PPHeight$ and obtain a term $\PPind\arglist
$.
Since $t$ represents $p$, and $\height$ has been be decomposed
into separate operations for each sort of justification,
we can now use theorem~\ref{} to obtain the desired result.
Suppose that $t_g$ represents the sequent $g$,
$t_j$ represents the unjustification $j$,
$t_n$ represents the natural number $n$.
Suppose that for each $i$ between
$1$ and $n$, if $t_i$ represents $i$,
then $t_s(t_i)$ represents the sequent $s_i$, and
$t_h(t_i)$ represents $\height(s_i)$.
We must show that $1 + \maxterm
$
represents $\height_u(g, j, (s_1, \ldots, s_n))$.
That is, we must show that it represents
$1 + \max_1\le i\le n \height(s_i)$.
But this follows immediately from our hypotheses,
and the definitions of $\maxop$ and $+$.
If, instead, $t_j$ represents a primitive rule $j$,
we must show that $1 + \maxterm
$
represents $\height_r(g, j, (s_1, \ldots, s_n))$.
That is, we must show that it represents
$1 + \max_1\le i\le n \height(s_i)$. But we have already done that.
Finally, suppose instead that $t_j$ represents a tactic pre-proof $j$.
In addition, suppose that $t'_h$ represents $\height(j)$.
Now we must show that the term
$1 + \maxtwoterm{\maxterm
{t_h}}
$
represents $\height_t(g, j, (s_1, \ldots, s_n))$; that is,
that it represents
$1 + \max(\max_1\le i\le n \height(s_i), \height(j))$.
But this follows immediately from our hypotheses,
and the definitions of $\maxop$, $\maxtwo$, and $+$.
This completes our discussion of the new definition of
$\PreProof$. We are now ready to embark on the second portion of our
representation of proofs with this sort of tactic. As before, we use
the Nuprl set type constructor, and as before we define an operator
$\Foo$ to represent the proof selection predicate.
% This operator can be defined just as before.
We must change the definition of $\Foo$
% which represents the predicate satisfied by exactly those pre-proofs
% in which all the nodes match up correctly. This needs to be changed
to account for tactic justifications, and also to use the new $\PPind$
operator. The latter is essential, since among other things, we must now
ensure that all tactic pre-proof justifications are in fact proofs.
This leads to the following definition.
Because of the case split inherent in the new $\PPind$
operator, it is now more convenient to perform case analysis
immediately, rather than deferring it to the definitions of
$\IsApplicable$ and $\TopGoals$. In any case, we can't use the old
definitions of $\IsApplicable$ and $\TopGoals$ since they depend on
the internal structure of justifications, and this has changed. For
this reason, we also define three new operators $\MatchesUpUnjust$,
$\MatchesUpPrimRule$, and $\MatchesUpTactic$. We also introduce two
new operators $\IsApplicableTactic$ and $\AreSubsTactic$ analogous to
the corresponding operators for the other kinds of justifications,
which we defined earlier. For now, we just assume that they are
appropriately defined, but eventually we show how this is done.
\begin
[
\begin
\Footerm
\abstreq {}
\\\qquad
\PPind\argleft p\argsemi
\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argdot
\MatchesUpUnjustterm
{\TopGoalsterm
{n}}
\\\qquad\qquad\qquad {}
\wedge \forall x\colon \intsegterm
\argdot h
\argsemi\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argdot
\MatchesUpPrimRuleterm
{\TopGoalsterm
{n}}
\\\qquad\qquad\qquad {}
\wedge \forall x\colon \intsegterm
\argdot h
\argsemi\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argcomma x\argdot
x
\wedge \MatchesUpTacticterm
{\TopGoalsterm
{n}}
\\\qquad\qquad\qquad {}
\wedge \forall x\colon \intsegterm
\argdot h
\argright
\MatchesUpUnjustterm
\abstreq {}
\\\qquad
\IsApplicableUnjustterm
\wedge \AreSubsUnjustterm
\end
]
% BOGUS
[
\begin
%
\MatchesUpPrimRuleterm
\abstreq {}
\\\qquad
\IsApplicablePrimRuleterm
\wedge \AreSubsPrimRuleterm
\MatchesUpTacticterm
\abstreq {}
\\\qquad
\IsApplicableTacticterm
\wedge \AreSubsTacticterm
\end
]
\end
\begin
The operator $\Foo$ represents the predicate $\foo$ on pre-proofs.
\end
Recall that the predicate $\foo(p)$ on pre-proofs $p$ is satisfied if
and only if every single node in $p$ matches up correctly. We must show
that for any pre-proof $p$, and any pair of terms $t$ and $t'$ which
both represent $p$, the terms $\Footerm
$ and $\Footerm
$ are equal types,
and that these types are inhabited if and only if $\foo(p)$ holds.
Let $p = \langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle$,
and for each integer $i$ between $1$ and $n$, let $s_i$ be
the topmost goal sequent of $q_i$. The predicate
$\foo(p)$ holds if and only if $\foo(q)$ holds for all sub-pre-proofs
$q$ of $p$, and $g$, $j$ and the sequents $(s_1, \ldots, s_n)$ are
appropriately. The required relation between $g$, $j$ and $\sequence
$
depends on the sort of justification $j$ is.
If we expand the operator $\Foo$ in $\Footerm
$ and $\Footerm
$,
we obtain terms of the form $\PPind\arglist
$ and
$\PPind\arglist
$. Since $t$ and $t'$ represent the
same pre-proof $p$, and since $\foo(p)$ can be defined by case analysis
on the topmost justification of $p$, we can use theorem~\ref{} to complete our
proof.
Let $g$ be a sequent, $j$ an unjustification, and $n$ a natural number.
For each $i$ between $1$ and $n$, let $q_i$ be a pre-proof. Suppose that
$t_g$ and $t'_g$ both represent $g$, $t_j$ and $t'_j$ both represent $j$,
and $t_n$ and $t'_n$ both represent $n$. Suppose that for any
integer $i$ between $1$ and $n$, if both $t_i$ and $t'_i$ represent $i$,
then $t_q(t_i)$ and $t'_q(t'_i)$ represent $q_i$ and
then $t_h(t_i)$ and $t'_h(t'_i)$ are equal types that are inhabited
if and only if $\foo(q_i)$ holds. We must show that
the terms
[
\MatchesUpUnjustterm
{\TopGoalsterm
{t_n}}
\wedge \forall x\colon \intsegterm
\argdot t_h
]
and
[
\MatchesUpUnjustterm
{\TopGoalsterm
{t'_n}}
\wedge \forall x\colon \intsegterm
\argdot t'_h
]
are equal types, and that these types are inhabited if and only if
$\foo_\unjust(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$
holds.
Here, $\foo_\unjust$ is the restruction of the predicate $\foo$ to
pre-proofs that have an unjustification as their topmost
justification. Let $s_i$ denote the topmost goal sequent of $q_i$ for
each $i$ between $1$ and $n$. Then, $\foo_\unjust(\langle g, \langle j,
(q_1, \ldots, q_n)\rangle\rangle)$ holds if and only if $\foo(q_i)$
holds for all $i$ between $1$ and $n$, and if
$\matchesup_\unjust(g, j, (s_1, \ldots, s_n))$ holds.
The predicate $\matchesup_\unjust$ is the restriction of the predicate
$\matchesup$ to pre-proofs that have an unjustification as their topmost
justification. But $\matchesup(g, j, \sequence
)$ holds if and only if
both $\isapplicable(g, j)$ and $\aresubs(g, j, \sequence
)$ do.
And since $j$ is an unjustification $\isapplicable(g, j)$ holds
if and only if $\aresubs_unjust(g, j)$ does. Likewise,
$\aresubs(g, j, \sequence
)$ holds if and only if
$\aresubs_unjust(g, j, \sequence
)$ does. Thus,
$\matchesup_\unjust(g, j, \sequence
)$ holds if and only if
both $\isapplicable_unjust(g, j)$ and $\aresubs_unjust(g, j, \sequence
)$ do.
Earlier, we showed that if the term $v_n$ represents the integer $n$;
if for all $i$ between $1$ and $n$, whenever $v_i$ represents $i$,
the term $v_q(v_i)$ represents the pre-proof $p_i$;
and if for all such $i$, $z_i$ is the topmost goal sequent of $p_i$;
then $\TopGoalsterm
$ represents the sequence
$(z_1, \ldots, z_n)$ of sequents.
From this together with our hypotheses concerning $t_n$, $t'_n$,
$t_q$ and $t'_q$, we can conclude that the terms
$\TopGoalsterm
$ and $\TopGoalsterm
$ both
represent the sequence $(s_1, \ldots s_n)$.
We also showed earlier that the operator
$\IsApplicableUnjust$ represents the predicate $\isapplicable_\unjust$
Since both $t_g$ and $t'_g$ represent the sequent $g$, and both
$t_j$ and $t'_j$ represent the unjustification $j$, we
can conclude that the terms $\IsApplicableterm
$
and $\IsApplicableUnjustterm
$ are equal types
which are inhabited if and only if $\isapplicable_\unjust(g, j)$
holds. Similarly, since we showed that $\AreSubsUnjust$ represents
the predicate $\aresubs_\unjust$, we can conclude that the terms
$\AreSubsUnjustterm
{\TopGoalsterm
{t_n}}$
and
$\AreSubsUnjustterm
{\TopGoalsterm
{t'_n}}$
are equal types and are inhabited if and only if
$\aresubs_\unjust(g, j, (s_1, \ldots, s_n))$ holds.
But $\MatchesUpUnjustterm
{\TopGoalsterm
{t_n}}$
expands to
[
\IsApplicable
\wedge \AreSubsUnjustterm
{\TopGoalsterm
{t_n}}.
]
Similarly, $\MatchesUpUnjustterm
{\TopGoalsterm
{t'_n}}$
expands to
[
\IsApplicable
\wedge \AreSubsUnjustterm
{\TopGoalsterm
{t'_n}}.
]
Using the definition of $\wedge$, we can conclude that the expanded versions
of the two terms are equal types, and that these types are inhabited if
and only both $\isapplicable_\unjust(g, j)$ and
$\aresubs_\unjust(g, j, (s_1, \ldots, s_n))$ hold. But then,
$\MatchesUpUnjustterm
{\TopGoalsterm
{t_n}}$ and
$\MatchesUpUnjustterm
{\TopGoalsterm
{t'_n}}$
are equal types, inhabited if and only if
$\matchesup_\unjust(g, j, (s_1, \ldots, s_n))$ holds.
Since $t_n$ and $t'_n$ represent the same integer $n$,
both evaluate to the term $\natnumterm
$. Thus $t$ and $t'$ are
equal members of the type $\inttype$. Thus, the types
$\intsegterm
$ and $\intsegterm
$ are equal types.
Two terms $t_i$ and $t'_i$ are equal members of the type $\intsegterm
$
if and only if both evaluate to a term $\natnumterm
$, and
the type $1 \le \natnumterm
\le t_n$ is inhabited. The latter
condition is satisfied if and only if $1 \le i \le n$. Thus
if $t_i$ and $t'_i$ are equal members of $\intsegterm
$,
they both represent an integer $i$ between $1$ and $n$.
Thus, whenever $t_i$ and $t'_i$ are equal members of $\intsegterm
$,
we can use our hypotheses concerning $t_h$ and $t'_h$ to conclude that
$t_h(t_i)$ and $t'_h(t'_i)$ are equal types, and that these types are
inhabited if and only if $\foo(q_i)$ holds. From this, we
can conclude that the terms
$\forall x\colon \intsegterm
\argdot t_h$
and
$\forall x\colon \intsegterm
\argdot t'_h$
are equal types which are inhabited if and only if
$\foo(q_i)$ holds for all $i$ such that $1 \le i \le n$.
But these pre-proofs $q_i$ are the only sub-pre-proofs of
$\langle g, \langle j, \sequence
\rangle\rangle$,
so these two types are inhabited if and only if $\foo(q)$
holds for all sub-pre-proofs
$q$ of $\langle g, \langle j, \sequence
\rangle\rangle$.
Then by the definition of $\wedge$
[
\MatchesUpUnjustterm
{\TopGoalsterm
{t_n}}
\wedge \forall x\colon \intsegterm
\argdot t_h
]
and
[
\MatchesUpUnjustterm
{\TopGoalsterm
{t'_n}}
\wedge \forall x\colon \intsegterm
\argdot t'_h
]
are equal types, and that these types are inhabited if and only if
$\foo_\unjust(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$
holds.
Let $g$ be a sequent, $j$ a primitive rule, and $n$ a natural number.
For each $i$ between $1$ and $n$, let $q_i$ be a pre-proof. Suppose that
$t_g$ and $t'_g$ both represent $g$, $t_j$ and $t'_j$ both represent $j$,
and $t_n$ and $t'_n$ both represent $n$. Suppose that for any
integer $i$ between $1$ and $n$, if both $t_i$ and $t'_i$ represent $i$,
then $t_q(t_i)$ and $t'_q(t'_i)$ represent $q_i$ and
then $t_h(t_i)$ and $t'_h(t'_i)$ are equal types that are inhabited
if and only if $\foo(q_i)$ holds. We must show that
the terms
[
\MatchesUpPrimRuleterm
{\TopGoalsterm
{t_n}}
\wedge \forall x\colon \intsegterm
\argdot t_h
]
and
[
\MatchesUpPrimRuleterm
{\TopGoalsterm
{t'_n}}
\wedge \forall x\colon \intsegterm
\argdot t'_h
]
are equal types, and that these types are inhabited if and only if
$\foo_\primrule(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$
holds. An analogous argument to that just given for the unjustification
case shows that this is indeed the case.
Finally, let $g$ be a sequent, $j$ a tactic pre-proof justification,
and $n$ a natural number.
For each $i$ between $1$ and $n$, let $q_i$ be a pre-proof. Suppose that
$t_g$ and $t'_g$ both represent $g$, $t_j$ and $t'_j$ both represent $j$,
and $t_n$ and $t'_n$ both represent $n$. Suppose that for any
integer $i$ between $1$ and $n$, if both $t_i$ and $t'_i$ represent $i$,
then $t_q(t_i)$ and $t'_q(t'_i)$ represent $q_i$ and
then $t_h(t_i)$ and $t'_h(t'_i)$ are equal types that are inhabited
if and only if $\foo(q_i)$ holds. And suppose that
$t_x$ and $t'_x$ are equal types which are inhabited if and only if
$\foo(j)$ holds.
We must show that
the terms
[
t_x \wedge
\MatchesUpTacticterm
{\TopGoalsterm
{t_n}}
\wedge \forall x\colon \intsegterm
\argdot t_h
]
and
[
t'_x \wedge
\MatchesUpTacticterm
{\TopGoalsterm
{t'_n}}
\wedge \forall x\colon \intsegterm
\argdot t'_h
]
are equal types, and that these types are inhabited if and only if
$\foo_\tactic(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$
holds.
An argument similar to that given for the unjustification case
allows us to conclude that
the terms
$\MatchesUpTacticterm
{\TopGoalsterm
{t_n}}$
and
$\MatchesUpTacticterm
{\TopGoalsterm
{t'_n}}$
are equal types, and are inhabited if and only if
$\matchesup_\tactic(g, j, (s_1, \ldots, s_n))$ holds.
Of course, now instead of having already shown
that $\IsApplicableTactic$ and $\AreSubsTactic$ are appropriately
defined, we have assumed it temporarily. Later, we fill this
gap in our proof. In a similar fashion, we can conclude that
$\forall x\colon \intsegterm
\argdot t_h$
and
$\forall x\colon \intsegterm
\argdot t'_h$
are equal types, inhabited if and only if $\foo(q_i)$ holds
for each $i$ between $1$ and $n$. By hypothesis,
$t_x$ and $t'_x$ are equal types which are inhabited if and only if
$\foo(j)$ holds.
This allows us to conclude, using the definition of $\wedge$
that the two terms $t_x \wedge \ldots$ and $t'_x \wedge \ldots$
displayed above are equal types which are inhabited if and only if
$\matchesup_\tactic(g, j, (s_1, \ldots, s_n))$ holds,
$\foo(q_i)$ holds for each $i$ between $1$ and $n$,
and $\foo(j)$ holds. That is, they are inhabited if and only if
$\matchesup_\tactic(g, j, (s_1, \ldots, s_n))$ holds,
and $\foo(q)$ holds for each sub-pre-proof $q$ of
$\langle g, \langle j, \sequence
\rangle\rangle$.
That is, they are inhabited if and only if
$\foo_\tactic(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$
holds. This completes our proof, modulo the gap noted above.
Since we are viewing tactics extensionally, by the time a
tactic justification becomes visible to the system, it has already run
successfully to produce a pre-proof. Thus, by the time
the system encounters a tactic invocation, the tactic is
guaranteed to apply. For this reason, we define
$\isapplicable_\tactic(g, j)$ to be satisfied
for all goal sequents $g$ and pre-proofs $p$. This makes it
very easy to represent.
\begin
[
\IsApplicableTacticterm
\abstreq \trueprop
]
\end
\begin
The operator $\IsApplicableTactic$ represents
the predicate $\isapplicable_\tactic$.
\end
Suppose both $t_g$ and $t'_g$ represent the same sequent $g$, and
that $t_j$ and $t'_j$ represent the same pre-proof $j$.
Then the terms $\IsApplicableTacticterm
$ and
$\IsApplicableTacticterm
$ both expand to $\trueprop$.
The term $\trueprop$ is a type that is always inhabited.
But $\isapplicable_\tactic(g, j)$ always holds.
We conclude that
$\IsApplicableTacticterm
$ and
$\IsApplicableTacticterm
$ are equal types that are inhabited
if and only if $\isapplicable_\tactic(g, j)$ holds.
All that remains is to show how $\AreSubsTactic$ must be defined.
The predicate $\aresubs_\tactic(g, j, \sequence
)$ holds if and only
if $g$ is the topmost goal sequent of $j$, and the sequence $\sequence
$
is the
of the pre-proof $j$, where frontier is defined as
follows.
\begin
Let $p=\langle g, \langle j, (p_1, \ldots, p_n)\rangle$ be a pre-proof.
If $j$ is the unjustification, then the frontier of $p$ is the
one element sequence $(g)$. Otherwise,
suppose that $(s_
, \ldots, s_
)$ is the frontier of $p_i$
The\/
of $p$ is
the sequence
$(s_
, \ldots, s_
, \ldots, s_
, \ldots, s_
)$.
\end
Note that for the purposes of this definition, unjustified nodes in
tactic sub-pre-proofs of $p$ are
included.
Note too that we assume that unjustified goals have no subgoals.
This adequate for our purposes since we only use $\Frontier$
inside the definition $\MatchesUpTactic$, which is used only on pre-proofs
that are already known to be proofs.
Suppose that we have defined the operator $\Frontier$ so that it
represents the operation $\frontier$ that maps pre-proofs $p$ to their
frontiers. We can then define $\AreSubsTactic$ as follows.
\begin
[\begin
\AreSubsTacticterm
\abstreq {}
\qquad
{\equalitytype
{\TopGoalterm
}} \wedge
{\equalitytype{\listtype{\Sequent}}
{\Frontierterm
}}
\end
]
\end
\begin
The operator $\AreSubsTactic$ represents the predicate
$\aresubs_\tactic$.
\end
Suppose that $t_g$ and $t'_g$ both represent the sequent $g$,
$t_j$ and $t'_j$ both represent the tactic justification $j$, and
$t_s$ and $t'_s$ both represent the sequence $\sequence
$ of sequents.
We show that the terms $\AreSubsTacticterm
$
and $\AreSubsTacticterm
$ are equal types, and that these
types are inhabited if and only if $\aresubs_\tactic(g, j, \sequence
)$
holds.
Since $t_g$ and $t'_g$ represent the same sequent $g$,
they are equal members of the type $\Sequent$. Since $t_j$ and
$t'_j$ represent the same pre-proof $j$, the terms $\TopGoalterm
$ and
$\TopGoalterm
$ both represent the same sequent, the topmost goal of
$j$, and so are equal members of $\Sequent$. Thus the types
$\equalitytype
{\TopGoalterm{t_j}}$ and
$\equalitytype
{\TopGoalterm{t'_j}}$ are equal types.
They are inhabited if and only if $t_g$ and $\TopGoalterm
$ are
equal members of the type $\Sequent$. Thus, they are inhabited if and only
if these terms represent the same sequent; that is, if and only if $g$ is
the topmost goal of $j$.
Since $t_s$ and $t'_s$ both represent the same sequence $\sequence
$
of sequents, they are equal members of the type $\listtype
$.
Since $t_j$ and
$t'_j$ represent the same pre-proof $j$, the terms $\Frontierterm
$ and
$\Frontierterm
$ both represent the same sequence of sequents,
the frontier of $j$, and so are equal members of the type
$\listtype
$. From this we conclude that
$\equalitytype{\listtype{\Sequent}}
{\Frontierterm{t_j}}$ and
$\equalitytype{\listtype{\Sequent}}
{\Frontierterm{t'_j}}$
are equal types. They are inhabited if and only if
$t_s$ and $\Frontierterm
$ are equal members of
the type $\listtype
$. Thus, they are inhabited if
and only if $t_s$ and $\Frontierterm
$ represent the same
sequence of sequents; that is, if and only if $\sequence
$ is
the frontier of $j$.
The term $\AreSubsTacticterm
$
expands to
[
{\equalitytype
{\TopGoalterm
}} \wedge
{\equalitytype{\listtype{\Sequent}}
{\Frontierterm
}},
]
and the term $\AreSubsTacticterm
$
expands to
[
{\equalitytype
{\TopGoalterm
}} \wedge
{\equalitytype{\listtype{\Sequent}}
{\Frontierterm
}}.
]
By the definition of $\wedge$, these types are equal and are inhabited if
and only if $g$ is the topmost goal sequent of $j$ and
$\sequence
$ is the frontier of $j$. That is, they are
inhabited if and only if $\aresubs_\tactic(g, j, \sequence
)$ holds.
We still need to define the operator $\Frontier$ to really
complete our proof. This is done as follows.
\begin
[
\begin
\Frontierauxterm
\abstreq {}
\qquad
\lambda f\argcomma i\argcomma l\argdot\inteqterm
{f (i-1) (\appendterm
)}
\Frontierterm
\abstreq {}
\qquad
\PPind \argleft p \argsemi
\qquad\qquad
g \argcomma j \argcomma n \argcomma s \argcomma h\argdot [g]\argsemi
\qquad\qquad
g \argcomma j \argcomma n \argcomma s \argcomma h\argdot
\ycomb (\Frontierauxterm
) \nilterm\argsemi
\qquad\qquad
g \argcomma j \argcomma n \argcomma s \argcomma h\argcomma x\argdot
\ycomb (\Frontierauxterm
) \nilterm
\argright
\end
]
\end
\begin
The operator $\Frontier$ represents the operation $\frontier$.
\end
Suppose that $t_p$ represents a pre-proof $p$.
We must show that $\Frontierterm
$ represents the frontier of $p$.
Since $\Frontierterm
$ expands to a term
$\PPind\arglist
$, we use theorem~\ref{}.
Suppose that $t_g$ represents the sequent $g$, that $t_j$
represents the unjustification $j$, and that $t_n$ represents the natural
number $n$. Suppose that for each integer $i$ between $1$ and $n$,
if $t_i$ represents $i$, $t_s(t_i)$ represents the pre-proof $q_i$ and
$t_h(t_i)$ represents $\frontier(q_i)$. We must show that
the term $[t_g]$ represents
$\frontier(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$.
Clearly, $[t_g]$ represents the one element sequence $(g)$,
which, because $j$ is the unjustification is exactly what is required.
Suppose that $t_g$ represents the sequent $g$, that $t_j$
represents the primitive rule $j$, and that $t_n$ represents the natural
number $n$. Suppose that for each integer $i$ between $1$ and $n$,
if $t_i$ represents $i$, $t_s(t_i)$ represents the pre-proof $q_i$ and
$t_h(t_i)$ represents $\frontier(q_i)$. We must show that
the term $\ycomb (\Frontierauxterm
) (t_n) \nilterm\argsemi$ represents
$\frontier(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)$.
For each of the pre-proofs $q_i$, let $(s_
,\ldots, s_
)$ be
the frontier of $q_i$. We must show that the term
$\ycomb (\Frontierauxterm
) (t_n) \nilterm\argsemi$ represents
the sequence
$(s_
, \ldots, s_
, \ldots, s_
, \ldots, s_
)$.
To do this we show that if $t_h$ is as described above, $i$ is
a natural number less than ore equal to $n$, $t_i$ represents $i$, and
$t_l$ represents the sequence $(s_
,\ldots,s_
)$,
then $\ycomb (\Frontierauxterm
) t_i\; t_l$ represents
the sequence $(s_
, \ldots, s_
)$. Our proof is by induction on $i$.
Regardless of the value of $i$, we replace the term
$\ycomb (\Frontierauxterm
)$ with the
computationally equivalent term
$\Frontierauxterm
(\ycomb (\Frontierauxterm
)$.
Then we expand the first of $\Frontieraux$, and contract the
resulting beta redices. This yields the term
[
\inteqterm
{\ycomb (\Frontierauxterm
) (t_i-1)
(\appendterm
)}.
]
If $i$ is $0$, $t_i$ evaluates to $\natnumterm
$, so this term
is computationally equivalent to $t_l$, which represents the
sequence $(s_
,\ldots, s_
)$. Otherwise,
$t_i$ evaluates to the term $\natnumterm
$, in which $i \neq 0$.
Then the displayed term is computationally equivalent to
${\ycomb (\Frontierauxterm
) (t_i-1) (\appendterm
)}$.
Clearly $i > 0$, so $0 \le i - 1 < i \le n$. Since $t_i$ represents
$i$, $t_i-1$ represents $i -1$. Moreover, $t_h(t_i)$
represents $\frontier(q_i) = (s_
, \ldots, s_
)$.
By hypothesis, $t_l$ represents the sequence
$(s_
, \ldots, s_
)$. Therefore,
$\appendterm
$ represents the sequence
$(s_
, \ldots, s_
)$. But $i = (i-1) + 1$,
so this sequence is $(s_
, \ldots, s_
)$.
By the induction hypothesis, the term
${\ycomb (\Frontierauxterm
) (t_i-1) (\appendterm
)}$
represents the sequence $(s_
, \ldots, s_
)$.
In particular, $0 \le n \le n$, $t_n$ represents $n$,
and since the sequence $(s_
, \ldots, s_
)$ is empty,
it is represented by $\nilterm$. We conclude that
$\ycomb (\Frontierauxterm
) (t_n) \nilterm\argsemi$ represents
the sequence
$(s_
, \ldots, s_
, \ldots, s_
, \ldots, s_
)$.
The final case, in which $t_j$ represents a tactic, is identical to
the case in which $t_j$ represents a primitive rule, except, of course,
that $t_j$ now represents a tactic, and that we have
a further hypothesis stating that $t_x$ represents $\frontier(j)$.
Since neither $t_x$ nor $t_j$ occur in the term
$\ycomb (\Frontierauxterm
) (t_n) \nilterm\argsemi$
these differences have no effect.
\section
In the previous section we showed that, if tactics are treated
extensionally, then proofs that include tactics can be easily represented.
This treatment of tactics is all very well, but it is somewhat dissatisfying.
Generally speaking, people do not think of tactics in this fashion.
Either they think of them even more extensionally, or they think of
them intensionally. In the first case, only the generated subgoals matter
to the user. In this case, tactics' generation of validations
is thought of as a non-logical implementation detail: it is how the
system ensures soundness. In the second case, the user distinguishes
between textually distinct tactic invocations.
In this section, we argue that it is also possible to
represent tactics if they are viewed intensionally. We believe that
doing so has certain benefits compared to the previous section's
extensional treatment of tactics.
First, treating the evaluation of
tactics to produce validations as a mere implementation detail seems
almost to be cheating. The complexity of this operation makes it seem
very different from other things, such as the exact machine
representation of various objects, that we normally consider to be
extra-logical implementation details. This treatment leaves an uneasy
feeling that we might be hiding a logical mistake in the guise of an
implementation detail.
Second, one goal of the reflection effort
is to provide a formal explanation of the Nuprl system. If we
leave the association of tactics with their validations unrepresented,
we fail to provide an explanation of one of the most complicated features
of the system. This hardly seems desirable.
Third, and most important, if we tactics are treated only
extensionally, we cannot even state, let alone prove, theorems
asserting that tactics written in a particular fashion have particular
properties. For example, we would not be able even to state theorems
about the properties of the various tacticals. This is a serious shortcoming,
since it precludes our use of the reflection mechanism to verify that
particular tactic programs behave as we expect.
Why, then, did we discuss extensional tactics in so much detail.
First, they are easier to represent. There may be applications in
which they are sufficient. In such applications, it might make sense
to use the simpler treatment of tactics. Second, certain ideas
introduced in connection with extensional tactics also appear in
our treatment of intensional tactics. In particular, the definition
of the frontier of a pre-proof carries over directly. Moreover, the
our definition of sub-proof, to include tactic validations, or,
equivalently our inclusion of the height of tactic validations in
the height of a proof, also carries over.%
\footnote{%
Although now, this is true only of sub-proofs, not of
sub-pre-proofs.%
}
Third, our ability to treat tactics extensionally provides an intuitive
explanation of why we believe tactics work at all.
So now, a tactic is a program that produces a validation
proof. Thus, we need to provide a representation for such objects.
We treat the fact that a tactic is a program as part of the pre-proof,
and the fact that this program produces a proof as part of the
proof selection predicate.
We have already shown how programs written in the Nuprl term language
may be represented; this is the purpose of the relation $\reps$ and
the type $\Term$ defined in chapter~\ref{}. For this reason,
it is convenient to assume that the
Nuprl term language is the language in which tactics are written.
This saves us the trouble of having to repeat the construction for
a different programming language, without obscuring significant details.
Moreover, we already have a logic with which to reason about programs
written in the Nuprl term language: the Nuprl logic. This means that
we do not have to concoct some sort of programming logic with which to reason
about tactics, we can use the Nuprl logic.
In fact, since evaluation is defined
only for closed terms, it is the class of closed terms we need to represent.
For this, we can still use the relation $\reps$, but must use the
type $\ClosedTerm$, also defined in chapter~\ref{}.
Recall that a tactic is a program that produces a validation.
Intuitively, we mean that when a tactic $t$ is evaluated, the result
is a proof. But terms do not evaluate to proofs, they evaluate to
other terms. What we really mean is that the value of $t$ must
represent a proof. Equivalently, since representation is computationally
closed, $t$ is required to represent a validation proof. Note that
this point is not Nuprl specific, it would apply even if tactics were written
some more conventional programming language. Programs don't evaluate to
proofs, they evaluate to values. These values may then be defined to
represent proofs.
Note that this also removes an apparent circularity from our
discussion. Instead of a situation where proofs contain tactics, and
tactics evaluate to proofs, our situation is now much more
tractable. Proofs include tactics, and tactics represent proofs.
It turns out that we can define the representation of proofs
almost independently of our definition of proofs.
For pre-proofs, the tactic justifications are no longer pre-proofs, so
we can return to the simple representation used for primitive proofs
in the representation of pre-proofs. Recall that this leads to the
following definition.
[
\PreProof \abstreq \recterm
{
\indepproducttype
{
\indepproducttype
{\listtype{p}}}}.
]
All that needs to be changed is the representation of justifications,
which must now include three cases, one for each sort of justification.
We represent this threefold choice in much the same fashion as we did
for extensional tactics. Of course, since the final case is different,
its representation is too.
\begin
Define the relation $t \repsrelfor
j$
between terms $t$ and justifications $j$ so that it is satisfied
if and only if one of the following conditions holds.
\begin
\item
$j$ is an unjustification, $\evalsto
{\inlterm{t'}}$, and
$t' \repsrelfor
j$.
\item
$j$ is a primitive rule, $\evalsto
{\inrterm{t'}}$,
$\evalsto
{\inlterm{t''}}$, and $t'' \repsrelfor
j$.
\item
$j$ is a tactic, $\evalsto
{\inrterm{t'}}$,
$\evalsto
{\inrterm{t''}}$, and $t'' \reps j$.
\end
\end
\begin
The relation $\repsrelfor
$ is a computationally closed
representation relation for the class of justifications.
\end
A justification is either the
unjustification, or a primitive rule, or a tactic.
Recall that for the purposes of pre-proofs, a tactic is simply a closed term.
We consider each case in turn. If $j$ is the unjustification, then since
$\repsrelfor
$ is a representation relation for the class of
unjustifications, there is a term $t$ such that $t
\repsrelfor
j$. Since $\inl$ is value producing,
$\inlterm
$ evaluates to itself, and so $\inlterm
\repsrelfor
j$. If $j$ is a primitive rule, then
since $\repsrelfor
$ is a representation relation for the
class of primitive rules, there is a term $t$ such that $t
\repsrelfor
j$. Since $\inl$ is value producing,
$\inlterm
$ evaluates to itself. Since $\inr$ is value producing,
$\inrterm{\inlterm{t}}$ also evaluates to itself. Thus,
$\inrterm{\inlterm{t}} \repsrelfor
j$. If $j$ is a
closed term, then since $\reps$ is a representation relation for the
class of closed terms, $t$ such that $t \reps j$. Since $\inr$ is
value producing, $\inrterm
$ evaluates to itself. Likewise,
$\inrterm{\inrterm{t}}$ evaluates to itself. Thus,
$\inrterm{\inrterm{t}} \repsrelfor
j$.
Suppose that $t \repsrelfor
j$ and
$t \repsrelfor
j'$ both hold for some closed term $t$, and
justifications $j$ and $j'$. $j$ is either the
unjustification, or a primitive rule, or a closed term.
Likewise, $j'$ is either the
unjustification, or a primitive rule, or a closed term.
Suppose that $j$ is the unjustification.
Then $\evalsto
{\inlterm{t'}}$
for some term $t'$. Since evaluation is single valued, this
means that $t$ does not evaluate to a term of the form $\inrterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be a primitive rule or tactic. It follows that
$j'$ must be the unjustification too.
Otherwise, $j$ is either a primitive rule or a tactic.
Then, $\evalsto
{\inrterm{t'}}$
for some term $t'$. Since evaluation is single valued, this
means that $t$ does not evaluate to a term of the form $\inlterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be the unjustification; it must also be either a primitive rule
or a tactic.
If $j$ is a primitive rule, then $\evalsto
{\inlterm{t''}}$
for some term $t''$. Since evaluation is single valued, this
means that $t'$ does not evaluate to a term of the form $\inrterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be a tactic; it must be a primitive rule too.
Furthermore, $t'' \repsrelfor
j$ and
$t'' \repsrelfor
j'$ must both hold. Since
$\repsrelfor
$ is a representation relation for the class of
primitive rules, we can conclude that $j$ is $j'$.
If $j$ is a term
$\evalsto
{\inrterm{t''}}$
for some term $t''$. Since evaluation is single valued, this
means that $t'$ does not evaluate to a term of the form $\inlterm
$.
Therefore, since $t \repsrelfor
j'$ holds, $j'$
cannot be a primitive rule; it must be a
tactic too.
Furthermore, $t'' \reps j$ and
$t'' \reps j'$ must both hold. Since
$\reps$ is a representation relation for the class of
closed terms, we can conclude that $j$ is $j'$.
Thus, it must always be the case that whenever both
$t \repsrelfor
j$ and
$t \repsrelfor
j'$ hold, $j$ and $j'$ are identical.
Now suppose that $t \repsrelfor
j$ holds
and $t \squiggle t'$. If $j$ is the unjustification, then
$\evalsto
{\inlterm{s}}$. Since $t \squiggle t'$,
$\evalsto
{\inlterm{s'}}$ for some term $s'$ such that $s \squiggle s'$.
Also, $s \repsrelfor
j$. Therefore, since $\repsrelfor
$ is
computationally closed, $s' \repsrelfor
j$.
Therefore, $t' \repsrelfor
j$.
If $j$ is a primitive rule,
then $\evalsto
{\inrterm{s}}$. Since $t \squiggle t'$,
$\evalsto
{\inrterm{s'}}$ for some term $s'$ such that $s \squiggle s'$.
Furthermore, $\evalsto
{\inlterm{r}}$, and so, since $s \squiggle s'$,
$\evalsto
{\inlterm{r'}}$ for some term $r'$ such that $r \squiggle r'$.
Also, $r \repsrelfor
j$. Therefore, since $\repsrelfor
$
is computationally closed, $r' \repsrelfor
j$.
Therefore, $t' \repsrelfor
j$.
If $j$ is a term $\evalsto
{\inrterm{s}}$.
Since $t \squiggle t'$, $\evalsto
{\inrterm{s'}}$ for some term $s'$
such that $s \squiggle s'$.
Furthermore, $\evalsto
{\inrterm{r}}$, and so, since $s \squiggle s'$,
$\evalsto
{\inrterm{r'}}$ for some term $r'$ such that $r \squiggle r'$.
Also, $r \reps j$. Therefore, since $\reps$
is computationally closed, $r' \reps j$.
Therefore, $t' \repsrelfor
j$.
We define a representation function and an unrepresentation
function for this relation in the obvious fashion. and then define
a type which represents the class of justifications using this relation,
again in essentially the obvious fashion.
\begin
The function $\repfunfor
(j)$ maps
justifications $j$ to terms. If $j$ is the unjustification,
[
\repfunfor
(j) =
\inlterm{\repfunfor
(j)}.
]
If $j$ is a primitive rule,
[
\repfunfor
(j) =
\inrterm{\inlterm{\repfunfor
(j)}}.
]
If $j$ is a tactic rule,
[
\repfunfor
(j) =
\inrterm{\inrterm{\rep(j)}}.
]
The partial function $\unrepfunfor
(t)$ maps
terms $t$ to justifications.
If $\eval(t)$ is $\inlterm
$ then
[
\unrepfunfor
(t) =
\unrepfunfor
(t').
]
If $\eval(t)$ is $\inrterm
$ and $\eval(t')$ is $\inlterm
$ then
[
\unrepfunfor
(t) =
\unrepfunfor
(t'').
]
If $\eval(t)$ is $\inrterm
$ and $\eval(t')$ is $\inrterm
$ then
[
\unrepfunfor
(t) = \unrep(t'').
]
\end
\begin
The function $\repfunfor
$ is a representation function for
the relation $\repsrelfor
$.
The function $\unrepfunfor
$ is a unrepresentation function for
the relation $\repsrelfor
$.
\end
First, we consider $\repfunfor
$.
For each justification $j$, we must show that
$\repfunfor
(j) \repsrelfor
j$.
The justification $j$ is either the unjustification,
or a primitive rule, or a tactic.
We consider each possibility in turn.
If $j$ is the unjustification,
then $\repfunfor
(j) = \inlterm{\repfunfor
(j)}$.
$\inl$ is value producing, and $\repfunfor
$ is
a representation function for the relation
$\repsrelfor
$. We conclude that
$\evalsto{\inlterm{\repfunfor
(j)}}{\inlterm{\repfunfor
(j)}}$.
We also conclude that $\repfunfor
(j) \repsrelfor
j$.
Thus, $\repfunfor
(j) \repsrelfor
j$.
If $j$ is a primitive rule,
then $\repfunfor
(j) =
\inrterm{\inlterm{\repfunfor
(j)}}$.
$\inr$ and $\inl$ are value producing, and $\repfunfor
$ is
a representation function for the relation
$\repsrelfor
$. We conclude that
$\evalsto{\inrterm{\inlterm{\repfunfor
(j)}}}
{\inrterm{\inlterm{\repfunfor
(j)}}}$,
and that
$\evalsto{\inlterm{\repfunfor
(j)}}
{\inlterm{\repfunfor
(j)}}$.
We also conclude that $\repfunfor
(j) \repsrelfor
j$.
Thus, $\repfunfor
(j) \repsrelfor
j$.
If $j$ is a tactic term,
then $\repfunfor
(j) =
\inrterm{\inrterm{\rep(j)}}$.
$\inr$ is value producing, and $\rep$ is
a representation function for the relation
$\reps$. We conclude that
$\evalsto{\inrterm{\inrterm
}}
{\inrterm{\inrterm
}}$,
and that
$\evalsto{\inrterm{\rep(j)}}
{\inrterm{\rep(j)}}$.
We also conclude that $\rep(j) \reps j$.
Thus, $\repfunfor
(j) \repsrelfor
j$.
Now consider $\unrepfunfor
$. We must show that
whenever $t \repsrelfor
j$, $\unrepfunfor
(t)$
is $j$. Again, our proof is by case analysis on the sort of justification
$j$ is.
If $j$ is the unjustification, then
$\evalsto
{\inlterm{t'}}$, and $t' \repsrelfor
j$.
But then, by the definition of $\eval$,
$\eval(t)$ is $\inlterm
$. Since $\unrepfunfor
$
is an unrepresentation function for the relation $\repsrelfor
$,
we can conclude that $\unrepfunfor
(t')$ is $j$.
Therefore, $\unrepfunfor
(t)$ is $j$.
If $j$ is a primitive rule, then
$\evalsto
{\inrterm{t'}}$, $\evalsto
{\inlterm{t''}}$,
and $t'' \repsrelfor
j$.
But then, by the definition of $\eval$,
$\eval(t)$ is $\inrterm
$, and $\eval(t')$ is $\inlterm
$.
Since $\unrepfunfor
$
is an unrepresentation function for the relation $\repsrelfor
$,
we can conclude that $\unrepfunfor
(t'')$ is $j$.
Therefore, $\unrepfunfor
(t)$ is $j$.
If $j$ is a tactic term, then
$\evalsto
{\inrterm{t'}}$, $\evalsto
{\inrterm{t''}}$,
and $t'' \reps j$.
But then, by the definition of $\eval$,
$\eval(t)$ is $\inrterm
$, and $\eval(t')$ is $\inrterm
$.
Since $\unrep$
is an unrepresentation function for the relation $\repsrelfor
$,
we can conclude that $\unrep(t'')$ is $j$.
Therefore, $\unrepfunfor
(t)$ is $j$.
\begin
[
\Justification \abstreq \uniontype
{\uniontype
{\ClosedTerm}}
]
\end
\begin
The type $\Justification$ unrepresents the class of justifications using the
relation $\repsrelfor
$.
\end
Suppose that two terms $t$ and $t'$ are equal members of the type
$\Justification$. Then either $\evalsto
{\inlterm{s}}$ and
$\evalsto
{\inlterm{s'}}$ for terms $s$ and $s'$ equal in $\unittype$
or $\evalsto
{\inrterm{s}}$ and
$\evalsto
{\inrterm{s'}}$ for terms $s$ and $s'$ equal in
the type $\uniontype
$. In the first case, since
$\unittype$ represents the class of unjustifications using the relation
$\repsrelfor
$, we can conclude that $s$ and $s'$
represent the same unjustification $j$. But then,
$t \repsrelfor
j$ and $t' \repsrelfor
j$.
Otherwise, $\evalsto
{\inlterm{r}}$ and
$\evalsto
{\inlterm{r'}}$ for terms $s$ and $s'$ equal in
the type $\PrimRule$, or $\evalsto
{\inrterm{r}}$ and
$\evalsto
{\inrterm{r'}}$ for terms $s$ and $s'$ equal in
the type $\ClosedTerm$. In the first sub-case, since
$\PrimRule$ represents the class of primitive rules using the relation
$\repsrelfor
$, we can conclude that $r$ and $r'$
represent the same primitive rule $j$. But then,
$t \repsrelfor
j$ and $t' \repsrelfor
j$.
Otherwise, since $\ClosedTerm$ represents the class of closed
terms using the relation $\reps$, we can
conclude that $r$ and $r'$ represent the same tactic term $j$. But then,
$t \repsrelfor
j$ and $t' \repsrelfor
j$.
Conversely, suppose that $t \repsrelfor
j$
and $t' \repsrelfor
j$. If $j$ is the unjustification,
this implies that $\evalsto
{\inlterm{s}}$, $\evalsto
{\inlterm{s'}}$,
$s \repsrelfor
j$, and $s' \repsrelfor
j$. But then,
since $\unittype$ represents the class of unjustifications using the relation
$\repsrelfor
$, we can conclude that $s$ and $s'$ are equal members
of $\unittype$. This in turn implies that $t$ and $t'$ are
equal members of $\Justification$. If $j$ is a primitive rule,
this implies that $\evalsto
{\inrterm{s}}$, $\evalsto
{\inrterm{s'}}$,
$\evalsto
{\inlterm{r}}$, $\evalsto
{\inlterm{r'}}$,
$r \repsrelfor
j$, and $r' \repsrelfor
j$. But then,
since $\PrimRule$ represents the class of primitive rules using the relation
$\repsrelfor
$, we can conclude that $r$ and $r'$ are equal members
of $\PrimRule$. This in turn implies that $s$ and $s'$ are
equal members of $\uniontype
$, and so that
$t$ and $t'$ are equal members of $\Justification$.
If $j$ is a tactic term,
this implies that $\evalsto
{\inrterm{s}}$, $\evalsto
{\inrterm{s'}}$,
$\evalsto
{\inrterm{r}}$, $\evalsto
{\inrterm{r'}}$,
$r \reps j$, and $r' \reps j$. But then,
since $\ClosedTerm$ represents the class of closed terms using the relation
$\reps$, we can conclude that $r$ and $r'$ are equal members
of $\ClosedTerm$. This in turn implies that $s$ and $s'$ are
equal members of $\uniontype
$, and so that
$t$ and $t'$ are equal members of $\Justification$.
Now, as was the case for primitive proofs, the only sub-pre-proofs
of a pre-proof are the sub-goal pre-proofs. There are no tactic
sub-pre-proofs to account for. This means that primitive recursion
over pre-proofs is essentially the same as it was for primitive proofs.
In particular, since our definition of the $\PPind$ operator
for primitive proofs does not depend in any way on the internal
structure of the representation relation for justifications, but only on the
fact that this relation is a computationally closed representation relation
for the class of justifications, we can use it here without change.
In particular theorems~\ref{} and~\ref{} still hold.
Using it, we can define an operator $\Frontier$ to represent
the frontier of a proof, in the sense of definition~\ref{}. The only reason
we have to redefine $\Frontier$ is to account for our change of the $\PPind$
back to the simple version used for primitive proofs. This is required because
there is no longer a tactic sub-pre-proof associated with nodes
justified by tactics.%
\footnote{%
Actually, since we simply ignore that particular binding
corresponding to the induction hypothesis for the tactic sub-pre-proof
in the old definition of $\Frontier$, we could still use it, but that
seems ugly.%
}
This yields the following definition.
\begin
[
\Frontierterm
\abstreq {}
\qquad
\PPindterm
{\progcase
{\inlterm{u}} [g] \orcase{\inrterm{v}}
\ycomb (\Frontierauxterm
) \nilterm}
]
\end
\begin
The operator $\Frontier$ represents the operation $\frontier$.
\end
For any pre-proof $p$, if $t_p$ represents $p$, we must show
that $\Frontierterm
$ represents the frontier of $p$. Since
this term expands to a term of the form $\PPind\arglist
$,
theorem~\ref{} applies. We assume that $t_g$ represents
the sequent $g$, $t_j$ represents the justification $j$, $t_n$ represents
the natural number $n$. We also assume that for any integer $i$
between $1$ and $n$ and any term $t_i$ which represents $i$,
$t_q(t_i)$ represents the pre-proof $q_i$, and $t_h(t_i)$ represents
$\frontier(q_i)$. We must show that the term
[
{\progcase
{\inlterm{u}} [t_g] \orcase{\inrterm{v}}
\ycomb (\Frontierauxterm
) (t_n) \nilterm}
]
represents the frontier of the pre-proof
[
\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle.
]
There are two cases. Either $j$ is the unjustification, or it isn't.
In the first case, the required frontier is $(g)$. Moreover,
since $t_j$ represents $j$, it must evaluate to a term of the form
$\inlterm
$. But then, the term displayed above is computationally
equivalent to $[t_g]$. Since $t_g$ represents $g$, this term represents
the sequence $(g)$.
Otherwise, for each integer $i$ between
$1$ and $n$ let $\frontier(q_i) = (s_
, \ldots, s_
)$.
Then, since $j$ is not the unjustification,
[
\frontier(\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle)
]
is the sequence
[
(s_
, \ldots, s_
, \ldots, s_
, \ldots, s_
).
]
Moreover, $t_j$ evaluates to a term of the form
$\inrterm
$, and the displayed term is computationally equivalent to
$\ycomb (\Frontierauxterm
) (t_n) \nilterm$. Earlier, we showed
that if $t_n$ represents $n$, and for each integer $i$ between
$1$ and $n$, and term $t_i$ which represents $i$,
$t_h(t_i)$ represents $(s_
, \ldots, s_
)$,
then this term represents the sequence
[
(s_
, \ldots, s_
, \ldots, s_
, \ldots, s_
).
]
Since, by hypothesis, these conditions are satisfied, we conclude
that $\ycomb (\Frontierauxterm
) (t_n) \nilterm$
represents the frontier of
$\langle g, \langle j, (q_1, \ldots, q_n)\rangle\rangle$.
This completes our discussion of the representation
of pre-proofs. We must now show how the $\foo$ predicate
is to be represented. We would like to do this just as we
did for primitive proofs. that is we would like to define operators to
represent the $\isapplicable$ and $\aresubs$ predicates
for each sort of justification, and then use these
to define a representation for $\foo$.
Unfortunately, a slight complication arises when we try
to define these predicates for the tactic case.
Recall that $\matchesup(g, j, \sequence
)$
should hold if and only if
$\isapplicable(g, j)$ and $\aresubs(g, j, \sequence
)$
both hold. And if $j$ is a tactic justification,
we want $\matchesup(g, j, \sequence
)$ to
hold if and only if each of the following conditions holds.
First, $j$ must represent a proof $p$. Second, the topmost goal
of $p$ must be $g$. Third, the frontier of $p$ must be the sequence
$\sequence
)$. This definition is somewhat problematic in that it
depends on the definition of proof. Since the representation of the
class of proofs depends upon the representation of $\foo$,
attempts to use this definition directly fail.
We can begin to solve this problem by noting that
if $p$ is a proof, it is a pre-proof for which $\foo(p)$ holds.
Thus, we can restate the requirement that $j$ must represent a proof
to assert that $j$ must represent a
$p$ such
that $\foo(p)$ holds. This eliminates the reference to
the class of proofs. This does not completely
solve the problem, because $p$ is not a sub-pre-proof of
the pre-proof in which $j$ occurs. Since $\matchesup$ is intended
to be used in the definition of $\foo$, which is itself defined by structural
induction on pre-proofs, this use of $\foo$ results in a circularity.
Our only hope is to define $\foo$ differently.
Our solution is to define the predicate $\foo(p)$ by induction
on the height of the proof $p$, where the height of a proof is defined in
much the same way as the height of an extensional-tactic pre-proof was.
Intuitively, the reason we accept intensional tactic proofs is that,
at least in principle, we can evaluate their tactic justifications to
produce proofs that fill in the details. If we do this to
every tactic justification (including any that occur in the proofs produced
by tactics) in the proof, we produce an extensional tactic proof.
Therefore, only intensional tactic pre-proofs for which this is possible
ought to be considered proofs. Once we have imposed this restriction,
we can define the $\foo$ predicate by structural induction on the underlying
extensional tactic proof. In practice, it is slightly more convenient
to use induction on the height of this underlying proof.
We define a two place predicate $\foo(n, p)$ on natural
numbers $n$ and intensional tactic pre-proofs $p$. Intuitively,
this predicate is satisfied if $p$ has an underlying extensional
proof of height $n$ or less. Since there are no proofs
of height $0$, $\foo(0, p)$ is, necessarily, always false, regardless of $p$.
\begin
The two place predicate $\foo(n, p)$ on natural
numbers $n$ and intensional tactic pre-proofs $p$ is defined by induction
on $n$ as follows.
\begin
\item
$\foo(0, p)$ is false for all pre-proofs $p$.
\item
If $j$ is the unjustification or a primitive rule,
and for each pre-proof $q_i$, $s_i$ is the
topmost goal sequent of $q_i$,
then
$\foo(n+1, \langle g, \langle j, (q_1, \ldots, q_m)\rangle\rangle)$
holds if and only if
$\foo(n, q_i)$ holds for each $i$ between $1$ and $m$,
and
$\matchesup(g, j, (s_1, \ldots, s_m))$ holds.
\item
If $j$ is a tactic
and for each pre-proof $q_i$, $s_i$ is the
topmost goal sequent of $q_i$,
then
$\foo(n+1, \langle g, \langle j, (q_1, \ldots, q_m)\rangle\rangle)$
holds if and only if
there is a pre-proof $p'$ such that
$j \repsrelfor
p'$,
$\foo(n, p')$ holds,
$\matchesup_\tactic(g, p', (s_1, \ldots, s_m))$ holds, and
for each $i$ between $1$ and $m$, $\foo(n, q_i)$ holds.
\end
Here, $\matchesup$ is defined as for primitive proofs, and
$\matchesup_\tactic$ is as defined for extensional tactic proofs.
\end
With this done, we can define the predicate $\foo(p)$ on
pre-proofs $p$ as follows.
\begin
The predicate $\foo(p)$ on pre-proofs $p$ is defined so that
$\foo(p)$ holds if and only if $\foo(n, p)$ holds, for some natural
number $n$.
\end
Now, we define operators $\Foo$ and $\Foon$ to
represent these predicates. In doing so, we assume the existence of
and operator $\RepsPreProof$ to represent the two place predicate
$\repsrelfor
$.
\begin
[
\begin
\Fooauxterm \abstreq {}
\qquad
\lambda f\argcomma n\argcomma p\argdot
\inteq\argleft n\argsemi 0\argsemi\falseprop\argsemi
\qquad\qquad
\proglet{\pairterm
{\pairterm
}}
\progin {}
\qquad\qquad\qquad
\forall i\colon\intsegterm
{\lengthterm{s}}\argdot
f(n-1)(\nthterm
)
\qquad\qquad\qquad {} \wedge
\progcase
{\inlterm{u}}{}
\qquad\qquad\qquad\qquad\qquad {}
\MatchesUpUnjustterm
{\TopGoals'\arglist{s}}
\qquad\qquad\qquad\qquad {}
\orcase{\inrterm{\inlterm
}}{}
\qquad\qquad\qquad\qquad\qquad {}
\MatchesUpPrimRuleterm
{\TopGoals'\arglist{s}}
\qquad\qquad\qquad\qquad {}
\orcase{\inrterm{\inrterm
}}
\qquad\qquad\qquad\qquad\qquad {}
\exists q\colon\PreProof\argdot
\RepsPreProofterm
\wedge
f(n-1)(q)
\qquad\qquad\qquad\qquad\qquad {}
\wedge
\MatchesUpTacticterm
{\TopGoals'\arglist{s}}
\argright
\Foonterm
\abstreq \ycomb \Fooaux \;n\;p
\Footerm
\abstreq \exists n\colon
\argdot \Foonterm
\end
]
\end
\begin
The operator $\Foon$ represents the predicate
$\foo(n, p)$ on natural numbers $n$ and pre-proofs $p$.
\end
We have already shown that most of the operators
used in the definition of $\Fooaux$ have the properties we
expect them to. The principal exception is the operator
$\RepsPreProof$. We shall assume, for now, that it
represents the predicate $\repsrelfor
$. Later
we show how it is defined, and prove that it really does
represent $\repsrelfor
$.
We must show that whenever $t_n$ and $t'_n$ represent
the same natural number $n$, and $t_p$ and $t'_p$ represent
the same pre-proof $p$, the terms
$\Foonterm
$ and $\Foonterm
$ are equal types,
and that these types are inhabited if and only if
$\foo(n, p)$ holds. The proof is by induction on $n$.
In each of the terms, we expand the operator $\Foon$. Then we
replace subterms of the form $\ycomb\Fooaux$ in the resulting term
with the computationally equivalent $\Fooauxterm(\ycomb\Fooauxterm)$.
Next, we expand the first instance of $\Fooaux$, and contract the resulting
beta redices. Finally, we replace subterms of the form
$\ycomb\Fooaux\;a\;b$ with the term $\Foonterm
$.
This last step is permissible because $\Foonterm
$
expands to $\ycomb\Fooaux\;a\;b$. After all of these
manipulations we are left with the terms
[
\begin
\inteq\argleft t_n\argsemi 0\argsemi\falseprop\argsemi
\qquad
\proglet{\pairterm
{\pairterm
}}
\progin {}
\qquad\qquad
\forall i\colon\intsegterm
{\lengthterm{s}}\argdot
\Foonterm
{\nthterm
{s}}
\qquad\qquad {} \wedge
\progcase
{\inlterm{u}}{}
\MatchesUpUnjustterm
{\TopGoals'\arglist{s}}
\qquad\qquad\qquad {}
\orcase{\inrterm{\inlterm
}}{}
\MatchesUpPrimRuleterm
{\TopGoals'\arglist{s}}
\qquad\qquad\qquad {}
\orcase{\inrterm{\inrterm
}}
\qquad\qquad\qquad\qquad {}
\exists q\colon\PreProof\argdot
\RepsPreProofterm
\wedge
\Foonterm
\qquad\qquad\qquad\qquad {}
\wedge
\MatchesUpTacticterm
{\TopGoals'\arglist{s}}
\argright
\end
]
and
[
\begin
\inteq\argleft t'_n\argsemi 0\argsemi\falseprop\argsemi
\qquad
\proglet{\pairterm
{\pairterm
}}
\progin {}
\qquad\qquad
\forall i\colon\intsegterm
{\lengthterm{s}}\argdot
\Foonterm
{\nthterm
{s}}
\qquad\qquad {} \wedge
\progcase
{\inlterm{u}}{}
\MatchesUpUnjustterm
{\TopGoals'\arglist{s}}
\qquad\qquad\qquad {}
\orcase{\inrterm{\inlterm
}}{}
\MatchesUpPrimRuleterm
{\TopGoals'\arglist{s}}
\qquad\qquad\qquad {}
\orcase{\inrterm{\inrterm
}}
\qquad\qquad\qquad\qquad {}
\exists q\colon\PreProof\argdot
\RepsPreProofterm
\wedge
\Foonterm
\qquad\qquad\qquad\qquad {}
\wedge
\MatchesUpTacticterm
{\TopGoals'\arglist{s}}
\argright.
\end
]
We show that these terms are equal types, and that they are inhabited if
and only if $\foo(n, p)$ holds.
If $n = 0$, then $t_n$ evaluates to $\natnumterm
$.
Thus, a term of the for $\inteqterm
$ is computationally
equivalent to $a$. We conclude that the first displayed term
is computationally equivalent to the term $\falseprop$.
An analogous argument shows that the second displayed term does too.
The term $\falseprop$ is a type, and this type is never inhabited.
But $\foo(0, p)$ never holds. We conclude that the two terms
are equal types, and that they are inhabited if and only if
$\foo(0, p)$ holds.
Otherwise, $n = k + 1$ for some natural number $k$.
The term $t_n$ evaluates to $\natnumterm
$, and since $n \neq 0$,
the terms of the form $\inteqterm
$ are computationally
equivalent to $b$. Likewise, terms of the form
$\inteqterm
$ are computationally
equivalent to $b'$. In this case, $b$ is of the form
$\proglet{\pairterm
{\pairterm
}}
$. Since $t_p$
represents a pre-proof
$p = \langle g, \langle j, (q_1, \ldots, q_m)\rangle\rangle$,
there are terms $t_g$, $t_2$, $t_j$ and $t_s$ such that
$t_g$ represents $g$, $t_j$ represents $j$, and $t_s$
represents $(q_1, \ldots, q_n)$. Moreover, $t_p$
evaluates to $\pairterm
$ and $t_2$ evaluates to
$\pairterm
$. Thus, a term of the form
$\proglet{\pairterm
{\pairterm
}}
$
is computationally equivalent to the term
$\subst
$.
Similarly, $b'$ is a term of the form
$\proglet{\pairterm
{\pairterm
}}
$.
Since $t'_p$ also represents $p$, we can conclude, using an analogous
argument that there exist terms
$t'_g$, $t'_j$ and $t'_s$ such that
$t'_g$ represents $g$, $t'_j$ represents $j$, $t'_s$
represents $(q_1, \ldots, q_n)$, and $b'$ is
computationally equivalent to the term
$\subst
$.
The term $\subst
$
is of the form
[
(\forall i\colon\intsegterm
{\lengthterm{t_s}}\argdot
\Foonterm
{\nthterm
{t_s}})
\wedge
\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\orcase{\inrterm{\inrterm
}}
.
]
While the term $\subst
$
is of the form
[
(\forall i\colon\intsegterm
{\lengthterm{t'_s}}\argdot
\Foonterm
{\nthterm
{t'_s}})
\wedge
\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\orcase{\inrterm{\inrterm
}}
.
]
We abbreviate these as $c_1 \wedge c_2$ and $c'_1 \wedge c'_2$
respectively. We show first that $c_1$ and $c'_1$
are equal types, and that they are inhabited if and only if
$\foo(k, q_i)$ holds for each $i$ between $1$ and $m$.
Then we show that $c_2$ and $c'_2$ are equal types.
For each $i$, let $s_i$ be the topmost goal sequent of $q_i$.
If $j$ is the unjustification or a primitive rule,
we show that $c_2$ is inhabited if and only if
$\matchesup(g, j, (s_1, \ldots, s_m))$ holds.
If $j$ is a tactic term
we show that $c_2$ is inhabited if and only if
there is a pre-proof $q$ such that
$j \repsrelfor
q$, and both
$\foo(k, q)$
and
$\matchesup_\tactic(g, q, (s_1, \ldots, s_m))$ hold.
This allows us to conclude that
$c_1\wedge c_2$ and $c'_1\wedge c'_2$ are equal types, and that
they are inhabited if and only if $\foo(k+1, p)$ holds.
But this implies that
$\Foonterm
$ and $\Foonterm
$ are equal types,
which are inhabited if and only if $\foo(k+1, p)$ holds.
Both $t_s$ and $t'_s$ represent the sequence
$(q_1, \ldots, q_m)$. Thus, for any natural number between
$1$ and $m$, if $t_i$ and $t'_i$ each represent $i$,
the terms $\nthterm
$ and $\nthterm
$
represent $q_i$. Both $t_n$ and $t'_n$ represent $n = k + 1$.
Thus, both $t_n-1$ and $t'_n-1$ represent $k$. Then, by the induction
hypothesis, $\Foonterm
{\nthterm
{t_s}}$ and
$\Foonterm
{\nthterm
{t_s}}$ are equal types,
and are inhabited if and only if $\foo(k, q_i)$ holds.
Now consider the terms $\intsegterm
{\lengthterm{t_s}}$
and $\intsegterm
{\lengthterm{t'_s}}$. Since
$t_s$ and $t'_s$ both represent the sequence
$(q_1, \ldots, q_m)$, the terms $\lengthterm
$ and
$\lengthterm
$ both represent $m$. But then,
$\intsegterm
{\lengthterm{t_s}}$
and $\intsegterm
{\lengthterm{t'_s}}$ are equal types.
Suppose $t_i$ and $t'_i$ are equal members of this type,
then they represent the same integer $i$ between
$1$ and $m$. But then, $\Foonterm
{\nthterm
{t_s}}$ and
$\Foonterm
{\nthterm
{t_s}}$ are equal types.
This allows us to conclude that
$c_1 = \forall i\colon\intsegterm
{\lengthterm{t_s}}\argdot
\Foonterm
{\nthterm
{t_s}}$
and
$c'_1 = \forall i\colon\intsegterm
{\lengthterm{t'_s}}\argdot
\Foonterm
{\nthterm
{t'_s}}$
are equal types. Moreover, since
$\Foonterm
{\nthterm
{t_s}}$ is inhabited if and only if
$\foo(k, q_i)$ holds, we can conclude that $c_1$ and $c'_1$ are
inhabited if and only if $\foo(k, q_i)$ holds for all $i$ between $1$ and
$m$.
For the second pair of conjuncts $c_2$ and $c'_2$,
our argument proceeds by case analysis on $j$,
with one case for each sort of justification.
If $j$ is the unjustification, then since
$t_j$ represents $j$, there is a term
$t_u$ such that $t_j$ evaluates to $\inlterm
$
and $t_u \repsrelfor
j$. This means that
a term of the form $\progcase
{\inlterm{u}}d\mid\ldots$
is computationally equivalent to the term $\subst
$.
In this case, we conclude that $c_2$ is computationally equivalent to
$\MatchesUpUnjustterm
{\TopGoals'\arglist{t_s}}$.
Similarly, the term $c'_2$
is computationally equivalent to
$\MatchesUpUnjustterm
{\TopGoals'\arglist{t'_s}}$
for some term $t'_u$ such that $t'_u \repsrelfor
j$.
Earlier we showed that if a term $q$ represents the
sequence $(q_1, \ldots, q_m)$
of pre-proofs, the term $\TopGoals'\arglist
$
represents the sequence $(s_1, \ldots, s_m)$ of sequents, in which
$s_i$ is the topmost goal sequent of $q_i$.
Thus, $\TopGoals'\arglist
$ and $\TopGoals'\arglist
$
both represent the sequence $(s_1, \ldots, s_m)$.
Also, $t_g$ and $t'_g$ represent the sequent $g$, and
$t_j$ and $t'_j$ both represent the unjustification $j$.
Earlier, we showed that $\MatchesUpUnjust$ represents
the predicate $\matchesup_\unjust$. Therefore,
$\MatchesUpUnjustterm
{\TopGoals'\arglist{t_s}}$
and
$\MatchesUpUnjustterm
{\TopGoals'\arglist{t'_s}}$
are equal types, and are inhabited if and only if
$\matchesup_\unjust(g, j, (s_1, \ldots, s_m))$ holds.
Since $j$ is an unjustification, this predicate holds if
and only if $\matchesup(g, j, (s_1, \ldots, s_m))$ does.
If $j$ is a primitive rule, then since
$t_j$ represents $j$, there are terms $t_1$ and $t_r$
such that $t_j$ evaluates to $\inrterm
$,
$t_1$ evaluates to $\inlterm
$,
and $t_r \repsrelfor
j$. This means that
a term of the form
$\progcase
{\inlterm{u}}d\orcase{\inrterm{\inlterm
}}e\mid\ldots$
is computationally equivalent to the term $\subst
$.
In this case, we conclude that $c_2$ is computationally equivalent to
$\MatchesUpPrimRuleterm
{\TopGoals'\arglist{t_s}}$.
Similarly, the term $c'_2$
is computationally equivalent to
$\MatchesUpPrimRuleterm
{\TopGoals'\arglist{t'_s}}$
for some term $t'_r$ such that $t'_r \repsrelfor
j$.
As before, $\TopGoals'\arglist
$ and $\TopGoals'\arglist
$
both represent the sequence $(s_1, \ldots, s_m)$.
Earlier, we showed that $\MatchesUpPrimRule$ represents
the predicate $\matchesup_\primrule$. Therefore
$\MatchesUpPrimRuleterm
{\TopGoals'\arglist{t_s}}$
and
$\MatchesUpPrimRuleterm
{\TopGoals'\arglist{t'_s}}$
are equal types, and are inhabited if and only if
$\matchesup_\primrule(g, j, (s_1, \ldots, s_m))$ holds.
Since $j$ is a primitive rule, this predicate holds if
and only if $\matchesup(g, j, (s_1, \ldots, s_m))$ does.
Finally, if $j$ is a tactic,
there are terms $t_1$ and $t_t$
such that $t_j$ evaluates to $\inrterm
$,
$t_1$ evaluates to $\inrterm
$,
and $t_t \reps j$. This means that
a term of the form
$\progcase
{\inlterm{u}}d\orcase{\inrterm{\inlterm
}}e
\orcase{\inrterm{\inrterm
}}f$
is computationally equivalent to the term $\subst
$.
In this case, we conclude that $c_2$ is computationally equivalent to
[
\exists q\colon\PreProof\argdot
\RepsPreProofterm
\wedge
\Foonterm
\wedge
\MatchesUpTacticterm
{\TopGoals'\arglist{t_s}}
]
$\MatchesUpPrimRuleterm
{\TopGoals'\arglist{t_s}}$.
Similarly, the term $c'_2$
is computationally equivalent to
[
\exists q\colon\PreProof\argdot
\RepsPreProofterm
\wedge
\Foonterm
\wedge
\MatchesUpTacticterm
{\TopGoals'\arglist{t'_s}}
]
for some term $t'_t$ such that $t'_t \reps j$.
We have already shown that the type $\PreProof$ represents
the class of pre-proofs. Suppose that two terms $t_q$ and $t'_q$
are equal members of $\PreProof$. Then they both represent the same
pre-proof $q$.
Since $t_t$ and $t'_t$ represent the same term $j$
and $\RepsPreProof$ represents the predicate $\repsrelfor
$,
we conclude that the terms $\RepsPreProofterm
$ and
$\RepsPreProofterm
$ are equal types. They are inhabited
if and only if $j \repsrelfor
q$.
Since $t_n$ and $t'_n$ each represent $n = k + 1$,
$t_n - 1$ and $t'_n - 1$ each represent $k$. But then, by the
induction hypothesis $\Foonterm
$ and $\Foonterm
$
are equal types. They are inhabited if and only if $\foo(k, q)$
holds.
As above, $\TopGoals'\arglist
$ and
$\TopGoals'\arglist
$ represent the sequences $(s_1, \ldots, s_m)$.
Earlier, we showed that $\MatchesUpTactic$ represents the predicate
$\matchesup_\tactic$. Recall that this predicate is a predicate on sequents,
pre-proofs, and sequences of sequents. We can conclude that
$\MatchesUpTacticterm
{\TopGoals'\arglist{t_s}}$
and
$\MatchesUpTacticterm
{\TopGoals'\arglist{t'_s}}$
are equal types. They are inhabited if and only if
$\matchesup_\tactic(g, q, (s_1, \ldots, s_m))$ holds.
From this, we can conclude that the terms of of
the form $\exists q \colon \PreProof\argdot\ldots$ displayed above
are equal types. They are inhabited if and only if there is a pre-proof
$q$ such that $j \repsrelfor
q$, $\foo(k, q)$, and
$\matchesup_\tactic(g, q, (s_1, \ldots, s_m))$.
\begin
The operator $\Foo$ represents the predicate $\foo(p)$
on pre-proofs $p$.
\end
Suppose $p$ is a pre-proof, and that $t_p$ and $t'_p$ both represent
$p$. Show that $\Footerm
$ and $\Footerm
$ are equal types
and that these types are inhabited if and only if $p$ holds.
The term $\Footerm
$ expands to
$\exists n\colon
\argdot \Foonterm
$.
Likewise, $\Footerm
$ expands to
$\exists n\colon
\argdot \Foonterm
$.
The term $\Bbb N$ is a type. Suppose that $t_n$ and $t'_n$ are
equal members of $\Bbb N$. Then they each represent the
same natural number $n$. Then,
by the theorem just proved, $\Foonterm
$ and
$\Foonterm
$ are equal types. They are inhabited if and only if
$\foo(n, p)$ holds. Therefore,
$\exists n\colon
\argdot \Foonterm
$.
and
$\exists n\colon
\argdot \Foonterm
$
are equal types which are inhabited if and only if
for some natural number $n$, $\foo(n, k)$ holds.
That is, they are inhabited if and only if $\foo(p)$ holds.
\section
All that remains is to show how $\RepsPreProof$ is defined.
Basically, the idea is that we completely redo the definition
of representations, except formally this time. Note that we
only need to represent the representation relation, not the
representation function or the unrepresentation function.
Our presentation of this definition falls into five basic stages.
First, we show that the two uniform constructions of representation
relations for complex objects which are given in chapter~\ref{}
can be represented. Second, we give a representation of the representation
relations for each of the index families. Third, we show how
the relation $\reps$ may be represented. Fourth, we discuss the representation
of the relation $\repsrelfor
$. Last, we use
give a representation for the relation $\repsrelfor
$.
\subsection
Recall that if $\repsrelfor
$ is a representation relation for
the class $\cal K$, then $\repsrelforseq
$ is a representation
relation for the class $
^*$ of finite sequences with elements
chosen from the class $\cal K$. The relation $\repsrelforseq
$ is
defined from $\repsrelfor
$ by a uniform construction. In a sense,
we have defined a representation relation valued operation on
representation relations. We show that, in a sense, this
operation can be represented.
We define an operator $\RepsSeq$ with the following property
If the operator $\Reps_K$ represents the predicate
$\repsrelfor
$, and the operator $\Reps_K^*$
is defined by
[
\Reps_K^*\arglist
\abstreq
\RepsSeqterm
{\Reps_K\arglist{t\argsemi a}}
,
]
then the operator $\Reps_K^*$ represents $\repsrelforseq
$.
Note that this does
imply that $\RepsSeq$
represents the operation which constructs sequence representations.
The problem is that we have not shown that
[
\RepsSeqterm
{\Reps_K\arglist{t\argsemi a}}
]
and
[
\RepsSeqterm
{\Reps_K\arglist{t\argsemi a}}
,
]
are equal types whenever $\Reps_K$ and $\Reps'_K$ represent
$\repsrelfor
$; that is, we have not shown that
$\RepsSeq$ is functional in its first argument.
Nevertheless, this property is sufficient for our needs.
It gives us a very convenient way to represent
representation relations which are defined as $\repsrelforseq
$.
\begin
[
\begin
\RepsSeqauxterm
\abstreq {}
\\\qquad
\lambda F\argcomma T\argcomma A\argdot
\progcase
\EvalsToterm
\\\qquad\qquad
\orcase{\consterm
{A_t}}
\exists a\argcomma b\colon\ClosedTerm\argdot
\\\qquad\qquad\qquad
\EvalsToterm
{\Consterm
{b}}
\wedge
R[a\argsemi A_h]
\wedge
F(b)(A_t)
\RepsSeqterm
\abstreq
\ycomb (\RepsSeqauxterm
)(T)(A)
\Nilterm \abstreq \pairterm{\pairterm{\opidterm{nil}}{\nilterm}}
\Consterm
\abstreq
\pairterm{\pairterm{\opidterm{cons}}{\nilterm}}
{[\pairterm
\argsemi\pairterm
]}
\end
]
\end
\begin
Let $\cal K$ be a class of objects, and let
$\repsrelfor
$ be a representation relation for $\cal K$.
Suppose that for any element $a$ of $\cal K$, and any closed term
$t$, and for any closed terms $t_a$, $t'_a$, $t_t$, and $t'_t$
such that $t_a \repsrelfor
a$, $t'_a \repsrelfor
a$,
$t_t \reps t$, and $t'_t \reps t$, the terms
$\subst
$ and $\subst
$
are equal types which are inhabited if and only if
$t \repsrelfor
a$.
Suppose that $s$ is a sequence from $
^*$, and that
$t_s$ and $t'_s$ are closed terms such that
$t_s \repsrelforseq
s$ and $t'_s \repsrelforseq
s$.
Suppose that $z$ is closed term and that
$t_z$ and $t'_z$ are closed terms such that
$t_z \reps z$ and $t'_z \reps z$.
Then, the terms
$
\RepsSeqterm
$
and
$
\RepsSeqterm
$
are equal types.
Moreover, they are inhabited if and only if
$z \repsrelforseq
s$.
\end
Our proof is by induction on the length of $s$.
We begin by replacing the two terms with computationally
equivalent terms.
The term $\RepsSeqterm
$
expands to $\ycomb (\RepsSeqauxterm
)(T_s)(t_z)$.
We replace the subterm $\ycomb (\RepsSeqauxterm
)$ with the
computationally equivalent term
$\RepsSeqauxterm
(\ycomb \RepsSeqauxterm
)$.
Then we expand the first instance of $\RepsSeqaux$, and contract
the resulting beta redices.
Finally, we replace the term $\ycomb(\RepsSeqauxterm
)(b)(A_t)$
with the term $\RepsSeqterm
$ which expands to it.
This yields the term
[
\begin
{r@{}l}
\progcase
{}&
\EvalsToterm
\orcase{\consterm
{A_t}}{}&
\exists a\argcomma b\colon\ClosedTerm\argdot
\\\multicolumn
{\qquad
\EvalsToterm
{\Consterm
{b}}
\wedge
\subst
\wedge
\RepsSeqterm
.}
\end
]
In a similar fashion, we can replace the term
$\RepsSeqterm
$
with
[
\begin
{r@{}l}
\progcase
{}&
\EvalsToterm
\orcase{\consterm
{A_t}}{}&
\exists a\argcomma b\colon\ClosedTerm\argdot
\\\multicolumn
{\qquad
\EvalsToterm
{\Consterm
{b}}
\wedge
\subst
\wedge
\RepsSeqterm
.}
\end
]
If $s$ is of length $0$, then it is the empty sequence $()$.
Since $t_s \repsrelforseq
s$, we can conclude that
$t_s$ evaluates to $\nilterm$. Likewise, $t'_s$ also evaluates
to $\nilterm$. But then, the two terms are computationally equivalent
to the terms
$
\EvalsToterm
$
and
$
\EvalsToterm
$
respectively.
By hypothesis, $t_z$ and $t'_z$ each represent the closed term
$z$. It is easy to show that $\Nil$ represents the closed
term $\nilterm$. And in chapter~\ref{}, we define
$\EvalsTo$ to represent the $\evalstoarg$ predicate.
Therefore, these terms are equal types; moreover, they are inhabited
if and only if $\evalsto
$. But
$z \repsrelforseq
()$ if and only if $\evalsto
$.
Otherwise, $s$ is a non-empty sequence
$(s_1, \ldots, s_n)$ of length $n=k+1$.
Since $t_s$ represents $s$, we can conclude that there are terms
$t_a$ and $t_b$ such that $t_s$ evaluates to $\consterm
$,
$t_a \repsrelfor
s_1$ and $t_b \repsrelforseq
(s_2,\ldots,s_n)$.
Since $t_s$ is closed, so too is $\consterm
$.
Thus, $t_a$ and $t_b$ are closed.
In a similar fashion, we deduce the existence of closed terms $t'_a$
and $t'_b$ such that
$\evalsto
{\consterm
{t'_b}}$,
$t'_a \repsrelfor
s_1$,
and $t'_b \repsrelforseq
(s_2,\ldots,s_n)$.
From this, we can conclude that $\RepsSeqterm
$
and $\RepsSeqterm
$ are computationally equivalent to
[
\begin
\exists a\argcomma b\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Consterm
{b}}
\wedge
\subst
\wedge
\RepsSeqterm
,
\end
]
and
[
\begin
\exists a\argcomma b\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Consterm
{b}}
\wedge
\subst
\wedge
\RepsSeqterm
.
\end
]
respectively.
Now, we need to show that two terms of the form
$\exists a\argcomma b \colon \ClosedTerm\argdot Q$ and
$\exists a\argcomma b \colon \ClosedTerm\argdot Q'$ are equal
types which are inhabited if and only if $z$ represents $s$.
Since $s$ is the non-empty sequence $(s_1, \ldots, s_n)$,
this is the case if and only if there are closed
terms $A$ and $B$ such that $z$ evaluates to
$\consterm
$, $A \repsrelfor
s_1$, and
$B \repsrelforseq
(s_2, \ldots, s_n)$.
Since the type $\ClosedTerm$ represents the class of
closed terms using the relation $\reps$, two terms are equal members
of $\ClosedTerm$ if and only if they represent the same closed term.
For this reason it suffices to show that for any
closed terms $A$ and $B$, if $t_A$ and $t'_A$ both represent $A$, and
$t_B$ and $t'_B$ both represent $B$, then
the types $\subst
$ and
$\subst
$ are equal types inhabited
if and only if $\consterm
$, $A \repsrelfor
s_1$, and
$B \repsrelforseq
(s_2, \ldots, s_n)$.
To show that this is the case, we consider each conjunct,
one at a time.
It is easy to
show that $\Consterm
$ and $\Consterm
$
both represent $\consterm
$. Then,
$\EvalsToterm
{\Consterm
{t_B}}$ and
$\EvalsToterm
{\Consterm
{t'_B}}$ are equal types.
They are inhabited if and only if $z$ evaluates to $\consterm
$.
Note that $t_A$ and $t'_A$ both represent the same
closed term $A$, and that $t_a$ and $t'_a$ both represent
the same element $s_1$ of $\cal K$. By assumption,
$\subst
$ and $\subst
$
are equal types. They are inhabited if and only if
$A \repsrelfor
s_1$.
Note that $t_B$ and $t'_B$ represent the same closed term
$B$. Note too that $t_b$ and $t'_b$ both represent the
sequence $(s_2, \ldots, s_n)$. This sequence is of length $k$,
so the induction hypothesis applies. We conclude that
the terms
$\RepsSeqterm
$ and $\RepsSeqterm
$
are equal types, and that they are inhabited if and only if
$B \repsrelforseq
(s_2, \ldots, s_n)$.
\subsection
Recall that if $\repsrelfor
$ is a representation relation for the
class $\cal K$, and if for each object $k$ of $\cal K$
$\repsrelfor
$ is a representation relation for the
class $
_k$ then the relation $\repsdp
$
is a representation relation for the class $x\colon
_x$.
Recall that the class $x\colon
_x$ contains those objects
which consists of an object $k$ from $\cal K$ together with an object
$l$ from $
_k$.
Just as for our construction of representation
relations for sequences, we can think of the construction
of $\repsdp
$ from the representation relation
$\repsrelfor
$ and the family of relations $\repsrelfor
$
as an operation. This time, the operation maps representation
relations and families of representation relations to representation
relations. We represent the construction in much the same way as
we represented the construction of $\repsrelforseq
$ from
$\repsrelfor
$.
The fact that the second argument to this construction
is a family of representation relation causes no real difficulty.
We can define an operation which maps elements $k$ of $\cal K$
to the corresponding representation relation $\repsrelfor
$.
We then uncurry this operation to yield a three place predicate on elements
$k$ of $\cal K$, closed terms $t$, and elements $l$ of $
_k$.
This predicate is satisfied if and only if $t \repsrelfor
l$.
This allows us to think of our construction as a predicate valued operation
in two predicate arguments.
\begin
[
\begin
\RepsProdterm
\abstreq {}
\\\qquad
\proglet{\pairterm
{b}}
\progin
\exists A\argcomma B\colon\ClosedTerm\argdot {}
\\\qquad\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge
R[A\argsemi a]
\wedge
S[a\argsemi B\argsemi b]
\end
]
\end
\begin
Let $\cal K$ be a class of objects, and let
$\repsrelfor
$ be a representation relation for $\cal K$.
For each $k$ in $\cal K$ let $
_k$ be a class of objects,
and let $\repsrelfor
$ be a representation relation for $
_k$.
Suppose that for any element $k$ of $\cal K$, and any closed term
$t$, and for any closed terms $t_k$, $t'_k$, $t_t$, and $t'_t$
such that $t_k \repsrelfor
k$, $t'_k \repsrelfor
k$,
$t_t \reps t$, and $t'_t \reps t$, the terms
$\subst
$ and $\subst
$
are equal types which are inhabited if and only if
$t \repsrelfor
k$.
Suppose that for any element $k$ of $\cal K$, any closed term
$t$, and any element $l$ of $
_k$,
and for any closed terms $t_k$, $t'_k$, $t_t$, $t'_t$,
$t_l$, and $t'_l$,
such that $t_k \repsrelfor
k$, $t'_k \repsrelfor
k$,
$t_t \reps t$, $t'_t \reps t$,
$t_l \repsrelfor
k$, and $t'_l \repsrelfor
k$,
the terms
$\subst
$ and
$\subst
$
are equal types which are inhabited if and only if
$t \repsrelfor
b$.
Suppose that $p$ is an element of $x\colon
_x$,
and that $t_p$ and $t'_p$ are closed terms such that
$t_p \repsdp
p$ and $t'_p \repsdp
p$.
Suppose that $z$ is closed term and that
$t_t$ and $t'_t$ are closed terms such that
$t_t \reps z$ and $t'_t \reps z$.
Then, the terms
$
\RepsProdterm
$
and
$
\RepsProdterm
$
are equal types.
Moreover, they are inhabited if and only if
$z \repsdp
p$.
\end
Since $p$ is an element of $x\colon
_x$,
it is an object of the form $\langle k, l rangle$. Since $t_p$
represents $p$, there are terms $t_k$ and $t_l$ such that
$\evalsto
{\pairterm
{t_l}}$, $t_k \repsrelfor
k$, and
$t_l \repsrelfor
l$. Similarly, there are terms $t'_k$ and $t'_l$
such that $\evalsto
{\pairterm
{t'_l}}$, $t'_k \repsrelfor
k$,
and $t'_l \repsrelfor
l$.
If we expand $\RepsProdterm
$,
we obtain a term of the form $\proglet{\pairterm
{b}}
\progin C$.
And since $t_p$ evaluates to $\pairterm
$, this term is
computationally equivalent to the term $\subst
$.
Thus, $\RepsProdterm
$ is computationally
equivalent to
[
\exists A\argcomma B\colon\ClosedTerm\argdot {}
\EvalsToterm
{\Pairterm
{B}}
\wedge
\subst
\wedge
\subst
]
In a similar fashion, we conclude that
$\RepsProdterm
$ is computationally
equivalent to
[
\exists A\argcomma B\colon\ClosedTerm\argdot {}
\EvalsToterm
{\Pairterm
{B}}
\wedge
\subst
\wedge
\subst
]
We must show that these two terms are equal types
and that they are inhabited if and only if $t \repsdp
p$.
By definition, this is the case if and only if there are terms
$a$ and $b$ such that $\evalsto
{\pairterm
{b}}$,
$a \repsrelfor
k$, and $b \repsrelfor
l$.
Since $t$ is closed, $a$ and $b$ must be closed as well.
Because the type $\ClosedTerm$ represents the class of
closed terms using the relation $\reps$, two terms are equal members
of $\ClosedTerm$ if and only if they represent the same closed term.
For this reason, it suffices to show that for any closed terms $A$
and $B$ and terms $t_A$, $t'_A$, $t_B$ and $t'_B$ such that
$t_A \reps A$, $t'_A \reps A$, $t_B \reps B$, and $t'_B \reps B$,
the following terms are equal types, and are inhabited if and only
$\evalsto
{\pairterm
{B}}$,
$A \repsrelfor
k$, and $B \repsrelfor
l$:
[
\begin
\EvalsToterm
{\Pairterm
{t_B}}
\wedge
\subst
\wedge
\subst
\\\\
\EvalsToterm
{\Pairterm
{t'_B}}
\wedge
\subst
\wedge
\subst
\end
]
This is shown by considering each pair of corresponding conjuncts,
one at a time.
We must show that each is a pair of equal types, and that
all conjuncts are inhabited if and only if
$\evalsto
{\pairterm
{B}}$,
$A \repsrelfor
k$, and $B \repsrelfor
l$:
Since $t_A$ and $t'_A$ both represent $A$, and
$t_B$ and $t'_B$ both represent $B$, the terms $\Pairterm
$ and
$\Pairterm
$ both represent $\pairterm
$.
Then since $t_t$ and $t'_t$ both represent the same term $t$,
the terms $\EvalsToterm
{\Pairterm
{t_B}}$ and
$\EvalsToterm
{\Pairterm
{t'_B}}$ are equal types.
Moreover they are inhabited if and only if $\evalsto
{\pairterm
{B}}$.
Since $t_k$ and $t'_k$ both represent the object $k$ of $\cal K$,
and since $t_A$ and $t'_A$ both represent the closed term $A$,
we can deduce, from our assumptions, that the terms
$\subst
$ and $\subst
$ are
equal types. Moreover, they are inhabited if and only if
$A \repsrelfor
k$.
Since $t_k$ and $t'_k$ both represent the object $k$ of $\cal K$,
since $t_l$ and $t'_l$ both represent the object $l$ of $
_k$,
and since $t_B$ and $t'_B$ both represent the closed term $B$,
we can deduce, from our assumptions, that the terms
$\subst
$ and $\subst
$ are
equal types. Moreover, they are inhabited if and only if
$B \repsrelfor
l$.
\subsection
Whenever a new index family name is introduced, representation
fragments are provided for it. Thus, for each index family name $f$,
there is a computationally closed representation relation $\repsrelfor
$
for the corresponding index family. In a sense, then,
the representation relation fragment can be thought of as a
representation relation valued operation on index family names.
We use the fact that there is a correspondence between
index family names and the representation relation for the
corresponding index families. Consider the representation relation for
tagged parameters. It is defined as $\repsdp
$.
For this to be sensible, there must be a representation relation
$\repsrelfor
$ corresponding to each index family. For it to be correct,
$\repsrelfor
$ must be a representation relation for the index family
corresponding to $f$. For this reason, it is essential that we
represent not only the individual representation fragments, but also
the entire representation fragment operation.
Recall that the class of index family names is open-ended.
Moreover, each representation relation is defined independently:
there are no uniformity condition on these relations. Thus,
any attempt to represent the representation fragment operation
must explicitly take into account this open-endedness. Otherwise,
the addition of new index family names will almost certainly render
the representation wrong. So far, the only primitive operator
that has a definition which is automatically extended each time a
new index family name is added is $\IFam$. Unfortunately, there does
not seem to be any way to use it to give a representation
of the representation fragment operation. For each index family name,
it provides a type that represents the corresponding index family
using the representation relation $\repsrelfor
$. But it
provides no connection between a term of this type and the object it
represents. In fact, we could still gather these terms as a type,
with the same equality, even if there were no underlying index family.
Therefore, we must add a new operator to represent the
representation fragment operation.
Our solution is to introduce a new three place type
constructor $\RepsRelFrag$. We define this operator as a new type
constructor in such a way that
it represents the
representation fragment operation. Recall that our method of
representing predicate valued operations requires that we first
uncurry them. This means that $\RepsRelFrag$ should represent a three
place predicate on index family names $f$, closed terms $t$, and
objects $x$ that belong to the index family named by $f$. This
predicate is satisfied if and only $t \repsrelfor
x$. Thus, if $F$
represents an index family name $f$, $T$ represents a closed term $t$, and
$X$ represents an object $x$ of the index family named by $f$,
the term $\RepsRelFragterm
$ should be a type.
This type is either inhabited or not depending on the truth of
$t \repsrelfor
x$. Only one question really remains:
which terms belong to $\RepsRelFragterm
$ when it is inhabited?
Just as is the case with the type $\equalitytype
$, there
doesn't seem to be any further information to convey. For this reason,
we declare that the only terms that can belong to $\RepsRelFragterm
$,
are those that evaluate to $\axiom$. Furthermore, all members of
$\RepsRelFragterm
$ are equal. We can state this
more formally as a clause in the definition of the Nuprl type theory.
\begin
Suppose that $t$ evaluates to $\RepsRelFragterm
$,
and $t'$ evaluates to $\IFamterm
$.
The terms $t$ and $t'$ are equal types if and only if
there is an index family name $f$, a closed term $s$, and
an object $x$ of the index family corresponding to $f$, such that
$F \repsrelfor
f$, $F' \repsrelfor
f$,
$S \reps s$, $S' \reps s$, $X \repsrelfor
x$, and
$X' \repsrelfor
x$. Two terms $r$ and $r'$ are
equal members of these types if and only if
$\evalsto
$, $\evalsto
$
and $s \repsrelfor
x$.
\end
Simply adding a type like this is insufficient. We must also provide
inference rules with which to prove theorems about the type and its elements.
We begin by introducing a rule which allows us to prove that terms
are equal types because of this clause of the definition of the Nuprl
type system.
[
\begin
\sequent
{\equalitytype{\universeterm{i}}
{\RepsRelFragterm
{X}}
{\RepsRelFragterm
}}
\qquad\sequent
{\equalitytype
{F'}}
\qquad\sequent
{\equalitytype
{T'}}
\qquad\sequent
{\equalitytype{\IFamterm{F}}
{X'}}
\end
]
Earlier we showed that two terms $F$ and $F'$ are equal members of the type
$\IFName$ if and only if they represent the same index family
$f$. Likewise, $T$ and $T'$ are equal members of the type
$\ClosedTerm$ if and only if they represent the same closed term.
Since $F$ represents an index family name $f$,
$\IFamterm
$ is a type. $X$ and $X'$ are equal members of
$\IFamterm
$ if and only if they represent the same object $x$ of
the index family corresponding to $f$. Thus, if each of the
subgoal sequents is true, so is the goal sequent. Therefore, this
rule is valid.
Next we need to be able to prove theorems asserting the inhabitation
of terms of the form $\RepsRelFragterm
$. Just as was the case
for $\IFam$, two classes of rules seem to be useful. First, a general,
open-ended rule, which axiomatizes $\RepsRelFragterm
$ fully
whenever $F$, $T$, and $X$ are closed terms. As before, the problems with
this rule are that it says nothing at all about situations in which
one or more of these terms has free variables (declared in the hypotheses
of the sequent), and that it has a complicated side condition. In
any case, the rule allows us to prove the goal sequent
[
\sequent
{\RepsRelFragterm
{X}}
]
with no subgoals, provided $F$ represents an index family name $f$,
$T$ represents a closed term $t$, $X$ represents an object $x$ of
the index family associated with $f$, and $t \repsrelfor
x$.
Second, we include rules for reasoning about
$\RepsRelFragterm
$, when $F$ represents a particular
index family name. For example, we might include the following rule.
[
\begin
\sequent
{\RepsRelFragterm{\ifidterm
}
{X}}
\qquad\sequent
{\EvalsToterm
{\Ifidterm
}}
\qquad\sequent
{\membershiptype
{T}}
\qquad\sequent
{\membershiptype
{X}}
\end
]
where the operator $\Ifid$ is defined so that
$\Ifidterm
$ represents $\ifidterm
$ whenever $X$ represents the
index family name $x$. This is done as follows,
[
\Ifidterm
\abstreq
\pairterm{\pairterm{\opidterm{\ifid}}
{[\pairterm{\ifidterm{\ifname}}
]}}
.
]
Recall that $t \repsrelfor
x$ if and only if
$\evalsto
{\ifidterm{x}}$, this condition is enforced by the first subgoal
of the proposed rule. The remaining subgoals ensure that
the goal conclusion $\RepsRelFragterm{\ifidterm{\ifname}}
$is,
in fact, a type. Since $\ifidterm
$ represents
the index family name $\ifname$, we only need two subgoals, rather than
three. Similar rules can be given for several of the other
index family names, in particular $\opname$, $\token$ and $\natnumber$.
A somewhat more interesting example is provided by the following
rules:
[
\begin
\sequent
{\RepsRelFragterm{\ifidterm
}
{X}}
\qquad\sequent
{\RepsSeqterm
{\RepsVarCharterm
{y}}
{X}}
\sequent
{\RepsSeqterm
{\RepsVarCharterm
{y}}
{X}}
\qquad\sequent
{\RepsRelFragterm{\ifidterm
}
{X}}
\end
]
These rules use the operator $\RepsSeq$ defined above, and also use
the operator $\RepsVarChar$, which is intended to represent the
predicate $\repsrelfor
$, and which we discuss below.
Recall that the $\repsrelfor
$ is defined as
$\repsrelforseq
$. Assuming that
$\RepsVarChar$ represents the relation $\repsrelfor
$,
we can conclude that whenever $S$ and $S'$ represent the same
closed term $s$, and $C$ and $C'$ represent the same variable character $c$,
the terms $\RepsVarCharterm
$ and $\RepsVarCharterm
$
are equal types which are inhabited if and only if
$s \repsrelfor
c$. Therefore, if $T$ and $T'$ represent the
same term, and $X$ and $X'$ represent the same sequence $x$
of variable characters, theorem~\ref{} allows us to conclude that
$\RepsSeq
{\RepsVarCharterm
{y}}
$ and
$\RepsSeq
{\RepsVarCharterm
{y}}
$ are equal types
and that they are inhabited if and only if
$t \repsrelforseq
x$. But since $x$ is a sequence of
characters, it is a variable name. Moreover, by definition,
$t \repsrelfor
x$ if and only if $t \repsrelforseq
x$.
By definition, $\RepsRelFragterm{\ifidterm
}
$ holds
if and only if $t \repsrelforseq
x$.
We conclude that $\RepsSeq
{\RepsVarCharterm
{y}}
$
is inhabited if and only if $\RepsRelFragterm{\ifidterm{\varname}}
$
is. This justifies the above rules.
\begin
[
\begin
\RepsVarCharterm
\abstreq
\EvalsToterm
{\Natnumterm{C}} \wedge 0 \le C \le 255
\Natnumterm
\abstreq
\pair{
\pair{\opidterm{\natnum}}{[\pair{\ifidterm
}
]}}
\end
]
\end
\begin
The operator $\RepsVarChar$ represents the relation
$\repsrelfor
$.
\end
Suppose that $T$ and $T'$ represent the closed term $t$ and that
$C$ and $C'$ represent the variable character $c$. We show that
the terms $\RepsVarCharterm
$ and $\RepsVarCharterm
$
are equal types and are inhabited if and only if
$t \repsrelfor
c$.
By definition $C$ evaluates to $\natnumterm{\varcharcode{c}}$. But
then, $C$ also represents the natural number parameter
$\varcharcode
$. Similarly, $C'$ represents the natural number
parameter $\varcharcode
$ too. In particular, this means that the
terms $\Natnumterm
$ and $\Natnumterm
$ both represent the term
$\natnumterm{\varcharcode{c}}$.
Then, the terms $\EvalsToterm
{\Natnumterm{C}}$ and
$\EvalsToterm
{\Natnumterm{C'}}$ are equal types which are inhabited
if and only if $\evalsto
{\natnumterm{\varcharcode
}}$; that is,
if and only f $t \repsrelfor
c$.
Since $C$ and $C'$ both evaluate to the same term
$\natnumterm{\varcharcode{c}}$, the terms
$0 \le C \le 255$ and $0 \le C' \le 255$ are equal types;
moreover, since $\varcharcode
$ is always between $0$ and $255$,
this type is always inhabited.
The reason for adding the additional clause $0 \le C \le 255$
is to ensure that $\RepsVarCharterm
$ is only provably inhabited if
$C$ actually represents a variable character; otherwise,
we would be able to prove that $\RepsVarCharterm
$ is
inhabited if $C$ represents an integer $n$, and $t$ represents
a closed term which represents $n$.
In certain circumstances, we may need to prove that if
$\RepsRelFragterm
$ is inhabited, then $\axiom$ belongs to it.
This suggests the following additional rule:
[
\sequent
{\equalitytype{\RepsRelFragterm
{X}}
{\axiom}}
\\\qquad\sequent
{\RepsRelFrag
{X}}.
]
Used together with the direct computation rule, this rule allows us
to show that any pair of terms which both evaluate to $\axiom$ are equal
members of $\RepsRelFrag
$, provided it has members at all.
\subsection
Using the operators defined in the previous sections, we can give
representations of the representation relations for various components
of terms.
\begin
[
\begin
\RepsIFNameterm
\abstreq \RepsRelFragterm{\ifidterm{\ifname}}
\RepsOpNameterm
\abstreq \RepsRelFragterm{\ifidterm{\opname}}
\RepsVarNameterm
\abstreq
\RepsRelFragterm{\ifidterm
}
\RepsParamterm
\abstreq
\RepsProdterm
{\RepsIFNameterm
{y}}
{\RepsRelFragterm
{w}}
\RepsParamsterm
\abstreq
\RepsSeqterm
{\RepsParamterm
{y}}
\RepsOperatorterm
\abstreq
\RepsProdterm
{\RepsOpNameterm
{y}}
{\RepsParamsterm
{w}}
\RepsBindingsterm
\abstreq
\RepsSeqterm
{\RepsVarNameterm
}
\end
]
\end
\begin
$\RepsIFName$ represents the relation $\repsrelfor
$.
$\RepsOpName$ represents the relation $\repsrelfor
$.
$\RepsVarName$ represents the relation $\repsrelfor
$.
$\RepsParam$ represents the relation $\repsrelfor
$.
$\RepsParams$ represents the relation $\repsrelfor
$.
$\RepsOperator$ represents the relation $\repsrelfor
$.
$\RepsBindings$ represents the relation $\repsrelfor
$.
\end
The first three conclusions follow immediately by
expansion and the definition of $\RepsRelFrag$.
Thus, if $A$ and $A'$ represent the closed term $a$, and
$F$ and $F'$ represent the index family name $f$, the terms
$\RepsIFNameterm
$ and $\RepsIFNameterm
$ are equal types,
and are inhabited if and only if $a \repsrelfor
f$.
If $G$ and $G'$ represent an index family name $g$,
$B$ and $B'$ represent a closed term $b$, and $X$ and $X'$
represent an object $x$ of the index family associated with $g$,
then the terms $\RepsRelFragterm
$ and $\RepsRelFragterm
$
are equal types, and are inhabited if and only if
$b \repsrelfor
x$. Therefore, by theorem~\ref{}
if $T$ and $T'$ represent the closed term $t$,
and $P$ and $P'$ represent an object $p$ which consists
of an index family name together with an object of the corresponding
index family, then the terms
[
\RepsRelFragterm
{\RepsIFNameterm
{y}}
{\RepsRelFragterm
{w}}
]
and
[
\RepsRelFragterm
{\RepsIFNameterm
{y}}
{\RepsRelFragterm
{w}}
]
are equal types, and are inhabited if and only if
[
t \repsdp
p.
]
But $p$ is a tagged parameter, and $\repsdp
$
is $\repsrelfor
$. Since the displayed terms are the
terms to which $\RepsParamterm
$ and $\RepsParamterm
$ expand,
we conclude that $\RepsParam$ represents the relation $\repsrelfor
$.
Suppose that $T$ and $T'$ represent the same closed term $t$,
and that $P$ and $P'$ represent the same sequence of tagged parameters $p$.
The term $\RepsParamsterm
$ expands to
$\RepsSeqterm
{\RepsParamterm
}
$,
and $\RepsParamsterm
$ expands to
$\RepsSeqterm
{\RepsParamterm
{y}}
$.
Since $\RepsParam$ represents the predicate $\repsrelfor
$,
theorem~\ref{} allows us to conclude that
these terms are equal types, and that they are inhabited if and only
if $t \repsrelforseq
p$; that is, if and only if
$t \repsrelfor
p$.
Suppose that $T$ and $T'$ represent the same closed term $t$,
and that $O$ and $O'$ represent the same operator $o$.
The term $\RepsOperatorterm
$ expands to
[
\RepsProdterm
{\RepsOpNameterm
{y}}
{\RepsParamsterm
{w}}
]
and $\RepsOperatorterm
$ expands to
[
\RepsProdterm
{\RepsOpNameterm
{y}}
{\RepsParamsterm
{w}}
]
Suppose that $A$ and $A'$ represent the same term $a$, and that
$Q$ and $Q'$ represent the operator name $q$.
We conclude that $\RepsOpName
$ and $\RepsOpName
$ are equal types
which are inhabited if and only if $a \repsrelfor
q$.
And if $Z$ and $Z'$ represent the operator name $z$,
$B$ and $B'$ represent the same term $p$, and
$P$ and $P'$ represent the same sequence of tagged parameters $p$,
the terms $\RepsParamsterm
$ and $\RepsParamsterm
$ are
equal types and are inhabited if and only if
$b \repsrelfor
p$.
Using theorem~\ref{}, we conclude that
[
\RepsProdterm
{\RepsOpNameterm
{y}}
{\RepsParamsterm
{w}}
]
and
[
\RepsProdterm
{\RepsOpNameterm
{y}}
{\RepsParamsterm
{w}}
]
are equal types, and are inhabited if and only if
$t \repsip
o$; that is, if and only if
$t \repsrelfor
o$.
Suppose that $T$ and $T'$ represent the same closed term $t$,
and that $B$ and $B'$ represent the same sequence of variable names $b$.
The term $\RepsBindingsterm
$ expands to
$\RepsSeqterm
{\RepsVarNameterm
}
$,
and $\RepsBindingsterm
$ expands to
$\RepsSeqterm
{\RepsVarNameterm
}
$.
Since $\RepsVarName$ represents the predicate $\repsrelfor
$,
theorem~\ref{} allows us to conclude that
these terms are equal types, and that they are inhabited if and only
if $t \repsrelforseq
b$; that is, if and only if
$t \repsrelfor
b$.
Representing the relation $\reps$ itself is somewhat more difficult.
Recall that, effectively, $\reps$ is defined by induction on the height
of the term to be represented. We could, instead have used induction on
the
of this term. We would have achieved the same results.
This suggests that we ought to use the operator $\Termind$ in
our representation of $\reps$ since it is intended to represent
primitive recursion on terms.
\begin
[
\begin
\Repsgenterm
\abstreq {}
\qquad
\lambda F\argcomma i\argcomma S\argdot
\inteq\argleft i\argsemi n+1 \argsemi \EvalsToterm
\argsemi
\\\qquad\qquad
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad\qquad{}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad\qquad{}
\wedge \RepsBindingsterm
\wedge h(D)
\wedge F(i + 1)(B)\argright
\Repsterm
\abstreq {}
\qquad
(\Termind\argleft X \argsemi
o \argcomma n\argcomma b \argcomma s \argcomma h\argdot\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)\argright
\qquad
)(T)
\end
]
\end
\begin
The operator $\Reps$ represents the predicate $\reps$.
\end
We need to show that if $T$ and $T'$ both represent a
closed term $t$, and $X$ and $X'$ both represent a term $x$,
then $\Repsterm
$ and $\Repsterm
$ are equal types, and are
inhabited if and only if $t \reps x$. First, we prove a technical
lemma concerning the operator $\Repsgen$, using this, together with
theorem~\ref{}, which characterizes the operator $\Termind$, the
desired theorem follows easily.
Suppose that $t_n$ and $t'_n$ each represent a natural number $n$,
that $t_S$ and $t'_S$ each represent a closed term $S$, and that
$t_m$ and $t'_m$ each represent a natural number $m$, with $1 \le m \le n + 1$.
Suppose that for each integer $i$ between $1$ and $n$,
there is a sequence of variable names $\sequence
_i$ and
a term $s_i$.
Suppose that for each natural number $i$ between $1$ and $m$,
if both $t_i$ and $t'_i$ represent $i$, then $t_b(t_i)$ and $t'_b(t'_i)$
both represent a sequence $\sequence
_i$ of variable names.
Suppose that for each integer $i$ between $1$ and $n$,
and all closed terms $A$,
if both $t_i$ and $t'_i$ represent $i$, and both $T_A$ and $t'_A$ represent
$A$, then $t_b(t_i)(t_A)$ and $t'_b(t'_i)(t'_A)$ are equal types,
and these types are inhabited if and only if $A \reps s_i$.
Then, the terms
[
\ycomb (\Repsgenterm
) (t_m) (t_S)
]
and
[
\ycomb (\Repsgenterm
) (t'_m) (t'_S)
]
are equal types,
and are inhabited if and only if
[
S \mathrel{({\repsip
{\term}})^*}
(\langle \sequence
_m, s_m\rangle,
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
The proof is by induction on $n + 1 - m$. Since $m \le n + 1$,
this is always positive. First, we
replace each of the terms with a computationally equivalent term.
Consider
[
\ycomb (\Repsgenterm
) (t_m) (t_S).
]
We replace the subterm $\ycomb (\Repsgenterm
)$
with the computationally equivalent term
[
(\Repsgenterm
) (\ycomb (\Repsgenterm
)).
]
We then expand the first instance of $\Repsgen$, and contract the resulting
beta redices. This yields the term
[
\begin
\inteq\argleft t_m\argsemi t_n+1 \argsemi
\EvalsToterm
\argsemi
\\\qquad
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad{}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad{}
\wedge \RepsBindingsterm
\wedge t_h(t_m)(D)
\wedge \ycomb (\Repsgenterm
)(t_m + 1)(B)\argright
\end
]
In a similar fashion, we can replace
[
(\Repsgenterm
) (\ycomb (\Repsgenterm
))
]
with
[
\begin
\inteq\argleft t'_m\argsemi t'_n+1 \argsemi
\EvalsToterm
\argsemi
\\\qquad
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad{}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad{}
\wedge \RepsBindingsterm
\wedge t'_h(t'_m)(D)
\wedge \ycomb (\Repsgenterm
)(t'_m + 1)(B)
\argright.
\end
]
Now, suppose that $n+1-m =0$. Then, $n+1 = m$.
Since $t_n$ represents $n$, $t_n + 1$ represents $n+1$.
But then $t_n + 1$ evaluates to the term $\natnumterm
$.
And since $t_m$ represents $m$, it evaluates to $\natnumterm
$.
But $m$ is $n+1$, so $\natnumterm
$ is $\natnumterm
$.
This allows us to conclude that a term of the form
$\inteqterm
$ is computationally equivalent
to $A$. Similarly, a term of the form $\inteqterm
$
is computationally equivalent to $A'$.
Furthermore, since $m > n$, the sequence
[
(\langle \sequence
_m, s_m\rangle,
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
is empty.
Thus, we need only show that
the terms $\EvalsToterm
$ and
$\EvalsToterm
$ are equal types, and that they are
inhabited if and only if $S$ represents the empty sequence.
Since $\Nilterm$ represents the term $\nilterm$, and $t_S$ and $t'_S$
represent the same closed term $S$, these two terms are equal types.
They are inhabited if and only if $\evalsto
$.
But $S \mathrel{({\repsip
{\term}})^*} ()$ if and only if
$\evalsto
$.
Otherwise, $n+1-m > 0$. Then, $m \le n$. In addition, we assumed
that $m \ge 1$. Since both $t_m$ and $t'_m$ represents $m$,
we can conclude that $t_b(t_m)$ and $t'_b(t'_m)$ each represent
the sequence $\sequence
_m$ of variable names. Likewise,
for any closed term $R$, if both $t_R$ and $t'_R$ represent
$R$, $t_h(t_m)(t_R)$ and $t'_h(t'_m)(t'_R)$ are equal types
and are inhabited if and only if $R \reps s_m$.
As before, $t_m$ evaluates to a term $\natnumterm
$ and
$t_n+1$ evaluates to a term $\natnumterm
$. This time,
however, the $m$ and $n+1$ are distinct. This allows us to
conclude that a term of the form $\inteq
$
is computationally equivalent to $Y$. Similarly, a term of the
form $\inteq
$
is computationally equivalent to $Y'$.
Therefore, we need only show that the terms
[
\begin
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
{}
\wedge \EvalsToterm
{\Pairterm
{D}}
{}
\wedge \RepsBindingsterm
\wedge t_h(t_m)(D)
\wedge \ycomb (\Repsgenterm
)(t_m + 1)(B)
\argright
\end
]
and
[
\begin
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
{}
\wedge \EvalsToterm
{\Pairterm
{D}}
{}
\wedge \RepsBindingsterm
\wedge t'_h(t'_m)(D)
\wedge \ycomb (\Repsgenterm
)(t'_m + 1)(B)
\argright.
\end
]
are equal types, and are inhabited if and only if
[
S \mathrel{({\repsip
{\term}})^*}
(\langle \sequence
_m, s_m\rangle,
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
Since $m \le n$, the sequence $S$ is required to represent is
non-empty. This means that $S$ represents it
if and only if there
are closed terms $A$ and $B$ such that $S$ evaluates to
$\consterm
$,
[
A \repsip
\langle \sequence
_i, s_m\rangle
]
and
[
B \mathrel{({\repsip
{\term}})^*}
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
$A$ represents the required pair if and only if
there are closed terms $C$ and $D$ such that $A$
evaluates to $\pairterm
$, $C \repsrelfor
\sequence
_m$
and $D \reps s_m$.
Terms of the form $\exists x\colon X\argdot P$ and
$\exists x'\colon X'\argdot P'$ are equal types if and only if
$X$ and $X'$ are equal types, and for all terms $a$ and $a'$ that are
equal members of $X$, $\subst
$ and $\subst
$.
They are inhabited if and only if there is a term $a$ that is a member of
$X$, and for which $\subst
$ is inhabited.
Since $\ClosedTerm$ is a type, two terms
$\exists A\argcomma B\argcomma C\argcomma D\colon \ClosedTerm P$
and
$\exists A\argcomma B\argcomma C\argcomma D\colon \ClosedTerm P'$
are equal types if and only if
for all terms $t_A$, $t'_A$, $t_B$, $t'_B$, $t_C$, $t'_C$, $t_D$,
and $t'_D$,
if $t_A$ and $t'_A$ are equal members of $\ClosedTerm$,
$t_B$ and $t'_B$ are equal members of $\ClosedTerm$,
$t_C$ and $t'_C$ are equal members of $\ClosedTerm$, and
$t_D$ and $t'_D$ are equal members of $\ClosedTerm$,
then $\subst
$
and $\subst
$ are equal types.
They are inhabited if and only if there are terms
$t_A$, $t_B$, $t_C$, and $t_D$ that are members of $\ClosedTerm$,
and for which $\subst
$ is inhabited.
The type $\ClosedTerm$ represents the class of closed terms, using the
relation $\reps$. Thus, $t_A$ and $t'_A$ are equal members of
$\ClosedTerm$ if and only if the represent the same closed term.
Moreover, $t_A$ belongs to $\ClosedTerm$ if and only if it represents
a closed term. Therefore,
two terms
$\exists A\argcomma B\argcomma C\argcomma D\colon \ClosedTerm P$
and
$\exists A\argcomma B\argcomma C\argcomma D\colon \ClosedTerm P'$
are equal types if and only if
for all terms $t_A$, $t'_A$, $t_B$, $t'_B$, $t_C$, $t'_C$, $t_D$,
and $t'_D$,
if $t_A$ and $t'_A$ represent the same closed term,
$t_B$ and $t'_B$ represent the same closed term,
$t_C$ and $t'_C$ represent the same closed term,
$t_D$ and $t'_D$ represent the same closed term,
then $\subst
$
and $\subst
$ are equal types.
They are inhabited if and only if there are terms
$t_A$, $t_B$, $t_C$, and $t_D$ that represent closed terms
and for which $\subst
$ is inhabited.
Suppose that $t_A$ and $t'_A$ represent a closed term $A$,
$t_B$ and $t'_B$ represent a closed term $B$,
$t_C$ and $t'_C$ represent a closed term $C$,
and $t_D$ and $t'_D$ represent a closed term $D$.
If we show that
[
\begin
\EvalsToterm
{\Consterm
{t_B}}
\wedge \EvalsToterm
{\Pairterm
{t_D}}
{}
\wedge \RepsBindingsterm
\wedge t_h(t_m)(t_D)
\wedge \ycomb (\Repsgenterm
)(t_m + 1)(t_B)
\argright.
\end
]
and
[
\begin
\EvalsToterm
{\Consterm
{t'_B}}
\wedge \EvalsToterm
{\Pairterm
{t'_D}}
{}
\wedge \RepsBindingsterm
\wedge t'_h(t'_m)(t'_D)
\wedge \ycomb (\Repsgenterm
)(t'_m + 1)(t'_B)
\argright.
\end
]
are equal types, then we have also show that the two
terms of the form
$\exists A\argcomma B\argcomma C\argcomma D\colon \ClosedTerm P$
displayed above are equal types.
If we show that these terms are inhabited if and only if
$\evalsto
{\consterm
{B}}$, $\evalsto
{\pairterm
{D}}$,
$C \repsrelfor
\sequence
_m$,
$D \reps s_m$ and
[
B \mathrel{({\repsip
{\term}})^*}
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
then we have also show that the terms of the form
$\exists A\argcomma B\argcomma C\argcomma D\colon \ClosedTerm P$
displayed above are inhabited if and only if there are closed terms
$A$, $B$, $C$ and $D$ for which these conditions hold;
that is they are inhabited if and only if
[
S \mathrel{({\repsip
{\term}})^*}
(\langle \sequence
_m, s_m\rangle,
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
Each of these is easily shown by analyzing each of the conjuncts in turn.
We need to show that each pair of corresponding conjuncts are equal types,
and that all of them are inhabited if and only if the required condition is
met.
Since $t_A$ and $t'_A$ both represent the closed term $A$, and
$t_B$ and $t'_B$ both represent the closed term $B$, we can conclude that
$\Consterm
$ and $\Consterm
$ both represent the term
$\consterm
$. Since $A$ and $B$ are closed, so too is $\consterm
$.
We also know that $t_S$ and $t'_S$ represent the closed term $S$.
From this we conclude that the terms
$\EvalsToterm
{\Consterm
{t_B}}$ and
$\EvalsToterm
{\Consterm
{t'_B}}$ are equal types,
and that they are inhabited if and only if
$\evalsto
{\consterm
{B}}$.
Since $t_C$ and $t'_C$ both represent the closed term $C$, and
$t_D$ and $t'_D$ both represent the closed term $D$, we can conclude that
$\Pairterm
$ and $\Pairterm
$ both represent the term
$\pairterm
$. Since $C$ and $D$ are closed, so too is $\pairterm
$.
We also know that $t_A$ and $t'_A$ represent the closed term $A$.
From this we conclude that the terms
$\EvalsToterm
{\Pairterm
{t_D}}$ and
$\EvalsToterm
{\Pairterm
{t'_D}}$ are equal types,
and that they are inhabited if and only if
$\evalsto
{\pairterm
{D}}$.
$t_C$ and $t'_C$ both represent the closed term $C$.
$t_b(t_m)$ and $t'_b(t'_m)$ both represent the sequence $\sequence
_m$
of variable names. We conclude that
$\RepsBindingsterm
$ and $\RepsBindingsterm
$
are equal types. They are inhabited if and only if
$C \repsrelfor
\sequence
_m$.
Since $t_D$ and $t'_D$ represent the same closed term $D$, the
terms $t_h(t_m)(t_D)$ and $t'_h(t'_m)(t'_D)$ are equal types, and are
inhabited if and only if $D \reps s_m$.
Finally, consider the terms
[
\ycomb (\Repsgenterm
)(t_m + 1)(t_B)
]
and
[
\ycomb (\Repsgenterm
)(t'_m + 1)(t'_B).
]
We know that $t_B$ and $t'_B$ represent the same closed term $B$.
We also know that both $t_m$ and $t'_m$ represent the integer $m$, and
that $1 \le m \le n$. But then $t_m+1$ and $t'_m+1$ each represent $m+1$.
Since $1 \le m \le n$, $1 \le m +1 \le n +1$.
Moreover, $n + 1 - m > n + 1 - (m + 1)$, so the induction hypothesis
applies. We conclude that these two terms are equal types,
and that they are inhabited if and only if
[
B \mathrel{({\repsip
{\term}})^*}
\langle \sequence
_
, s_
\rangle, \ldots
\langle \sequence
_n, s_n\rangle).
]
This completes the proof of our lemma concerning
$\Repsgen$. We use it together with theorem~\ref{}
to show that if $T$ and $T'$ both represent a
closed term $t$, and $X$ and $X'$ both represent a term $x$,
then $\Repsterm
$ and $\Repsterm
$ are equal types, and are
inhabited if and only if $t \reps x$.
Expanding $\Repsterm
$ yields the term
[
\begin
(\Termind\argleft X \argsemi
o \argcomma n\argcomma b \argcomma s \argcomma h\argdot\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)\argright
\qquad)(T)
\end
]
and expanding $\Repsterm
$ yields the term
[
\begin
(\Termind\argleft X' \argsemi
o \argcomma n\argcomma b \argcomma s \argcomma h\argdot\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)\argright
\qquad)(T')
\end
]
Since $X$ and $X'$ represent the same term, and $T$ and $T'$ represent
the same closed term, theorem~\ref{} applies.
We need only show that for any term
$x = \theta\arglist{\sequence
_1\argdot s_1\argsemi\ldots\argsemi
\sequence
_n\argdot s_n}$, and any closed term $t$,
if each of the following conditions hold
\begin
\item The terms $t_\theta$ and $t'_\theta$ both represent the
operator $\theta$.
\item The terms $t_n$ and $t'_n$ both represent the natural number $n$.
\item For each natural number $i$ between $1$ and $n$, if $t_i$ and $t'_i$
both represent $i$, then $t_b(t_i)$ and $t'_b(t'_i)$ both represent
the sequence $\sequence
_i$.
\item For each natural number $i$ between $1$ and $n$, if $t_i$ and $t'_i$
both represent $i$, then $t_s(t_i)$ and $t'_s(t'_i)$ both represent
the term $s_i$.
\item For each natural number $i$ between $1$ and $n$ and each closed term
$r$, if $t_i$ and $t'_i$ both represent $i$, and $t_r$ and $t'_r$
both represent $r$, then $t_h(t_i)(t_r)$ and $t'_h(t'_i)(t'_r)$
are equal types and are inhabited if and only if
$r \reps s_i$.
\item The terms $t_t$ and $t'_t$ represent the closed term $t$.
\end
Then,
[
\begin
(\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)
\qquad)(t_t)
\end
]
and
[
\begin
(\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)
\qquad)(t'_t)
\end
]
are equal types, and are inhabited if and only $t \reps x$.
We contract the beta redices in each term, and then
note that each term is then of the form
$\exists A\argcomma B\colon \ClosedTerm\argdot P$.
We suppose that $t_A$ and $t'_A$ represent the same closed term $A$, and
that $t_B$ and $t'_B$ represent the same closed term $B$.
We show that
[
\begin
\EvalsToterm
{\Pairterm
{t_B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(t_B)
\end
]
and
[
\begin
\EvalsToterm
{\Pairterm
{t'_B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(t'_B)
\end
]
are equal types, and that they are inhabited if and only if
$\evalsto
{\pairterm
{B}}$, $A \repsrelfor
\theta$,
and
[
B \mathrel{({\repsip
{\term}})^*}
(\langle \sequence
_1, s_1\rangle, \ldots,
\langle \sequence
_n, s_n).
]
We do this one conjunct at a time.
Since $t_A$ and $t'_A$ both represent $A$, and $t_B$ and $t'_B$
represent $B$, we can conclude that $\pairterm
$ and
$\pairterm
$ both represent $\pairterm
$.
Since both $A$ and $B$ are closed, so is $\pairterm
$.
Then $\EvalsToterm
{\Pairterm
{t_B}}$
and $\EvalsToterm
{\Pairterm
{t'_B}}$
are equal types. They are inhabited if and only if
$\evalsto
{\pairterm
{B}}$.
Since $t_A$ and $t'_A$ represent the same closed
term $A$, and $t_\theta$ and $t'_\theta$ both represent the
same operator $\theta$, we can conclude that
$\RepsOperatorterm
$ and $\RepsOperatorterm
$
are equal types, and are inhabited if and only if
$A \repsrelfor
\theta$.
Since $n$ is a natural number, $n+1 \ge 1$. Therefore, $0 \le
1 \le n + 1$. The term $1$ represents the natural number $1$. By
hypothesis, $t_n$ and $t'_n$ both represent $n$. For each natural
number $i$ between $1$ and $n$, if $t_i$ and $t'_i$ both represent
$i$, then $t_b(t_i)$ and $t'_b(t'_i)$ both represent the sequence
$\sequence
_i$. For each natural number $i$ between $1$ and $n$ and
each closed term $r$, if $t_i$ and $t'_i$ both represent $i$,
and $t_r$ and $t'_r$ both represent $r$, then $t_h(t_i)(t_r)$ and
$t'_h(t'_i)(t'_r)$ are equal types and are inhabited if and only
if $r \reps s_i$. The terms $t_B$ and $t'_B$
both represent the closed term $B$.
Hence, the terms
[
\ycomb (\Repsgenterm
)(1)(t_B)
]
and
[
\ycomb (\Repsgenterm
)(1)(t'_B)
]
satisfy the hypotheses of our lemma concerning $\Repsgen$.
We conclude that they are equal types, and that they are inhabited
if and only if
[
B \mathrel{({\repsip
{\term}})^*}
(\langle \sequence
_1, s_1\rangle, \ldots,
\langle \sequence
_n, s_n).
]
From this, we conclude that the two terms of the
[
\begin
(\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)
\qquad)(t_t)
\end
]
and
[
\begin
(\lambda S\argdot
\exists A\argcomma B\colon\ClosedTerm\argdot
\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \RepsOperatorterm
\qquad {}
\wedge \ycomb (\Repsgenterm
)(1)(B)
\qquad)(t'_t)
\end
]
are equal types, and that they are inhabited if and
only if there are closed terms $A$ and $B$ such that
$\evalsto
{\pairterm
{B}}$, $A \repsrelfor
\theta$,
and
[
B \mathrel{({\repsip
{\term}})^*}
(\langle \sequence
_1, s_1\rangle, \ldots,
\langle \sequence
_n, s_n).
]
But this is the case if and only if
[
t \mathrel{{\repsrelfor{\operator}} \times
{({\repsip
{\term}})^*}}
\langle \theta,
(\langle \sequence
_1, s_1\rangle, \ldots,
\langle \sequence
_n, s_n)\rangle.
]
But the required relation is, by definition
$
[{\repsrelfor{\term}}]$. And any object that consists
of an operator together with a sequence of pairs, each of which
consists of a a sequence of variable names and a term, is itself a term.
Thus, we can rewrite this condition as
[
t \mathrel{
[{\repsrelfor{\term}}]}
\theta\arglist{\sequence
_1\argdot s_1\argsemi\ldots\argsemi
\sequence
_n\argdot s_n}.
]
And by theorem~\ref{}, this holds if and only if
[
t \reps \theta\arglist{\sequence
_1\argdot s_1\argsemi\ldots\argsemi
\sequence
_n\argdot s_n}.
]
\subsection
There are two things to be done here. We must
define operators that represent the representation relations
for each sort of operator, and we must show how these
operators can be put together to give a representation
of the predicate $\repsrelfor
$.
To represent $\repsrelfor
$ we define an operator
$\RepsUnjust$, and to represent $\repsrelfor
$
we define the operator $\RepsPrimRule$. Recall that tactic justifications
are represented by the relation $\reps$. We have already
define $\Reps$ to represent $\reps$.
Only the definition of $\RepsPrimRule$ is at all difficult,
and even there, the only problem is the complexity of
the $\repsrelfor
$ relation which results form the number
and non-uniformity of the primitive rules. For now, we assume
that $\RepsPrimRule$ can be defined appropriately. The other operators
are defined by the following definition.
\begin
[
\begin
\RepsJustification
\abstreq {}
\qquad
\progcase
{\inlterm{u}}
\exists x\colon\ClosedTerm\argdot
\EvalsToterm
{\Inlterm{x}} \wedge
\RepsUnjustterm
\qquad\qquad
\orcase{\inrterm{\inlterm
}}
\exists x\argcomma y\colon\ClosedTerm\argdot
\EvalsToterm
{\Inrterm{x}} \wedge
\EvalsToterm
{\Inlterm{y}} \wedge
\RepsPrimRuleterm
\qquad\qquad
\orcase{\inrterm{\inrterm
}}
\exists x\argcomma y\colon\ClosedTerm\argdot
\EvalsToterm
{\Inrterm{x}} \wedge
\EvalsToterm
{\Inrterm{y}} \wedge
\Repsterm
\RepsUnjust
\abstreq \EvalsTo
\Inlterm
\abstreq
\pairterm{\pairterm{\opidterm{inl}}{\nilterm}}
{[\pairterm
]}
\Inrterm
\abstreq
\pairterm{\pairterm{\opidterm{inr}}{\nilterm}}
{[\pairterm
]}
\UnitObjectterm \abstreq
\pairterm{\pairterm{\opidterm{\unitobject}}{\nilterm}}
\end
]
\end
\begin
The operator $\RepsUnjust$ represents the predicate
$\repsrelfor
$.
The operator $\RepsJustification$ represents the predicate
$\repsrelfor
$.
\end
Suppose that $T$ and $T'$ represent a closed term $t$, and
that $U$ and $U'$ represent the unjustification $u$. It is easy to
show that $\UnitObject$ represents the term $\unitobjectterm$. Thus,
the terms $\EvalsToterm
$ and
$\EvalsToterm
$ are equal types, and are inhabited if
and only if $t$ evaluates to $\unitobjectterm$. But $t
\repsrelfor
u$ if and only if $\evalsto
$.
The terms $\RepsUnjustterm
$ and $\RepsUnjustterm
$ expand to
$\EvalsToterm
$ and
$\EvalsToterm
$ respectively.
We conclude that $\RepsUnjustterm
$ and $\RepsUnjustterm
$
are equal types, and are inhabited if and only if
$t \repsrelfor
u$.
Now suppose that $T$ and $T'$ represent the closed term
$t$, and $J$ and $J'$ represent the justification $j$.
We expand the term $\RepsJustificationterm
$,
and get a term of the form
[
\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\orcase{\inrterm{\inrterm
}}
]
Likewise, $\RepsJustificationterm
$,
expands to a term of the form
[
\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\orcase{\inrterm{\inrterm
}}
]
We proceed by case analysis on $j$, with one case for
each possible sort of justification.
If $j$ is the unjustification, then since $J$ represents
it, there is a term $t_u$ such that $J$ evaluates to $\inlterm
$,
and $t_u \repsrelfor
j$. Then a term of the form
$\progcase
{\inlterm
}
\mid \ldots$ is
computationally equivalent to $\subst
$. Similarly,
there is a term $t'_u$ such that $t'_u \repsrelfor
j$ and terms
of the form
$\progcase
{\inlterm{u}}
\mid \ldots$ are
computationally equivalent to $\subst
$.
Therefore, we need only show that
[
\exists x\colon\ClosedTerm\argdot
\EvalsToterm
{\Inlterm{x}} \wedge
\RepsUnjustterm
]
and
[
\exists x\colon\ClosedTerm\argdot
\EvalsToterm
{\Inlterm{x}} \wedge
\RepsUnjustterm
]
are equal types that are inhabited if and only if
$t \repsrelfor
j$.
Suppose that $t_x$ and $t'_x$ represent the same closed term $t'$.
Then $\Inlterm
$ and $\Inlterm
$ represent the term
$\inlterm
$. Since both $T$ and $T'$ represent $t$,
we can conclude that $\EvalsToterm
{\Inlterm{t_x}}$
and $\EvalsToterm
{\Inlterm{t'_x}}$
are equal types which are inhabited if and only if
$\evalsto
{\inlterm{t'}}$.
Also since $t_u$ and $t'_u$ both represent the unjustification $j$,
$\RepsUnjustterm
$
and $\RepsUnjustterm
$ are equal types, and are inhabited
if and only if $t' \repsrelfor
j$.
From this, we can conclude that the two terms displayed
above are equal types, and that they are inhabited if and only if there
is a closed term $t'$ such that $t$ evaluates to $\inlterm
$ and
$t' \repsrelfor
j$. But,
since $j$ is an unjustification, $t \repsrelfor
j$
holds if and only if there is a closed term $t'$ such that
$\EvalsToterm
{\inlterm{t'}}$ and $t' \repsrelfor
j$.
Therefore, we can conclude that the two terms displayed are equal types,
and that they are inhabited if and only if $t \repsrelfor
j$.
If $j$ is a primitive rule, then since $J$ represents
it, there are terms $t_u$ and $t_v$ such that $J$ evaluates
to $\inrterm
$, $t_u$ evaluates to $\inlterm
$,
and $t_v \repsrelfor
j$. Then a term of the form
$\progcase
{\inlterm
}
\orcase{\inrterm{\inlterm
}}
\mid \ldots$ is
computationally equivalent to $\subst
$. Similarly,
there is a term $t'_v$ such that $t'_v \repsrelfor
j$ and
terms of the form
$\progcase
{\inlterm{u}}
\orcase{\inrterm{\inlterm
}}
\mid \ldots$
are computationally equivalent to $\subst
$.
Therefore, we need only show that
[
\exists x\argcomma y\colon\ClosedTerm\argdot
\EvalsToterm
{\Inrterm{x}} \wedge
\EvalsToterm
{\Inlterm{y}} \wedge
\RepsPrimRuleterm
]
and
[
\exists x\argcomma y\colon\ClosedTerm\argdot
\EvalsToterm
{\Inrterm{x}} \wedge
\EvalsToterm
{\Inlterm{y}} \wedge
\RepsPrimRuleterm
]
are equal types that are inhabited if and only if
$t \repsrelfor
j$.
Suppose that $t_x$ and $t'_x$ represent the same closed term $t'$,
and that $t_y$ and $t'_y$ represent the same closed term $t''$,
Then $\Inrterm
$ and $\Inrterm
$ represent the term
$\inrterm
$. Since both $T$ and $T'$ represent $t$,
we can conclude that $\EvalsToterm
{\Inrterm{t_x}}$
and $\EvalsToterm
{\Inrterm{t'_x}}$
are equal types which are inhabited if and only if
$\evalsto
{\inrterm{t'}}$.
Likewise, $\EvalsToterm
{\Inlterm{t_y}}$
and $\EvalsToterm
{\Inlterm{t'_y}}$
are equal types which are inhabited if and only if
$\evalsto
{\inlterm{t''}}$.
Also since $t_v$ and $t'_v$ both represent the primitive rule $j$,
$\RepsPrimRuleterm
$
and $\RepsPrimRuleterm
$ are equal types, and are inhabited
if and only if $t'' \repsrelfor
j$.
From this, we can conclude that the two terms displayed
above are equal types, and that they are inhabited if and only if there
are closed terms $t'$ and $t''$ such that $t$ evaluates to $\inrterm
$,
$t'$ evaluates to $\inlterm
$, and
$t'' \repsrelfor
j$. But,
since $j$ is an primitive rule, $t \repsrelfor
j$
holds if and only if there are closed terms $t'$ and $t''$ such that
$\EvalsToterm
{\inrterm{t'}}$, $\EvalsToterm
{\inlterm{t''}}$,
and $t'' \repsrelfor
j$.
Therefore, we can conclude that the two terms displayed are equal types,
and that they are inhabited if and only if $t \repsrelfor
j$.
If $j$ is a tactic, then since $J$ represents
it, there are terms $t_u$ and $t_v$ such that $J$ evaluates
to $\inrterm
$, $t_u$ evaluates to $\inrterm
$,
and $t_v \reps j$. Then a term of the form
[
\progcase
{\inrterm{u}}
\orcase{\inrterm{\inrterm
}}
\orcase{\inrterm{\inrterm
}}
]
is
computationally equivalent to $\subst
$. Similarly,
there is a term $t'_v$ such that $t'_v \reps j$ and
terms of the form
[
\progcase
{\inrterm{u}}
\orcase{\inrterm{\inrterm
}}
\orcase{\inrterm{\inrterm
}}
]
are computationally equivalent to $\subst
$.
Therefore, we need only show that
[
\exists x\argcomma y\colon\ClosedTerm\argdot
\EvalsToterm
{\Inrterm{x}} \wedge
\EvalsToterm
{\Inrterm{y}} \wedge
\Repsterm
]
and
[
\exists x\argcomma y\colon\ClosedTerm\argdot
\EvalsToterm
{\Inrterm{x}} \wedge
\EvalsToterm
{\Inrterm{y}} \wedge
\Repsterm
]
are equal types that are inhabited if and only if
$t \repsrelfor
j$.
Suppose that $t_x$ and $t'_x$ represent the same closed term $t'$,
and that $t_y$ and $t'_y$ represent the same closed term $t''$,
Then $\Inrterm
$ and $\Inrterm
$ represent the term
$\inrterm
$. Since both $T$ and $T'$ represent $t$,
we can conclude that $\EvalsToterm
{\Inrterm{t_x}}$
and $\EvalsToterm
{\Inrterm{t'_x}}$
are equal types which are inhabited if and only if
$\evalsto
{\inrterm{t'}}$.
Likewise, $\EvalsToterm
{\Inrterm{t_y}}$
and $\EvalsToterm
{\Inrterm{t'_y}}$
are equal types which are inhabited if and only if
$\evalsto
{\inrterm{t''}}$.
Also since $t_v$ and $t'_v$ both represent the tactic term $j$,
$\Repsterm
$
and $\Repsterm
$ are equal types, and are inhabited
if and only if $t'' \reps j$.
From this, we can conclude that the two terms displayed
above are equal types, and that they are inhabited if and only if there
are closed terms $t'$ and $t''$ such that $t$ evaluates to $\inrterm
$,
$t'$ evaluates to $\inrterm
$, and
$t'' \reps j$. But,
since $j$ is an tactic, $t \repsrelfor
j$
holds if and only if there are closed terms $t'$ and $t''$ such that
$\EvalsToterm
{\inrterm{t'}}$, $\EvalsToterm
{\inrterm{t''}}$,
and $t'' \reps j$.
Therefore, we can conclude that the two terms displayed are equal types,
and that they are inhabited if and only if $t \repsrelfor
j$.
All that remains is to discuss the definition of the operator
$\RepsPrimRule$. Recall that for each rule name $n$, we
define a representation relation $\repsrelfor
$ for the class of
parameter objects suitable for use with $n$, and that
$\repsrelfor
$ is defined as $\repsdp
$.
This means that if we can represent the relation $\repsrelfor
$
and the operation that maps rule names $n$ to representation relations
$\repsrelfor
$, we can use the operator $\RepsProd$ to represent
$\repsrelfor
$. Representing the relation $\repsrelfor
$
is simple: since tokens are an index family, we can use $\RepsRelFrag$.
The operation that maps rule names $n$ to representation
relations $\repsrelfor
$ is, as usual, treated as three place
predicate. It is treated as a predicate on rule names $n$, closed
terms $t$, and parameters suitable for use with the rule name $n$.
This predicate is satisfied if and only if $t \repsrelfor
p$. To
represent it, we define an operator $\RepsPrimParam$ so that if $t_n$
and $t'_n$ represent the same rule name $n$, $t_t$ and $t'_t$
represent the same closed term $t$, and $t_p$ and $t'_p$ represent the
same parameter $p$ suitable for use with $n$, then the terms
$\RepsPrimParamterm
$ and
$\RepsPrimParamterm
$ are equal types, and are
inhabited if and only if $t \repsrelfor
p$.
Since the class of rule names is finite, and fixed, we define
the operator $\RepsPrimParam$ by exhaustive case analysis
on possible rule names. For each rule name $n$,
we define an operator $\RepsPrimParamp
$ to represent the
two place predicate $t \repsrelfor
p$ on terms $t$ and
parameters $p$ suitable for use with $n$. Then,
we arrange that if
$t_n$ represents the rule name $n$,
$\RepsPrimParamterm
$ is computationally
equivalent to the term $\RepsPrimParampterm
$.
This is done using Nuprl's $\atomeq$ operator.
The definition of $\RepsPrimParamp
$ for each operator
$n$ is quite easy, since the definition of the relations
$\repsrelfor
$ are quite regular in structure. If
$n$ takes no parameters, then $\repsrelfor
$ is
$\repsrelfor
$, and so, we can make the definition
[
\RepsPrimParampterm
\abstreq \RepsUnjustterm
.
]
If $n$ takes a single parameter chosen from the class $\cal A$,
$\repsrelfor
$ is $\repsrelfor
$, the representation
relation for $\cal A$. The class $\cal A$ must be
either an index family, or the class terms, or the class of bound terms.
If $\cal A$ is an index family, let $f$ be the name of the index family,
and then $\repsrelfor
$ is $\repsrelfor
$.
This means that we can make the definition
[
\RepsPrimParampterm
\abstreq \RepsRelFragterm{\ifidterm{f}}
.
]
If $\cal A$ is the class of terms, then $\repsrelfor
$ is $\reps$.
Then, we can make the following definition.
[
\RepsPrimParampterm
\abstreq \Repsterm
.
]
Finally, if $\cal A$ is the class of bound terms, then $\repsrelfor
$ is
$\repsrelfor
$. Since $\repsrelfor
$ is
defined as $\repsip
$, we can make the following definition
[
\RepsPrimParampterm
\abstreq
\RepsProdterm
{\RepsBindingsterm
{y}}
{\Repsterm
}
.
]
This is possible because if $t_x$ and $t'_x$ represent the closed
term $x$, and $t_y$ and $t'_y$ represent the sequence $y$
of variable names, the terms
$\RepsBindingsterm
$ and $\RepsBindingsterm
$
are equal types that are inhabited if and only if $x$
represents $y$. Likewise, if $t_u$ and $t'_u$ represent the same
sequence of variable names, $t_v$ and $t'_v$ represent the same
closed term $v$, and $t_w$ and $t'_w$ represent the same term $w$,
the terms $\Repsterm
$ and$\Repsterm
$ are equal types,
and are inhabited if and only if $v \reps w$. This means that
If $t_t$ and $t'_t$ represent the same closed term $t$, and
$t_p$ and $t'_p$ represent the same bound term $p$, then
[
\RepsProdterm
{\RepsBindingsterm
{y}}
{\Repsterm
{w}}
.
]
and
[
\RepsProdterm
{\RepsBindingsterm
{y}}
{\Repsterm
{w}}
.
]
are equal types, and are inhabited if and only if
$t \repsip
p$.
If $n$ takes $n > 1$ parameters chosen from classes
$
_1$, \dots, $
_n$, then $\repsrelfor
$ is
the relation
[
{\repsrelfor{A_1}} \times
( {\repsrelfor{A_2}} \times ( \cdots \times
(\repsrelfor{A_{n-1}} \times {\repsrelfor{A_n}})
\cdots)).
]
Each of the classes of $
_i$ is either an index family, the class of
terms, or the class of bound terms. Thus for each $i$
can define an operator $\Reps_
$ to
represent $\repsrelfor
$. If $A_i$ is an index family named $f$,
use
[
\Reps_
\arglist
\abstreq
\RepsRelFragterm{\ifidterm{f}}
.
]
If $A_i$ is the class of terms
use
[
\Reps_
\arglist
\abstreq
\Repsterm
.
]
If $A_i$ is the class of bound terms use
[
\Reps_
\arglist
\abstreq
\RepsProdterm
{\RepsBindingsterm
{y}}
{\Repsterm
{w}}
.
]
Now, we can define $\RepsPrimParamp
$ using
the operator $\RepsProd$, as follows
[
\begin
\RepsPrimParampterm
\abstreq {}
\qquad
\RepsProd\argleft
\\\qquad\qquad
x_1\argcomma y_1\argdot\Reps_
\arglist
\argsemi
\\\qquad\qquad
u_1\argcomma v_1\argcomma w_1\argdot
\RepsProd\argleft
\\\qquad\qquad\qquad
x_2 \argcomma y_2\argdot
\Reps_
\arglist
\argsemi
\\\qquad\qquad\qquad u_2\argcomma v_2\argcomma w_2\argdot\cdots
\\\qquad\qquad\qquad\qquad
\RepsProd\argleft
\\\qquad\qquad\qquad\qquad\qquad
x_
\argcomma y_
\argdot \Reps_{A_{n-1}}
\arglist{x_
\argsemi y_{n-1}}\argsemi
\\\qquad\qquad\qquad\qquad\qquad
u_
\argcomma v_
\argcomma w_
\argdot
\Reps_{A_{n}}\arglist{v_
\argsemi w_{n-1}}\argsemi
\\\qquad\qquad\qquad\qquad\qquad
v_
\argsemi w_
\argright\argsemi
\\\qquad\qquad\qquad\qquad\cdots
\\\qquad\qquad\qquad
\argsemi v_1\argsemi w_1\argright
\\\qquad\qquad\argsemi t\argsemi p\argright
\end
]
To illustrate this discussion of the definition
of the various $\RepsPrimParamp
$ operators, we consider three examples.
The first example is the provided by the rule name $\atomEquality$.
Primitive rules formed using this rule take no (non-trivial) parameter.
Therefore, by the discussion above, we can declare that
$\RepsPrimParamp
$ stand for the operator
$\RepsPrimParam\atomEquality$, and make the following abstraction definition:
[
\RepsPrimParam\atomEquality\arglist
\abstreq \RepsUnjustterm
.
]
Since $\repsrelfor
$ is defined to be $\repsrelfor
$,
such a definition is clearly appropriate.
Next, consider the rule name $\applyEquality$. It takes a single
parameter, and this parameter must be a term. Our discussion above
suggests that we should declare that
$\RepsPrimParamp
$ stands for the operator
$\RepsPrimParam\applyEquality$, and make the following abstraction definition:
[
\RepsPrimParam\applyEquality\arglist
\abstreq \Repsterm
.
]
Since $\repsrelfor
$ is defined to be $\reps$,
such a definition is clearly appropriate.
Last, we consider the rule name $\productElimination$.
Primitive rules formed using this rule name take three parameters,
an integer, and two variable names. Recall that we treat all
rules as taking a single parameter, and simulate multiple parameters
using tupling. This means that we view the rule name
$\productElimination$ as requiring a single parameter that consists of an
integer together with a pair of variable names. Our discussion above
suggests that we declare
$\RepsPrimParamp
$ to stand for the operator
$\RepsPrimParam\productElimination$, and make the following
abstraction definition:
[
\RepsPrimParam\productElimination\arglist
\abstreq
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
}
{w}}
]
It is, perhaps, somewhat less obvious that this definition is appropriate
than was the case for $\RepsPrimParamp
$ or
$\RepsPrimParamp
$. Thus, we shall present a more careful
argument for its correctness.
Suppose that $t_t$ and $t'_t$ represent the same term $t$,
and $t_v$ and $t'_v$ represent the same variable name $v$.
Since $\ifidterm
$ represents
the index family name $\varname$, we can conclude that the terms
$\RepsRelFragterm{\ifidterm{\varname}}
$ and
$\RepsRelFragterm{\ifidterm{\varname}}
$
are equal types, and are inhabited if and only if
$t \repsrelfor
v$.
Now suppose that $t_t$ and $t'_t$ represent the same term $t$,
and $t_p$ and $t'_p$ represent the same object $p$,
where $p$ consists of a pair of variable names.
We can conclude that the terms
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
{w'}}
]
and
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
{w'}}
]
are equal types, and that they are inhabited if and only if
$t \repsip
p$.
Now suppose that $t_t$ and $t'_t$ represent the same term $t$,
and $t_n$ and $t'_n$ represent the same integer $n$.
Since $\ifidterm
$ represents
the index family name $\natnumber$, we can conclude that the terms
$\RepsRelFragterm{\ifidterm{\natnumber}}
$ and
$\RepsRelFragterm{\ifidterm
}
$
are equal types, and are inhabited if and only if
$t \repsrelfor
n$.
Now suppose that $t_t$ and $t'_t$ represent the same term $t$,
and $t_p$ and $t'_p$ represent the same object $p$,
where $p$ consists of an integer together with a pair of variable names.
We can conclude that the terms
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
}
{w}}
]
and
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
}
{w}}
]
are equal types, and that they are inhabited if and only if
[
t \mathrel{{\repsrelfor{\natnumber}} \times ({\repsip
{\varname}})} p.
]
But if $p$ consists of an integer together with a pair of
variable names, it is suitable for use as a rule parameter for the
rule name $\productElimination$. Moreover, the relation
$\repsrelfor
$ is defined as
[
{\repsrelfor{\natnumber}} \times ({\repsip
{\varname}})
]
Moreover,
$\RepsPrimParam\productElimination\arglist
$
expands to
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
}
{w}}
]
and $\RepsPrimParam\productElimination\arglist
$
expands to
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y'}}
{\RepsRelFragterm{\ifidterm
}
}
{w}}
]
We conclude that these terms are equal types, and are inhabited
if and only if
[
t \mathrel{{\repsrelfor{\natnumber}} \times ({\repsip
{\varname}})} p.
]
We could continue in this fashion, almost indefinitely: there
are, after all, over a hundred primitive rules in our version of Nuprl.
However, we believe that the discussion above, together with the examples
provide enough detail to allow the rapid construction of
$\RepsPrimParamp
$ for any particular rule name $n$.
Using these three operators, and others like them,
we can define $\RepsPrimParam$ and then, $\RepsPrimRule$.
\begin
[
\begin
\RepsPrimParamterm
\abstreq {}
\\\qquad
\atomeq\argleft n \argsemi \tokenterm
\argsemi
\RepsParam\atomEquality\arglist
\argsemi
\\\qquad\qquad
\atomeq\argleft n \argsemi \tokenterm
\argsemi
\RepsParam\applyEquality\arglist
\argsemi
\\\qquad\qquad\qquad
\atomeq\argleft n \argsemi \tokenterm
\argsemi
\RepsParam\productElimination\arglist
\argsemi
\\\qquad\qquad\qquad\qquad\vdots
\\\qquad\qquad\qquad\argright\argright\argright
\RepsPrimRuleterm
\abstreq {}
\\\qquad
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{\RepsPrimParamterm
{w}}
\end
]
Note that the definition of the operator $\RepsPrimParam$
includes one case for each primitive rule name.
\end
\begin
The operator $\RepsPrimRule$ represents the predicate
$\repsrelfor
$.
\end
Suppose that $t_t$ and $t'_t$ represent the same closed term
$t$, and suppose that $t_n$ and $t'_n$ represent the same rule name $n$.
Since $n$ is a primitive rule name, it is also a token. And
since $\ifidterm
$ represents the index family name
$\token$, we can conclude that the terms
$\RepsRelFragterm{\ifidterm{\token}}
$ and
$\RepsRelFragterm{\ifidterm{\token}}
$ are equal types,
and that they are inhabited if and only if
$t \repsrelfor
n$.
Suppose that $n$ is a rule name, $t$ is a closed term,
and $p$ is a rule parameter suitable for use with $n$.
Suppose that $t_n$ and $t'_n$ represent the token $n$, and
that $t_t$ and $t'_t$ represent the term $t$.
And suppose that $t_p$ and $t'_p$ represent $p$;
that is, suppose that $t_p \repsrelfor
p$ and
$t'_p \repsrelfor
p$ both hold.
The term $\RepsPrimParamterm
$ expands to a term of the form
[
\begin
\atomeq\argleft t_n \argsemi \tokenterm
\argsemi
\RepsPrimParampterm
\argsemi
\\\qquad
\atomeq\argleft t_n \argsemi \tokenterm
\argsemi
\RepsPrimParampterm
\argsemi
\\\qquad\qquad\vdots
\\\qquad\argright\argright,
\end
]
which includes a case for every rule name $n_i$.
In particular, for some natural number $k$, $n_k$ is $n$,
and so there is a case of the form
[
\atomeqterm
{\tokenterm{n}}{\RepsPrimParampterm
{t_p}}
.
]
We show by induction on $k - i$, that for $1 \le i \le k$, the term
[
\begin
\atomeq\argleft t_n \argsemi \tokenterm
\argsemi
\RepsPrimParampterm
\argsemi
\\\qquad
\atomeq\argleft t_n \argsemi \tokenterm{n_{i+1}} \argsemi
\RepsPrimParampterm{n_
}
\argsemi
\\\qquad\qquad\vdots
\\\qquad\argright\argright,
\end
]
is computationally equivalent to $\RepsPrimParampterm
$.
If $k - i = 0$, then $i = k$. Then $n_i$ is $n$.
Since $t_n$ represents $n$, it must evaluate to the term
$\tokenterm
$. Therefore, a term of the form
[
\atomeqterm
{\tokenterm{n_i}}{\RepsPrimParampterm
{t_p}}
]
is computationally equivalent to
$\RepsPrimParampterm
$, which is
$\RepsPrimParampterm
$.
Otherwise, since $i \le k$, $k - i > 0$. Moreover $n_i$ is not
$n$. But then, since $t_n$ evaluates to $\tokenterm
$, a term of the form
[
\begin
\atomeq\argleft t_n \argsemi \tokenterm
\argsemi
\RepsPrimParampterm
\argsemi
\\\qquad
\atomeq\argleft t_n \argsemi \tokenterm{n_{i+1}} \argsemi
\RepsPrimParampterm{n_{i+1}}
\argsemi
\\\qquad\qquad\vdots
\\\qquad\argright\argright,
\end
]
is computationally equivalent to
[
\atomeq\argleft t_n \argsemi \tokenterm{n_{i+1}} \argsemi
\RepsPrimParampterm{n_{i+1}}
\argsemi\ldots\argright.
]
But $k - (i + 1) = (k - i) - 1 < k - i$, so the induction hypothesis
holds. Therefore, this term is computationally equivalent to
$\RepsPrimParampterm
$. But then, by the transitivity
of $\squiggle$ so is
[
\atomeq\argleft t_n \argsemi \tokenterm
\argsemi
\RepsPrimParampterm
\argsemi\ldots\argright.
]
In particular, since $k$ is at least $1$, this is true for $i = 1$.
This means that the term to which $\RepsPrimParamterm
$ expands
is computationally equivalent to
$\RepsPrimParampterm
$.
In a similar fashion, we can show that
$\RepsPrimParamterm
$ expands to a term
computationally equivalent to the term
$\RepsPrimParampterm
$.
But $\RepsPrimParampterm
$ and
$\RepsPrimParampterm
$ are equal types, and are inhabited
if and only if $t \repsrelfor
p$ holds. Therefore,
$\RepsPrimParamterm
$ and
$\RepsPrimParamterm
$ are equal types, and are
inhabited if and only if $t \repsrelfor
p$ holds.
Now suppose that $t_t$ and $t'_t$ represent the closed term
$t$. Suppose too that $t_r$ and $t'_r$ represent the
primitive rule $r$. Then $r$ is an object that consists of
a rule name $n$ together with a parameter suitable for use with $n$.
We conclude then, using theorem~\ref{}, that the terms
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{\RepsPrimParamterm
{w}}
]
and
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{\RepsPrimParamterm
{w}}
]
are equal types, and that they are inhabited if and only if
$t \repsdp
r$.
That is, they are inhabited if and only if $t \repsrelfor
r$.
Since these terms are the results of expanding
$\RepsPrimRuleterm
$ and $\RepsPrimRuleterm
$,
respectively, this allows us to conclude that $\RepsPrimRule$ represents
$\repsrelfor
$.
\subsection
We are now almost finished with our representation of
the relation $\repsrelfor
$. We need only to
represent the relation $\repsrelfor
$, which is
mostly a matter of putting operators we have already defined together
in the appropriate fashion: the only really new point here is the need
to represent the representation of the hidden attribute of hypotheses,
that is, we must represent the relation $\repsrelfor{{\Bbb B}}$.
Then, we can define a representation for $\repsrelfor
$
in much the same fashion as we defined $\Reps$.
First, we define the operator $\RepsYesNo$ to represent the relation
$\repsrelfor{{\Bbb B}}$.
\begin
[
\begin
\RepsYesNoterm
\abstreq
\progifthen
{\EvalsToterm
{\Btrue}}\progelse
{\EvalsToterm
{\Bfalse}}
\Btrueterm{} \abstreq
\pairterm{\pairterm{\opidterm{\btrueop}}{\nilterm}}
\Bfalseterm{} \abstreq
\pairterm{\pairterm{\opidterm{\bfalseop}}
}
\end
]
\end
\begin
The operator $\RepsYesNo$ represents the predicate $\repsrelfor{{\Bbb B}}$.
\end
Suppose that $t_t$ and $t'_t$ represent the same closed term,
and that $t_b$ and $t'_b$ represent ``yes''. Then, $t_b$
evaluates to $\btrue$. This means that a term of the form
$\progifthen
\progelse
$ is computationally equivalent to $A$.
In particular, the term
[
\progifthen
{\EvalsToterm
{\Btrue}}\progelse
{\EvalsToterm
{\Bfalse}},
]
which arises through the expansion of $\RepsYesNoterm
$,
is computationally equivalent to $\EvalsToterm
$.
Likewise, $\RepsYesNoterm
$ expands to a term
computationally equivalent to the term
$\EvalsToterm
$.
Since $t_t$ and $t'_t$ represent the same closed term $t$, and
$\Btrue$ represents the term $\btrue$, we can conclude that
$\EvalsToterm
$ and $\EvalsToterm
$
are equal types. They are inhabited if and only if
$t$ evaluates to $\btrue$; that is, if and only if
%rle changed 2010 in attempt to get latex to work.
%$t \repsrelfor{{\Bbb}} ``yes''$.
$t \repsrelfor{{\Bbb ``yes''}}$.
Suppose that $t_t$ and $t'_t$ represent the same closed term,
and that $t_b$ and $t'_b$ represent ``no''. Then, $t_b$
evaluates to $\bfalse$. This means that a term of the form
$\progifthen
\progelse
$ is computationally equivalent to $B$.
In particular, the term
[
\progifthen
{\EvalsToterm
{\Bfalse}}\progelse
{\EvalsToterm
{\Bfalse}},
]
which arises through the expansion of $\RepsYesNoterm
$,
is computationally equivalent to $\EvalsToterm
$.
Likewise, $\RepsYesNoterm
$ expands to a term
computationally equivalent to the term
$\EvalsToterm
$.
Since $t_t$ and $t'_t$ represent the same closed term $t$, and
$\Bfalse$ represents the term $\bfalse$, we can conclude that
$\EvalsToterm
$ and $\EvalsToterm
$
are equal types. They are inhabited if and only if
$t$ evaluates to $\bfalse$; that is, if and only if
%rle changed 2010 in attempt to get latex to work.
%$t \repsrelfor{{\Bbb}} ``no''$.
$t \repsrelfor{{\Bbb ``no''}}$.
%rle changed 2010 in attempt to get latex to work.
% Since $t \repsrelfor{{\Bbb}} b$ is only well defined if
Since $t \repsrelfor{{\Bbb b}}$ is only well defined if
$t$ is a closed term, and $b$ is either ``yes'' or ``no'', these
two cases are all that need to be considered. We
%rle changed 2010 in attempt to get latex to work.
%conclude that $\RepsYesNo$ represents $\repsrelfor{{\Bbb}}$.
conclude that $\RepsYesNo$ represents $\repsrelfor{{\Bbb b}}$.
With this done, the definition of $\RepsHyp$ to define
the represent the relation $\repsrelfor
$, is simply a matter
of putting previously defined operators together using the
operator $\RepsProd$. And then $\RepsSequent$ is defined
using $\RepsSeq$ and $\RepsProd$.
\begin
[
\begin
\RepsHypterm
\abstreq
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{\RepsProdterm
{\Repsterm
}
{\RepsYesNoterm
{w}}
{w}}
\RepsSequentterm
\abstreq
\RepsProdterm
{\Repsterm
{y}}
{\RepsSeqterm
{\RepsHypterm
}
{w}}
\end
]
\end
\begin
The operator $\RepsHyp$ represents the predicate
$\repsrelfor
$.
The operator $\RepsSequent$ represents the predicate
$\repsrelfor
$.
\end
The operator $\Reps$ represents the predicate $\reps$, and the
operator $\RepsYesNo$ represents the predicate $\repsrelfor{{\Bbb B}}$.
Using theorem~\ref{} we can conclude that whenever $t_t$ and $t'_t$
represent the same closed term $t$, and $t_p$ and $t'_p$ represent
the same object $p$, where $p$ consists of a term and either ``yes''
or ``no'', then the terms
[
{\RepsProdterm
{\Repsterm
{y}}
{\RepsYesNoterm
}
{t_p}}
]
and
[
{\RepsProdterm
{\Repsterm
{y}}
{\RepsYesNoterm
{w}}
{t'_p}}
]
are equal types, and are inhabited if and only if
$t \repsip
\Bbb B
p$. Suppose that $t_s$ and $t'_s$ represent the
same closed term $s$, and $t_v$ and $t'_v$ represent the same
variable name $v$. Since $\ifidterm
$ represents the index family
name $\varname$, we can conclude that
$\RepsRelFragterm{\ifidterm{\varname}}
$ and
$\RepsRelFragterm{\ifidterm{\varname}}
$ are equal types;
they are inhabited if and only if $s \repsrelfor
v$.
But then, using theorem~\ref{} again, we can conclude that
whenever $t_r$ and $t'_r$ represent the same closed term $r$, and
$t_h$ and $t'_h$ represent the same object $h$, where $h$
consists of a variable name together with a pair consisting of
a term and either ``yes'' or ``no'', the terms
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{\RepsProdterm
{\Repsterm
{y}}
{\RepsYesNoterm
}
{w}}
]
and
[
\RepsProdterm
{\RepsRelFragterm{\ifidterm
}
{y}}
{\RepsProdterm
{\Repsterm
{y}}
{\RepsYesNoterm
{w}}
{w}}
]
are equal types. They are inhabited if and only if
[
r \mathrel{{\repsrelfor{\varname}} \times {\repsip
}} h.
]
But then $h$ is a hypothesis, and the condition required
for the types to be inhabited is just
[
r \repsrelfor
h.
]
Since the two terms above are, respectively, the expansions of
$\RepsHypterm
$ and $\RepsHypterm
$, we
conclude that $\RepsHyp$ represents $\repsrelfor
$.
It follows immediately, using theorem~\ref{}, that whenever $t_t$ and
$t'_t$ represent the same closed term $t$, and $t_h$ and $t'_h$ represent the
same finite sequence $h$ of hypotheses, the terms
$\RepsSeqterm
{\RepsHypterm
{v}}
$
and
$\RepsSeqterm
{\RepsHypterm
{v}}
$
are equal types, and are inhabited if and only if
$t \repsrelforseq
h$. Recall that $\Reps$ represents
$\reps$. We can conclude using theorem~\ref{}
that whenever $t_r$ and $t'_r$ represent the same closed term $r$, and
$t_s$ and $t'_s$ represent the same pair $s$ consisting of a
finite sequence of hypotheses together with a term,
the terms
[
\RepsProdterm
{\Repsterm
{y}}
{\RepsSeqterm
{\RepsHypterm
}
{w}}
]
and
[
\RepsProdterm
{\Repsterm
{y}}
{\RepsSeqterm
{\RepsHypterm
}
{w}}
]
are equal types, and are inhabited if and only if
[
r \mathrel{{\repsrelforseq{\hypclass}} \times \repsrelfor{\term}} s.
]
But then $s$ is a sequent, and the condition required
for the types to be inhabited is just
[
r \repsrelfor
s.
]
Since the two terms above are, respectively, the expansions of
$\RepsSequentterm
$ and $\RepsSequentterm
$, we
conclude that $\RepsSequent$ represents $\repsrelfor
$.
We are now ready to define an operator $\RepsPP$ to represent the
predicate $\repsrelfor
$. Our definition is
much like the definition of $\Reps$. Instead of using $\Termind$ which
represents primitive recursion on terms, we use $\PPind$ which
represents primitive recursion on pre-proofs.
\begin
[
\begin
\RepsPPgenterm
\abstreq {}
\qquad
\lambda F\argcomma i\argcomma S\argdot
\inteq\argleft i\argsemi n+1 \argsemi \EvalsToterm
\argsemi
\\\qquad\qquad
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad\qquad{}
\wedge h(A)
\wedge F(i + 1)(B)\argright
\RepsPPterm
\abstreq {}
\qquad
(\PPind\argleft P \argsemi
g \argcomma j\argcomma n \argcomma s \argcomma h\argdot\lambda S\argdot
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)\argright
\\\qquad
)(T)
\end
]
\end
\begin
The operator $\RepsPP$ represents the predicate
$\repsrelfor
$.
\end
As with the proof that $\reps$ represents $\reps$, we must first prove
a technical lemma, this time concerning $\RepsPPgen$.
Suppose that $n$ is a natural number, and that for each $i$ between
$1$ and $n$, $q_i$ is a pre-proof. Suppose that $t$ is a closed term,
and that, $m$ is a natural number such that $1 \le m \le n + 1$.
Suppose that $t_n$ and $t'_n$ represent $n$, $t_m$ and $t'_m$ represent $m$,
and $t_t$ and $t'_t$ represent $t$. Also suppose that for any integer
$i$ between $1$ and $n$, and any closed term $s$,
if $t_i$ and $t'_i$ both represent $i$,
and $t_s$ and $t'_s$ both represent $s$,
then the terms $t_h(t_i)$ and $t'_h(t'_i)$ are equal types, and
these types are inhabited if and only if $s \repsrelfor
q_i$.
If all these conditions hold, then the terms
$\ycomb (\RepsPPgenterm
)(t_m)(t_t)$
and
$\ycomb (\RepsPPgenterm
)(t'_m)(t'_t)$
are equal types, and are inhabited if and only if
$t \repsrelforseq
(q_m, q_
, \ldots, q_n)$.
Our proof is by induction on $n + 1 - m$. Since $m \le n + 1$,
$n + 1 - m$ is always non-negative. First,
we replace each of the two terms with a computationally
equivalent term. In the term $\ycomb (\RepsPPgenterm
)(t_m)(t_t)$
we replace $\ycomb (\RepsPPgenterm
)$ with the computationally
equivalent $\RepsPPgenterm
(\ycomb (\RepsPPgenterm
))$,
we expand the first instance of $\RepsPPgen$, and contract the
resulting beta redices. This yields the term
[
\begin
\inteq\argleft t_m\argsemi t_n+1 \argsemi
\EvalsToterm
\argsemi
\\\qquad
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad{}
\wedge t_h(t_m)(A)
\wedge \ycomb (\RepsPPgenterm
)t_m + 1)(B)\argright.
\end
]
In a similar fashion we can replace
$\ycomb (\RepsPPgenterm
)(t'_m)(t'_t)$
with
[
\begin
\inteq\argleft t'_m\argsemi t'_n+1 \argsemi
\EvalsToterm
\argsemi
\\\qquad
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad{}
\wedge t'_h(t'_m)(A)
\wedge \ycomb (\RepsPPgenterm
)t'_m + 1)(B)\argright.
\end
]
Suppose $n+1-m = 0$. Then, $m = n+1$. Therefore, $t_m$ represents
$n + 1$. Since $t_n$ represents $n$, $t_n + 1$ represents $n + 1$.
This means that both $t_m$ and $t_n + 1$ evaluate to
$\natnumterm
$. This means that a term of the
form $\inteqterm
$ is computationally equivalent to $A$.
In this case, this means that the first displayed term
is computationally equivalent to $\EvalsToterm
$.
In a similar fashion, we can conclude that the second displayed term is
computationally equivalent to the term $\EvalsToterm
$.
Since $t_t$ and $t'_t$ represent the same closed term $t$, and $\Nilterm$
represents the term $\nilterm$, we can conclude that these terms
are equal types, and that they are inhabited if and only if
$\evalsto
$. Since $m > n$, the sequence
$(q_m, q_
, \ldots, q_n)$ is empty. This means that
$t$ represents it if and only if $t$ evaluates to $\nilterm$.
Therefore, the types are inhabited if and only if
$t \repsrelforseq
(q_m, q_
, \ldots, q_n)$.
Otherwise, $n+1-m > 0$, and $1 \le m \le n$.
Since $t_m$ represents an integer $m$, it evaluates to the term
$\natnumterm
$, $t_n + 1$ still evaluates to the term
$\natnumterm
$. Since $m \neq n +1$, these values are distinct.
This means that terms of the form $\inteqterm
$ are
computationally equivalent to $Y$. This allows us to replace
the first displayed term with
[
\begin
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad{}
\wedge t_h(t_m)(A)
\wedge \ycomb (\RepsPPgenterm
)t_m + 1)(B)\argright.
\end
]
Likewise, we can replace the second term with
[
\begin
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
\\\qquad{}
\wedge t'_h(t'_m)(A)
\wedge \ycomb (\RepsPPgenterm
)t'_m + 1)(B)\argright.
\end
]
Let $t_A$ and $t'_A$ represent the same
closed term $A$, and $t_B$ and $t'_B$ represent the same closed term
$B$. The terms $\Consterm
$ and $\Consterm
$
both represent $\consterm
$. And since both $t_t$ and
$t'_t$ represent the closed term $t$, the terms
$\EvalsToterm
{\Consterm
{t_B}}$
and $\EvalsToterm
{\Consterm
{t'_B}}$ are equal
types, and are inhabited if and only if $\evalsto
{\consterm
{B}}$.
Both $t_m$ and $t'_m$ represent $m$, and $1 \le m \le n$.
And both $t_A$ and $t'_A$ represent the closed term $A$. Thus, we
can use our hypothesis concerning $t_h$ and $t'_h$ to conclude that
the terms $t_h(t_m)(t_A)$ and $t'_h(t'_m)(t'_A)$ are equal terms,
and that they are inhabited if and only if $A \repsrelfor
q_m$.
Since $t_m$ and $t'_m$ represent $m$, $t_m+1$ and $t'_m+1$
represent $m + 1$. Since $n + 1 - (m + 1) = n + 1 - m - 1 < n + 1 - m$,
the induction hypothesis applies. The terms
$t_B$ and $t'_B$ represent the same closed term $B$,
so using the induction hypothesis, we conclude that
$\ycomb (\RepsPPgenterm
)t_m + 1)(t_B)$ and
$\ycomb (\RepsPPgenterm
)t'_m + 1)(t'_B)$ are equal types,
and that they are inhabited if and only if
$B \repsrelforseq
(q_
, \ldots, q_n)$.
But then, since the type $\ClosedTerm$ represents the class of
closed terms, we can conclude that the terms
[
\begin
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
{}
\wedge t_h(t_m)(A)
\wedge \ycomb (\RepsPPgenterm
)t_m + 1)(B)\argright.
\end
]
Likewise, we can replace the second term with
[
\begin
\exists A\argcomma B\colon\ClosedTerm\argdot
\EvalsToterm
{\Consterm
{B}}
{}
\wedge t'_h(t'_m)(A)
\wedge \ycomb (\RepsPPgenterm
)t'_m + 1)(B)\argright.
\end
]
are equal types, and that they are inhabited if and only if
there are closed terms $A$ and $B$ such that
$\evalsto
{\consterm
{B}}$, $A \repsrelfor
q_m$,
and $B \repsrelforseq
(q_
, \ldots, q_n)$.
That is, they are inhabited if and only if
$t \repsrelforseq (q_m, q_
, \ldots, q_n)$.
Using this lemma, together with theorem~\ref{}, we show that
whenever $t_t$ and $t'_t$ represent the same closed term $t$, and
$t_p$ and $t'_p$ represent the same pre-proof $p$, the terms
$\RepsPPterm
$ and $\RepsPPterm
$ are equal types,
and are inhabited if and only if $t \repsrelfor
p$.
First, we expand the two terms. This yields the terms
[
\begin
(\PPind\argleft t_p \argsemi
g \argcomma j\argcomma n \argcomma s \argcomma h\argdot\lambda S\argdot
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)\argright
)(t_t)
\end
]
and
[
\begin
(\PPind\argleft t'_p \argsemi
g \argcomma j\argcomma n \argcomma s \argcomma h\argdot\lambda S\argdot
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)\argright
)(t'_t).
\end
]
We must show that these terms are equal types, and are inhabited if and only if
$t \repsrelfor
p$. Since $t_p$ and $t'_p$ represent the
same pre-proof, and $t_t$ and $t'_t$
represent the same term, theorem~\ref{} applies.
By theorem~\ref{}, it suffices to show that for
any preproof $p$ with goal $g$, justification $j$,
and $n$ subgoals $q_1$, \dots, $q_n$, and any closed term $t$,
if the following conditions hold
\begin
\item $t_g$ and $t'_g$ both represent the sequent $g$.
\item $t_j$ and $t'_j$ both represent the justification $j$.
\item $t_n$ and $t'_n$ both represent the natural number $n$.
\item For any integer $i$ between $1$ and $n$,
and any terms $t_i$ and $t'_i$ that represent $i$,
the terms $t_q(t_i)$ and $t'_q(t'_i)$ both represent the
pre-proof $q_i$.
\item For any integer $i$ between $1$ and $n$, any closed
term $s$, any terms $t_i$ and $t'_i$ that represent $i$,
and any terms $t_s$ and $t'_s$ that represent $s$,
the terms $t_h(t_i)(t_s)$ and $t'_h(t'_i)(t'_s)$
are equal types, and are inhabited if
and only if $s \repsrelfor
q_i$.
\item The terms $t_t$ and $t'_t$ both represent the closed term $t$.
\end
Then the terms
[
\begin
(\lambda S\argdot
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)\argright
)(t_t)
\end
]
and
[
\begin
(\lambda S\argdot
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)\argright
)(t_t)
\end
]
are equal types, and are inhabited if and only if
$t \repsrelfor
p$. We beta reduce them, and then
use the definition of $\exists$ to prove this.
We suppose that $t_A$ and $t'_A$ represent the same closed term $A$,
that $t_B$ and $t'_B$ represent the same closed term $B$,
that $t_C$ and $t'_C$ represent the same closed term $C$,
and that $t_D$ and $t'_D$ represent the same closed term $D$.
and consider each pair of corresponding conjuncts one at a time.
Since $t_A$ and $t'_A$ both represent $A$, and $t_B$
and $t'_B$ both represent $B$, the terms $\Pairterm
$
and $\Pairterm
$ both represent $\pairterm
$.
But then, since $t_t$ and $t'_t$ both represent
$t$, the terms $\EvalsToterm
{\Pairterm
{t_B}}$
and $\EvalsToterm
{\Pairterm
{t'_B}}$ are equal types,
and are inhabited if and only if $\evalsto
{\pairterm
{B}}$.
Similarly, the terms $\EvalsToterm
{\Pairterm
{t_D}}$
and $\EvalsToterm
{\Pairterm
{t'_D}}$ are equal types,
and are inhabited if and only if $\evalsto
{\pairterm
{D}}$.
The operator $\RepsSequent$ represents the predicate
$\repsrelfor
$. Therefore, since both $t_A$ and $t'_A$
represent the closed term $A$, and both $t_g$ and $t'_g$ represent the
sequent $g$, the terms $\RepsSequentterm
$
$\RepsSequentterm
$ are equal types, and are inhabited if
and only if $A \repsrelfor
g$.
The operator $\RepsJustification$ represents the predicate
$\repsrelfor
$. Therefore, since both $t_C$ and $t'_C$
represent the closed term $C$, and both $t_j$ and $t'_j$ represent the
justification $j$, the terms $\RepsJustificationterm
$
$\RepsJustificationterm
$ are equal types, and are inhabited if
and only if $C \repsrelfor
j$.
Let $m = 1$. Then, the term $1$ represents the natural number $m$.
Since $n$ is a natural number $n \ge 0$, and so $n + 1 \ge 1 = m$. The
terms $t_D$ and and $t'_D$ represent the same closed term $D$. The
terms $t_n$ and $t'_n$ both represent $n$. For any integer $i$
between $1$ and $n$, and any closed term $s$, if $t_i$ and $t'_i$ both
represent $i$, and $t_s$ and $t'_s$ both represent $s$, then the terms
$t_h(t_i)(t_s)$ and $t'_h(t'_i)(t'_s)$ are equal types, and are
inhabited if and only if $s \repsrelfor
p_i$. Thus, all
the conditions for applying the lemma proved earlier hold. We
conclude that $\ycomb (\RepsPPgenterm
)(1)(t_D)$ and $\ycomb
(\RepsPPgenterm
)(1)(t'_D)$ are equal types, and are inhabited
if and only if $D \repsrelforseq
(q_1, \ldots, q_n)$.
Since the type $\ClosedTerm$ represents the class of closed
terms, we can conclude that the terms
[
\begin
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)
\end
]
and
[
\begin
\exists A\argcomma B\argcomma C\argcomma D\colon\ClosedTerm\argdot
\\\qquad
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad {}
\wedge \RepsSequentterm
\wedge \RepsJustificationterm
\\\qquad {}
\wedge \ycomb (\RepsPPgenterm
)(1)(D)
\end
]
are equal types, and that they are inhabited if and only if
there exists closed terms $A$, $B$, $C$, and $D$, such that
$\evalsto
{\pairterm
{B}}$,
$\evalsto
{\pairterm
{D}}$,
$A \repsrelfor
g$,
$C \repsrelfor
j$, and
$D \repsrelforseq
(q_1, \ldots, q_n)$.
But the conditions $\evalsto
{\pairterm
{D}}$,
$C \repsrelfor
j$, and
$D \repsrelforseq
(q_1, \ldots, q_n)$
are equivalent to the condition
[
B \mathrel{{\repsrelfor{\justification}} \times
{\repsrelforseq
}}
\langle j , (q_1, \ldots q_n)\rangle.
]
and this condition together with the remaining conditions
$\evalsto
{\pairterm
{B}}$, and
$A \repsrelfor
g$,
is equivalent to the condition
[
t \mathrel{{\repsrelfor{\sequentclass}}
\times ({\repsrelfor{\justification}} \times
{\repsrelforseq{\preproof}})}
\langle g, \langle j , (q_1, \ldots q_n)\rangle\rangle.
]
Because $p$ is $\langle g, \langle j , (q_1, \ldots q_n)\rangle\rangle$.
and ${\repsrelfor{\sequentclass}}
\times ({\repsrelfor{\justification}} \times
{\repsrelforseq{\preproof}})$
is $\pprepsgen{\repsrelfor{\preproof}}$,
this condition can be re-written as
[
t \pprepsgen{\repsrelfor{\preproof}} p.
]
And this holds if and only if $t \repsrelfor
p$.
\section
In this section, we very briefly sketch a third possible
view of tactics. This view can be thought of, in some sense,
as a combination of the other two. Every tactic is regarded as
a pair of objects: the program term which the user types in as
a refinement together with the proof it produces.
As was the case for extensional tactics, the pre-proof portion
of each tactic justification can be viewed as a structural
sub-pre-proof of the pre-proof in which the tactic appears. This
allows us to define the $\foo$ predicate by structural induction
on pre-proofs, rather than having to introduce some auxiliary order
as we did for intensional proofs.
Representing this view of tactics records the program text
actually used to generate the pre-proof. Therefore, like representing
pure intensional tactics, this view allows us to reason intensionally
about programs. Moreover, it has the same sort of explicative power
of the tactic mechanism as did a representation of intensional tactics.
Finally, perhaps even to a greater extent than was the case for a
representation of intensional tactics, representing this view
of tactics dispels the lingering doubts which accompany
a representation of extensional tactics. We no longer feel as if we might
be disguising some important logical feature of the system as a mere
implementation detail.
Thus, it appears that representing this view of tactics has
all the advantages of reflecting intensional tactics, without sacrificing
the simplicity of representing intensional tactics. Its principal
disadvantage is that now, when we wish to provide a term that represents a
tactic justification, we must provide both a representative $t$ of the tactic
term, and a representative $t$ of the proof to which it evaluates.
Moreover, if this justification representative is to serve as part
of a proof representative, we must ensure that the type
$\RepsPreProof
$ holds. It seems that this significantly complicates
the task of proving that particular terms belong to the $\Proof$ type.
Furthermore, there is a sense in which this representation is redundant.
There ought to be no need to record the pre-proof represented
by a tactic term, since it can always be recovered using
$\unrepfunfor
$. Thus, we choose to use the somewhat
more complicated representation of intensional proofs which has
already been described.
If, however, this view of tactics is taken, we can represent the class
of pre-proofs using the following type
[
\recterm
{\indepproducttype
{\indepproducttype{(\uniontype
{\uniontype
{(\indepproducttype
)}})}{\listtype{p}}}}.
]
While a detailed proof that this type represents the class of pre-proofs
is impossible without stating exactly
which representation relation is to be used,
we can give an informal argument.
Because of the syntactic
structure of the term $\recterm
$ given above, it can be shown
that it is a type, and that two terms are equal members of this type
if and only if they are equal members of some finite unrolling of this
type. Unrolling the type $0$ times produces the empty type,
and each subsequent unrolling is produced by substituting the previous
unrolling for $p$ in $T$. If $Q_i$ stands for the $i$\/th unrolling,
we can write this as
\begin
Q_0 &=& \voidtype
Q_
&=& \indepproducttype
{\indepproducttype{(\uniontype
{\uniontype
{(\indepproducttype
)}})}{\listtype
}}
\end
The class of pre-proofs is
still a class of finitely branching, tree-structured objects. Therefore,
we can still define the height of a pre-proof. Then we show,
by induction on $i$, that
for each $i$, the type $Q_i$ represents the class of pre-proofs of height
$i$ or less (using the representation relation for the
full class of pre-proofs). Since there are still no pre-proofs of height
$0$, and the type $\voidtype$ is empty, the base case is trivial.
A pre-proof of height $n+1$ consists of a goal sequent, a
justification and a finite sequence of proofs of height $n$ or less.
By the induction hypothesis, the type $Q_n$ represents the class of
proofs of height $n$ or less, and so the type $\listtype
$
represents sequences of such proofs. And since the type $\Sequent$
represents the class of sequents, it suffices to show that
[
\uniontype
{\uniontype
{(\indepproducttype
)}}
]
represents the class of justifications. A justification is either
an unjustification, or a primitive rule, or a tactic. Since the
the type $\unittype$ represents the class of unjustification,
and the type $\PrimRule$ represents the class of primitive rules,
it suffices to show that $\indepproducttype
$
represents the class of tactics. But a tactic consists of
a closed term, together with a pre-proof. This pre-proof is a
sub-pre-proof of the proof in which the tactic appears; therefore,
in this case, it must be of height $n$ or less.
The predicate $\foo(p)$ on pre-proofs $p$, which selects
those pre-proofs that are proofs, can be defined by straightforward
structural induction on $p$. Let $p$ be a pre-proof
$p$ consisting of a goal $g$, justification $j$ and
sub-pre-proofs $\sequence
$. And for each pre-proof
$q_i$ on $\sequence
$, let $s_i$ be the topmost goal sequent
of $q_i$. The predicate $\foo(p)$ holds
if and only if $\matchesup(g, j, \sequence
)$, and for every immediate
sub-pre-proof $r$ of $p$, $\foo(r)$ holds. Note particularly
that if $j$ is a tactic justification consisting of a closed term $t$ and
a pre-proof $v$, the set of immediate sub-pre-proofs of $p$ includes
all the pre-proofs $q_i$ on $\sequence
$, and also includes $v$.
This means that $\foo(p)$ holds only if $\foo(v)$ does.
For primitive rules and the unjustification $\matchesup$
can be left unchanged, but it must once again be reconsidered
for tactic justifications. Let $g$ be a sequent,
let $\sequence
$ be a sequence of sequents, and let
$j$ be a tactic justification made up of a closed term $t$
and a pre-proof validation $v$. The predicate
$\matchesup(g, j, \sequence
)$ holds if and only if,
$t$ represents $v$, $g$ is the topmost goal sequent of
$v$, and $\sequence
$ is the frontier of $v$.
As before, we can define an operator $\PPind$ to represent primitive
recursion on pre-proofs. The definition is almost identical to that
given by definition~\ref{}, in the section on extensional tactics.
Using this operator, we can define the operator $\Foo$ to
represent the predicate $\foo$. Our definition is very similar to the one
given for extensional proofs.
[
\begin
\Footerm
\abstreq {}
\\\qquad
\PPind\argleft p\argsemi
\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argdot
\MatchesUpUnjustterm
{\TopGoalsterm
{n}}
\\\qquad\qquad\qquad {}
\wedge \forall x\colon \intsegterm
\argdot h
\argsemi\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argdot
\MatchesUpPrimRuleterm
{\TopGoalsterm
{n}}
\\\qquad\qquad\qquad {}
\wedge \forall x\colon \intsegterm
\argdot h
\argsemi\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argcomma x\argdot
x
\wedge \MatchesUpTacticterm
{\TopGoalsterm
{n}}
\\\qquad\qquad\qquad {}
\wedge \forall x\colon \intsegterm
\argdot h
\argright
\end
]
Also, using $\PPind$, we can define the operator $\Frontier$, to
represent the operation of which maps pre-proofs to their frontiers.
Since the frontier of a proof $p$ does not include unjustified
subgoals that appear inside tactic justifications of $p$, the tactic
sub-proofs are ignored completely. Thus, the new definition of
$\Frontier$ differs from the one given by definition~\ref, in the
section on extensional tactics, only in that it uses the new version
of the $\PPind$ operator.
We can also use the new $\PPind$ operator to give a new definition of
the operator $\RepsPP$. This time, some small changes have to be made.
However, these is simply a matter of working out the details, and are not
difficult. We give the definition, in any case, partly for the sake of
completeness, and partly because it makes somewhat more explicit the
definition of $\repsrelfor
$ we have in mind.
[
\begin
%\RepsPPgenterm
\abstreq {}
%\qquad
% \lambda F\argcomma i\argcomma S\argdot
% \inteq\argleft i\argsemi n+1 \argsemi \EvalsToterm
\argsemi
%\\\qquad\qquad
% \exists A\argcomma B\colon\ClosedTerm\argdot
% \EvalsToterm
{\Consterm
{B}}
%\\\qquad\qquad{}
% \wedge h(A)
% \wedge F(i + 1)(B)\argright
%
\RepsPPterm
\abstreq {}
\\\qquad
(\PPind\argleft p\argsemi
\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argdot
\lambda t\argdot
\exists A\argcomma B\argcomma C\argcomma D\argcomma E\colon
\ClosedTerm\argdot
\\\qquad\qquad\qquad{}
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad\qquad\qquad{}
\wedge \EvalsToterm
{\Inlterm{E}}
\wedge \RepsSequentterm
\\\qquad\qquad\qquad{}
\wedge \RepsUnjustterm
%\\\qquad\qquad\qquad{}
\wedge \ycomb (\RepsPPgenterm
) (1) (D)
\argsemi\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argdot
\lambda t\argdot
\exists A\argcomma B\argcomma C\argcomma D\argcomma E\argcomma F\colon
\ClosedTerm\argdot
\\\qquad\qquad\qquad{}
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad\qquad\qquad{}
\wedge \EvalsToterm
{\Inrterm{E}}
\wedge \EvalsToterm
{\Inlterm{F}}
\\\qquad\qquad\qquad{}
\wedge \RepsSequentterm
\wedge \RepsPrimRuleterm
\\\qquad\qquad\qquad{}
\wedge \ycomb (\RepsPPgenterm
) (1) (D)
\argsemi\\\qquad\qquad
g\argcomma j\argcomma n\argcomma s\argcomma h\argcomma x\argdot
\lambda t\argdot
\exists A\argcomma B\argcomma C\argcomma D\argcomma E\argcomma F\argcomma G
\argcomma H\colon\ClosedTerm\argdot
\\\qquad\qquad\qquad{}
\EvalsToterm
{\Pairterm
{B}}
\wedge \EvalsToterm
{\Pairterm
{D}}
\\\qquad\qquad\qquad{}
\wedge \EvalsToterm
{\Inrterm{E}}
\wedge \EvalsToterm
{\Inrterm{F}}
\\\qquad\qquad\qquad{}
\wedge \EvalsToterm
{\Pairterm
{H}}
\wedge \RepsSequentterm
\\\qquad\qquad\qquad{}
\wedge \Repsterm
\wedge x(H)
\\\qquad\qquad\qquad{}
\wedge \ycomb (\RepsPPgenterm
) (1) (D)
\argright)
\\\qquad
(t)
\end
]
Note that $\RepsPPgen$ is defined exactly as for intensional tactic pre-proofs.
The operator $\MatchesUpTactic$ can be defined, as before, as
a conjunction of terms formed using the operators
$\IsApplicableTactic$ and $\AreSubsTactic$. As before, we can define
$\IsApplicableTacticterm
$ so that it always expands to
$\trueprop$. However, we can also define it as follows
[
\IsApplicableTacticterm
\abstreq \RepsPPterm
]
to emphasize the fact that only those tactic justifications $j$
in which the term component $t$ represents the pre-proof validation component
$v$ are actually admissible as tactics in proofs. Note that if
$t_j$ represents $j$, $\pi_1(t_j)$ represents $t$, and $\pi_2(t_j)$
represents $v$, so this definition is sensible.
If we define $\IsApplicableTactic$ as described above, the
appropriate definition of $\AreSubsTactic$ is the following
[
\begin
\AreSubsTacticterm
\abstreq {}
\\\qquad
\equalitytype
{\TopGoalterm{\pi_2(j)}}
\wedge \equalitytype{\listtype{\Sequent}}
{\Frontierterm{\pi_2(j)}}.
\end
]
Note that this definition can completely ignore the term component of the
tactic. Otherwise, if it is still defined so it always expands to
$\trueprop$, we must also include a representation of the requirement
that the term component of a tactic actually represent the validation
component. Which of the two definitions of $\IsApplicableTactic$ one
chooses seems to be mostly a matter of taste.
\section
In this section, we give a high level description of how
tactics of the sort described above can be integrated in a system like
Nuprl. Then we argue that this is just one of many approaches
to adding complex inference rules to refinement style theorem provers.
We suggest certain other options.
The process of determining whether a given tactic refinement
is acceptable, and of generating subgoals can be decomposed into four
conceptual steps. This is not to say that an actual implementation
needs to be subdivided in this fashion. In fact, after we have discussed
each of the stages, we sketch an implementation which performs the four
actions concurrently. This has the advantage of ensuring that certain
invalid tactic refinements are detected more rapidly, at the price of
increased complexity of implementation. In any case, the process
takes as input a sequent to be refined, and a Nuprl term that is
supposed to be used as a justification. It may succeed, it may fail, or
it may diverge. If it succeeds, it produces a sequence of subgoal sequents.
The term is accepted by the system as a justification if and only if this
procedure succeeds, and in that case, it uses the generated subgoals
as the subgoals of the current node.
As the first step of the process the theorem proving system
must determine whether the term $t$ provided as a refinement represents
a pre-proof, and if so which one. If this step of the procedure
succeeds, it produces the pre-proof that $t$ represents. This
step of the process can be done using the operation $\unrepfunfor
$,
provided that this function is sufficiently carefully defined.
There are two key issues here. First, $\unrepfunfor
$ must be
partial computable. Second, $\unrepfunfor
(t)$ may only be
a pre-proof if $t$ actually represents a pre-proof.
Each of these conditions is easy to satisfy provided the operation
$\eval$ is appropriately defined. In addition to the standard
requirements, we need to know that $\eval(t)$ is a partial computable
function, and that it is a term $t'$ only if $\evalsto
$.
Each of these additional requirements is satisfied by the current
version of Nuprl, and by many reasonable extensions of Nuprl.
Moreover, if we take a partial computable function $\eval$ as
our primitive notion of evaluation, and then define
the $\evalstoarg$ relation as the graph of this function,
these conditions are trivially satisfied. Note too that $\eval$
is partial recursive if all of the valuation fragments are.
In addition, we need to assume that various simple operations
on terms are partial recursive. For example, deciding whether a term
has a particular leading operator, or extracting a particular subterm.
We believe that this will be true of any reasonable implementation
of Nuprl.
Given these assumptions, we argue that every unrepresentation
function we use is partial computable, and that the unrepresentation of
some term $t$ is defined only if $t$ actually represents an object of the
appropriate form. To do so, we consider two examples: the
unrepresentation fragment for operator names, and the unrepresentation
function for pairs.
$\unrepfunfor
(t)$ is defined so that if
$\eval(t)$ is a term of the form $\opidterm
$, then
$\unrepfunfor
(t)$ is $o$. If we add a clause to this definition
stating that otherwise, $\unrepfunfor
(t)$ is divergent, then
we can prove the required property of $\unrepfunfor
$.
Clearly, $\unrepfunfor
(t)$ is partial computable. First, compute
$\eval(t)$. If this diverges, so does $\unrepfunfor
(t)$.
Otherwise, check to see if the resulting term $t'$ is of the appropriate form.
If it is, extract the operator name to be returned from $t'$.
If it is not, diverge. Clearly, with this more careful
definition, $\unrepfunfor
(t)$ is an operator name $o$,
if and only if $\eval(t)$ is $\opidterm
$.
Now, suppose that $t \repsrelfor
o$. This is the case if and only
if $\evalsto
{\opidterm{o}}$. But this is the case if and only if
$\eval
$ is $\opidterm
$. Thus, $\unrepfunfor
(t)$
is an operator name $o$ if and only if $t \repsrelfor
o$.
Now consider $\unrepfundp
(t)$. It is defined
so that if $\eval(t)$ is of the form $\uglypairterm
$,
$\unrepfunfor
(t_a)$ is $a$, and $\unrepfunfor
(t_b)$ is $b$,
then $\unrepfundp
(t)$ is the pair $\langle a, b\rangle$.
Again add a further condition stating that otherwise
$\unrepfundp
(t)$ is divergent. Clearly, the resulting
function is computable. Furthermore, if we assume that
$\unrepfunfor
(t_a)$ and $\unrepfunfor
(t_b)$ are only
defined if $t_a$ represents an object of $\cal A$, and $t_b$
represents an object of $\cal B$, we can easily show that
$\unrepfundp
(t)$ is only defined if
if $t$ represents an object of $\cal A\times B$.
To see this note that $t \repsdp
\langle a, b\rangle$
if and only if $\evalsto
{\pairterm
{t_b}}$,
$t_a \repsrelfor
a$, and $t_b \repsrelfor
b$.
The first of these conditions is satisfied if and only if
$\eval(t)$ is $\pairterm
$, the second is satisfied
if and only if $\unrepfunfor
(t_a)$ is $a$, and the third
is satisfied if and only if $\unrepfunfor
(t_b)$ is $b$.
If these three conditions hold,
$\unrepfundp
(t)$ is $\langle a, b\rangle$. Otherwise,
$\unrepfundp
(t)$ is divergent.
By modifying all our earlier definitions of
unrepresentation functions in this fashion, we can
arrange that $\unrepfunfor
$ have the required properties.
The second step of checking the applicability of a particular
tactic refinement is to ensure that the topmost goal of the generated
pre-proof $p$ is identical to the goal sequent the tactic refines.
This step is trivial to implement, provided of course that the
basic destructuring and decision operations concerning pre-proofs,
sequents and terms are computable. This step succeeds
if and only if the topmost goal of $p$ matches the sequent
being refined.
The third step is to ensure that the generated
pre-proof is, in fact, a proof. This requires that
we check that every node of the pre-proof matches up appropriately.
Thus, this step can be implemented using a tree walk of the pre-proof.
All that needs to be explained is how each node is checked to
ensure that it matches up. How this is done depends on the
sort of justification used at the node. If the node is unjustified,
all that need be done is ensure that it has no subgoals. If the
node is justified by a primitive rule, then it consists of
a goal sequent $g'$, a primitive rule $p$, and a sequence
of sub-pre-proofs $\sequence
$. For each sub-pre-proof $q_i$,
compute the topmost goal $s_i$ of $q_i$. Now, call the
subgoal generating procedure for primitive applications, with
$g'$ and $p$ as arguments. The node matches up if and only if
the sequence of subgoals $\sequence
$ generated by this
procedure exactly matches the sequence $\sequence
$.
Otherwise the node consists of a goal $g'$, a tactic $t'$, and
sub-pre-proofs $\sequence
$. Again we compute the sequence $\sequence
$
consisting of the topmost goals of $\sequence
$. Then
we call the procedure we are describing recursively, using $g'$
and $t'$ as arguments. The node matches up if and only if the
resulting sequence of sequents exactly matches $\sequence
$.
This step succeeds if and only if every node matches up.
If all three of the previous steps are successful, the fourth
step is to generate subgoals. To do this, all that is required is
that the frontier of pre-proof generated in the first step be
computed. Otherwise, the tactic refinement fails.
Note that the third step of this procedure terminates only if there is
a bound on the depth of recursion required to verify each tactic node.
This amounts to a requirement that after a finite number of tactic
unrollings, a primitive proof must arise.
As we stated earlier it is not necessary to perform these
steps sequentially, rather they can be performed in parallel.
The key point is that the natural implementation of the
function $\unrepfunfor
$ produces pre-proofs top down.
The basic idea, then is to perform the various other tests
as soon as $\unrepfunfor
$ has produced enough of
the pre-proof, rather than waiting for it to finish.
It is almost trivial to combine steps one and two.
Suppose that we are attempting to check the refinement of
a goal sequent $g$ by a tactic $t$. Suppose that step one is successful.
Then, $\unrepfunfor
(t)$ is a preproof
$p = \langle g', \langle j,\sequence
\rangle\rangle$.
Step two is successful if and only if $g$ is $g'$.
Recall that $\unrepfunfor
(t)$ is defined as
[
(\unrepfunfor
\times
(\unrepfunfor
\times \unrepfunforseq
))(t).
]
But this is defined if and only if $\eval(t)$ is of the form
$\uglypairterm
$, $\unrepfunfor
$ is $g'$,
and $(\unrepfunfor
\times \unrepfunforseq
)(t_x)$
is $\langle j, \sequence
\rangle$, for some sequent $g'$, justification $j$
and sequence $\sequence
$ of pre-proofs. In this case,
$\unrepfunfor
(t)$ is
$\langle g', \langle j, \sequence
\rangle\rangle$.
Consider the following function. First compute
$\eval(t)$. If this is defined, but not of the form
$\uglypairterm
$, then diverge.
If $\eval(t)$ is of the form $\uglypairterm
$ compute
$\unrepfunfor
(t_g)$. If this produces a sequent $g'$,
then check if $g$ and $g'$ are identical. If they are not, then diverge.
Otherwise, compute
$(\unrepfunfor
\times \unrepfunforseq
)(t_x)$.
If it returns a pair $\langle j, \sequence
\rangle$
of the appropriate sort, then return
$\langle g', \langle j, \sequence
\rangle\rangle$.
In all other cases, diverge. Clearly, this procedure
succeeds if and only if
$\eval(t)$ is of the form
$\uglypairterm
$, $\unrepfunfor
$ is $g$,
and $(\unrepfunfor
\times \unrepfunforseq
)(t_x)$
is $\langle j, \sequence
\rangle$, for some justification $j$
and sequence $\sequence
$ of pre-proofs. In this case,
$\unrepfunfor
(t)$ is
$\langle g, \langle j, \sequence
\rangle\rangle$.
That is, it succeeds if and only if both of steps one and two do.
If it succeeds, it has the same value as step one does.
The remaining steps can be integrated in a similar fashion,
although the details are rather more complicated.
Recall that a principal purpose of tactics is to provide a
means through which a user may soundly extend the logic with new
inference rules. For inference rules, what is important is what
subgoals they produce, and how they guarantee that only valid proofs
may be constructed. To make the inference rule effective, we must also,
at least, explain how the subgoals are produced.
Tactics of the form described here are just one way to implement
this sort of inference rule. A tactic is just a program written in
some untyped programming language. Before the system accepts a
particular tactic justification of a goal $g$, it must verify that the tactic
actually represents a pre-proof $p$ that has $g$ as its topmost goal.
It must also verify that $p$ is a proof. The generated subgoals
are the frontier $\sequence
$ of $p$. Because $p$ is a
more primitive proof of $g$ from the subgoals $\sequence
$, it is
easy to believe that this for user supplied inference rule is valid.
Except for our use of dependent data types in
the representation of tagged operator parameters and of
primitive rule parameters, a type much like our $\PreProof$ type
could be defined using Standard ML datatypes. In the case
of rule parameters, we argued earlier that other representations could be
used which do not require dependent types. For tagged operator
parameters, we might sacrifice the open-endedness of
the class of index family names, and then use a disjoint
union type (implemented using SML datatypes) to represent
operator parameters. Or we might use an abstract datatype together
with injection functions for each index family.
We could argue, using the Semantics of Standard ML~\cite{},
that is a SML program has the SML type $\PreProof$,
and has a value, then this value represents a pre-proof.
Suppose that we did this. Now, we could define a tactic as an
SML program with the SML type $\PreProof$. Since type checking of
SML programs is decidable, this is a recognizable class, so
such a definition is sensible. Now, before the system accepts the
program as a justification of a goal $g$, it must first evaluate the
program. If this produces a value, then this value
represent a pre-proof $p$, so there is no need to check this: we need
only generate $p$. The system must still check that the topmost goal
of $p$ is $g$, and that $p$ is a proof. Subgoals are generated, as
before, by calculating the frontier of $p$. The only way
that the program can produce no value is if it diverges; therefore,
the system must also diverge then.
Yet another way to implement tactics involves the use of a
SML abstract data type $\Proof$. Provided we are sufficiently
careful in our implementation of the constructors for this
type, we can arrange that if a program has a value, and has type $\Proof$,
then it represents a
. If we did this, we could
define tactics as SML programs of of type $\Proof$. Again,
this definition is sensible because type checking is decidable for
SML. Now, before the system accepts the
program as a justification of a goal $g$, it need only evaluate
the program. If a value is produced, the system must produce the
the proof $p$ which it generates, and check that the topmost goal
of $p$ is $g$. Yet again, subgoals are generated by calculating the frontier
of $p$.
Still another approach to adding complex inference rules
is to allow users to justify goals $g$ with terms $t$.
The system accepts such a term $t$ as a justification
of a sequent $g$ if there is a finite sequence of
sequents $\sequence
$ such that
$t \repsrelforseq
\sequence
$.
The system generates the subgoals $\sequence
$. To ensure that
only sound reasoning is allowed when justifications like this are used, the
user is expected to provide a (paper and pencil) proof that if every sequent in
$\sequence
$ is true, then so is $g$.
The last of these approaches is rather different from the
first three. In the first three approaches, a single theorem
asserting the validity of tactic proofs can be proved by the
implementor. This means that we can provide any of the first
three mechanisms as a means through which ordinary users may provide
system extensions. If the system accepts a user's program as a
justification, then the justification must be valid. In contrast,
the fourth approach requires that each time a complex inference is used,
it must somehow be proven valid. Unless we can find some way to
ensure that users always complete these proofs, and that these proofs
are correct, we cannot both allow users access to this fourth mechanism,
and expect to provide strong guarantees concerning system correctness.
However, just because we cannot allow ordinary users access the
fourth mechanism for system extension does not mean that this
technique is completely useless. In the current version of Nuprl
several inferences rules have been added in just this fashion.
The key point is that they were added very carefully, and with a
certain reluctance, by experienced system implementors. Examples
of this sort of system extension are the $\arith$ rules, the
$\equality$ rule, and the \verb+SupInf+ tactic.%
\footnote{%
In fact, it can be shown that the $\arith$ and $\equality$
allow the proof of certain theorems which are not otherwise provable.
For example,
$\forall x\colon
\argdot\equalitytype{{\Bbb Z}}
$
and $\forall A\argcomma B\colon \universeterm
\argcomma c\colon A\argdot
\equalitytype{\universeterm{i}}
\Rightarrow \membershiptype
$.
This occurs because there are no, more primitive, rules asserting
the basic arithmetic properties, and the basic properties of
equality. For example, the only axiomatization of
the fact that $0$ is the additive identity is provided
by the $\arith$ rule itself. Likewise, the only
axiomatization of the fact that types equal in some
universe are extensionally equal is provided by the
$\equality$ rule. There is a small set of valid, genuinely primitive
inference rules with which every inference supported by the
$\arith$ rule can be made. Similarly, we can replace
the $\equality$ rule with more primitive inference rules.%
}
Despite the care of implementation, and the experience of
the implementors, bugs have been found in all of these rules. Imagine
how much worse the situation would be if ordinary users were allowed
to extend the system in this fashion.
Arguably, primitive rules are just like compound rules of
the fourth sort, since they are justified by extra-theoretic
semantic arguments. However, there seems to be a genuine
difference between ordinary primitive rules of Nuprl, such as the
$\applyEquality$ rule and more complicated rules like the
$\arith$ rule. Principally the difference is one of simplicity.
In the first case, we allow only one sort of reasoning, we allow
reasoning that appears to be a single atomic step, and the
implementation involves only pattern matching and substitution.
In the second case, different sorts of inference are supported,
apparently compound inferences are justified in a single step, and
the implementation is complex, involving special purpose
techniques, tailored to the current rule's implementation.
It is worth emphasizing that the difference between
the first three extension techniques and the last one is
that
the fourth technique requires additional justification beyond
an argument that primitive proofs are correct. All four techniques
require that. Rather, the difference is that in each of the previous
techniques all the justification can be done ahead of time, while
in the final technique a new justification must be provided for each
complex inference rule.
For the first technique, we must accept that the
$\unrepfunfor
$ operation is correctly implemented, we
must accept that the test that the topmost goal of a pre-proof is
a particular sequent is correct, and we must accept that our
implementation of $\foo$ is correct. In particular,
$\unrepfunfor
$ must never successfully produce a
non-pre-proof. Each of these requirements is easily believable.
Of the three requirements, the third is the most complicated,
but, as our earlier discussion showed, hardly any new code is
needed beyond that already required for primitive proofs.
The second technique somewhat relaxes the correctness
condition on $\unrepfunfor
$, since there is no longer a need to
check for terms that do not represent pre-proofs. But it requires that
we accept that our ML type checker is correct, and also that
ML typing has the properties we expect of it. Moreover,
we must show that the ML type $\PreProof$ represents the class of
proofs. Note that the first technique does
require this: it only requires that $\unrep
(t)$ is
a pre-proof if it is well-defined.
The third technique has similar requirements. In addition,
however, we must now make sure that the proof constructors are
all correctly implemented. It seems that there needs to be one
proof constructor for each primitive rule. Thus, it seems
that this might be very tedious to check. But there is a trick.
We can write an ML procedure \verb+refine+ which takes a representation
of a justification, and a sequent, and calls the real refinement
engine to generate subgoals. Note that there is no
requirement that the justification argument to \verb+refine+
be a primitive rule: it might just as easily be a tactic justification.
This allows tactics to produce proofs that include tactics.
This is a useful feature, since it allows users to unfold
tactic proofs, one level at a time, until they discover a proof constructed
at the appropriate level of detail.
The final technique requires that we believe that
$\unrepfunforseq
$ is correctly implemented, and that
we believe the argument given to show that each justification of
this sort is correct. Since $\unrepfunforseq
$ is so
simple, it is easy to check that it is correct, but the second
requirement may not be so easily met. If the inference supported
by the justification is very simple, as is the case for primitive
rules, then, of course, it is easy to show that the justification
is right. But if the inference is complicated, and the procedure
used to generate it clever---as is the case with the $\arith$ and
$\SupInf$ rules---then this argument may be arbitrarily
difficult. Moreover, a new argument is needed for each different
justification. Each of $\arith$, $\equality$, and $\SupInf$
requires its own argument. As a result, even if we limit this
technique to system implementors, we jeopardize the correctness
of the system by allowing it.
The problem is that in the first three techniques
tactics are self-verifying, while in the last they not.
This means that in the first three methodologies,
provided we implement the tactic mechanism carefully and
correctly, we do not have to fret over the implementation of particular
tactics. No matter how careless we are in the writing of a tactic, the
worst that can happen is that it does not allow inferences we expect it to.
In contrast, if we are careless when we write tactics using the
fourth approach, we are likely to introduce unsound inference rules.
In fact, for sufficiently complicated inferences, unsoundness is
probable even if we are careful.
Nevertheless, the fact that the fourth technique requires no
proof to be constructed can also be seen as an advantage. First,
it saves us the computational expense of constructing a potentially
large and probably complicated data structure. Second, and
perhaps more important, it frees us from the straitjacket of having to
write our tactics to facilitate the generation of validation proofs.
This contrast is particularly noticeable when the fourth
approach to system enhancement is compared to the third approach,
since the use of abstract data type constructors to construct
proofs means that tactics tend to be written in a highly stylized fashion.
In the next chapter, we show how the reflected $\Proof$
type can be used to provide a means of system extension that
combines the strong soundness guarantees of the first three techniques
described above, without giving up the efficiency and convenience of the
fourth approach. The basic idea is to use a Nuprl
proof that the justification is correct rather than a
paper and pencil proof. We only allow inferences
that can be justified by proofs. That is, we must be able
somehow to provide a proof that fills in the details. The key point
is that the $\Proof$ type represents the class of proofs, and so,
each element of this type corresponds to a real proof.