Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Geb.Prototypes.Computability.BitTree.Elias.CodeBits
import Geb.Prototypes.Computability.BitTree.Counter
meta import GebMeta -- shake: keep

set_option doc.verso true

Elias delta codes for natural numbers

The positive integer n + 1 is encoded by the Elias delta code: the gamma code of its binary size, followed by the remaining bits after its leading one. The gamma code prefixes the binary representation by one zero for each bit after its leading one. This is the delta code of Section V of

[Elias1975]

Peter Elias (1975). “Universal codeword sets and representations of the integers”. IEEE Transactions on Information Theory 21(2), pp. 194–203. https://doi.org/10.1109/TIT.1975.1055349.

, shifted to include zero.

Main definitions

encodeNat encodes a natural number.
readNat decodes one number and retains its unconsumed suffix.

Main statements

readNat_encodeNat_append is the roundtrip law with an arbitrary suffix.
readNat_eq_some proves that successful decoding identifies a canonical prefix.
length_encodeNat gives the exact length.
length_encodeNat_le bounds the length by three times the binary size.

References

[Elias1975]
Peter Elias (1975). “Universal codeword sets and representations of the integers”. IEEE Transactions on Information Theory 21(2), pp. 194–203. https://doi.org/10.1109/TIT.1975.1055349.

Tags

Elias delta code, Elias gamma code, prefix code, binary encoding

@[expose] public sectionnamespace Geb.BitTree.Elias

Read the number of zeros preceding the next one, failing if there is no one.

def readZeros : List Bool → Option (ℕ × List Bool) :=
  List.rec none fun b bs next ↦
    if b then some (0, bs) else next.map fun p ↦ (p.1 + 1, p.2)

One recursive clause of the zero-prefix reader.

theorem readZeros_cons (b : Bool) (bs : List Bool) :
    readZeros (b :: bs) =
      if b then some (0, bs) else (readZeros bs).map fun p ↦ (p.1 + 1, p.2) := rfl

A unary length prefix reads back with its suffix intact.

theorem readZeros_append (k : ℕ) (rest : List Bool) :
    readZeros (List.replicate k false ++ true :: rest) = some (k, rest) := byk:ℕrest:List Bool⊢ readZeros (List.replicate k false ++ true :: rest) = some (k, rest)
  apply Nat.rec (motive := fun k ↦
    readZeros (List.replicate k false ++ true :: rest) = some (k, rest)) ?_ ?_ kk:ℕrest:List Bool⊢ readZeros (List.replicate Nat.zero false ++ true :: rest) = some (Nat.zero, rest)k:ℕrest:List Bool⊢ ∀ (n : ℕ),
  readZeros (List.replicate n false ++ true :: rest) = some (n, rest) →
    readZeros (List.replicate n.succ false ++ true :: rest) = some (n.succ, rest)
  ·k:ℕrest:List Bool⊢ readZeros (List.replicate Nat.zero false ++ true :: rest) = some (Nat.zero, rest) rflAll goals completed! 🐙
  ·k:ℕrest:List Bool⊢ ∀ (n : ℕ),
  readZeros (List.replicate n false ++ true :: rest) = some (n, rest) →
    readZeros (List.replicate n.succ false ++ true :: rest) = some (n.succ, rest) intro k ihk✝:ℕrest:List Boolk:ℕih:readZeros (List.replicate k false ++ true :: rest) = some (k, rest)⊢ readZeros (List.replicate k.succ false ++ true :: rest) = some (k.succ, rest)
    rw [List.replicate_succ,k✝:ℕrest:List Boolk:ℕih:readZeros (List.replicate k false ++ true :: rest) = some (k, rest)⊢ readZeros (false :: List.replicate k false ++ true :: rest) = some (k.succ, rest) List.cons_append,k✝:ℕrest:List Boolk:ℕih:readZeros (List.replicate k false ++ true :: rest) = some (k, rest)⊢ readZeros (false :: (List.replicate k false ++ true :: rest)) = some (k.succ, rest) readZeros_consk✝:ℕrest:List Boolk:ℕih:readZeros (List.replicate k false ++ true :: rest) = some (k, rest)⊢ (if false = true then some (0, List.replicate k false ++ true :: rest)
  else Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros (List.replicate k false ++ true :: rest))) =
  some (k.succ, rest)]k✝:ℕrest:List Boolk:ℕih:readZeros (List.replicate k false ++ true :: rest) = some (k, rest)⊢ (if false = true then some (0, List.replicate k false ++ true :: rest)
  else Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros (List.replicate k false ++ true :: rest))) =
  some (k.succ, rest)
    simp only [Bool.false_eq_true, ↓reduceIte, ih, Option.map_some]All goals completed! 🐙

