The closure library, part V: the binary successor, and unary to binary

The successor on binary numerals (incBitsProg, PolyTimeFun.inc: flip the leading 1s and the first 0, in two passes as decProg), the conversion of a unary numeral to binary (PolyTimeFun.unaryToBin, a fold of the successor), data as its own encoding, the bits of a number, and the tagging combinator (PolyTimeFun.tagged) for constructors of encoded inductive types (planning/succinct-cook-levin.md, S3).

Data as data

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingData : SizedEncoding Data

Data encode as themselves.

Equations

• MIPRE.Cost.instSizedEncodingData = { encode := id, decode := some, decode_encode := MIPRE.Cost.instSizedEncodingData._proof_1 }

@[simp]

theorem MIPRE.Cost.encode_data (d : Data) : encode d = d

@[simp]

theorem MIPRE.Cost.esize_data (d : Data) : esize d = d.size

Bit strings

theorem MIPRE.Cost.esize_bitStr_cons (b : Bool) (l : BitStr) : esize (b :: l) = (Data.ofBool b).size + esize l + 1

@[simp]

theorem MIPRE.Cost.esize_bitStr_nil : esize [] = 1

@[simp]

theorem MIPRE.Cost.esize_true : esize true = 3

@[simp]

theorem MIPRE.Cost.esize_false : esize false = 1

theorem MIPRE.Cost.esize_true_cons (l : BitStr) : esize (true :: l) = esize l + 4

theorem MIPRE.Cost.esize_false_cons (l : BitStr) : esize (false :: l) = esize l + 2

theorem MIPRE.Cost.esize_bitStr_append (l₁ l₂ : BitStr) : esize (l₁ ++ l₂) + 1 = esize l₁ + esize l₂

theorem MIPRE.Cost.esize_replicate_true (j : ℕ) : esize (List.replicate j true) = 4 * j + 1

theorem MIPRE.Cost.esize_replicate_false (j : ℕ) : esize (List.replicate j false) = 2 * j + 1

noncomputable def MIPRE.Cost.PolyTimeFun.natBits : PolyTimeFun ℕ BitStr

The bits of a number, as a polynomial-time function: the encoding is the same.

Equations

• MIPRE.Cost.PolyTimeFun.natBits = MIPRE.Cost.PolyTimeFun.ofEncodeEq Nat.bits MIPRE.Cost.PolyTimeFun.natBits._proof_1

@[simp]

theorem MIPRE.Cost.PolyTimeFun.natBits_apply (n : ℕ) : natBits.toFun n = n.bits

noncomputable def MIPRE.Cost.PolyTimeFun.natData : PolyTimeFun ℕ Data

A number as its encoding.

Equations

• MIPRE.Cost.PolyTimeFun.natData = MIPRE.Cost.PolyTimeFun.ofEncodeEq (fun (n : ℕ) => MIPRE.Cost.encode n) MIPRE.Cost.PolyTimeFun.natData._proof_1

noncomputable def MIPRE.Cost.PolyTimeFun.progData : PolyTimeFun Prog Data

A program as its encoding.

Equations

• MIPRE.Cost.PolyTimeFun.progData = MIPRE.Cost.PolyTimeFun.ofEncodeEq MIPRE.Cost.Prog.toData MIPRE.Cost.PolyTimeFun.progData._proof_1

The binary successor

def MIPRE.Cost.incBits : BitStr → BitStr

The successor of a binary numeral (least significant bit first).

Equations

• MIPRE.Cost.incBits [] = [true]
• MIPRE.Cost.incBits (false :: l) = true :: l
• MIPRE.Cost.incBits (true :: l) = false :: MIPRE.Cost.incBits l

theorem MIPRE.Cost.incBits_bits (n : ℕ) : incBits n.bits = (n + 1).bits

theorem MIPRE.Cost.esize_incBits_le (l : BitStr) : esize (incBits l) ≤ esize l + 4

def MIPRE.Cost.incTail : BitStr → BitStr

The tail of the successor after the leading 1s: [] becomes [1], 0 · r becomes 1 · r.

Equations

• MIPRE.Cost.incTail [] = [true]
• MIPRE.Cost.incTail (head :: r) = true :: r

theorem MIPRE.Cost.incBits_replicate_true (j : ℕ) (rest : BitStr) (hrest : rest = [] ∨ ∃ (r : List Bool), rest = false :: r) : incBits (List.replicate j true ++ rest) = List.replicate j false ++ incTail rest

theorem MIPRE.Cost.exists_leading_trues (l : BitStr) : ∃ (j : ℕ) (rest : BitStr), l = List.replicate j true ++ rest ∧ (rest = [] ∨ ∃ (r : List Bool), rest = false :: r)

