FormalConjecturesForMathlib.Computability.BitstringEncoding

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Computability.Encoding
public import Mathlib.Algebra.Field.Rat

Bitstring encodings

This section provides a typeclass-inferrable version of Mathlib's Computability.Encoding, specialized to the alphabet Bool.

Making it a class makes it easier to quickly ask if a function is computable in polynomial time, without having to explicitly pass around the encoding (See IsPolyTime).

We set up instances for common types like Bool, ℕ, ℤ, ℚ, and instance derivations for Prod and List types, so that we obtain instances for many common types appearing in algorithms and complexity theory.

While different references may choose different encodings, generally our encodings should be polytime-transcodable with any other reasonable binary encoding for a given type. Thus, while it may not be obvious without further examination which of several essentially equivalent encodings of a type is being used, we can at least be sure that for functions between types with BitstringEncoding instances, formalizations of questions of polynomial-time computability will capture the intended meaning.

@[expose] public sectionopen Computabilitysection BitstringEncodings

A canonical encoding of a type as bitstrings (List Bool).

This is a class version of Mathlib's Computability.Encoding, specialized to the alphabet Bool.

class BitstringEncoding α extends Computability.Encoding α Boolnamespace BitstringEncodingvariable {α β : Type*}

The encoding function of the canonical BitstringEncoding of α.

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

The decoding function of the canonical BitstringEncoding of α.

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

Decoding is a left inverse of encoding.

@[simp]
theorem bitDecode_bitEncode [BitstringEncoding α] (a : α) : bitDecode (bitEncode a) = some a :=
  toEncoding.decode_encode a

theorem bitEncode_injective [BitstringEncoding α] :
    Function.Injective (bitEncode : α → List Bool) :=
  (toEncoding (α := α)).encode_injective

Transport a BitstringEncoding along an injection f with partial inverse g.

@[instance_reducible]
def ofLeftInverse [BitstringEncoding β] (f : α → β) (g : β → Option α)
    (h : ∀ x, g (f x) = some x) : BitstringEncoding α where
  encode a := bitEncode (f a)
  decode l := (bitDecode l).bind g
  decode_encode a := byα:Type u_1β:Type u_2inst✝:BitstringEncoding βf:α → βg:β → Option αh:∀ (x : α), g (f x) = some xa:α⊢ (bitDecode (bitEncode (f a))).bind g = some a simp [h]All goals completed! 🐙

ℕ is encoded by its (little-endian) binary representation, as in Computability.encodeNat.

instance : BitstringEncoding ℕ where
  encode := Computability.encodeNat
  decode l := some (Computability.decodeNat l)
  decode_encode n := congrArg some (Computability.decode_encodeNat n)

Bool is encoded as a singleton bitstring.

instance : BitstringEncoding Bool where
  encode b := [b]
  decode l := match l with
    | [b] => some b
    | _ => none
  decode_encode _ := rfl

Make a bitstring self-delimiting: each payload bit b becomes the two bits [true, b], and the block is terminated by false.

def delimit : List Bool → List Bool
  | [] => [false]
  | b :: l => true :: b :: delimit l

Parse one self-delimiting block from the front of the input, returning the payload and the remaining input.

def undelimit : List Bool → Option (List Bool × List Bool)
  | false :: rest => some ([], rest)
  | true :: b :: input => (undelimit input).map fun p => (b :: p.1, p.2)
  | _ => none

@[simp]
theorem undelimit_delimit (l rest : List Bool) :
    undelimit (delimit l ++ rest) = some (l, rest) := byl:List Boolrest:List Bool⊢ undelimit (delimit l ++ rest) = some (l, rest)
  induction l with
  | nil =>nilrest:List Bool⊢ undelimit (delimit [] ++ rest) = some ([], rest) rflAll goals completed! 🐙
  | cons b l ih =>consrest:List Boolb:Booll:List Boolih:undelimit (delimit l ++ rest) = some (l, rest)⊢ undelimit (delimit (b :: l) ++ rest) = some (b :: l, rest) simp [delimit, undelimit, ih]All goals completed! 🐙