Successful zero-prefix parsing identifies the exact consumed prefix.

theorem readZeros_eq_some (w : List Bool) : ∀ k rest,
    readZeros w = some (k, rest) → w = List.replicate k false ++ true :: rest :=
  List.rec
    (fun k rest h ↦ byw:List Boolk:ℕrest:List Boolh:readZeros [] = some (k, rest)⊢ [] = List.replicate k false ++ true :: rest cases hAll goals completed! 🐙)
    (fun b bs ih k rest h ↦ byw:List Boolb:Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:readZeros (b :: bs) = some (k, rest)⊢ b :: bs = List.replicate k false ++ true :: rest
      cases b with
      | true =>truew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:readZeros (true :: bs) = some (k, rest)⊢ true :: bs = List.replicate k false ++ true :: rest
        change some (0, bs) = some (k, rest) at htruew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:some (0, bs) = some (k, rest)⊢ true :: bs = List.replicate k false ++ true :: rest
        obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj h)truew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: resth:some (0, bs) = some (0, bs)⊢ true :: bs = List.replicate 0 false ++ true :: bs
        rflAll goals completed! 🐙
      | false =>falsew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:readZeros (false :: bs) = some (k, rest)⊢ false :: bs = List.replicate k false ++ true :: rest
        rw [readZeros_consfalsew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:(if false = true then some (0, bs) else Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs)) = some (k, rest)⊢ false :: bs = List.replicate k false ++ true :: rest] at hfalsew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:(if false = true then some (0, bs) else Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs)) = some (k, rest)⊢ false :: bs = List.replicate k false ++ true :: rest
        simp only [Bool.false_eq_true, ↓reduceIte] at hfalsew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs) = some (k, rest)⊢ false :: bs = List.replicate k false ++ true :: rest
        cases hx : readZeros bs with
        | none =>false.nonew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs) = some (k, rest)hx:readZeros bs = none⊢ false :: bs = List.replicate k false ++ true :: rest simp only [hx, Option.map_none, reduceCtorEq] at hAll goals completed! 🐙
        | some p =>false.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs) = some (k, rest)p:ℕ × List Boolhx:readZeros bs = some p⊢ false :: bs = List.replicate k false ++ true :: rest
          rcases p with ⟨j, suffix⟩false.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (readZeros bs) = some (k, rest)j:ℕsuffix:List Boolhx:readZeros bs = some (j, suffix)⊢ false :: bs = List.replicate k false ++ true :: rest
          rw [hxfalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)⊢ false :: bs = List.replicate k false ++ true :: rest] at hfalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)⊢ false :: bs = List.replicate k false ++ true :: rest
          have he := Option.some.inj hfalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)⊢ false :: bs = List.replicate k false ++ true :: rest
          have hk := congrArg Prod.fst hefalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:((fun p ↦ (p.fst + 1, p.snd)) (j, suffix)).fst = (k, rest).fst⊢ false :: bs = List.replicate k false ++ true :: rest
          have hr := congrArg Prod.snd hefalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:((fun p ↦ (p.fst + 1, p.snd)) (j, suffix)).fst = (k, rest).fsthr:((fun p ↦ (p.fst + 1, p.snd)) (j, suffix)).snd = (k, rest).snd⊢ false :: bs = List.replicate k false ++ true :: rest
          change j + 1 = k at hkfalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hr:((fun p ↦ (p.fst + 1, p.snd)) (j, suffix)).snd = (k, rest).sndhk:j + 1 = k⊢ false :: bs = List.replicate k false ++ true :: rest
          change suffix = rest at hrfalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:j + 1 = khr:suffix = rest⊢ false :: bs = List.replicate k false ++ true :: rest
          rw [← hk,false.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:j + 1 = khr:suffix = rest⊢ false :: bs = List.replicate (j + 1) false ++ true :: rest ← hr,false.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:j + 1 = khr:suffix = rest⊢ false :: bs = List.replicate (j + 1) false ++ true :: suffix List.replicate_succ,false.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:j + 1 = khr:suffix = rest⊢ false :: bs = false :: List.replicate j false ++ true :: suffix List.cons_append,false.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:j + 1 = khr:suffix = rest⊢ false :: bs = false :: (List.replicate j false ++ true :: suffix) ih j suffix hxfalse.somew:List Boolbs:List Boolih:∀ (k : ℕ) (rest : List Bool), readZeros bs = some (k, rest) → bs = List.replicate k false ++ true :: restk:ℕrest:List Boolj:ℕsuffix:List Boolh:Option.map (fun p ↦ (p.fst + 1, p.snd)) (some (j, suffix)) = some (k, rest)hx:readZeros bs = some (j, suffix)he:(fun p ↦ (p.fst + 1, p.snd)) (j, suffix) = (k, rest)hk:j + 1 = khr:suffix = rest⊢ false :: (List.replicate j false ++ true :: suffix) = false :: (List.replicate j false ++ true :: suffix)]All goals completed! 🐙) w

