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 Mathlib.Data.Nat.Size

set_option doc.verso true

Canonical positive binary words

Positive binary integers have a leading one. Removing that bit identifies positive integers with arbitrary finite bitstrings, read from most to least significant bit.

Main definitions

payload removes the leading one from a positive integer's binary representation.
fromPayload restores the implicit leading one and reads the remaining digits.
readFixed reads a fixed number of such remaining digits.

Main statements

fromPayload_payload and payload_fromPayload give the two inverse laws.
readFixed_eq_some characterizes a successful fixed-width read.

Tags

binary representation, prefix code, parsing

@[expose] public sectionnamespace Geb.BitTree.Elias

The digits after the leading one, from most to least significant.

def payload (n : ℕ) : List Bool := n.bits.reverse.tail

Read a most-significant-first payload with an implicit leading one.

def fromPayload (bs : List Bool) : ℕ := bs.foldl (fun n b ↦ Nat.bit b n) 1

A positive binary integer begins with one in most-significant-first order.

theorem reverse_bits_cons (n : ℕ) : n ≠ 0 → ∃ bs, n.bits.reverse = true :: bs := byn:ℕ⊢ n ≠ 0 → ∃ bs, n.bits.reverse = true :: bs
  apply Nat.binaryRec' (motive := fun n ↦ n ≠ 0 → ∃ bs, n.bits.reverse = true :: bs)
    ?_ ?_ nn:ℕ⊢ 0 ≠ 0 → ∃ bs, (Nat.bits 0).reverse = true :: bsn:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) →
    (n ≠ 0 → ∃ bs, n.bits.reverse = true :: bs) → Nat.bit b n ≠ 0 → ∃ bs, (Nat.bit b n).bits.reverse = true :: bs
  ·n:ℕ⊢ 0 ≠ 0 → ∃ bs, (Nat.bits 0).reverse = true :: bs intro hn:ℕh:0 ≠ 0⊢ ∃ bs, (Nat.bits 0).reverse = true :: bs
    exact (h rfl).elimAll goals completed! 🐙
  ·n:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) →
    (n ≠ 0 → ∃ bs, n.bits.reverse = true :: bs) → Nat.bit b n ≠ 0 → ∃ bs, (Nat.bit b n).bits.reverse = true :: bs intro b k hk ih _n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k ≠ 0 → ∃ bs, k.bits.reverse = true :: bsa✝:Nat.bit b k ≠ 0⊢ ∃ bs, (Nat.bit b k).bits.reverse = true :: bs
    rw [Nat.bits_append_bit k b hk,n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k ≠ 0 → ∃ bs, k.bits.reverse = true :: bsa✝:Nat.bit b k ≠ 0⊢ ∃ bs, (b :: k.bits).reverse = true :: bs List.reverse_consn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k ≠ 0 → ∃ bs, k.bits.reverse = true :: bsa✝:Nat.bit b k ≠ 0⊢ ∃ bs, k.bits.reverse ++ [b] = true :: bs]n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:k ≠ 0 → ∃ bs, k.bits.reverse = true :: bsa✝:Nat.bit b k ≠ 0⊢ ∃ bs, k.bits.reverse ++ [b] = true :: bs
    cases k with
    | zero =>zeron:ℕb:Boolhk:0 = 0 → b = trueih:0 ≠ 0 → ∃ bs, (Nat.bits 0).reverse = true :: bsa✝:Nat.bit b 0 ≠ 0⊢ ∃ bs, (Nat.bits 0).reverse ++ [b] = true :: bs
      have hb : b = true := hk rflzeron:ℕb:Boolhk:0 = 0 → b = trueih:0 ≠ 0 → ∃ bs, (Nat.bits 0).reverse = true :: bsa✝:Nat.bit b 0 ≠ 0hb:b = true⊢ ∃ bs, (Nat.bits 0).reverse ++ [b] = true :: bs
      subst bzeron:ℕih:0 ≠ 0 → ∃ bs, (Nat.bits 0).reverse = true :: bshk:0 = 0 → true = truea✝:Nat.bit true 0 ≠ 0⊢ ∃ bs, (Nat.bits 0).reverse ++ [true] = true :: bs
      exact ⟨[], rfl⟩All goals completed! 🐙
    | succ k =>succn:ℕb:Boolk:ℕhk:k + 1 = 0 → b = trueih:k + 1 ≠ 0 → ∃ bs, (k + 1).bits.reverse = true :: bsa✝:Nat.bit b (k + 1) ≠ 0⊢ ∃ bs, (k + 1).bits.reverse ++ [b] = true :: bs
      obtain ⟨bs, hbs⟩ := ih (Nat.succ_ne_zero k)succn:ℕb:Boolk:ℕhk:k + 1 = 0 → b = trueih:k + 1 ≠ 0 → ∃ bs, (k + 1).bits.reverse = true :: bsa✝:Nat.bit b (k + 1) ≠ 0bs:List Boolhbs:(k + 1).bits.reverse = true :: bs⊢ ∃ bs, (k + 1).bits.reverse ++ [b] = true :: bs
      exact ⟨bs ++ [b], byn:ℕb:Boolk:ℕhk:k + 1 = 0 → b = trueih:k + 1 ≠ 0 → ∃ bs, (k + 1).bits.reverse = true :: bsa✝:Nat.bit b (k + 1) ≠ 0bs:List Boolhbs:(k + 1).bits.reverse = true :: bs⊢ (k + 1).bits.reverse ++ [b] = true :: (bs ++ [b]) rw [hbsn:ℕb:Boolk:ℕhk:k + 1 = 0 → b = trueih:k + 1 ≠ 0 → ∃ bs, (k + 1).bits.reverse = true :: bsa✝:Nat.bit b (k + 1) ≠ 0bs:List Boolhbs:(k + 1).bits.reverse = true :: bs⊢ true :: bs ++ [b] = true :: (bs ++ [b])]n:ℕb:Boolk:ℕhk:k + 1 = 0 → b = trueih:k + 1 ≠ 0 → ∃ bs, (k + 1).bits.reverse = true :: bsa✝:Nat.bit b (k + 1) ≠ 0bs:List Boolhbs:(k + 1).bits.reverse = true :: bs⊢ true :: bs ++ [b] = true :: (bs ++ [b]); rflAll goals completed! 🐙⟩

