Data as a primcodable type

Data is denumerable through Cantor pairing (Data.encodeNat/Data.decodeNat), hence Primcodable, with primitive recursive constructor, projections, a tree-recursion principle (Data.primrec_recD), unary numerals, list indexing and the decoders of bit strings. This is the interface between the ambient model and Mathlib's computability (Cost/Partrec.lean): everything the model manipulates is Data — programs included, through Prog.toData — so no separate encoding of Prog is needed.

Data ≃ ℕ

def MIPRE.Cost.Data.encodeNat : Data → ℕ

Data as natural numbers through Cantor pairing: nil ↦ 0, cons a b ↦ pair a b + 1.

Equations

• MIPRE.Cost.Data.nil.encodeNat = 0
• (a.cons b).encodeNat = Nat.pair a.encodeNat b.encodeNat + 1

@[irreducible]

def MIPRE.Cost.Data.decodeNat : ℕ → Data

The inverse of encodeNat.

Equations

• MIPRE.Cost.Data.decodeNat 0 = MIPRE.Cost.Data.nil
• MIPRE.Cost.Data.decodeNat n.succ = (MIPRE.Cost.Data.decodeNat (Nat.unpair n).1).cons (MIPRE.Cost.Data.decodeNat (Nat.unpair n).2)

@[simp]

theorem MIPRE.Cost.Data.encodeNat_nil : nil.encodeNat = 0

@[simp]

theorem MIPRE.Cost.Data.encodeNat_cons (a b : Data) : (a.cons b).encodeNat = Nat.pair a.encodeNat b.encodeNat + 1

@[simp]

theorem MIPRE.Cost.Data.decodeNat_zero : decodeNat 0 = nil

@[simp]

theorem MIPRE.Cost.Data.decodeNat_succ (n : ℕ) : decodeNat (n + 1) = (decodeNat (Nat.unpair n).1).cons (decodeNat (Nat.unpair n).2)

@[simp]

theorem MIPRE.Cost.Data.decodeNat_encodeNat (d : Data) : decodeNat d.encodeNat = d

@[simp]

theorem MIPRE.Cost.Data.encodeNat_decodeNat (n : ℕ) : (decodeNat n).encodeNat = n

def MIPRE.Cost.Data.equivNat : Data ≃ ℕ

Data ≃ ℕ.

Equations

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

@[instance_reducible]

instance MIPRE.Cost.Data.instDenumerable : Denumerable Data

Equations

• MIPRE.Cost.Data.instDenumerable = Denumerable.mk' MIPRE.Cost.Data.equivNat

theorem MIPRE.Cost.Data.encode_eq (d : Data) : Encodable.encode d = d.encodeNat

theorem MIPRE.Cost.Data.ofNat_eq (n : ℕ) : Denumerable.ofNat Data n = decodeNat n

Primitive recursive constructor and projections

theorem MIPRE.Cost.Data.primrec_decodeNat : Primrec decodeNat

theorem MIPRE.Cost.Data.primrec_cons : Primrec₂ cons

def MIPRE.Cost.Data.left : Data → Data

The head of a pair (nil on nil).

Equations

• MIPRE.Cost.Data.nil.left = MIPRE.Cost.Data.nil
• (a.cons b).left = a

def MIPRE.Cost.Data.right : Data → Data

The tail of a pair (nil on nil).

Equations

• MIPRE.Cost.Data.nil.right = MIPRE.Cost.Data.nil
• (a.cons b).right = b

@[simp]

theorem MIPRE.Cost.Data.left_nil : nil.left = nil

@[simp]

theorem MIPRE.Cost.Data.left_cons (a b : Data) : (a.cons b).left = a

@[simp]

theorem MIPRE.Cost.Data.right_nil : nil.right = nil

@[simp]

theorem MIPRE.Cost.Data.right_cons (a b : Data) : (a.cons b).right = b

theorem MIPRE.Cost.Data.encodeNat_left (d : Data) : d.left.encodeNat = if d.encodeNat = 0 then 0 else (Nat.unpair d.encodeNat.pred).1

theorem MIPRE.Cost.Data.encodeNat_right (d : Data) : d.right.encodeNat = if d.encodeNat = 0 then 0 else (Nat.unpair d.encodeNat.pred).2

theorem MIPRE.Cost.Data.primrec_left : Primrec left

theorem MIPRE.Cost.Data.primrec_right : Primrec right