Gamma code of a positive integer; zero is assigned the same word as one.

def encodeGamma (n : ℕ) : List Bool :=
  List.replicate (n.size - 1) false ++ true :: payload n

Read one gamma-coded positive integer.

def readGamma (w : List Bool) : Option (ℕ × List Bool) :=
  (readZeros w).bind fun p ↦ readFixed p.1 p.2

A gamma-coded positive integer reads back with its suffix intact.

theorem readGamma_encodeGamma_append (n : ℕ) (hn : n ≠ 0) (rest : List Bool) :
    readGamma (encodeGamma n ++ rest) = some (n, rest) := byn:ℕhn:n ≠ 0rest:List Bool⊢ readGamma (encodeGamma n ++ rest) = some (n, rest)
  simp only [readGamma, encodeGamma, List.append_assoc, List.cons_append, readZeros_append,
    Option.bind_some]n:ℕhn:n ≠ 0rest:List Bool⊢ readFixed (n.size - 1) (payload n ++ rest) = some (n, rest)
  rw [← length_payload,n:ℕhn:n ≠ 0rest:List Bool⊢ readFixed (payload n).length (payload n ++ rest) = some (n, rest) readFixed_append,n:ℕhn:n ≠ 0rest:List Bool⊢ some (fromPayload (payload n), rest) = some (n, rest) fromPayload_payload n hnn:ℕhn:n ≠ 0rest:List Bool⊢ some (n, rest) = some (n, rest)]All goals completed! 🐙

Successful gamma decoding identifies a positive number and its exact canonical prefix.