The leading one and payload reconstruct a positive integer's binary digits.

theorem reverse_bits_eq (n : ℕ) (hn : n ≠ 0) : n.bits.reverse = true :: payload n := byn:ℕhn:n ≠ 0⊢ n.bits.reverse = true :: payload n
  obtain ⟨bs, hbs⟩ := reverse_bits_cons n hnn:ℕhn:n ≠ 0bs:List Boolhbs:n.bits.reverse = true :: bs⊢ n.bits.reverse = true :: payload n
  simp only [payload, hbs, List.tail_cons]All goals completed! 🐙

Reading the least-significant-first representation returns its original number.

theorem foldr_bits (n : ℕ) : n.bits.foldr Nat.bit 0 = n := byn:ℕ⊢ List.foldr Nat.bit 0 n.bits = n
  apply Nat.binaryRec' (motive := fun n ↦ n.bits.foldr Nat.bit 0 = n) ?_ ?_ nn:ℕ⊢ List.foldr Nat.bit 0 (Nat.bits 0) = 0n:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) → List.foldr Nat.bit 0 n.bits = n → List.foldr Nat.bit 0 (Nat.bit b n).bits = Nat.bit b n
  ·n:ℕ⊢ List.foldr Nat.bit 0 (Nat.bits 0) = 0 rflAll goals completed! 🐙
  ·n:ℕ⊢ ∀ (b : Bool) (n : ℕ),
  (n = 0 → b = true) → List.foldr Nat.bit 0 n.bits = n → List.foldr Nat.bit 0 (Nat.bit b n).bits = Nat.bit b n intro b k hk ihn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:List.foldr Nat.bit 0 k.bits = k⊢ List.foldr Nat.bit 0 (Nat.bit b k).bits = Nat.bit b k
    rw [Nat.bits_append_bit k b hk,n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:List.foldr Nat.bit 0 k.bits = k⊢ List.foldr Nat.bit 0 (b :: k.bits) = Nat.bit b k List.foldr_cons,n:ℕb:Boolk:ℕhk:k = 0 → b = trueih:List.foldr Nat.bit 0 k.bits = k⊢ Nat.bit b (List.foldr Nat.bit 0 k.bits) = Nat.bit b k ihn:ℕb:Boolk:ℕhk:k = 0 → b = trueih:List.foldr Nat.bit 0 k.bits = k⊢ Nat.bit b k = Nat.bit b k]All goals completed! 🐙