@[simp]
theorem length_delimit (l : List Bool) : (delimit l).length = 2 * l.length + 1 := byl:List Bool⊢ (delimit l).length = 2 * l.length + 1
  induction l with
  | nil =>nil⊢ (delimit []).length = 2 * [].length + 1 rflAll goals completed! 🐙
  | cons b l ih =>consb:Booll:List Boolih:(delimit l).length = 2 * l.length + 1⊢ (delimit (b :: l)).length = 2 * (b :: l).length + 1 simp [delimit, ih]consb:Booll:List Boolih:(delimit l).length = 2 * l.length + 1⊢ 2 * l.length + 1 + 1 = 2 * (l.length + 1); omegaAll goals completed! 🐙

Parse a sequence of self-delimiting blocks, using fuel to bound the number of blocks.

This is the auxiliary, fuel-carrying implementation of undelimitBlocks; since every block is nonempty, input.length is always enough fuel.

def undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))
  | _, [] => some []
  | 0, _ :: _ => none
  | fuel + 1, input =>
    -- `p.1` is the parsed block and `p.2` the remaining input; using projections rather than a
    -- pattern-matching lambda keeps the body free of matchers.
    (undelimit input).bind fun p => (undelimitBlocksAux fuel p.2).map (p.1 :: ·)

Parse a sequence of self-delimiting blocks off the front of the input.

Since every block is nonempty, input.length bounds the number of blocks, so it always suffices as fuel for undelimitBlocksAux.

def undelimitBlocks (input : List Bool) : Option (List (List Bool)) :=
  undelimitBlocksAux input.length input

theorem length_le_length_flatten_delimit (l : List (List Bool)) :
    l.length ≤ ((l.map delimit).flatten).length := byl:List (List Bool)⊢ l.length ≤ (List.map delimit l).flatten.length
  induction l with
  | nil =>nil⊢ [].length ≤ (List.map delimit []).flatten.length simpAll goals completed! 🐙
  | cons b t ih =>consb:List Boolt:List (List Bool)ih:t.length ≤ (List.map delimit t).flatten.length⊢ (b :: t).length ≤ (List.map delimit (b :: t)).flatten.length
    simp only [List.map_cons, List.flatten_cons, List.length_append, List.length_cons,
      length_delimit]consb:List Boolt:List (List Bool)ih:t.length ≤ (List.map delimit t).flatten.length⊢ t.length + 1 ≤ 2 * b.length + 1 + (List.map delimit t).flatten.length
    omegaAll goals completed! 🐙