theorem readGamma_eq_some (w : List Bool) (n : ℕ) (rest : List Bool)
    (h : readGamma w = some (n, rest)) : n ≠ 0 ∧ w = encodeGamma n ++ rest := byw:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest
  cases hx : readZeros w with
  | none =>nonew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)hx:readZeros w = none⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest simp only [readGamma, hx, Option.bind_none, reduceCtorEq] at hAll goals completed! 🐙
  | some p =>somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)p:ℕ × List Boolhx:readZeros w = some p⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest
    rcases p with ⟨k, suffix⟩somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest
    have hf : readFixed k suffix = some (n, rest) := by
      simpa only [readGamma, hx, Option.bind_some] using hsomew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest
    obtain ⟨hn, hs, hw⟩ := readFixed_eq_some k suffix n rest hfsomew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ rest⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest
    refine ⟨hn, ?_⟩somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ rest⊢ w = encodeGamma n ++ rest
    have hl : n.size - 1 = k := byw:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)⊢ n ≠ 0 ∧ w = encodeGamma n ++ rest omegasomew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ resthl:n.size - 1 = k⊢ w = encodeGamma n ++ rest
    rw [readZeros_eq_some w k suffix hx,somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ resthl:n.size - 1 = k⊢ List.replicate k false ++ true :: suffix = encodeGamma n ++ rest hw,somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ resthl:n.size - 1 = k⊢ List.replicate k false ++ true :: (payload n ++ rest) = encodeGamma n ++ rest encodeGamma,somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ resthl:n.size - 1 = k⊢ List.replicate k false ++ true :: (payload n ++ rest) = List.replicate (n.size - 1) false ++ true :: payload n ++ rest hlsomew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ resthl:n.size - 1 = k⊢ List.replicate k false ++ true :: (payload n ++ rest) = List.replicate k false ++ true :: payload n ++ rest]somew:List Booln:ℕrest:List Boolh:readGamma w = some (n, rest)k:ℕsuffix:List Boolhx:readZeros w = some (k, suffix)hf:readFixed k suffix = some (n, rest)hn:n ≠ 0hs:n.size = k + 1hw:suffix = payload n ++ resthl:n.size - 1 = k⊢ List.replicate k false ++ true :: (payload n ++ rest) = List.replicate k false ++ true :: payload n ++ rest
    simp only [List.append_assoc, List.cons_append]All goals completed! 🐙

Elias delta code of the positive integer one greater than the argument.

def encodeNat (n : ℕ) : List Bool := encodeGamma (n + 1).size ++ payload (n + 1)

Decode one shifted Elias delta code and retain the remaining input.

def readNat (w : List Bool) : Option (ℕ × List Bool) :=
  (readGamma w).bind fun p ↦
    (readFixed (p.1 - 1) p.2).bind fun q ↦ some (q.1 - 1, q.2)

Encoding followed by decoding recovers both the number and any appended suffix.

theorem readNat_encodeNat_append (n : ℕ) (rest : List Bool) :
    readNat (encodeNat n ++ rest) = some (n, rest) := byn:ℕrest:List Bool⊢ readNat (encodeNat n ++ rest) = some (n, rest)
  have hp := size_pos (n + 1) (byn:ℕrest:List Bool⊢ n + 1 ≠ 0 omegaAll goals completed! 🐙)n:ℕrest:List Boolhp:0 < (n + 1).size⊢ readNat (encodeNat n ++ rest) = some (n, rest)
  simp only [readNat, encodeNat, List.append_assoc]n:ℕrest:List Boolhp:0 < (n + 1).size⊢ ((readGamma (encodeGamma (n + 1).size ++ (payload (n + 1) ++ rest))).bind fun p ↦
    (readFixed (p.fst - 1) p.snd).bind fun q ↦ some (q.fst - 1, q.snd)) =
  some (n, rest)
  rw [readGamma_encodeGamma_append (n + 1).size (byn:ℕrest:List Boolhp:0 < (n + 1).size⊢ (n + 1).size ≠ 0 omegaAll goals completed! 🐙)]n:ℕrest:List Boolhp:0 < (n + 1).size⊢ ((some ((n + 1).size, payload (n + 1) ++ rest)).bind fun p ↦
    (readFixed (p.fst - 1) p.snd).bind fun q ↦ some (q.fst - 1, q.snd)) =
  some (n, rest)
  simp only [Option.bind_some]n:ℕrest:List Boolhp:0 < (n + 1).size⊢ ((readFixed ((n + 1).size - 1) (payload (n + 1) ++ rest)).bind fun q ↦ some (q.fst - 1, q.snd)) = some (n, rest)
  rw [← length_payload,n:ℕrest:List Boolhp:0 < (n + 1).size⊢ ((readFixed (payload (n + 1)).length (payload (n + 1) ++ rest)).bind fun q ↦ some (q.fst - 1, q.snd)) = some (n, rest) readFixed_append,n:ℕrest:List Boolhp:0 < (n + 1).size⊢ ((some (fromPayload (payload (n + 1)), rest)).bind fun q ↦ some (q.fst - 1, q.snd)) = some (n, rest) fromPayload_payload (n + 1) (byn:ℕrest:List Boolhp:0 < (n + 1).size⊢ n + 1 ≠ 0 omegaAll goals completed! 🐙)]n:ℕrest:List Boolhp:0 < (n + 1).size⊢ ((some (n + 1, rest)).bind fun q ↦ some (q.fst - 1, q.snd)) = some (n, rest)
  rflAll goals completed! 🐙