theorem MIPRE.Cost.Data.primrec_ite_nil {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {f : α → Data} {g : α → σ} {h : α → Data → Data → σ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec fun (p : α × Data × Data) => h p.1 p.2.1 p.2.2) : Primrec fun (a : α) => if f a = nil then g a else h a (f a).left (f a).right

Case analysis on Data, primitive recursively.

Tree recursion

def MIPRE.Cost.Data.recD {σ : Type u_1} (base : σ) (step : Data → Data → σ → σ → σ) : Data → σ

Structural recursion on Data with a first-order result.

Equations

• MIPRE.Cost.Data.recD base step MIPRE.Cost.Data.nil = base
• MIPRE.Cost.Data.recD base step (a.cons b) = step a b (MIPRE.Cost.Data.recD base step a) (MIPRE.Cost.Data.recD base step b)

@[simp]

theorem MIPRE.Cost.Data.recD_nil {σ : Type u_1} (base : σ) (step : Data → Data → σ → σ → σ) : recD base step nil = base

@[simp]

theorem MIPRE.Cost.Data.recD_cons {σ : Type u_1} (base : σ) (step : Data → Data → σ → σ → σ) (a b : Data) : recD base step (a.cons b) = step a b (recD base step a) (recD base step b)

theorem MIPRE.Cost.Data.getD_range_map {σ : Type u_1} [Inhabited σ] (F : ℕ → σ) {n i : ℕ} (hi : i < n) : (List.map F (List.range n)).getD i default = F i

theorem MIPRE.Cost.Data.primrec_recD {σ : Type u_1} [Primcodable σ] [Inhabited σ] (base : σ) (step : Data → Data → σ → σ → σ) (hstep : Primrec fun (p : (Data × Data) × σ × σ) => step p.1.1 p.1.2 p.2.1 p.2.2) : Primrec (recD base step)

Tree recursion is primitive recursive (through the pairing encoding, structural recursion on Data is strong recursion on ℕ).

Unary numerals and list indexing

theorem MIPRE.Cost.Data.ofNat_eq_iterate (n : ℕ) : ofNat n = (fun (d : Data) => nil.cons d)^[n] nil

theorem MIPRE.Cost.Data.primrec_ofNat : Primrec ofNat

def MIPRE.Cost.Data.unaryToNat : Data → ℕ

The length of the right spine: reads a unary numeral (unaryToNat (ofNat n) = n).

Equations

• MIPRE.Cost.Data.unaryToNat = MIPRE.Cost.Data.recD 0 fun (x x_1 : MIPRE.Cost.Data) (x_2 rb : ℕ) => rb + 1

@[simp]

theorem MIPRE.Cost.Data.unaryToNat_nil : nil.unaryToNat = 0

@[simp]

theorem MIPRE.Cost.Data.unaryToNat_cons (a b : Data) : (a.cons b).unaryToNat = b.unaryToNat + 1

@[simp]

theorem MIPRE.Cost.Data.unaryToNat_ofNat (n : ℕ) : (ofNat n).unaryToNat = n

theorem MIPRE.Cost.Data.primrec_unaryToNat : Primrec unaryToNat

def MIPRE.Cost.Data.getList (d : Data) (n : ℕ) : Data

The n-th element of a cons-chain (nil beyond the end).

Equations

• d.getList n = (MIPRE.Cost.Data.right^[n] d).left

theorem MIPRE.Cost.Data.primrec_getList : Primrec₂ getList

theorem MIPRE.Cost.Data.getList_list (l : List Data) (i : ℕ) : (list l).getList i = Env.get l i

Decoding bit strings

theorem MIPRE.Cost.Data.toBool?_eq (d : Data) : d.toBool? = if d = nil then some false else if d = nil.cons nil then some true else none

theorem MIPRE.Cost.Data.primrec_toBool? : Primrec toBool?

theorem MIPRE.Cost.Data.toList?_eq_recD {α : Type u_1} (g : Data → Option α) (d : Data) : toList? g d = recD (some []) (fun (a x : Data) (x_1 rb : Option (List α)) => (g a).bind fun (x : α) => Option.map (fun (x_2 : List α) => x :: x_2) rb) d

theorem MIPRE.Cost.Data.primrec_toList? {α : Type u_1} [Primcodable α] {g : Data → Option α} (hg : Primrec g) : Primrec (toList? g)

theorem MIPRE.Cost.Data.primrec_decode_bitStr : Primrec fun (d : Data) => decode d

Decoding bit strings from Data is primitive recursive.

Encoding naturals

The companion of primrec_decode_bitStr in the other direction. A natural is encoded as the bit string of Nat.bits, so its encoding satisfies the halving recursion below, and strong recursion on ℕ turns that into a primitive recursive definition. Every budgeted run of the tabulation feeds the machine an encode (n, …), so this is on the critical path of MIPRE.Halting.tab_computable.

theorem MIPRE.Cost.Data.encode_nat_rec (n : ℕ) : encode n = if n = 0 then nil else (if n % 2 = 1 then nil.cons nil else nil).cons (encode (n / 2))

The binary encoding of a natural as data, in recursive form.

theorem MIPRE.Cost.Data.primrec_encode_nat : Primrec fun (n : ℕ) => encode n

Encoding a natural as data is primitive recursive.

Two small gaps in the ambient library

theorem MIPRE.Cost.primrec_nat_pow : Primrec₂ fun (x1 x2 : ℕ) => x1 ^ x2

Exponentiation is primitive recursive. Mathlib has Nat.Primrec.pow on the unpaired form but no Primrec₂ spelling.

theorem MIPRE.Cost.List.idxOf_congr_inst {α : Type u_1} (i1 i2 : BEq α) [LawfulBEq α] [LawfulBEq α] (a : α) (l : List α) : List.idxOf a l = List.idxOf a l

Two LawfulBEq instances give the same List.idxOf. List Bool has its own BEq, while Mathlib's Primrec.list_idxOf is stated at the one derived from DecidableEq; the two are propositionally equal, but reducing them to a common normal form sends whnf a very long way indeed, so the bridge is proved once, here, rather than left to unification.

theorem MIPRE.Cost.primrec_idxOf_bitStr : Primrec₂ fun (a : BitStr) (l : List BitStr) => List.idxOf a l

The index of a bit string in a list of bit strings, at the instance the enumerations of Halting/Enumerate.lean actually elaborate to.