1. Geb
  2. Mathlib
  3. Data
  4. Tree
  5. Ranked
  6. Binary
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.Mathlib.Data.Tree.Ranked.Preorder public import Mathlib.Data.Fin.VecNotation

The two-symbol ranked alphabet

The alphabet of one nullary and one binary symbol, spelled by one bit each. Its terms are the unlabelled binary trees, the initial algebra of F X = 1 + X × X, and its preorder encoding is RankedAlphabet.spell at this alphabet.

At width one every block is a single bit, so the validity scan carries no incomplete block and its state reduces to a pending count and a liveness verdict. This module names that counter form and gives it one bit at a time, which is the shape a recognizer over the encoding is stated against.

Main definitions

    RankedAlphabet.Binary.binRanked — the alphabet.

    RankedAlphabet.Binary.leaf, RankedAlphabet.Binary.node — the two forms of its terms.

    RankedAlphabet.Binary.depth, RankedAlphabet.Binary.ok — the validity scan's pending count and its liveness verdict, read off a whole word.

Main statements

    RankedAlphabet.Binary.buf_scanFinal_eq_nil — at width one no incomplete block survives a step.

    RankedAlphabet.Binary.depth_le_length — the pending count never exceeds the word length, which is the bound Cobham.length_combSem_le asks for.

    RankedAlphabet.Binary.valid_iff_ok_and_depth_eq_one — validity is the two conditions on the counter form, the third holding of every word.

    RankedAlphabet.Binary.ok_cons_false, RankedAlphabet.Binary.ok_cons_true, RankedAlphabet.Binary.depth_cons_false_of_ok, RankedAlphabet.Binary.depth_cons_true_of_ok_of_two_le_depth — the counter form one bit at a time.

Implementation notes

leafSym and nodeSym name the two indices rather than each use site writing ⟨0, by decide⟩: a symbol index whose bound proof is still an unassigned metavariable blocks arity from reducing, so the child family's domain is then neither Fin 0 nor Fin 2 and the family does not elaborate. Against a symbol index that is a pattern variable, a child index's bound is ascribed rather than proved where it stands: the goal 0 < binRanked.arity ⟨1, h⟩ carries the free variable h, which decide refuses, and presents the arity as an atom, which omega cannot unfold. show (0 : ℕ) < 2 replaces it with the definitionally equal closed goal.

spell_leaf and spell_node have no consumer in this module: they are kept as the alphabet's characteristic spelling equations, stating what the preorder encoding is at this alphabet, and so belong to its public interface rather than to internal machinery.

depth and ok are @[expose], as the declarations they project are: a consuming module's rfl and decide reduce through them only if they unfold across the module boundary. ok_cons_false and ok_cons_true are @[simp], being unconditional rewrite rules on that form; the two depth cons-lemmas are not, since neither ok w = true nor 2 ≤ depth w is a side condition simp discharges here, so as simp rules they would be inert.

scanStep_of_not_live holds at any width — a failed scan absorbs whatever the block layout — and is stated here because here is where it is used.

decide_length_eq_width proceeds by cases b rather than decide alone: decide refuses a goal carrying a free variable, so the case analysis is what closes b, even though [b].length is 1 either way.

code_leafSym and code_nodeSym are proved by decide rather than by rfl. Nat.land, which Nat.testBit runs through, is not exposed, so a block does not reduce during elaboration, while the kernel evaluates it.

Tags

binary tree, ranked alphabet, term algebra, preorder, scan

namespace RankedAlphabet.Binarypublic section

The alphabet of one nullary and one binary symbol, one bit to a block.

@[`@[expose]` has no effect outside a `module` fileexpose] def binRanked : RankedAlphabet := ⟨2, 1, Nat.one_pos, ⊢ 2 ≤ 2 ^ 1 All goals completed! 🐙, ![0, 2]⟩

The nullary symbol.

@[`@[expose]` has no effect outside a `module` fileexpose] def leafSym : Fin binRanked.card := ⟨0, ⊢ 0 < binRanked.card All goals completed! 🐙⟩

The binary symbol.