def MIPRE.Cost.Prog.incBitsStop1 : Prog

Body of the successor loop: on cons xs acc, if xs is empty stop with (acc, [1]); if its head is 0 stop with (acc, 1 · tail); if its head is 1 continue with (tail, 0 · acc). Reversing the first component onto the second then gives the successor.

Equations

• MIPRE.Cost.Prog.incBitsStop1 = MIPRE.Cost.Prog.nil.cons ((MIPRE.Cost.Prog.var 1).cons (MIPRE.Cost.Prog.const ((MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons MIPRE.Cost.Data.nil)))

def MIPRE.Cost.Prog.incBitsStop2 : Prog

The stop on a head 0: (acc, 1 · tail).

Equations

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

def MIPRE.Cost.Prog.incBitsCont : Prog

The continuation on a head 1: (tail, 0 · acc).

Equations

• MIPRE.Cost.Prog.incBitsCont = (MIPRE.Cost.Prog.nil.cons MIPRE.Cost.Prog.nil).cons ((MIPRE.Cost.Prog.var 3).cons (MIPRE.Cost.Prog.nil.cons (MIPRE.Cost.Prog.var 5)))

def MIPRE.Cost.Prog.incBitsBody : Prog

The body of the successor loop.

Equations

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

theorem MIPRE.Cost.Prog.incBitsBody_wellScoped : WellScoped 1 incBitsBody

theorem MIPRE.Cost.Prog.incBitsBody_empty (acc : BitStr) : Eval [(encode []).cons (encode acc)] incBitsBody (Data.nil.cons ((encode acc).cons (encode [true]))) (esize acc + 11)

theorem MIPRE.Cost.Prog.incBitsBody_false (rest acc : BitStr) : Eval [(encode (false :: rest)).cons (encode acc)] incBitsBody (Data.nil.cons ((encode acc).cons (encode (true :: rest)))) (esize acc + esize rest + 12)

theorem MIPRE.Cost.Prog.incBitsBody_true (rest acc : BitStr) : Eval [(encode (true :: rest)).cons (encode acc)] incBitsBody ((Data.nil.cons Data.nil).cons ((encode rest).cons (encode (false :: acc)))) (esize acc + esize rest + 12)

theorem MIPRE.Cost.Prog.incBitsLoop_runs (j : ℕ) (rest : BitStr) (hrest : rest = [] ∨ ∃ (r : List Bool), rest = false :: r) (acc : BitStr) (env : Env) (S : ℕ) (hS : esize rest + esize acc + 4 * j ≤ S) : ∃ t ≤ (j + 1) * (S + 13), Eval ((encode (List.replicate j true ++ rest)).cons (encode acc) :: env) incBitsBody.loop ((encode (List.replicate j false ++ acc)).cons (encode (incTail rest))) t

The successor loop on 1^j · rest (with rest empty or starting with 0) from the accumulator acc stops with (0^j · acc, incTail rest).

def MIPRE.Cost.Prog.incBitsProg : Prog

The successor of a binary numeral: incBitsProg on encode l computes encode (incBits l).

Equations

• MIPRE.Cost.Prog.incBitsProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ (MIPRE.Cost.Prog.incBitsBody.loop.let_ MIPRE.Cost.Prog.revOntoProg)

theorem MIPRE.Cost.Prog.incBitsProg_wellScoped : WellScoped 1 incBitsProg

theorem MIPRE.Cost.Prog.incBitsProg_runs (l : BitStr) : ∃ t ≤ (List.length l + 2) * (3 * esize l + 32), incBitsProg.Runs (encode l) (encode (incBits l)) t

noncomputable def MIPRE.Cost.PolyTimeFun.inc : PolyTimeFun ℕ ℕ

The successor on binary numerals, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.inc_apply (n : ℕ) : inc.toFun n = n + 1

theorem MIPRE.Cost.esize_succ_le (n : ℕ) : esize (n + 1) ≤ esize n + 4

noncomputable def MIPRE.Cost.PolyTimeFun.unaryToBin : PolyTimeFun Unary ℕ

A unary numeral to binary, by a fold of the successor.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.unaryToBin_apply (u : Unary) : unaryToBin.toFun u = List.length u

Tagged constructors

noncomputable def MIPRE.Cost.PolyTimeFun.tagged {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (k : ℕ) (f : α → β) (h : ∀ (a : α), encode (f a) = (Data.ofNat k).cons (encode a)) : PolyTimeFun α β

A constructor whose encoding pairs a unary tag with the encoding of its argument.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.tagged_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (k : ℕ) (f : α → β) (h : ∀ (a : α), encode (f a) = (Data.ofNat k).cons (encode a)) (a : α) : (tagged k f h).toFun a = f a