A successfully decoded word has exactly the canonical code as its consumed prefix.

theorem readNat_eq_some (w : List Bool) (n : ℕ) (rest : List Bool)
    (h : readNat w = some (n, rest)) : w = encodeNat n ++ rest := byw:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)⊢ w = encodeNat n ++ rest
  cases hg : readGamma w with
  | none =>nonew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)hg:readGamma w = none⊢ w = encodeNat n ++ rest simp only [readNat, hg, Option.bind_none, reduceCtorEq] at hAll goals completed! 🐙
  | some p =>somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)p:ℕ × List Boolhg:readGamma w = some p⊢ w = encodeNat n ++ rest
    rcases p with ⟨k, suffix⟩somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)⊢ w = encodeNat n ++ rest
    obtain ⟨hk, hw⟩ := readGamma_eq_some w k suffix hgsomew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffix⊢ w = encodeNat n ++ rest
    cases hf : readFixed (k - 1) suffix with
    | none =>some.nonew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixhf:readFixed (k - 1) suffix = none⊢ w = encodeNat n ++ rest simp only [readNat, hg, hf, Option.bind_some, Option.bind_none, reduceCtorEq] at hAll goals completed! 🐙
    | some p =>some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixp:ℕ × List Boolhf:readFixed (k - 1) suffix = some p⊢ w = encodeNat n ++ rest
      rcases p with ⟨m, tail⟩some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)⊢ w = encodeNat n ++ rest
      obtain ⟨hm, hs, ht⟩ := readFixed_eq_some (k - 1) suffix m tail hfsome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tail⊢ w = encodeNat n ++ rest
      have he : (m - 1, tail) = (n, rest) := Option.some.inj (byw:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tail⊢ some (m - 1, tail) = some (n, rest)
        simpa only [readNat, hg, hf, Option.bind_some] using hAll goals completed! 🐙)some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)⊢ w = encodeNat n ++ rest
      have hn := congrArg Prod.fst hesome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:(m - 1, tail).fst = (n, rest).fst⊢ w = encodeNat n ++ rest
      have hr := congrArg Prod.snd hesome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:(m - 1, tail).fst = (n, rest).fsthr:(m - 1, tail).snd = (n, rest).snd⊢ w = encodeNat n ++ rest
      change m - 1 = n at hnsome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hr:(m - 1, tail).snd = (n, rest).sndhn:m - 1 = n⊢ w = encodeNat n ++ rest
      change tail = rest at hrsome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = rest⊢ w = encodeNat n ++ rest
      have hm' : m = n + 1 := by omegasome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:m.size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1⊢ w = encodeNat n ++ rest
      rw [hm'some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1⊢ w = encodeNat n ++ rest] at hssome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1⊢ w = encodeNat n ++ rest
      have hk' : k = (n + 1).size := by omegasome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ w = encodeNat n ++ rest
      rw [hw,some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma k ++ suffix = encodeNat n ++ rest ht,some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma k ++ (payload m ++ tail) = encodeNat n ++ rest hm',some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma k ++ (payload (n + 1) ++ tail) = encodeNat n ++ rest hk',some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma (n + 1).size ++ (payload (n + 1) ++ tail) = encodeNat n ++ rest hr,some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma (n + 1).size ++ (payload (n + 1) ++ rest) = encodeNat n ++ rest encodeNat,some.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma (n + 1).size ++ (payload (n + 1) ++ rest) = encodeGamma (n + 1).size ++ payload (n + 1) ++ rest List.append_assocsome.somew:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)k:ℕsuffix:List Boolhg:readGamma w = some (k, suffix)hk:k ≠ 0hw:w = encodeGamma k ++ suffixm:ℕtail:List Boolhf:readFixed (k - 1) suffix = some (m, tail)hm:m ≠ 0hs:(n + 1).size = k - 1 + 1ht:suffix = payload m ++ tailhe:(m - 1, tail) = (n, rest)hn:m - 1 = nhr:tail = resthm':m = n + 1hk':k = (n + 1).size⊢ encodeGamma (n + 1).size ++ (payload (n + 1) ++ rest) = encodeGamma (n + 1).size ++ (payload (n + 1) ++ rest)]All goals completed! 🐙