Restoring the implicit leading one recovers the positive integer.

theorem fromPayload_payload (n : ℕ) (hn : n ≠ 0) : fromPayload (payload n) = n := byn:ℕhn:n ≠ 0⊢ fromPayload (payload n) = n
  have h : n.bits.reverse.foldl (fun n b ↦ Nat.bit b n) 0 = n := by
    rw [List.foldl_reversen:ℕhn:n ≠ 0⊢ List.foldr (fun x y ↦ Nat.bit x y) 0 n.bits = n]n:ℕhn:n ≠ 0⊢ List.foldr (fun x y ↦ Nat.bit x y) 0 n.bits = n
    exact foldr_bits nn:ℕhn:n ≠ 0h:List.foldl (fun n b ↦ Nat.bit b n) 0 n.bits.reverse = n⊢ fromPayload (payload n) = n
  rw [reverse_bits_eq n hnn:ℕhn:n ≠ 0h:List.foldl (fun n b ↦ Nat.bit b n) 0 (true :: payload n) = n⊢ fromPayload (payload n) = n] at hn:ℕhn:n ≠ 0h:List.foldl (fun n b ↦ Nat.bit b n) 0 (true :: payload n) = n⊢ fromPayload (payload n) = n
  exact hAll goals completed! 🐙

Appending a binary digit preserves positivity.

theorem bit_pos (b : Bool) (n : ℕ) (hn : 0 < n) : 0 < Nat.bit b n := byb:Booln:ℕhn:0 < n⊢ 0 < Nat.bit b n
  rw [Nat.bit_valb:Booln:ℕhn:0 < n⊢ 0 < 2 * n + b.toNat]b:Booln:ℕhn:0 < n⊢ 0 < 2 * n + b.toNat
  omegaAll goals completed! 🐙

Appending digits preserves positivity and extends the canonical binary representation.

