Supporting results for pointwise provable equality.

Unbounded minimization and substitution of a minimized value

Two constructors over the primitives of CategoricalRiceShapiro.ArithmeticCode.Basic.

codeRfindPos is the least argument at which a code is positive, expressed through Nat.ArithPart₁.Code.rfind, which searches for a zero. codeBind substitutes the value of one code for the head argument of another, and is the idiom in which a minimized value is consumed.

Each construction is accompanied by the theorem that it realizes the intended function over the natural numbers. Those Computes theorems are the input of the standard-model bridge, which turns a computation over ℕ into evaluation at standard numerals in an arbitrary model.

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeRfindPos {n : ℕ} (d : Nat.ArithPart₁.Code (n + 1)) : Nat.ArithPart₁.Code n

The least argument at which d takes a positive value.

Code.rfind searches for a zero, so the body is inverted twice: codePos normalises a positive value to 1, and codeInv exchanges 0 and 1.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeBind {n : ℕ} (dg : Nat.ArithPart₁.Code n) (dc : Nat.ArithPart₁.Code (n + 1)) : Nat.ArithPart₁.Code n

Evaluate dc with the value of dg as its head argument and the ambient arguments beneath it.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeBind dg dc = dc.comp fun (i : Fin (n + 1)) => Fin.cases dg (fun (i : Fin n) => PointwiseComposition.Nat.ArithPart₁.Code.proj i) i

Standard computations over the natural numbers

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeRfindPos {n : ℕ} {d : Nat.ArithPart₁.Code (n + 1)} {f : List.Vector ℕ (n + 1) → ℕ} (hd : Computes d f) : (codeRfindPos d).eval fun (v : List.Vector ℕ n) => Nat.rfind fun (m : ℕ) => Part.some (decide (0 < f (m ::ᵥ v)))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_codeBind {n : ℕ} {dg : Nat.ArithPart₁.Code n} {dc : Nat.ArithPart₁.Code (n + 1)} {gp : List.Vector ℕ n →. ℕ} {f : List.Vector ℕ (n + 1) → ℕ} (hg : dg.eval gp) (hc : Computes dc f) : (codeBind dg dc).eval fun (v : List.Vector ℕ n) => (gp v).bind fun (x : ℕ) => ↑(some (f (x ::ᵥ v)))