Supporting results for pointwise provable equality.
The length of a constructed evaluation history #
Except in the results described in the paragraphs below, every length
evaluation here is either supplied by a premise or reassembled from drop
evaluations supplied by premises. length_of_drops constructs only
the codeRfindPos presentation from those existing drop witnesses; it
constructs no drop evaluation, and the uniqueness result only identifies the
value of a supplied length evaluation.
Four results are of the opposite kind, and each asserts totality over 𝐏𝐀.
eval_codeEvaluatorRow_exists_of_value gives the row of a table a value at any
value of the table. eval_codeEvaluatorTableStep_exists_of_value composes that
row totality with eval_codeListSnoc_exists_of_values, giving the extended table
a value. eval_codeEvaluatorHistory_exists gives the history a value at every
stage, without a premise. eval_codeHistoryEvaluator_exists gives the lookup
in the history one step past the pair of the first two arguments a value at
every argument triple, composing history totality with
eval_codeTableLookup_exists_of_values. The row and history results are the
only results here that directly use the generic existence theorem for
codePrec.
Four generic readings, over 𝐏𝐀 and 𝐈𝐎𝐩𝐞𝐧, identify the arguments that the
evaluator cell reads at an arbitrary argument triple s, qCode, u.
eval_codeEvaluatorHistoryBeforeCell_exists is a further totality result,
derived from eval_codeEvaluatorHistory_exists: it gives
codeEvaluatorHistoryBeforeCell a value and identifies it with the history at
pair s qCode. eval_codeEvaluatorHistoryBeforeCell_length proves that the
length of that history is pair s qCode, using
eval_codeEvaluatorHistory_length_unique. eval_codeEvaluatorCell_fuel and
eval_codeEvaluatorCell_index read the two components of that length as s and
qCode. None of the four depends on the constructor number of qCode.
Two results relate a codeHistoryEvaluator evaluation at an earlier stage to a
lookup of the same row in the history at a later stage.
eval_codeHistoryEvaluator_succ_of_prefix_lookup derives the earlier
evaluation from the later lookup: it descends one stage at a time with
getAt_step_down, and every history evaluation it uses is supplied.
eval_prefix_lookup_succ_of_codeHistoryEvaluator derives the later lookup from
the earlier evaluation: it ascends one stage at a time with getAt_step_up,
which shows that the snoc step preserves an entry below the last row. History
totality gives each later stage a value, and
eval_codeListLength_exists_of_value gives the extended histories their
lengths.
eval_codeTableLookup_succ_iff_codeHistoryEvaluator_of_history is the
earlier-row bridge. For a history H evaluated at a row count N, a stage k
and a standard index q with pair k q < N, a successful lookup in H at
k, q and an input u is exactly a successful codeHistoryEvaluator
evaluation at k, q, u. Every code is supplied with its value, and the
proof uses no certificate persistence: it descends with getAt_descend and
ascends with getAt_step_up. input_lt_of_codeTableLookup_succ_of_history
derives u < k from such a lookup, and
eval_predecessor_lookup_succ_iff_codeHistoryEvaluator specializes the bridge
to the history before the cell at k + 1, q, read at the decremented stage
k.
eval_codeHistoryEvaluator_succ_iff_cell characterizes a successful lookup:
codeHistoryEvaluator has a successor value at s, qCode, u exactly when
u < s and the evaluator cell of the history one step earlier has that value
at index u. The bound is strict because the row appended at the pair of s
and qCode holds the cells at the indices below s; the row recursion also
evaluates its step at the terminal index, but that value is not part of the
row. The forward direction is the extraction argument of
eval_codeHistoryEvaluator_succ_extract_cell. The reverse direction
constructs the eager row and the history that appends it, using
eval_codeEvaluatorHistory_exists and eval_codeListLength_exists_of_value,
and locates the supplied cell in them with chain_match.
Reading a supplied length evaluation #
The cons layer and the iterated tail #
The iterated tail of a fixed list #
The recursion that appends one row #
Matching the append recursion against the iterated tail #
The length of a constructed history #
A supplied length evaluation of the history at m has the value m.
Existence is never asserted: the length evaluation is a premise, and the proof
only identifies its value. codeListLength is a minimization, and the generic
existence theorem for codePrec is not used here.
The program index read from the history #
A successful history-evaluator lookup one step past the pair of s and
qCode exhibits qCode as the second Cantor component of the length of the
history one step earlier.
The evaluator cell read from the history #
A successful history-evaluator lookup one step past the pair of s and
qCode exhibits qCode as the second Cantor component of the length of the
history one step earlier, and exhibits its own value as the evaluator cell of
that history at index u.
Entries of an encoded list, independently of how the list is written #
An entry older than the last row survives one step back #
An entry below the last row survives one step forward #
Descending to the stage that first records the row #
A positive lookup at an earlier stage #
A successful lookup of an earlier row in the history at a later stage is
already a successful codeHistoryEvaluator evaluation at that earlier stage.
𝐈𝐎𝐩𝐞𝐧 is listed only so that Foundation's pair elaborates in the
statement; it is implied by 𝐏𝐀.
Totality of one evaluation row #
The row of a table has a value at any value of the table.
The row is primitive recursion on the fuel read from the table length, so
eval_codePrec_exists_of_total applies: the base is the empty list and the step
conses one evaluator cell onto the row built so far. The step is constructed at
every recursion index and every predecessor row, the terminal index included,
because the bounded search inside codePrec evaluates its step there as well.
Only existence is asserted. Nothing here decodes the row, and table is not
assumed to encode a well-formed table.
Extending a table by one row has a value at any value of the table.
The row has a value by eval_codeEvaluatorRow_exists_of_value, and appending it
has a value by eval_codeListSnoc_exists_of_values. Only existence is
asserted: neither the table nor the row is decoded.
The history has a value at every stage.
The history is codePrec with base codeListNil and step
codeEvaluatorTableStep applied to the projection onto the predecessor table,
so eval_codePrec_exists_of_total applies: the base has value 0, and the step
has a value by eval_codeEvaluatorTableStep_exists_of_value. The step is
constructed at every recursion index and every predecessor table, the terminal
index included, because the bounded search inside codePrec evaluates its step
there as well.
Only existence is asserted. Nothing here decodes the history or any table in it.
The history and cell arguments read before the cell #
The history one step before the cell has a value at every argument triple, and that value is the history at the pair of the first two arguments.
codeEvaluatorHistoryBeforeCell is codeEvaluatorHistory composed with the
pair of the first two projections. History totality,
eval_codeEvaluatorHistory_exists, gives the history a value H at the stage
pair s qCode, and eval_codePair gives the composed argument that value.
The length of the history read before the cell is the pair of the first two arguments.
The history has a value by eval_codeEvaluatorHistoryBeforeCell_exists, its
length has a value by eval_codeListLength_exists_of_value, and
eval_codeEvaluatorHistory_length_unique identifies that value with the stage
pair s qCode.
The fuel that the evaluator cell reads, the first component of the history length, is the first argument.
The program index that the evaluator cell reads, the second component of the history length, is the second argument.
The history evaluator has a value at every argument triple.
At s, qCode, u the three projections have values s, qCode and u, the
pair of the first two has value pair s qCode by eval_codePair, and its
successor has value pair s qCode + 1. The history has a value H at that
stage by eval_codeEvaluatorHistory_exists, so the composed table argument of
codeTableLookup has value H, and the lookup has a value by
eval_codeTableLookup_exists_of_values. 𝐈𝐎𝐩𝐞𝐧 is installed inside the proof
for eval_codePair and is derived from 𝐏𝐀 through 𝐈Σ 1.
Only existence is asserted. Nothing here decodes the history, the table, or the program index.
The same lookup at a later stage #
A successful lookup and a successful cell #
A successful lookup in a history at an earlier row #
Earlier-row bridge. Let H be the value of codeEvaluatorHistory at a
row count N, and let the row pair k q of the standard index q lie below
N. For codes dtable, dk, dq, dn whose values at v are H, k, the
numeral q and u, the table lookup succeeds with output y + 1 exactly when
codeHistoryEvaluator succeeds with output y + 1 at stage k, index q,
input u.
The stage k is arbitrary below the row bound; it need not be the stage that
produced H. No certificate persistence is used: the forward direction
descends from N to pair k q + 1 with getAt_step_down, and the reverse
direction ascends from pair k q + 1 to N with getAt_step_up.
Input bound. Under the hypotheses of the earlier-row bridge, a successful lookup forces the input below the earlier stage.
Predecessor-stage specialization. In the history before the cell at
k + 1, q, w (which holds the rows below pair (k + 1) q), the lookup at the
decremented stage read by the dispatcher, the program index read by the
dispatcher, and an input code dn with value u succeeds with output y + 1
exactly when codeHistoryEvaluator succeeds at y + 1, k, q, u.