Success is equivalent to having the canonical encoding as a prefix.

theorem readNat_eq_some_iff (w : List Bool) (n : ℕ) (rest : List Bool) :
    readNat w = some (n, rest) ↔ w = encodeNat n ++ rest :=
  ⟨readNat_eq_some w n rest, fun h ↦ h ▸ readNat_encodeNat_append n rest⟩

Both the encoded value and the end of its code are uniquely determined.

theorem encodeNat_append_injective (n m : ℕ) (s t : List Bool)
    (h : encodeNat n ++ s = encodeNat m ++ t) : n = m ∧ s = t := byn:ℕm:ℕs:List Boolt:List Boolh:encodeNat n ++ s = encodeNat m ++ t⊢ n = m ∧ s = t
  have he := congrArg readNat hn:ℕm:ℕs:List Boolt:List Boolh:encodeNat n ++ s = encodeNat m ++ the:readNat (encodeNat n ++ s) = readNat (encodeNat m ++ t)⊢ n = m ∧ s = t
  rw [readNat_encodeNat_append,n:ℕm:ℕs:List Boolt:List Boolh:encodeNat n ++ s = encodeNat m ++ the:some (n, s) = readNat (encodeNat m ++ t)⊢ n = m ∧ s = t readNat_encodeNat_appendn:ℕm:ℕs:List Boolt:List Boolh:encodeNat n ++ s = encodeNat m ++ the:some (n, s) = some (m, t)⊢ n = m ∧ s = t] at hen:ℕm:ℕs:List Boolt:List Boolh:encodeNat n ++ s = encodeNat m ++ the:some (n, s) = some (m, t)⊢ n = m ∧ s = t
  exact Prod.mk.inj (Option.some.inj he)All goals completed! 🐙

Distinct natural numbers have distinct delta codes.

theorem encodeNat_injective : Function.Injective encodeNat := by⊢ Function.Injective encodeNat
  intro n m hn:ℕm:ℕh:encodeNat n = encodeNat m⊢ n = m
  exact (encodeNat_append_injective n m [] [] (byn:ℕm:ℕh:encodeNat n = encodeNat m⊢ encodeNat n ++ [] = encodeNat m ++ [] simpa using hAll goals completed! 🐙)).1

Gamma coding adds one zero for each bit after the leading one.