private theorem undelimitBlocksAux_flatten_delimit (l : List (List Bool)) (fuel : ℕ)
    (hfuel : l.length ≤ fuel) : undelimitBlocksAux fuel ((l.map delimit).flatten) = some l := byl:List (List Bool)fuel:ℕhfuel:l.length ≤ fuel⊢ undelimitBlocksAux fuel (List.map delimit l).flatten = some l
  induction l generalizing fuel with
  | nil =>nilfuel:ℕhfuel:[].length ≤ fuel⊢ undelimitBlocksAux fuel (List.map delimit []).flatten = some [] cases fuelnil.zerohfuel:[].length ≤ 0⊢ undelimitBlocksAux 0 (List.map delimit []).flatten = some []nil.succn✝:ℕhfuel:[].length ≤ n✝ + 1⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit []).flatten = some [] <;>nil.zerohfuel:[].length ≤ 0⊢ undelimitBlocksAux 0 (List.map delimit []).flatten = some []nil.succn✝:ℕhfuel:[].length ≤ n✝ + 1⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit []).flatten = some [] rflAll goals completed! 🐙
  | cons b t ih =>consb:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tfuel:ℕhfuel:(b :: t).length ≤ fuel⊢ undelimitBlocksAux fuel (List.map delimit (b :: t)).flatten = some (b :: t)
    rw [List.length_consconsb:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tfuel:ℕhfuel:t.length + 1 ≤ fuel⊢ undelimitBlocksAux fuel (List.map delimit (b :: t)).flatten = some (b :: t)consb:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tfuel:ℕhfuel:t.length + 1 ≤ fuel⊢ undelimitBlocksAux fuel (List.map delimit (b :: t)).flatten = some (b :: t)] at hfuelconsb:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tfuel:ℕhfuel:t.length + 1 ≤ fuel⊢ undelimitBlocksAux fuel (List.map delimit (b :: t)).flatten = some (b :: t)
    cases fuelcons.zerob:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some thfuel:t.length + 1 ≤ 0⊢ undelimitBlocksAux 0 (List.map delimit (b :: t)).flatten = some (b :: t)cons.succb:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tn✝:ℕhfuel:t.length + 1 ≤ n✝ + 1⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit (b :: t)).flatten = some (b :: t) <;>cons.zerob:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some thfuel:t.length + 1 ≤ 0⊢ undelimitBlocksAux 0 (List.map delimit (b :: t)).flatten = some (b :: t)cons.succb:List Boolt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tn✝:ℕhfuel:t.length + 1 ≤ n✝ + 1⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit (b :: t)).flatten = some (b :: t) cases bcons.succ.nilt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tn✝:ℕhfuel:t.length + 1 ≤ n✝ + 1⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit ([] :: t)).flatten = some ([] :: t)cons.succ.const:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tn✝:ℕhfuel:t.length + 1 ≤ n✝ + 1head✝:Booltail✝:List Bool⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit ((head✝ :: tail✝) :: t)).flatten = some ((head✝ :: tail✝) :: t) <;>cons.zero.nilt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some thfuel:t.length + 1 ≤ 0⊢ undelimitBlocksAux 0 (List.map delimit ([] :: t)).flatten = some ([] :: t)cons.zero.const:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some thfuel:t.length + 1 ≤ 0head✝:Booltail✝:List Bool⊢ undelimitBlocksAux 0 (List.map delimit ((head✝ :: tail✝) :: t)).flatten = some ((head✝ :: tail✝) :: t)cons.succ.nilt:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tn✝:ℕhfuel:t.length + 1 ≤ n✝ + 1⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit ([] :: t)).flatten = some ([] :: t)cons.succ.const:List (List Bool)ih:∀ (fuel : ℕ), t.length ≤ fuel → undelimitBlocksAux fuel (List.map delimit t).flatten = some tn✝:ℕhfuel:t.length + 1 ≤ n✝ + 1head✝:Booltail✝:List Bool⊢ undelimitBlocksAux (n✝ + 1) (List.map delimit ((head✝ :: tail✝) :: t)).flatten = some ((head✝ :: tail✝) :: t) grind [delimit, undelimitBlocksAux, undelimit_delimit]All goals completed! 🐙

theorem undelimitBlocks_flatten_delimit (l : List (List Bool)) :
    undelimitBlocks ((l.map delimit).flatten) = some l :=
  undelimitBlocksAux_flatten_delimit l _ (length_le_length_flatten_delimit l)

@[simp]
theorem mapM_bitDecode_map_bitEncode [BitstringEncoding α] (l : List α) :
    (l.map bitEncode).mapM bitDecode = some l := byα:Type u_1inst✝:BitstringEncoding αl:List α⊢ List.mapM bitDecode (List.map bitEncode l) = some l
  induction l with
  | nil =>nilα:Type u_1inst✝:BitstringEncoding α⊢ List.mapM bitDecode (List.map bitEncode []) = some [] rflAll goals completed! 🐙
  | cons a t ih =>consα:Type u_1inst✝:BitstringEncoding αa:αt:List αih:List.mapM bitDecode (List.map bitEncode t) = some t⊢ List.mapM bitDecode (List.map bitEncode (a :: t)) = some (a :: t) simp [ih]All goals completed! 🐙

A pair is encoded as a self-delimiting block for the first component followed by the encoding of the second.

