Supporting results for pointwise provable equality.

Evaluation of the table-lookup code

This module states two results with different assumptions and different content.

eval_codeTableLookup_query_congr assumes no more than ORingStructure M. The query argument of codeTableLookup occurs only inside the Cantor pair that indexes the table, and every constructor between that occurrence and the whole code has a valuation-local congruence law. Composing those laws replaces the query by an equivalent one. That statement is local in every respect: one assignment v, one changed argument, and an equivalence quantified only over the possible query values. The three remaining arguments are never evaluated there, and it computes no value of the lookup.

eval_codeTableLookup_exists_of_values assumes 𝐏𝐀 and does produce a value: from values for all four arguments it builds one for the whole lookup, through the two encoded-list reads and the two subtractions of the option offset. It asserts existence only. The value is not identified with a decoded table entry, and no list semantics is attached to an arbitrary element of the model.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeTableLookup_query_congr {M : Type u_1} [FFL.ORingStructure M] {r : ℕ} (dtable dk dq dq' dn : Nat.ArithPart₁.Code r) (z : M) (v : Fin r → M) (hquery : ∀ (x : M), (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dq) ↔ (FFL.FirstOrder.Semiformula.Evalb (x :> v)) (FFL.FirstOrder.Arithmetic.code dq')) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable dk dq dn)) ↔ (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable dk dq' dn))

Replacing the query code by one with the same graph at v does not change the graph of the lookup at v.

theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.eval_codeTableLookup_exists_of_values {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {r : ℕ} (dtable dk dq dn : Nat.ArithPart₁.Code r) (table key query index : M) (v : Fin r → M) (htable : (FFL.FirstOrder.Semiformula.Evalb (table :> v)) (FFL.FirstOrder.Arithmetic.code dtable)) (hkey : (FFL.FirstOrder.Semiformula.Evalb (key :> v)) (FFL.FirstOrder.Arithmetic.code dk)) (hquery : (FFL.FirstOrder.Semiformula.Evalb (query :> v)) (FFL.FirstOrder.Arithmetic.code dq)) (hindex : (FFL.FirstOrder.Semiformula.Evalb (index :> v)) (FFL.FirstOrder.Arithmetic.code dn)) : ∃ (z : M), (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (codeTableLookup dtable dk dq dn))

The table lookup has a value at any values of its four arguments.

The Cantor pair indexing the table is reached through the public cons existence theorem: codeListCons dk dq is codeSucc (codePair dk dq), so eliminating eval_codeSucc_iff hands back an evaluation of the pair itself without a separate pairing lemma. The two encoded-list reads then supply the optional row and the optional entry, and eval_codeSub removes each option offset. Only existence is asserted.