1. Geb
  2. Prototypes
  3. Computability
  4. BitTree
  5. Scanner
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 Aesop public import Mathlib.Logic.IsEmpty.Defs public import Mathlib.Tactic.Attr.Core public import Mathlib.Tactic.Push public import Mathlib.Tactic.ToDual
set_option doc.verso true

One-pass scanner for binary trees with bitstring leaves

The scanner uses a mode and a pending-tree counter. Forks increase the counter; leaf terminators decrease it. Payload bits are read in their own mode.

Main definitions

  • step consumes one bit.

  • scan starts the scan with one pending tree.

  • validBool accepts exactly when the scanner ends in its accepting mode.

Tags

binary tree, recognizer, finite control, counter

@[expose] public sectionnamespace Geb.BitTree

Scanner modes distinguish tree tags, string tags, payload bits and terminal states.

inductive Mode where | tree | string | bit | done | dead deriving DecidableEq, Repr

A finite-control mode paired with the number of trees awaiting completion.

abbrev State := Mode × Nat

Complete one leaf, accepting only when the last pending tree is completed.

def finish (n : Nat) : State := if n = 1 then (.done, 0) else (.tree, n - 1)

Consume one input bit, with payload bits interpreted only in payload mode.

def step (s : State) (b : Bool) : State := match s.1 with | .tree => if b then (.tree, s.2 + 1) else (.string, s.2) | .string => if b then (.bit, s.2) else finish s.2 | .bit => (.string, s.2) | .done => (.dead, s.2) | .dead => s

Run the scanner from its single pending root.

def scan (w : List Bool) : State := w.foldl step (.tree, 1)

Accept exactly when one tree has ended at the end of the input.

def validBool (w : List Bool) : Bool := decide ((scan w).1 = .done)

Active modes always retain at least one pending tree.

def Active (s : State) : Prop := s.1 = .tree ∨ s.1 = .string ∨ s.1 = .bit → 0 < s.2

Reading a bit preserves positivity of the pending count in active modes.

theorem active_step (s : State) (b : Bool) (h : Active s) : Active (step s b) := s:Stateb:Boolh:Active s⊢ Active (step s b) b:Boolm:Moden:Nath:Active (m, n)⊢ Active (step (m, n) b) b:Booln:Nath:Active (Mode.tree, n)⊢ Active (step (Mode.tree, n) b)b:Booln:Nath:Active (Mode.string, n)⊢ Active (step (Mode.string, n) b)b:Booln:Nath:Active (Mode.bit, n)⊢ Active (step (Mode.bit, n) b)b:Booln:Nath:Active (Mode.done, n)⊢ Active (step (Mode.done, n) b)b:Booln:Nath:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) b) b:Booln:Nath:Active (Mode.tree, n)⊢ Active (step (Mode.tree, n) b)b:Booln:Nath:Active (Mode.string, n)⊢ Active (step (Mode.string, n) b)b:Booln:Nath:Active (Mode.bit, n)⊢ Active (step (Mode.bit, n) b)b:Booln:Nath:Active (Mode.done, n)⊢ Active (step (Mode.done, n) b)b:Booln:Nath:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) b) n:Nath:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) false)n:Nath:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) true) n:Nath:Active (Mode.tree, n)⊢ Active (step (Mode.tree, n) false)n:Nath:Active (Mode.tree, n)⊢ Active (step (Mode.tree, n) true)n:Nath:Active (Mode.string, n)⊢ Active (step (Mode.string, n) false)n:Nath:Active (Mode.string, n)⊢ Active (step (Mode.string, n) true)n:Nath:Active (Mode.bit, n)⊢ Active (step (Mode.bit, n) false)n:Nath:Active (Mode.bit, n)⊢ Active (step (Mode.bit, n) true)n:Nath:Active (Mode.done, n)⊢ Active (step (Mode.done, n) false)n:Nath:Active (Mode.done, n)⊢ Active (step (Mode.done, n) true)n:Nath:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) false)n:Nath:Active (Mode.dead, n)⊢ Active (step (Mode.dead, n) true) All goals completed! 🐙 n:Nath:0 < nh✝:n = 1⊢ (Mode.done, 0).fst = Mode.tree ∨ (Mode.done, 0).fst = Mode.string ∨ (Mode.done, 0).fst = Mode.bit → 0 < (Mode.done, 0).sndn:Nath:0 < nh✝:¬n = 1⊢ (Mode.tree, n - 1).fst = Mode.tree ∨ (Mode.tree, n - 1).fst = Mode.string ∨ (Mode.tree, n - 1).fst = Mode.bit → 0 < (Mode.tree, n - 1).snd n:Nath:0 < nh✝:n = 1⊢ (Mode.done, 0).fst = Mode.tree ∨ (Mode.done, 0).fst = Mode.string ∨ (Mode.done, 0).fst = Mode.bit → 0 < (Mode.done, 0).sndn:Nath:0 < nh✝:¬n = 1⊢ (Mode.tree, n - 1).fst = Mode.tree ∨ (Mode.tree, n - 1).fst = Mode.string ∨ (Mode.tree, n - 1).fst = Mode.bit → 0 < (Mode.tree, n - 1).snd n:Nath:0 < nh✝:¬n = 1⊢ 0 < n - 1 All goals completed! 🐙

A fold of scanner steps preserves the active-mode invariant.

theorem active_foldl (w : List Bool) : ∀ s, Active s → Active (w.foldl step s) := List.rec (fun _ h ↦ h) (fun b _ ih s h ↦ ih (step s b) (active_step s b h)) w

Every reachable active mode has a positive pending count.

theorem scan_active_pos (w : List Bool) : (scan w).1 = .tree ∨ (scan w).1 = .string ∨ (scan w).1 = .bit → 0 < (scan w).2 := active_foldl w (.tree, 1) (w:List Bool⊢ Active (Mode.tree, 1) All goals completed! 🐙)
end Geb.BitTree