Supporting results for pointwise provable equality.

Compilation of Foundation's finite-arity arithmetic codes to unary Mathlib program descriptions, with arithmetic proofs for the encoded inputs.

@[reducible, inline]

abbrev PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.ACode : ℕ → Type

The ACode construction in FailureOfComposition.ArithmeticCodeCompiler.

Equations

• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.ACode = PointwiseComposition.Nat.ArithPart₁.Code

noncomputable def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.encodeVector {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} : (Fin n → M) → M

Nested pairs ending in zero encode a fixed finite input vector.

Equations

• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.encodeVector x_2 = 0
• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.encodeVector v = ⟪v 0, PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.encodeVector fun (i : Fin n) => v i.succ⟫

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.projectionCode (n : ℕ) : Fin n → ProgramGraph.PCode

The projection Code construction in FailureOfComposition.ArithmeticCodeCompiler.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.projectionCode 0 i = i.elim0

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.tupleCode (n : ℕ) : (Fin n → ProgramGraph.PCode) → ProgramGraph.PCode

The tuple Code construction in FailureOfComposition.ArithmeticCodeCompiler.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.tupleCode 0 x_2 = Nat.Partrec.Code.zero

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.swapCode : ProgramGraph.PCode

The swap Code construction in FailureOfComposition.ArithmeticCodeCompiler.

Equations

• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.swapCode = Nat.Partrec.Code.right.pair Nat.Partrec.Code.left

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.searchZeroCode (c : ProgramGraph.PCode) : ProgramGraph.PCode

The search Zero Code construction in FailureOfComposition.ArithmeticCodeCompiler.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.compile {n : ℕ} : ACode n → ProgramGraph.PCode

Structural compilation preserves the finite vector coding at every constructor; minimization prepends its candidate to that vector.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.compile (PointwiseComposition.Nat.ArithPart₁.Code.zero x✝) = Nat.Partrec.Code.zero
• PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.compile (PointwiseComposition.Nat.ArithPart₁.Code.one x✝) = Nat.Partrec.Code.const 1

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.unaryCompile (c : ACode 1) : ProgramGraph.PCode

Unary programs accept the ordinary input directly.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_projection {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} (i : Fin n) (v : Fin n → M) (y : M) : ProgramGraph.Computes (projectionCode n i) (encodeVector v) y ↔ y = v i

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_tuple {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (n : ℕ) (d : Fin n → ProgramGraph.PCode) (x z : M) : ProgramGraph.Computes (tupleCode n d) x z ↔ ∃ (w : Fin n → M), z = encodeVector w ∧ ∀ (i : Fin n), ProgramGraph.Computes (d i) x (w i)

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_binary_application {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} (p : ProgramGraph.PCode) (i j : Fin n) (v : Fin n → M) (y : M) : ProgramGraph.Computes (Nat.Partrec.Code.comp p (Nat.Partrec.Code.pair (projectionCode n i) (projectionCode n j))) (encodeVector v) y ↔ ProgramGraph.Computes p ⟪v i, v j⟫ y

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_swap {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b z : M) : ProgramGraph.Computes swapCode ⟪a, b⟫ z ↔ z = ⟪b, a⟫

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_candidate_swap {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (a b z : M) : ProgramGraph.Computes (Nat.Partrec.Code.comp c swapCode) ⟪a, b⟫ z ↔ ProgramGraph.Computes c ⟪b, a⟫ z

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_pair_zero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (x z : M) : ProgramGraph.Computes (Nat.Partrec.Code.id.pair Nat.Partrec.Code.zero) x z ↔ z = ⟪x, 0⟫

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_searchZero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ProgramGraph.PCode) (x y : M) : ProgramGraph.Computes (searchZeroCode c) x y ↔ ProgramGraph.Computes c ⟪y, x⟫ 0 ∧ ∀ k < y, ∃ (z : M), z ≠ 0 ∧ ProgramGraph.Computes c ⟪k, x⟫ z

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_compile {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} (c : ACode n) (v : Fin n → M) (y : M) : ProgramGraph.Computes (compile c) (encodeVector v) y ↔ (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code c)

The structural compiler preserves the graph in every PA model. All input components and outputs may be nonstandard elements of that model.

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.computes_unaryCompile {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (c : ACode 1) (x y : M) : ProgramGraph.Computes (unaryCompile c) x y ↔ (FFL.FirstOrder.Semiformula.Evalb ![y, x]) (FFL.FirstOrder.Arithmetic.code c)

Unary compilation realizes the source arithmetic graph on the ordinary input, without exposing the tuple representation.

def PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.sourceGraph (c : ACode 1) : ProofSearch.Graph

The source arithmetic-code graph, in input-output argument order.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.sourceGraph_eval {M : Type u_1} [FFL.ORingStructure M] (c : ACode 1) (x y : M) : (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑(sourceGraph c) ↔ (FFL.FirstOrder.Semiformula.Evalb ![y, x]) (FFL.FirstOrder.Arithmetic.code c)

theorem PointwiseComposition.FailureOfComposition.ArithmeticCodeCompiler.unaryCompile_realizes (c : ACode 1) : ProofSearch.Uniform 𝐏𝐀 (ConcreteEvaluator.eventualGraph (Encodable.encode (unaryCompile c))) (sourceGraph c)

PA proves the uniform realization equation for this explicit compiler.