Supporting results for pointwise provable equality.

Codes acting on an encoded list

A list of natural numbers is represented by its Encodable code, in which the empty list is 0 and a cons cell is the successor of a Cantor pair of head and tail. codeListHead? and codeListTail invert that representation, and codeListDrop iterates the tail by primitive recursion, so that codeListGet? reads the entry at an index as an encoded Option. codeListLength minimizes the number of entries that must be dropped to reach the empty list, and codeOptionBind is the bind of the encoded option monad.

Only the code constructions are given here. The standard computation theorems over the natural numbers are not part of this migration.

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

The head of an encoded list, as an encoded Option.

Equations

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

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

The tail of an encoded list.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListDropCore : Nat.ArithPart₁.Code 2

Iterated tail of an encoded list, as a code in the index and the list.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListDrop {n : ℕ} (dlist didx : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

Drop didx entries from the encoded list dlist.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListDrop dlist didx = PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListDropCore.comp ![didx, dlist]

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListGetOptional {n : ℕ} (dlist didx : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The entry of the encoded list dlist at index didx, as an encoded Option.

Equations

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

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

The length of an encoded list: the least index at which dropping that many entries leaves the empty list.

Equations

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

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

Bind on an encoded Option: run dk on the payload when dopt encodes some, and return the encoding of none otherwise.

Equations

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

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListDrop_eq_comp {n : ℕ} (dlist didx : Nat.ArithPart₁.Code n) : codeListDrop dlist didx = codeListDropCore.comp ![didx, dlist]

codeListDrop applies one fixed arity-two code to its two arguments.

A context that changes only those arguments is therefore a composition context, to which eval_comp_congr applies. The arity-two code is an implementation detail and stays private; a proof reaches it by rewriting with this equation.

One-layer view of an encoded list

The pinned encoding of List ℕ satisfies encode [] = 0 and encode (x :: xs) = Nat.pair x (encode xs) + 1. The two constructors below name that layer as codes; no arithmetic property of the encoding is asserted here.

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

The encoded empty list.

Equations

• PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListNil = PointwiseComposition.Nat.ArithPart₁.Code.zero n

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListCons {n : ℕ} (dx dt : Nat.ArithPart₁.Code n) : Nat.ArithPart₁.Code n

The encoded list with head dx and tail dt.

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListSnocCore {r : ℕ} (dlist dx : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code (r + 1)

The recursion that rebuilds an encoded list with one entry appended: at recursion argument i the entry at index length - (i + 1) is consed onto the list built so far, starting from the singleton [dx].

Equations

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

def PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListSnoc {r : ℕ} (dlist dx : Nat.ArithPart₁.Code r) : Nat.ArithPart₁.Code r

Append dx to the end of the encoded list dlist.

Equations

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

theorem PointwiseComposition.CategoricalRiceShapiro.ArithmeticCode.codeListSnoc_eq_bind {r : ℕ} (dlist dx : Nat.ArithPart₁.Code r) : codeListSnoc dlist dx = codeBind (codeListLength dlist) (codePrec (codeListCons dx codeListNil) (codeListCons (codeSub (codeListGetOptional (codeLift (codeLift dlist)) (codeSub (codeListLength (codeLift (codeLift dlist))) (codeSucc (Nat.ArithPart₁.Code.proj 0)))) (codeConst 1)) (Nat.ArithPart₁.Code.proj 1)))

codeListSnoc binds the length of its list argument as the recursion argument of one fixed arity-r + 1 code.

The recursion is an implementation detail and stays private; a proof reaches it by rewriting with this equation.