theorem length_encodeGamma (n : ℕ) :
    (encodeGamma n).length = 2 * (n.size - 1) + 1 := byn:ℕ⊢ (encodeGamma n).length = 2 * (n.size - 1) + 1
  simp only [encodeGamma, List.length_append, List.length_replicate, List.length_cons,
    length_payload]n:ℕ⊢ n.size - 1 + (n.size - 1 + 1) = 2 * (n.size - 1) + 1
  omegaAll goals completed! 🐙

The exact length of the shifted Elias delta code.

theorem length_encodeNat (n : ℕ) :
    (encodeNat n).length = (n + 1).size + 2 * ((n + 1).size.size - 1) := byn:ℕ⊢ (encodeNat n).length = (n + 1).size + 2 * ((n + 1).size.size - 1)
  have hp := size_pos (n + 1) (byn:ℕ⊢ n + 1 ≠ 0 omegaAll goals completed! 🐙)n:ℕhp:0 < (n + 1).size⊢ (encodeNat n).length = (n + 1).size + 2 * ((n + 1).size.size - 1)
  simp only [encodeNat, List.length_append, length_encodeGamma, length_payload]n:ℕhp:0 < (n + 1).size⊢ 2 * ((n + 1).size.size - 1) + 1 + ((n + 1).size - 1) = (n + 1).size + 2 * ((n + 1).size.size - 1)
  omegaAll goals completed! 🐙

Delta coding uses at most three times the binary size of the shifted argument.

theorem length_encodeNat_le (n : ℕ) : (encodeNat n).length ≤ 3 * (n + 1).size := byn:ℕ⊢ (encodeNat n).length ≤ 3 * (n + 1).size
  have hs : (n + 1).size.size ≤ (n + 1).size :=
    Counter.size_le_of_lt_pow _ _ (Nat.lt_two_pow_self (n := (n + 1).size))n:ℕhs:(n + 1).size.size ≤ (n + 1).size⊢ (encodeNat n).length ≤ 3 * (n + 1).size
  rw [length_encodeNatn:ℕhs:(n + 1).size.size ≤ (n + 1).size⊢ (n + 1).size + 2 * ((n + 1).size.size - 1) ≤ 3 * (n + 1).size]n:ℕhs:(n + 1).size.size ≤ (n + 1).size⊢ (n + 1).size + 2 * ((n + 1).size.size - 1) ≤ 3 * (n + 1).size
  omegaAll goals completed! 🐙

Every encoded natural number consumes at least one bit.

theorem length_encodeNat_pos (n : ℕ) : 0 < (encodeNat n).length := byn:ℕ⊢ 0 < (encodeNat n).length
  have hp := size_pos (n + 1) (byn:ℕ⊢ n + 1 ≠ 0 omegaAll goals completed! 🐙)n:ℕhp:0 < (n + 1).size⊢ 0 < (encodeNat n).length
  rw [length_encodeNatn:ℕhp:0 < (n + 1).size⊢ 0 < (n + 1).size + 2 * ((n + 1).size.size - 1)]n:ℕhp:0 < (n + 1).size⊢ 0 < (n + 1).size + 2 * ((n + 1).size.size - 1)
  omegaAll goals completed! 🐙

Successful parsing strictly shortens the input.

theorem readNat_rest_length_lt (w : List Bool) (n : ℕ) (rest : List Bool)
    (h : readNat w = some (n, rest)) : rest.length < w.length := byw:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)⊢ rest.length < w.length
  have hp := length_encodeNat_pos nw:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)hp:0 < (encodeNat n).length⊢ rest.length < w.length
  rw [readNat_eq_some w n rest h,w:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)hp:0 < (encodeNat n).length⊢ rest.length < (encodeNat n ++ rest).length List.length_appendw:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)hp:0 < (encodeNat n).length⊢ rest.length < (encodeNat n).length + rest.length]w:List Booln:ℕrest:List Boolh:readNat w = some (n, rest)hp:0 < (encodeNat n).length⊢ rest.length < (encodeNat n).length + rest.length
  omegaAll goals completed! 🐙

end Geb.BitTree.Elias