theorem foldl_bits (bs : List Bool) : ∀ n, 0 < n →
    0 < bs.foldl (fun n b ↦ Nat.bit b n) n ∧
      (bs.foldl (fun n b ↦ Nat.bit b n) n).bits = bs.reverse ++ n.bits :=
  List.rec (fun n hn ↦ ⟨hn, rfl⟩) (fun b bs ih n hn ↦ bybs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < n⊢ 0 < List.foldl (fun n b ↦ Nat.bit b n) n (b :: bs) ∧
  (List.foldl (fun n b ↦ Nat.bit b n) n (b :: bs)).bits = (b :: bs).reverse ++ n.bits
    obtain ⟨hp, he⟩ := ih (Nat.bit b n) (bit_pos b n hn)bs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ 0 < List.foldl (fun n b ↦ Nat.bit b n) n (b :: bs) ∧
  (List.foldl (fun n b ↦ Nat.bit b n) n (b :: bs)).bits = (b :: bs).reverse ++ n.bits
    refine ⟨hp, ?_⟩bs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ (List.foldl (fun n b ↦ Nat.bit b n) n (b :: bs)).bits = (b :: bs).reverse ++ n.bits
    rw [List.foldl_cons,bs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ (List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = (b :: bs).reverse ++ n.bits he,bs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ bs.reverse ++ (Nat.bit b n).bits = (b :: bs).reverse ++ n.bits Nat.bits_append_bit n b (bybs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ n = 0 → b = true omegaAll goals completed! 🐙), List.reverse_consbs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ bs.reverse ++ b :: n.bits = bs.reverse ++ [b] ++ n.bits]bs✝:List Boolb:Boolbs:List Boolih:∀ (n : ℕ),
  0 < n →
    0 < List.foldl (fun n b ↦ Nat.bit b n) n bs ∧ (List.foldl (fun n b ↦ Nat.bit b n) n bs).bits = bs.reverse ++ n.bitsn:ℕhn:0 < nhp:0 < List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bshe:(List.foldl (fun n b ↦ Nat.bit b n) (Nat.bit b n) bs).bits = bs.reverse ++ (Nat.bit b n).bits⊢ bs.reverse ++ b :: n.bits = bs.reverse ++ [b] ++ n.bits
    simp only [List.append_assoc, List.singleton_append]All goals completed! 🐙) bs

Restoring the leading one always gives a positive number.

theorem fromPayload_pos (bs : List Bool) : 0 < fromPayload bs :=
  (foldl_bits bs 1 (bybs:List Bool⊢ 0 < 1 decideAll goals completed! 🐙)).1

The reconstructed number has exactly the prescribed digits after its leading one.

theorem payload_fromPayload (bs : List Bool) : payload (fromPayload bs) = bs := bybs:List Bool⊢ payload (fromPayload bs) = bs
  have he := (foldl_bits bs 1 (bybs:List Bool⊢ 0 < 1 decideAll goals completed! 🐙)).2bs:List Boolhe:(List.foldl (fun n b ↦ Nat.bit b n) 1 bs).bits = bs.reverse ++ Nat.bits 1⊢ payload (fromPayload bs) = bs
  simp only [payload, fromPayload, he, List.reverse_append, List.reverse_reverse,
    Nat.one_bits, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
    List.tail_cons]All goals completed! 🐙

A reconstructed payload has one extra bit for its leading one.

theorem size_fromPayload (bs : List Bool) : (fromPayload bs).size = bs.length + 1 := bybs:List Bool⊢ (fromPayload bs).size = bs.length + 1
  rw [← Nat.size_eq_bits_lenbs:List Bool⊢ (fromPayload bs).bits.length = bs.length + 1]bs:List Bool⊢ (fromPayload bs).bits.length = bs.length + 1
  change (bs.foldl (fun n b ↦ Nat.bit b n) 1).bits.length = _bs:List Bool⊢ (List.foldl (fun n b ↦ Nat.bit b n) 1 bs).bits.length = bs.length + 1
  rw [(foldl_bits bs 1 (bybs:List Bool⊢ 0 < 1 decideAll goals completed! 🐙)).2,
    List.length_append,bs:List Bool⊢ bs.reverse.length + (Nat.bits 1).length = bs.length + 1 List.length_reverse,bs:List Bool⊢ bs.length + (Nat.bits 1).length = bs.length + 1 Nat.one_bitsbs:List Bool⊢ bs.length + [true].length = bs.length + 1]bs:List Bool⊢ bs.length + [true].length = bs.length + 1
  rflAll goals completed! 🐙

Dropping the leading bit subtracts one from the binary size.

theorem length_payload (n : ℕ) : (payload n).length = n.size - 1 := byn:ℕ⊢ (payload n).length = n.size - 1
  simp only [payload, List.length_tail, List.length_reverse, Nat.size_eq_bits_len]All goals completed! 🐙

Positive numbers have positive binary size.

theorem size_pos (n : ℕ) (hn : n ≠ 0) : 0 < n.size := byn:ℕhn:n ≠ 0⊢ 0 < n.size
  have he := size_fromPayload (payload n)n:ℕhn:n ≠ 0he:(fromPayload (payload n)).size = (payload n).length + 1⊢ 0 < n.size
  rw [fromPayload_payload n hnn:ℕhn:n ≠ 0he:n.size = (payload n).length + 1⊢ 0 < n.size] at hen:ℕhn:n ≠ 0he:n.size = (payload n).length + 1⊢ 0 < n.size
  omegaAll goals completed! 🐙

Read a fixed-width payload, retaining the unconsumed suffix.

def readFixed (k : ℕ) (w : List Bool) : Option (ℕ × List Bool) :=
  if k ≤ w.length then some (fromPayload (w.take k), w.drop k) else none

Reading exactly a payload's length recovers its value and leaves the suffix untouched.

theorem readFixed_append (bs rest : List Bool) :
    readFixed bs.length (bs ++ rest) = some (fromPayload bs, rest) := bybs:List Boolrest:List Bool⊢ readFixed bs.length (bs ++ rest) = some (fromPayload bs, rest)
  simp only [readFixed, List.length_append, Nat.le_add_right, ↓reduceIte,
    List.take_left, List.drop_left]All goals completed! 🐙

A successful fixed-width read is precisely a canonical payload followed by its suffix.

theorem readFixed_eq_some (k : ℕ) (w : List Bool) (n : ℕ) (rest : List Bool)
    (h : readFixed k w = some (n, rest)) :
    n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest := byk:ℕw:List Booln:ℕrest:List Boolh:readFixed k w = some (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
  unfold readFixed at hk:ℕw:List Booln:ℕrest:List Boolh:(if k ≤ w.length then some (fromPayload (List.take k w), List.drop k w) else none) = some (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
  split at hisTruek:ℕw:List Booln:ℕrest:List Boolh✝:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ restisFalsek:ℕw:List Booln:ℕrest:List Boolh✝:¬k ≤ w.lengthh:none = some (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
  next hk =>k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
    have he := Option.some.inj hk:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
    have hn : fromPayload (w.take k) = n := congrArg Prod.fst hek:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = n⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
    have hr : w.drop k = rest := congrArg Prod.snd hek:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest
    refine ⟨?_, ?_, ?_⟩refine_1k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ n ≠ 0refine_2k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ n.size = k + 1refine_3k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ w = payload n ++ rest
    ·refine_1k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ n ≠ 0 have hp := fromPayload_pos (w.take k)refine_1k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = resthp:0 < fromPayload (List.take k w)⊢ n ≠ 0
      omegaAll goals completed! 🐙
    ·refine_2k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ n.size = k + 1 rw [← hn,refine_2k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ (fromPayload (List.take k w)).size = k + 1 size_fromPayload,refine_2k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ (List.take k w).length + 1 = k + 1 List.length_take_of_le hkrefine_2k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ k + 1 = k + 1]All goals completed! 🐙
    ·refine_3k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ w = payload n ++ rest rw [← hn,refine_3k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ w = payload (fromPayload (List.take k w)) ++ rest payload_fromPayload,refine_3k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ w = List.take k w ++ rest ← hr,refine_3k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ w = List.take k w ++ List.drop k w List.take_append_droprefine_3k:ℕw:List Booln:ℕrest:List Boolhk:k ≤ w.lengthh:some (fromPayload (List.take k w), List.drop k w) = some (n, rest)he:(fromPayload (List.take k w), List.drop k w) = (n, rest)hn:fromPayload (List.take k w) = nhr:List.drop k w = rest⊢ w = w]All goals completed! 🐙
  next =>k:ℕw:List Booln:ℕrest:List Boolh✝:¬k ≤ w.lengthh:none = some (n, rest)⊢ n ≠ 0 ∧ n.size = k + 1 ∧ w = payload n ++ rest contradictionAll goals completed! 🐙

end Geb.BitTree.Elias