Supporting results for pointwise provable equality.
Valuation-local congruence for the minimized constructors #
CategoricalRiceShapiro.ArithmeticCode.Evaluation proves congruence at a fixed
assignment for composition and for the constructors built directly from the
primitives. This module continues the same discipline through the constructors
defined by minimization.
The congruence laws assume only ORingStructure M. The general laws compare
two arities and assignments; their fixed-assignment specializations quantify
only over possible values of the argument codes.
The minimization step is the substantive one. Nat.ArithPart₁.Code.rfind
translates to a conjunction of two occurrences of the body formula, one at the
found value and one under a bounded quantifier, and an equivalence of bodies at
every extended assignment transports both.
Minimization #
Evaluation of a substitution: the body holds at the value the substituted code takes.
codeBind is a composition whose argument vector is the substituted code
followed by the projections, so this is eval_comp_iff with that vector
identified.
Evaluation of a minimization: the body is positive somewhere at the found value, and vanishes at every smaller one.
codeRfindPos searches for the least argument at which its body is positive,
which Code.rfind reaches by inverting the body twice. This states the search
directly in terms of the body, and is the form every use below needs.
Congruence across two arities and two assignments #
Congruence at a fixed assignment compares two codes of one arity.
Relating an entry that codePrec reads with the entry its step relation supplies
needs more: the two codeBeta applications there have different argument codes,
different arities and different assignments, and agree only through the values
their arguments take. EvalEq records exactly that agreement, and the closure
lemmas below propagate it.
Nothing here evaluates a code in the model, and no arithmetic meaning is
attached to remainder, unpairing or codeBeta; each is delta-reduced as a syntax
tree. No arithmetic theory is assumed.
Minimization preserves graph agreement under every extra search input.
Positive-test minimization preserves agreement at every extra search input.
Code binding preserves heterogeneous graph agreement.
The derived constructors, across two arities and assignments #
Subtraction-code construction preserves heterogeneous graph agreement.
Square-root-code construction preserves heterogeneous graph agreement.
Conditional-code construction preserves heterogeneous graph agreement.
Non-strict order-test code construction preserves heterogeneous graph agreement.
First-unpairing code construction preserves heterogeneous graph agreement.
Second-unpairing code construction preserves heterogeneous graph agreement.
Pairing-code construction preserves heterogeneous graph agreement.
Divisibility-test code construction preserves heterogeneous graph agreement.
Remainder-code construction preserves heterogeneous graph agreement.
Two codeBeta applications agree whenever their argument codes do, even at
different arities and under different assignments.
codeBeta is delta-reduced here as a syntax tree only; nothing evaluates it, and
no arithmetic meaning is attached to remainder or unpairing.
Equivalent bodies determine equivalent minimizations.
This is the congruence law for the minimization context, stated at the
assignment v and quantified over the value and the search argument.