@[`@[expose]` has no effect outside a `module` fileexpose] def nodeSym : Fin binRanked.card := ⟨1, ⊢ 1 < binRanked.card All goals completed! 🐙⟩

The term with the nullary head symbol.

@[`@[expose]` has no effect outside a `module` fileexpose] def leaf : binRanked.Term := Term.mk binRanked leafSym fun d ↦ absurd (show d.val < 0 from d.isLt) (d:Fin (binRanked.arity leafSym)⊢ ¬↑d < 0 All goals completed! 🐙)

The term with the binary head symbol and children l and r.

@[`@[expose]` has no effect outside a `module` fileexpose] def node (l r : binRanked.Term) : binRanked.Term := Term.mk binRanked nodeSym fun d ↦ if d.val = 0 then l else r

The nullary symbol's block is the single false bit.

theorem code_leafSym : binRanked.code leafSym = [false] := ⊢ binRanked.code leafSym = [false] All goals completed! 🐙

The binary symbol's block is the single true bit.

theorem code_nodeSym : binRanked.code nodeSym = [true] := ⊢ binRanked.code nodeSym = [true] All goals completed! 🐙

The nullary term is spelled by the single false bit.

@[simp] theorem spell_leaf : binRanked.spell leaf = [false] := ⊢ binRanked.spell leaf = [false] ⊢ [false] ++ (List.ofFn fun d ↦ binRanked.spell (absurd ⋯ ⋯)).flatten = [false] All goals completed! 🐙

A binary term is spelled by a true bit and its children's spellings.

@[simp] theorem spell_node (l r : binRanked.Term) : binRanked.spell (node l r) = true :: (binRanked.spell l ++ binRanked.spell r) := l:binRanked.Termr:binRanked.Term⊢ binRanked.spell (node l r) = true :: (binRanked.spell l ++ binRanked.spell r) l:binRanked.Termr:binRanked.Term⊢ [true] ++ (List.ofFn fun d ↦ binRanked.spell (if ↑d = 0 then l else r)).flatten = true :: (binRanked.spell l ++ binRanked.spell r) l:binRanked.Termr:binRanked.Term⊢ [true] ++ (binRanked.spell l ++ (binRanked.spell r ++ [])) = true :: (binRanked.spell l ++ binRanked.spell r) l:binRanked.Termr:binRanked.Term⊢ [true] ++ (binRanked.spell l ++ binRanked.spell r) = true :: (binRanked.spell l ++ binRanked.spell r) All goals completed! 🐙

The count of pending subterms the validity scan leaves.

@[`@[expose]` has no effect outside a `module` fileexpose] def depth (w : List Bool) : ℕ := (binRanked.scanFinal w).depth

Whether the validity scan has not failed.

@[`@[expose]` has no effect outside a `module` fileexpose] def ok (w : List Bool) : Bool := (binRanked.scanFinal w).live

At width one every block completes as it is read, so no incomplete block survives a step.

theorem buf_scanFinal_eq_nil (w : List Bool) : (binRanked.scanFinal w).buf = [] := w:List Bool⊢ (binRanked.scanFinal w).buf = [] w:List Boolh:(binRanked.scanFinal w).buf.length < 1⊢ (binRanked.scanFinal w).buf = [] exact List.eq_nil_of_length_eq_zero (w:List Boolh:(binRanked.scanFinal w).buf.length < 1⊢ (binRanked.scanFinal w).buf.length = 0 All goals completed! 🐙)

The pending count never exceeds the word length.

theorem depth_le_length (w : List Bool) : depth w ≤ w.length := binRanked.depth_scanFinal_le_length w

Validity is the counter form's two conditions: at width one the third, that no incomplete block remains, holds of every word.

theorem valid_iff_ok_and_depth_eq_one (w : List Bool) : binRanked.Valid w ↔ ok w = true ∧ depth w = 1 := w:List Bool⊢ binRanked.Valid w ↔ ok w = true ∧ depth w = 1 w:List Bool⊢ (binRanked.scanFinal w).live = true ∧ (binRanked.scanFinal w).buf = [] ∧ (binRanked.scanFinal w).depth = 1 ↔ ok w = true ∧ depth w = 1 All goals completed! 🐙