instance [BitstringEncoding α] [BitstringEncoding β] : BitstringEncoding (α × β) where
  encode p := delimit (bitEncode p.1) ++ bitEncode p.2
  decode input :=
    match undelimit input with
    | none => none
    | some (block, rest) =>
      match bitDecode block, bitDecode rest with
      | some a, some b => some (a, b)
      | _, _ => none
  decode_encode p := byα:Type u_1β:Type u_2inst✝¹:BitstringEncoding αinst✝:BitstringEncoding βp:α × β⊢ (match undelimit (delimit (bitEncode p.1) ++ bitEncode p.2) with
  | none => none
  | some (block, rest) =>
    match bitDecode block, bitDecode rest with
    | some a, some b => some (a, b)
    | x, x_1 => none) =
  some p simpAll goals completed! 🐙

A list is encoded as the concatenation of self-delimiting blocks for its elements.


instance [BitstringEncoding α] : BitstringEncoding (List α) where
  encode l := ((l.map bitEncode).map delimit).flatten
  decode input := (undelimitBlocks input).bind (·.mapM bitDecode)
  decode_encode l := byα:Type u_1β:Type u_2inst✝:BitstringEncoding αl:List α⊢ ((undelimitBlocks (List.map delimit (List.map bitEncode l)).flatten).bind fun x ↦ List.mapM bitDecode x) = some l
    rw [undelimitBlocks_flatten_delimit (l.map bitEncode)α:Type u_1β:Type u_2inst✝:BitstringEncoding αl:List α⊢ ((some (List.map bitEncode l)).bind fun x ↦ List.mapM bitDecode x) = some lα:Type u_1β:Type u_2inst✝:BitstringEncoding αl:List α⊢ ((some (List.map bitEncode l)).bind fun x ↦ List.mapM bitDecode x) = some l]α:Type u_1β:Type u_2inst✝:BitstringEncoding αl:List α⊢ ((some (List.map bitEncode l)).bind fun x ↦ List.mapM bitDecode x) = some l
    exact mapM_bitDecode_map_bitEncode lAll goals completed! 🐙

A subtype inherits the encoding of the ambient type; decoding additionally checks the defining predicate.

@[instance_reducible]
def ofSubtype {p : α → Prop} [BitstringEncoding α] [DecidablePred p] :
    BitstringEncoding (Subtype p) where
  encode x := bitEncode x.val
  decode input := (bitDecode input).bind fun a => if h : p a then some ⟨a, h⟩ else none
  decode_encode x := byα:Type u_1β:Type u_2p:α → Propinst✝¹:BitstringEncoding αinst✝:DecidablePred px:Subtype p⊢ ((bitDecode (bitEncode ↑x)).bind fun a ↦ if h : p a then some ⟨a, h⟩ else none) = some x simp [x.property]All goals completed! 🐙

ℕ+ is encoded as the subtype {n : ℕ // 0 < n} it is defined to be.

instance : BitstringEncoding ℕ+ :=
  ofSubtype (p := fun n : ℕ => 0 < n)

ℤ is encoded via the pair (n.toNat, (-n).toNat) (one component is always 0).

instance : BitstringEncoding ℤ :=
  ofLeftInverse (fun n : ℤ => (n.toNat, (-n).toNat))
    (fun p => some ((p.1 : ℤ) - (p.2 : ℤ))) (fun n => congrArg some (byα:Type u_1β:Type u_2n:ℤ⊢ ↑(n.toNat, (-n).toNat).1 - ↑(n.toNat, (-n).toNat).2 = n dsimp onlyα:Type u_1β:Type u_2n:ℤ⊢ ↑n.toNat - ↑(-n).toNat = n; omegaAll goals completed! 🐙))

ℚ is encoded as its (reduced) numerator-denominator pair.

instance : BitstringEncoding ℚ :=
  ofLeftInverse (fun q : ℚ => (q.num, q.den))
    (fun p => some ((p.1 : ℚ) / (p.2 : ℚ))) (fun q => byα:Type u_1β:Type u_2q:ℚ⊢ some (↑(q.num, q.den).1 / ↑(q.num, q.den).2) = some q simp [Rat.num_div_den]All goals completed! 🐙)

end BitstringEncodingend BitstringEncodings