Supporting results for pointwise provable equality.

Total arithmetic codes and their standard computations

Computes c f says that the partial-recursive code c realizes the total function f over the natural numbers. This module collects the constructors used throughout the development -- projection, zero, one, addition, multiplication, equality, strict order and composition -- together with the derived total constructors built from them, and records the standard computation theorem for each.

These are statements about the natural numbers. Arbitrary-model evaluation is the subject of CategoricalRiceShapiro.ArithmeticCode.Evaluation.

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.Computes {n : ℕ} (c : Nat.ArithPart₁.Code n) (f : List.Vector ℕ n → ℕ) : Prop

c realizes the total function f.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.Computes c f = c.eval fun (v : List.Vector ℕ n) => ↑(some (f v))

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.eval_of_eq {n : ℕ} {c : Nat.ArithPart₁.Code n} {f g : List.Vector ℕ n →. ℕ} (h : c.eval f) (e : f = g) : c.eval g

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.Computes.of_eq {n : ℕ} {c : Nat.ArithPart₁.Code n} {f g : List.Vector ℕ n → ℕ} (h : Computes c f) (e : ∀ (v : List.Vector ℕ n), f v = g v) : Computes c g

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_zero {n : ℕ} : Computes (Nat.ArithPart₁.Code.zero n) fun (x : List.Vector ℕ n) => 0

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_one {n : ℕ} : Computes (Nat.ArithPart₁.Code.one n) fun (x : List.Vector ℕ n) => 1

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_add {n : ℕ} (i j : Fin n) : Computes (Nat.ArithPart₁.Code.add i j) fun (v : List.Vector ℕ n) => v.get i + v.get j

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_mul {n : ℕ} (i j : Fin n) : Computes (Nat.ArithPart₁.Code.mul i j) fun (v : List.Vector ℕ n) => v.get i * v.get j

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_proj {n : ℕ} (i : Fin n) : Computes (Nat.ArithPart₁.Code.proj i) fun (v : List.Vector ℕ n) => v.get i

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_equal {n : ℕ} (i j : Fin n) : Computes (Nat.ArithPart₁.Code.equal i j) fun (v : List.Vector ℕ n) => Nat.isEqNat (v.get i) (v.get j)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_lt {n : ℕ} (i j : Fin n) : Computes (Nat.ArithPart₁.Code.lt i j) fun (v : List.Vector ℕ n) => Nat.isLtNat (v.get i) (v.get j)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_comp {m k : ℕ} {c : Nat.ArithPart₁.Code k} {d : Fin k → Nat.ArithPart₁.Code m} {f : List.Vector ℕ k → ℕ} {g : Fin k → List.Vector ℕ m → ℕ} (hc : Computes c f) (hd : ∀ (i : Fin k), Computes (d i) (g i)) : Computes (c.comp d) fun (v : List.Vector ℕ m) => f (List.Vector.ofFn fun (i : Fin k) => g i v)

Generic composition at the total-function layer.

Arity-specific composition

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_comp₁ {n : ℕ} {c : Nat.ArithPart₁.Code 1} {d : Nat.ArithPart₁.Code n} {f : ℕ → ℕ} {g : List.Vector ℕ n → ℕ} (hc : Computes c fun (w : List.Vector ℕ 1) => f (w.get 0)) (hd : Computes d g) : Computes (c.comp ![d]) fun (v : List.Vector ℕ n) => f (g v)

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_comp₂ {n : ℕ} {c : Nat.ArithPart₁.Code 2} {d₀ d₁ : Nat.ArithPart₁.Code n} {f : ℕ → ℕ → ℕ} {g₀ g₁ : List.Vector ℕ n → ℕ} (hc : Computes c fun (w : List.Vector ℕ 2) => f (w.get 0) (w.get 1)) (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (c.comp ![d₀, d₁]) fun (v : List.Vector ℕ n) => f (g₀ v) (g₁ v)

Derived total functions

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

The code Succ construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeSucc d = (PointwiseComposition.Nat.ArithPart₁.Code.add 0 1).comp ![d, PointwiseComposition.Nat.ArithPart₁.Code.one n]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeSucc {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codeSucc d) fun (v : List.Vector ℕ n) => g v + 1

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeConst {n : ℕ} : ℕ → Nat.ArithPart₁.Code n

The code Const construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeConst 0 = PointwiseComposition.Nat.ArithPart₁.Code.zero n

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeConst {n : ℕ} (m : ℕ) : Computes (codeConst m) fun (x : List.Vector ℕ n) => m

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

The code Inv construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeInv d = (PointwiseComposition.Nat.ArithPart₁.Code.equal 0 1).comp ![d, PointwiseComposition.Nat.ArithPart₁.Code.zero n]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeInv {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codeInv d) fun (v : List.Vector ℕ n) => Nat.inv (g v)

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

The code Pos construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codePos d = (PointwiseComposition.Nat.ArithPart₁.Code.lt 0 1).comp ![PointwiseComposition.Nat.ArithPart₁.Code.zero n, d]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codePos {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codePos d) fun (v : List.Vector ℕ n) => Nat.pos (g v)

Boolean combinators

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeAnd {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The code And construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

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

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeAnd {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeAnd d₀ d₁) fun (v : List.Vector ℕ n) => Nat.and (g₀ v) (g₁ v)

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeOr {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The code Or construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

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

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeOr {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeOr d₀ d₁) fun (v : List.Vector ℕ n) => Nat.or (g₀ v) (g₁ v)

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeEq {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The code Eq construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeEq d₀ d₁ = (PointwiseComposition.Nat.ArithPart₁.Code.equal 0 1).comp ![d₀, d₁]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeEq {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeEq d₀ d₁) fun (v : List.Vector ℕ n) => Nat.isEqNat (g₀ v) (g₁ v)

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeLt {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The code Lt construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeLt d₀ d₁ = (PointwiseComposition.Nat.ArithPart₁.Code.lt 0 1).comp ![d₀, d₁]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeLt {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeLt d₀ d₁) fun (v : List.Vector ℕ n) => Nat.isLtNat (g₀ v) (g₁ v)

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeAdd {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The code Add construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeAdd d₀ d₁ = (PointwiseComposition.Nat.ArithPart₁.Code.add 0 1).comp ![d₀, d₁]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeAdd {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeAdd d₀ d₁) fun (v : List.Vector ℕ n) => g₀ v + g₁ v

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeMul {n : ℕ} (d₀ d₁ : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The code Mul construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeMul d₀ d₁ = (PointwiseComposition.Nat.ArithPart₁.Code.mul 0 1).comp ![d₀, d₁]

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeMul {n : ℕ} {d₀ d₁ : Nat.ArithPart₁.Code n} {g₀ g₁ : List.Vector ℕ n → ℕ} (h₀ : Computes d₀ g₀) (h₁ : Computes d₁ g₁) : Computes (codeMul d₀ d₁) fun (v : List.Vector ℕ n) => g₀ v * g₁ v

Lifting a code under an extra search variable

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

The code Lift construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeLift d = d.comp fun (i : Fin n) => PointwiseComposition.Nat.ArithPart₁.Code.proj i.succ

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeLift {n : ℕ} {d : Nat.ArithPart₁.Code n} {g : List.Vector ℕ n → ℕ} (hd : Computes d g) : Computes (codeLift d) fun (w : List.Vector ℕ (n + 1)) => g w.tail

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

The code Head construction in CategoricalRiceShapiro.ArithmeticCode.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeHead = PointwiseComposition.Nat.ArithPart₁.Code.proj 0

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.computes_codeHead {n : ℕ} : Computes codeHead fun (w : List.Vector ℕ (n + 1)) => w.head