The block a bit completes has the alphabet's width.

theorem decide_length_eq_width (b : Bool) : decide (([b] : List Bool).length = binRanked.width) = true := b:Bool⊢ decide ([b].length = binRanked.width) = true ⊢ decide ([false].length = binRanked.width) = true⊢ decide ([true].length = binRanked.width) = true ⊢ decide ([false].length = binRanked.width) = true⊢ decide ([true].length = binRanked.width) = true All goals completed! 🐙

The nullary symbol's block denotes arity zero.

theorem arOf_decodeBits_false : binRanked.arOf (decodeBits [false]) = some 0 := ⊢ binRanked.arOf (decodeBits [false]) = some 0 All goals completed! 🐙

The binary symbol's block denotes arity two.

theorem arOf_decodeBits_true : binRanked.arOf (decodeBits [true]) = some 2 := ⊢ binRanked.arOf (decodeBits [true]) = some 2 All goals completed! 🐙

A leaf bit read by a live scan carrying no incomplete block: its arity is zero, which every pending count admits.

theorem scanStep_false_of_live_of_buf_nil (s : Scan) (hl : s.live = true) (hb : s.buf = []) : binRanked.scanStep false s = ⟨[], s.depth + 1, true⟩ := s:Scanhl:s.live = truehb:s.buf = []⊢ binRanked.scanStep false s = { buf := [], depth := s.depth + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []⊢ (match true with | false => s | true => match decide ([false].length = binRanked.width) with | false => { buf := [false], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [false]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []⊢ (match decide ([false].length = binRanked.width) with | false => { buf := [false], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [false]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []⊢ (match true with | false => { buf := [false], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [false]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []⊢ (match binRanked.arOf (decodeBits [false]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []⊢ (match some 0 with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth + 1, live := true } All goals completed! 🐙

A node bit read with two subterms pending pops both and pushes one.

theorem scanStep_true_of_live_of_buf_nil_of_two_le_depth (s : Scan) (hl : s.live = true) (hb : s.buf = []) (h2 : 2 ≤ s.depth) : binRanked.scanStep true s = ⟨[], s.depth - 2 + 1, true⟩ := s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ binRanked.scanStep true s = { buf := [], depth := s.depth - 2 + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ (match true with | false => s | true => match decide ([true].length = binRanked.width) with | false => { buf := [true], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth - 2 + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ (match decide ([true].length = binRanked.width) with | false => { buf := [true], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth - 2 + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ (match true with | false => { buf := [true], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth - 2 + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ (match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth - 2 + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ (match some 2 with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth - 2 + 1, live := true } s:Scanhl:s.live = truehb:s.buf = []h2:2 ≤ s.depth⊢ (match decide (2 ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - 2 + 1, live := true }) = { buf := [], depth := s.depth - 2 + 1, live := true } All goals completed! 🐙

A node bit read with fewer than two subterms pending fails the scan.

theorem scanStep_true_of_live_of_buf_nil_of_depth_lt_two (s : Scan) (hl : s.live = true) (hb : s.buf = []) (h2 : s.depth < 2) : binRanked.scanStep true s = ⟨[], s.depth, false⟩ := s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ binRanked.scanStep true s = { buf := [], depth := s.depth, live := false } s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ (match true with | false => s | true => match decide ([true].length = binRanked.width) with | false => { buf := [true], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth, live := false } s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ (match decide ([true].length = binRanked.width) with | false => { buf := [true], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth, live := false } s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ (match true with | false => { buf := [true], depth := s.depth, live := true } | true => match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth, live := false } s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ (match binRanked.arOf (decodeBits [true]) with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth, live := false } s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ (match some 2 with | none => { buf := [], depth := s.depth, live := false } | some r => match decide (r ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - r + 1, live := true }) = { buf := [], depth := s.depth, live := false } s:Scanhl:s.live = truehb:s.buf = []h2:s.depth < 2⊢ (match decide (2 ≤ s.depth) with | false => { buf := [], depth := s.depth, live := false } | true => { buf := [], depth := s.depth - 2 + 1, live := true }) = { buf := [], depth := s.depth, live := false } All goals completed! 🐙

A failed scan reads no further.

theorem scanStep_of_not_live (b : Bool) (s : Scan) (hl : s.live = false) : binRanked.scanStep b s = s := b:Bools:Scanhl:s.live = false⊢ binRanked.scanStep b s = s All goals completed! 🐙

A leaf bit cannot fail.

@[simp] theorem ok_cons_false (w : List Bool) : ok (false :: w) = ok w := w:List Bool⊢ ok (false :: w) = ok w w:List Bool⊢ (binRanked.scanStep false (binRanked.scanFinal w)).live = (binRanked.scanFinal w).live w:List Boolh:(binRanked.scanFinal w).live = false⊢ (binRanked.scanStep false (binRanked.scanFinal w)).live = falsew:List Boolh:(binRanked.scanFinal w).live = true⊢ (binRanked.scanStep false (binRanked.scanFinal w)).live = true w:List Boolh:(binRanked.scanFinal w).live = false⊢ (binRanked.scanStep false (binRanked.scanFinal w)).live = false All goals completed! 🐙 w:List Boolh:(binRanked.scanFinal w).live = true⊢ (binRanked.scanStep false (binRanked.scanFinal w)).live = true All goals completed! 🐙

A node bit fails when the scan has already failed, or when fewer than two subterms are pending.

@[simp] theorem ok_cons_true (w : List Bool) : ok (true :: w) = (ok w && decide (2 ≤ depth w)) := w:List Bool⊢ ok (true :: w) = (ok w && decide (2 ≤ depth w)) w:List Bool⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = ((binRanked.scanFinal w).live && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = false⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (false && decide (2 ≤ (binRanked.scanFinal w).depth))w:List Boolh:(binRanked.scanFinal w).live = true⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = false⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (false && decide (2 ≤ (binRanked.scanFinal w).depth)) All goals completed! 🐙 w:List Boolh:(binRanked.scanFinal w).live = true⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth < 2⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (true && decide (2 ≤ (binRanked.scanFinal w).depth))w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth ≥ 2⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth < 2⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth < 2⊢ { buf := [], depth := (binRanked.scanFinal w).depth, live := false }.live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth < 2⊢ false = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) All goals completed! 🐙 w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth ≥ 2⊢ (binRanked.scanStep true (binRanked.scanFinal w)).live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth ≥ 2⊢ { buf := [], depth := (binRanked.scanFinal w).depth - 2 + 1, live := true }.live = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) w:List Boolh:(binRanked.scanFinal w).live = trueh2:(binRanked.scanFinal w).depth ≥ 2⊢ true = (true && decide (2 ≤ (binRanked.scanFinal w).depth)) All goals completed! 🐙

A leaf bit raises the pending count by one, the scan being live before it.

theorem depth_cons_false_of_ok (w : List Bool) (h : ok w = true) : depth (false :: w) = depth w + 1 := w:List Boolh:ok w = true⊢ depth (false :: w) = depth w + 1 All goals completed! 🐙

A node bit pops two pending subterms and pushes one, the scan being live before it and two subterms pending.

theorem depth_cons_true_of_ok_of_two_le_depth (w : List Bool) (h : ok w = true) (h2 : 2 ≤ depth w) : depth (true :: w) = depth w - 1 := w:List Boolh:ok w = trueh2:2 ≤ depth w⊢ depth (true :: w) = depth w - 1 w:List Boolh:ok w = trueh2:2 ≤ (binRanked.scanFinal w).depth⊢ (binRanked.scanFinal (true :: w)).depth = (binRanked.scanFinal w).depth - 1 w:List Boolh:ok w = trueh2:2 ≤ (binRanked.scanFinal w).depth⊢ { buf := [], depth := (binRanked.scanFinal w).depth - 2 + 1, live := true }.depth = (binRanked.scanFinal w).depth - 1 w:List Boolh:ok w = trueh2:2 ≤ (binRanked.scanFinal w).depth⊢ (binRanked.scanFinal w).depth - 2 + 1 = (binRanked.scanFinal w).depth - 1 All goals completed! 🐙
endend RankedAlphabet.Binary