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.CobhamFoldProto.Initial
public import Geb.Mathlib.Data.W.BasicThe term algebra's destructor in the fold's language
The inverse of the initial algebra's structure map, as expressions of
Cobham's class, at the representation RankedAlphabet.spell fixes.
codeOf and dropCodeOf read a word's leading block and what follows it,
through a constant unary prefix that makes the word a self-delimiting entry
whose payload is that block, so no dispatch over the block is needed.
algPara is the paramorphism as a fold, at a carrier pairing a subterm's
spelling with the step's value, the value delimited so the two are separable.
The delimiting does not nest: each level reads only the spelling half of a
child's value, so a subterm's boundary is reached by a fold rather than at
the cost a nested encoding would carry. WType.para already exists, so no
recursion scheme is introduced here; algPara is the encoding at which it is
computed, and algPara_eq_para identifies the two.
Under the preorder encoding the structure map is the identity on
representations, RankedAlphabet.spell_mk stating that a symbol's block
followed by its children's spellings is the spelling of the term they build.
The content of the inverse laws is therefore that a valid word determines the
symbol and the children's spellings.
Main definitions
Geb.CobhamFold.codeOf, Geb.CobhamFold.dropCodeOf — the block reader and
its complement.
Geb.CobhamFold.ParaStep, Geb.CobhamFold.algPara — the paramorphism's
step, and the paramorphism as a fold.
Geb.CobhamFold.algCh — the delimited-children algebra, one instance of
the paramorphism.
Geb.CobhamFold.chGrowth — the per-symbol growth the delimited-children
algebra meets under its own invariant.
Geb.CobhamFold.algChOf — that algebra as an expression of the class.
Geb.CobhamFold.chFoldOf — the delimited-children fold as an expression.
Geb.CobhamFold.childSem, Geb.CobhamFold.childOf — a child's spelling,
read from a fold's value and read by an expression.
Main statements
Geb.CobhamFold.stepWord_codeOf, Geb.CobhamFold.stepWord_dropCodeOf —
what those two compute at an arbitrary word.
Geb.CobhamFold.stepWord_codeOf_spell_mk,
Geb.CobhamFold.stepWord_dropCodeOf_spell_mk — what they recover from a
spelling.
Geb.CobhamFold.dropEntry_algPara — the value's second half is the
spelling, whatever the step.
Geb.CobhamFold.takeEntry_algPara — the paramorphism's defining equation.
Geb.CobhamFold.algPara_eq_para — it is WType.para at the step that sees
each child's spelling in place of the subtree.
Geb.CobhamFold.sum_ofFn_length_eq_length_flatten,
Geb.CobhamFold.growth_algPara — a family's total length, and the
per-symbol growth a bounded step gives.
Geb.CobhamFold.dropEntry_algCh, Geb.CobhamFold.takeEntry_algCh — the
paramorphism's two laws at Geb.CobhamFold.algCh.
Geb.CobhamFold.length_algCh,
Geb.CobhamFold.five_mul_length_dropEntrySem_algCh_le — its length at
arbitrary arguments, and the bound its outputs satisfy.
Geb.CobhamFold.growth_algCh_of_dropEntrySem_le,
Geb.CobhamFold.stackSize_algCh_le — the per-symbol growth condition at
Geb.CobhamFold.algCh, and the linearity hypothesis it discharges.
Geb.CobhamFold.length_fold_algCh_le — that fold's value at a term is
linear in the term, the linearity in the input word read at a spelling.
Geb.CobhamFold.semAt_algChOf, Geb.CobhamFold.smashFreeBool_algChOf —
what Geb.CobhamFold.algChOf computes, and that it carries no smash.
Geb.CobhamFold.takeEntrySem_cons_true — the presence marker is absorbed
into the entry's unary prefix, so one further bit is read from what follows
the entry.
Geb.CobhamFold.fold_algCh_mk — the fold's value at a constructed term.
Geb.CobhamFold.childSem_mk, Geb.CobhamFold.childSem_of_le,
Geb.CobhamFold.stepWord_childOf,
Geb.CobhamFold.stepWord_childOf_of_le — the child reader recovers a
child's spelling and is total.
Geb.CobhamFold.smashFreeBool_chFoldOf,
Geb.CobhamFold.smashFreeBool_childOf — the fold and the child reader
carry no smash, which is what Cobham.SmashFree names.
Geb.CobhamFold.toSigma_mk — the term algebra's destructor at the
RankedAlphabet.Term.mk presentation.
Geb.CobhamFold.semAt_mkOf_spell — the constructor's expression at the
children's spellings is the spelling of the term they build.
Geb.CobhamFold.semAt_mkOf_childOf — the constructor at the children the
destructor reads returns the word.
Implementation notes
algCh does not meet the per-symbol growth condition
Geb.CobhamFold.stackSize_le_of_growth consumes, and not because
dropEntrySem fails to shrink — length_dropEntrySem_le bounds its result
by its argument. It duplicates its children's payloads, delimited and plain,
so its length is bounded by a multiple of the children's total rather than by
that total plus a constant. A multiplicative condition alone would not give
the linearity hypothesis either, a fold whose values multiply at every level
being exponential in depth. The route taken instead is
five_mul_length_dropEntrySem_algCh_le, a property of the algebra's own
outputs that needs no induction hypothesis,
carried along the scan by mem_stack_foldScanFinal and consumed by a
potential argument in the shape
Geb.CobhamFold.potential_foldScanStep_le_of_invariant's.
Variable.lean states the potential chain at a growth condition restricted
to values satisfying a predicate the scan's stack carries, and derives the
unrestricted forms from it at the trivial predicate. The restriction is what
algCh needs and what the unrestricted condition does not give.
Geb.CobhamFold.foldOutExprV's readout emits Geb.CobhamFold.outWordV,
which prefixes a presence marker. The marker is absorbed into the entry's
unary prefix rather than left beside it, so one further bit is read from what
follows the entry. Each equation is therefore stated in the "entries followed
by an arbitrary remainder" form, which takeEntrySem at an entryWord
tolerates, and the case past the last child is proved against that extra bit
rather than in its absence.
References
[Cobham1965]
[Meertens1992]
[Strahm2003]
Tags
Cobham, ranked tree, destructor, self-delimiting, subterm, paramorphism, smash-free
@[expose] public sectionnamespace Geb.CobhamFoldopen Cobham RankedAlphabetThe leading block of a word, as an expression of arity one: a constant unary prefix of the alphabet's width makes the word a self-delimiting entry whose payload is that block.
def codeOf (R : RankedAlphabet) : COf 1 :=
comp1Of takeEntryOf (prependOf (List.replicate R.width true ++ [false]) idOf)The word past its leading block, by the same prefix.
def dropCodeOf (R : RankedAlphabet) : COf 1 :=
comp1Of dropEntryOf (prependOf (List.replicate R.width true ++ [false]) idOf)The prefixed word, in the shape the payload primitives read.
private theorem stepWord_prefix (R : RankedAlphabet) (w : List Bool) :
stepWord (prependOf (List.replicate R.width true ++ [false]) idOf) w =
List.replicate R.width true ++ false :: w := R:RankedAlphabetw:List Bool⊢ stepWord (prependOf (List.replicate R.width true ++ [false]) idOf) w = List.replicate R.width true ++ false :: w
R:RankedAlphabetw:List Bool⊢ List.replicate R.width true ++ ([false] ++ w) = List.replicate R.width true ++ false :: w
All goals completed! 🐙The block reader truncates to the alphabet's width.
theorem stepWord_codeOf (R : RankedAlphabet) (w : List Bool) :
stepWord (codeOf R) w = w.take R.width := R:RankedAlphabetw:List Bool⊢ stepWord (codeOf R) w = List.take R.width w
All goals completed! 🐙Its complement drops the alphabet's width.
theorem stepWord_dropCodeOf (R : RankedAlphabet) (w : List Bool) :
stepWord (dropCodeOf R) w = w.drop R.width := R:RankedAlphabetw:List Bool⊢ stepWord (dropCodeOf R) w = List.drop R.width w
All goals completed! 🐙At a spelling the block reader recovers the head symbol's block.
theorem stepWord_codeOf_spell_mk (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) :
stepWord (codeOf R) (R.spell (Term.mk R i ch)) = R.code i := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Term⊢ stepWord (codeOf R) (R.spell (Term.mk R i ch)) = R.code i
All goals completed! 🐙And its complement recovers the children's spellings.
theorem stepWord_dropCodeOf_spell_mk (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) :
stepWord (dropCodeOf R) (R.spell (Term.mk R i ch)) =
(List.ofFn fun d ↦ R.spell (ch d)).flatten := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Term⊢ stepWord (dropCodeOf R) (R.spell (Term.mk R i ch)) = (List.ofFn fun d ↦ R.spell (ch d)).flatten
All goals completed! 🐙
A paramorphism's step: it receives each child's spelling beside its value.
Distinct from WType.paraStep, which pairs a subtree with its value; here the
subtree is replaced by its spelling, so the step is a function on
bitstrings.
abbrev ParaStep (R : RankedAlphabet) :=
(i : Fin R.card) → (Fin (R.arity i) → List Bool × List Bool) → List BoolThe paramorphism as a fold, at a carrier pairing a subterm's spelling with its value, the value delimited so the two are separable.
def algPara (R : RankedAlphabet) (phi : ParaStep R) (i : Fin R.card)
(f : Fin (R.arity i) → List Bool) : List Bool :=
entryWord (phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])) ++
algMk R i fun d ↦ dropEntrySem ![f d]The value's second half is the spelling, whatever the step, so the delimiting does not nest: each level reads only this half of a child's value.
theorem dropEntry_algPara (R : RankedAlphabet) (phi : ParaStep R) (t : R.Term) :
dropEntrySem ![Term.fold R (algPara R phi) t] = R.spell t :=
Term.induction (motive := fun t ↦
dropEntrySem ![Term.fold R (algPara R phi) t] = R.spell t)
(fun i ch ih ↦ R:RankedAlphabetphi:ParaStep Rt:R.Termi:Fin R.cardch:Fin (R.arity i) → R.Termih:∀ (d : Fin (R.arity i)), dropEntrySem ![Term.fold R (algPara R phi) (ch d)] = R.spell (ch d)⊢ dropEntrySem ![Term.fold R (algPara R phi) (Term.mk R i ch)] = R.spell (Term.mk R i ch)
R:RankedAlphabetphi:ParaStep Rt:R.Termi:Fin R.cardch:Fin (R.arity i) → R.Termih:∀ (d : Fin (R.arity i)), dropEntrySem ![Term.fold R (algPara R phi) (ch d)] = R.spell (ch d)⊢ (algMk R i fun d ↦ dropEntrySem ![Term.fold R (algPara R phi) (ch d)]) = R.spell (Term.mk R i ch)
All goals completed! 🐙) tThe step is applied to each child's spelling and value, which is the paramorphism's defining equation.
theorem takeEntry_algPara (R : RankedAlphabet) (phi : ParaStep R)
(i : Fin R.card) (ch : Fin (R.arity i) → R.Term) :
takeEntrySem ![Term.fold R (algPara R phi) (Term.mk R i ch)] =
phi i fun d ↦ (R.spell (ch d),
takeEntrySem ![Term.fold R (algPara R phi) (ch d)]) := R:RankedAlphabetphi:ParaStep Ri:Fin R.cardch:Fin (R.arity i) → R.Term⊢ takeEntrySem ![Term.fold R (algPara R phi) (Term.mk R i ch)] =
phi i fun d ↦ (R.spell (ch d), takeEntrySem ![Term.fold R (algPara R phi) (ch d)])
R:RankedAlphabetphi:ParaStep Ri:Fin R.cardch:Fin (R.arity i) → R.Term⊢ (phi i fun d ↦
(dropEntrySem ![Term.fold R (algPara R phi) (ch d)], takeEntrySem ![Term.fold R (algPara R phi) (ch d)])) =
phi i fun d ↦ (R.spell (ch d), takeEntrySem ![Term.fold R (algPara R phi) (ch d)])
All goals completed! 🐙
Read through its take-half, the fold at algPara is WType.para at the
step that sees each child's spelling in place of the subtree: the recursion
scheme is [Meertens1992]'s, computed at the bitstring representation.
theorem algPara_eq_para (R : RankedAlphabet) (phi : ParaStep R) (t : R.Term) :
takeEntrySem ![Term.fold R (algPara R phi) t] =
WType.para (α := Fin R.card) (β := fun i ↦ Fin (R.arity i)) (List Bool)
(fun x ↦ phi x.1 fun d ↦ (R.spell (x.2 d).1, (x.2 d).2)) t :=
Term.induction (motive := fun t ↦
takeEntrySem ![Term.fold R (algPara R phi) t] =
WType.para (α := Fin R.card) (β := fun i ↦ Fin (R.arity i)) (List Bool)
(fun x ↦ phi x.1 fun d ↦ (R.spell (x.2 d).1, (x.2 d).2)) t)
(fun i ch ih ↦ R:RankedAlphabetphi:ParaStep Rt:R.Termi:Fin R.cardch:Fin (R.arity i) → R.Termih:∀ (d : Fin (R.arity i)),
takeEntrySem ![Term.fold R (algPara R phi) (ch d)] =
WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (ch d)⊢ takeEntrySem ![Term.fold R (algPara R phi) (Term.mk R i ch)] =
WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (Term.mk R i ch)
R:RankedAlphabetphi:ParaStep Rt:R.Termi:Fin R.cardch:Fin (R.arity i) → R.Termih:∀ (d : Fin (R.arity i)),
takeEntrySem ![Term.fold R (algPara R phi) (ch d)] =
WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (ch d)h:WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (WType.mk i ch) =
phi
⟨i, fun b ↦
(ch b, WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (ch b))⟩.fst
fun d ↦
(R.spell
(⟨i, fun b ↦
(ch b,
WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (ch b))⟩.snd
d).1,
(⟨i, fun b ↦
(ch b, WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (ch b))⟩.snd
d).2)⊢ takeEntrySem ![Term.fold R (algPara R phi) (Term.mk R i ch)] =
WType.para (List Bool) (fun x ↦ phi x.fst fun d ↦ (R.spell (x.snd d).1, (x.snd d).2)) (Term.mk R i ch)
All goals completed! 🐙) tA family's lengths sum to the length of its flattening.
theorem sum_ofFn_length_eq_length_flatten {n : ℕ} (g : Fin n → List Bool) :
(List.ofFn fun d ↦ (g d).length).sum = ((List.ofFn g).flatten).length := n:ℕg:Fin n → List Bool⊢ (List.ofFn fun d ↦ (g d).length).sum = (List.ofFn g).flatten.length
n:ℕg:Fin n → List Bool⊢ (List.ofFn fun d ↦ (g d).length).sum = (List.ofFn (List.length ∘ g)).sum
All goals completed! 🐙The weighted length bound, over a list rather than a family: the payloads counted twice and the remainders together fit inside the words.
private theorem two_mul_length_flatten_take_add_drop_le : ∀ l : List (List Bool),
2 * ((l.map fun x ↦ takeEntrySem ![x]).flatten).length +
((l.map fun x ↦ dropEntrySem ![x]).flatten).length ≤ l.flatten.length :=
List.rec (Nat.le_refl 0) fun a t ih ↦ a:List Boolt:List (List Bool)ih:2 * (List.map (fun x ↦ takeEntrySem ![x]) t).flatten.length + (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length ≤
t.flatten.length⊢ 2 * (List.map (fun x ↦ takeEntrySem ![x]) (a :: t)).flatten.length +
(List.map (fun x ↦ dropEntrySem ![x]) (a :: t)).flatten.length ≤
(a :: t).flatten.length
a:List Boolt:List (List Bool)ih:2 * (List.map (fun x ↦ takeEntrySem ![x]) t).flatten.length + (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length ≤
t.flatten.lengthh:2 * (takeEntrySem ![a]).length + (dropEntrySem ![a]).length ≤ a.length⊢ 2 * (List.map (fun x ↦ takeEntrySem ![x]) (a :: t)).flatten.length +
(List.map (fun x ↦ dropEntrySem ![x]) (a :: t)).flatten.length ≤
(a :: t).flatten.length
a:List Boolt:List (List Bool)ih:2 * (List.map (fun x ↦ takeEntrySem ![x]) t).flatten.length + (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length ≤
t.flatten.lengthh:2 * (takeEntrySem ![a]).length + (dropEntrySem ![a]).length ≤ a.length⊢ 2 * ((takeEntrySem ![a]).length + (List.map (fun x ↦ takeEntrySem ![x]) t).flatten.length) +
((dropEntrySem ![a]).length + (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length) ≤
a.length + t.flatten.length
All goals completed! 🐙
A paramorphism whose step is bounded by its children's values, plus a
constant, meets the per-symbol growth condition at 2 * cphi + R.width + 1,
attained at a nullary symbol. The constant is unconditional because the
weighted bound holds at an arbitrary word rather than only at a fold's
value.
theorem growth_algPara (R : RankedAlphabet) (phi : ParaStep R) (cphi : ℕ)
(hphi : ∀ (i : Fin R.card) (g : Fin (R.arity i) → List Bool × List Bool),
(phi i g).length ≤ (List.ofFn fun d ↦ (g d).2.length).sum + cphi)
(i : Fin R.card) (f : Fin (R.arity i) → List Bool) :
(algPara R phi i f).length ≤
(List.ofFn fun d ↦ (f d).length).sum + (2 * cphi + R.width + 1) := R:RankedAlphabetphi:ParaStep Rcphi:ℕhphi:∀ (i : Fin R.card) (g : Fin (R.arity i) → List Bool × List Bool),
(phi i g).length ≤ (List.ofFn fun d ↦ (g d).2.length).sum + cphii:Fin R.cardf:Fin (R.arity i) → List Bool⊢ (algPara R phi i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + (2 * cphi + R.width + 1)
R:RankedAlphabetphi:ParaStep Rcphi:ℕhphi:∀ (i : Fin R.card) (g : Fin (R.arity i) → List Bool × List Bool),
(phi i g).length ≤ (List.ofFn fun d ↦ (g d).2.length).sum + cphii:Fin R.cardf:Fin (R.arity i) → List Boolhstep:(phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])).length ≤
(List.ofFn fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d]).2.length).sum + cphi⊢ (algPara R phi i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + (2 * cphi + R.width + 1)
R:RankedAlphabetphi:ParaStep Rcphi:ℕhphi:∀ (i : Fin R.card) (g : Fin (R.arity i) → List Bool × List Bool),
(phi i g).length ≤ (List.ofFn fun d ↦ (g d).2.length).sum + cphii:Fin R.cardf:Fin (R.arity i) → List Boolhstep:(phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])).length ≤
(List.ofFn fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d]).2.length).sum + cphihw:2 * (List.map (fun x ↦ takeEntrySem ![x]) (List.ofFn f)).flatten.length +
(List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length ≤
(List.ofFn f).flatten.length⊢ (algPara R phi i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + (2 * cphi + R.width + 1)
R:RankedAlphabetphi:ParaStep Rcphi:ℕhphi:∀ (i : Fin R.card) (g : Fin (R.arity i) → List Bool × List Bool),
(phi i g).length ≤ (List.ofFn fun d ↦ (g d).2.length).sum + cphii:Fin R.cardf:Fin (R.arity i) → List Boolhstep:(phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])).length ≤
(List.ofFn fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d]).2.length).sum + cphihw:2 * (List.map (fun x ↦ takeEntrySem ![x]) (List.ofFn f)).flatten.length +
(List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length ≤
(List.ofFn f).flatten.length⊢ 2 * (phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])).length + 1 +
((List.ofFn fun d ↦ (dropEntrySem ![f d]).length).sum + R.width) ≤
(List.ofFn fun d ↦ (f d).length).sum + (2 * cphi + R.width + 1)
R:RankedAlphabetphi:ParaStep Rcphi:ℕhphi:∀ (i : Fin R.card) (g : Fin (R.arity i) → List Bool × List Bool),
(phi i g).length ≤ (List.ofFn fun d ↦ (g d).2.length).sum + cphii:Fin R.cardf:Fin (R.arity i) → List Boolhstep:(phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])).length ≤
(List.ofFn fun d ↦ takeEntrySem ![f d]).flatten.length + cphihw:2 * (List.ofFn fun x ↦ takeEntrySem ![f x]).flatten.length + (List.ofFn fun x ↦ dropEntrySem ![f x]).flatten.length ≤
(List.ofFn f).flatten.length⊢ 2 * (phi i fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])).length + 1 +
((List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + R.width) ≤
(List.ofFn f).flatten.length + (2 * cphi + R.width + 1)
All goals completed! 🐙The delimited-children algebra: the paramorphism whose step returns its children's spellings, each delimited.
def algCh (R : RankedAlphabet) : (i : Fin R.card) →
(Fin (R.arity i) → List Bool) → List Bool :=
algPara R fun _ g ↦ (List.ofFn fun d ↦ entryWord (g d).1).flattenIts value's second half is the spelling.
theorem dropEntry_algCh (R : RankedAlphabet) (t : R.Term) :
dropEntrySem ![Term.fold R (algCh R) t] = R.spell t :=
dropEntry_algPara R _ t
Its first half is the children's spellings, each delimited, so the j-th
child is Geb.CobhamFold.entryOf j of it.
theorem takeEntry_algCh (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) :
takeEntrySem ![Term.fold R (algCh R) (Term.mk R i ch)] =
(List.ofFn fun d ↦ entryWord (R.spell (ch d))).flatten :=
takeEntry_algPara R _ i chA family's delimited spelling is the stack layout at the list it names.
theorem stackWordV_ofFn {n : ℕ} (g : Fin n → List Bool) :
stackWordV (List.ofFn g) = (List.ofFn fun d ↦ entryWord (g d)).flatten := n:ℕg:Fin n → List Bool⊢ stackWordV (List.ofFn g) = (List.ofFn fun d ↦ entryWord (g d)).flatten
n:ℕg:Fin n → List Bool⊢ (List.ofFn (entryWord ∘ g)).flatten = (List.ofFn fun d ↦ entryWord (g d)).flatten
All goals completed! 🐙The value's second half is the symbol's block followed by the children's own second halves, whatever the arguments.
theorem dropEntrySem_algCh (R : RankedAlphabet) (i : Fin R.card)
(f : Fin (R.arity i) → List Bool) :
dropEntrySem ![algCh R i f] =
R.code i ++ (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten := R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Bool⊢ dropEntrySem ![algCh R i f] = R.code i ++ (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten
All goals completed! 🐙Its length, at arbitrary arguments: five times the children's second halves, two bits per child, the sentinel and the block.
theorem length_algCh (R : RankedAlphabet) (i : Fin R.card)
(f : Fin (R.arity i) → List Bool) :
(algCh R i f).length =
5 * ((List.ofFn fun d ↦ dropEntrySem ![f d]).flatten).length +
2 * R.arity i + 1 + R.width := R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Bool⊢ (algCh R i f).length = 5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhlen:(stackWordV (List.ofFn fun d ↦ dropEntrySem ![f d])).length =
2 * stackSize (List.ofFn fun d ↦ dropEntrySem ![f d]) + (List.ofFn fun d ↦ dropEntrySem ![f d]).length⊢ (algCh R i f).length = 5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhlen:(List.ofFn fun d ↦ entryWord (dropEntrySem ![f d])).flatten.length =
2 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + (List.ofFn fun d ↦ dropEntrySem ![f d]).length⊢ (algCh R i f).length = 5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhlen:(List.ofFn fun d ↦ entryWord (dropEntrySem ![f d])).flatten.length =
2 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + (List.ofFn fun d ↦ dropEntrySem ![f d]).length⊢ 2 * (List.ofFn fun d ↦ entryWord ((fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])) d).1).flatten.length + 1 +
((List.ofFn fun d ↦ (dropEntrySem ![f d]).length).sum + R.width) =
5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhlen:(List.ofFn fun d ↦ entryWord (dropEntrySem ![f d])).flatten.length =
2 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + R.arity i⊢ 2 * (List.ofFn fun d ↦ entryWord (dropEntrySem ![f d])).flatten.length + 1 +
((List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + R.width) =
5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width
All goals completed! 🐙
Every value the delimited-children algebra produces carries its second
half within a fixed multiple of its own length. It needs no induction
hypothesis, holding at arbitrary arguments, and holds with equality at a
nullary symbol. This is what a potential argument runs over where the
per-symbol growth condition fails: algCh duplicates its children's
payloads, delimited and plain, so |algCh R i f| is bounded by a multiple of
the children's total rather than by that total plus a constant.
theorem five_mul_length_dropEntrySem_algCh_le (R : RankedAlphabet) (i : Fin R.card)
(f : Fin (R.arity i) → List Bool) :
5 * (dropEntrySem ![algCh R i f]).length + 1 ≤
(algCh R i f).length + 4 * R.width := R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Bool⊢ 5 * (dropEntrySem ![algCh R i f]).length + 1 ≤ (algCh R i f).length + 4 * R.width
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Bool⊢ 5 * (R.width + (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length) + 1 ≤
5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width + 4 * R.width
All goals completed! 🐙The per-symbol growth the delimited-children algebra meets under its own invariant, attained at a symbol of maximum arity whose children are all nullary.
def chGrowth (R : RankedAlphabet) : ℕ :=
4 * R.maxArity * R.width + R.maxArity + R.width + 1The children's second halves, bounded by their own lengths under the invariant, over a list rather than a family.
private theorem five_mul_length_flatten_dropEntrySem_le (R : RankedAlphabet) :
∀ l : List (List Bool),
(∀ x ∈ l, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width) →
5 * ((l.map fun x ↦ dropEntrySem ![x]).flatten).length + l.length ≤
l.flatten.length + 4 * R.width * l.length :=
List.rec (fun _ ↦ Nat.le_refl 0) fun a t ih h ↦ R:RankedAlphabeta:List Boolt:List (List Bool)ih:(∀ x ∈ t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width) →
5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthh:∀ x ∈ a :: t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width⊢ 5 * (List.map (fun x ↦ dropEntrySem ![x]) (a :: t)).flatten.length + (a :: t).length ≤
(a :: t).flatten.length + 4 * R.width * (a :: t).length
R:RankedAlphabeta:List Boolt:List (List Bool)ih:(∀ x ∈ t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width) →
5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthh:∀ x ∈ a :: t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.widthha:5 * (dropEntrySem ![a]).length + 1 ≤ a.length + 4 * R.width⊢ 5 * (List.map (fun x ↦ dropEntrySem ![x]) (a :: t)).flatten.length + (a :: t).length ≤
(a :: t).flatten.length + 4 * R.width * (a :: t).length
R:RankedAlphabeta:List Boolt:List (List Bool)ih:(∀ x ∈ t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width) →
5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthh:∀ x ∈ a :: t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.widthha:5 * (dropEntrySem ![a]).length + 1 ≤ a.length + 4 * R.widthht:5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.length⊢ 5 * (List.map (fun x ↦ dropEntrySem ![x]) (a :: t)).flatten.length + (a :: t).length ≤
(a :: t).flatten.length + 4 * R.width * (a :: t).length
-- `omega` atomises `4 * R.width * (t.length + 1)` and
-- `4 * R.width * t.length` separately, so the step is supplied by hand.
R:RankedAlphabeta:List Boolt:List (List Bool)ih:(∀ x ∈ t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width) →
5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthh:∀ x ∈ a :: t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.widthha:5 * (dropEntrySem ![a]).length + 1 ≤ a.length + 4 * R.widthht:5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthhd:4 * R.width * (t.length + 1) = 4 * R.width * t.length + 4 * R.width⊢ 5 * (List.map (fun x ↦ dropEntrySem ![x]) (a :: t)).flatten.length + (a :: t).length ≤
(a :: t).flatten.length + 4 * R.width * (a :: t).length
R:RankedAlphabeta:List Boolt:List (List Bool)ih:(∀ x ∈ t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.width) →
5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthh:∀ x ∈ a :: t, 5 * (dropEntrySem ![x]).length + 1 ≤ x.length + 4 * R.widthha:5 * (dropEntrySem ![a]).length + 1 ≤ a.length + 4 * R.widthht:5 * (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length + t.length ≤ t.flatten.length + 4 * R.width * t.lengthhd:4 * R.width * (t.length + 1) = 4 * R.width * t.length + 4 * R.width⊢ 5 * ((dropEntrySem ![a]).length + (List.map (fun x ↦ dropEntrySem ![x]) t).flatten.length) + (t.length + 1) ≤
a.length + t.flatten.length + 4 * R.width * (t.length + 1)
All goals completed! 🐙
The delimited-children algebra lengthens by at most chGrowth R per
symbol, at arguments satisfying the invariant its own outputs satisfy. It
does not meet the condition at arbitrary arguments: it duplicates its
children's payloads, delimited and plain.
theorem growth_algCh_of_dropEntrySem_le (R : RankedAlphabet) (i : Fin R.card)
(f : Fin (R.arity i) → List Bool)
(hf : ∀ d, 5 * (dropEntrySem ![f d]).length + 1 ≤
(f d).length + 4 * R.width) :
(algCh R i f).length ≤
(List.ofFn fun d ↦ (f d).length).sum + chGrowth R := R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.width⊢ (algCh R i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + chGrowth R
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.widthhlist:5 * (List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length + (List.ofFn f).length ≤
(List.ofFn f).flatten.length + 4 * R.width * (List.ofFn f).length⊢ (algCh R i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + chGrowth R
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.widthhlist:5 * (List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length + (List.ofFn f).length ≤
(List.ofFn f).flatten.length + 4 * R.width * (List.ofFn f).lengthharity:R.arity i ≤ R.maxArity⊢ (algCh R i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + chGrowth R
-- `omega` is linear: it atomises `4 * R.width * R.arity i` and
-- `4 * R.maxArity * R.width` separately and has no rule taking
-- `R.arity i ≤ R.maxArity` from one to the other, so the monotonicity and
-- the commutation are supplied by hand.
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.widthhlist:5 * (List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length + (List.ofFn f).length ≤
(List.ofFn f).flatten.length + 4 * R.width * (List.ofFn f).lengthharity:R.arity i ≤ R.maxArityhmono:4 * R.width * R.arity i ≤ 4 * R.width * R.maxArity⊢ (algCh R i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + chGrowth R
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.widthhlist:5 * (List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length + (List.ofFn f).length ≤
(List.ofFn f).flatten.length + 4 * R.width * (List.ofFn f).lengthharity:R.arity i ≤ R.maxArityhmono:4 * R.width * R.arity i ≤ 4 * R.width * R.maxArityhcomm:4 * R.width * R.maxArity = 4 * R.maxArity * R.width⊢ (algCh R i f).length ≤ (List.ofFn fun d ↦ (f d).length).sum + chGrowth R
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.widthhlist:5 * (List.map (fun x ↦ dropEntrySem ![x]) (List.ofFn f)).flatten.length + (List.ofFn f).length ≤
(List.ofFn f).flatten.length + 4 * R.width * (List.ofFn f).lengthharity:R.arity i ≤ R.maxArityhmono:4 * R.width * R.arity i ≤ 4 * R.width * R.maxArityhcomm:4 * R.width * R.maxArity = 4 * R.maxArity * R.width⊢ 5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width ≤
(List.ofFn f).flatten.length + (4 * R.maxArity * R.width + R.maxArity + R.width + 1)
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Boolhf:∀ (d : Fin (R.arity i)), 5 * (dropEntrySem ![f d]).length + 1 ≤ (f d).length + 4 * R.widthharity:R.arity i ≤ R.maxArityhmono:4 * R.width * R.arity i ≤ 4 * R.width * R.maxArityhcomm:4 * R.width * R.maxArity = 4 * R.maxArity * R.widthhlist:5 * (List.ofFn fun x ↦ dropEntrySem ![f x]).flatten.length + R.arity i ≤
(List.ofFn f).flatten.length + 4 * R.width * R.arity i⊢ 5 * (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten.length + 2 * R.arity i + 1 + R.width ≤
(List.ofFn f).flatten.length + (4 * R.maxArity * R.width + R.maxArity + R.width + 1)
All goals completed! 🐙
The pending values stay linear in the input at the delimited-children
algebra, which is the hypothesis Geb.CobhamFold.foldOutOfV takes. The
per-symbol growth condition does not apply, so the bound runs through the
invariant five_mul_length_dropEntrySem_algCh_le and a potential argument
over it, which charges each input bit at most chGrowth R and so needs no
assumption about how the pending subterms are laid out.
theorem stackSize_algCh_le (R : RankedAlphabet) (w : List Bool) :
stackSize (foldScanFinal R (algCh R) w).stack ≤ chGrowth R * w.length :=
stackSize_le_of_growth_of_invariant R (algCh R)
(fun v ↦ 5 * (dropEntrySem ![v]).length + 1 ≤ v.length + 4 * R.width)
(chGrowth R) (five_mul_length_dropEntrySem_algCh_le R) (growth_algCh_of_dropEntrySem_le R) w
A subterm's value is linear in that subterm, and not only in the word the
scan reads: at a spelling the scan ends with that value alone pending, so
stackSize_algCh_le there bounds the value itself, and
RankedAlphabet.length_spell turns the word's length into the subterm's node
count.
theorem length_fold_algCh_le (R : RankedAlphabet) (t : R.Term) :
(Term.fold R (algCh R) t).length ≤ chGrowth R * (R.width * t.size) := R:RankedAlphabett:R.Term⊢ (Term.fold R (algCh R) t).length ≤ chGrowth R * (R.width * t.size)
R:RankedAlphabett:R.Termh:stackSize (foldScanFinal R (algCh R) (R.spell t)).stack ≤ chGrowth R * (R.spell t).length⊢ (Term.fold R (algCh R) t).length ≤ chGrowth R * (R.width * t.size)
R:RankedAlphabett:R.Termh:stackSize { buf := [], stack := [Term.fold R (algCh R) t], live := true }.stack ≤ chGrowth R * (R.width * t.size)⊢ (Term.fold R (algCh R) t).length ≤ chGrowth R * (R.width * t.size)
R:RankedAlphabett:R.Termh:(Term.fold R (algCh R) t).length + 0 ≤ chGrowth R * (R.width * t.size)⊢ (Term.fold R (algCh R) t).length ≤ chGrowth R * (R.width * t.size)
All goals completed! 🐙
The delimited-children algebra as an expression of Cobham's class. Each
slot contributes its own second half, plain in the first argument and
delimited in the second; Geb.CobhamFold.flattenOf concatenates a family
through Geb.CobhamFold.compOf, so no new combinator is introduced.
def algChOf (R : RankedAlphabet) (i : Fin R.card) : COf (R.arity i) :=
concatCompOf (R.arity i)
(prependOf (R.code i)
(compOf (flattenOf (R.arity i)) fun d ↦
comp1Of dropEntryOf (projOf (R.arity i) d)))
(comp1Of entryWordOf
(compOf (flattenOf (R.arity i)) fun d ↦
comp1Of entryWordOf (comp1Of dropEntryOf (projOf (R.arity i) d))))The expression computes the algebra.
theorem semAt_algChOf (R : RankedAlphabet) (i : Fin R.card)
(f : Fin (R.arity i) → List Bool) :
semAt (R.arity i) (algChOf R i).1.1 (algChOf R i).2 f = algCh R i f := R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Bool⊢ semAt (R.arity i) ↑↑(algChOf R i) ⋯ f = algCh R i f
R:RankedAlphabeti:Fin R.cardf:Fin (R.arity i) → List Bool⊢ stepWord entryWordOf
(List.ofFn fun i_1 ↦
semAt (R.arity i) ↑↑(comp1Of entryWordOf (comp1Of dropEntryOf (projOf (R.arity i) i_1))) ⋯ f).flatten ++
(R.code i ++ (List.ofFn fun i_1 ↦ semAt (R.arity i) ↑↑(comp1Of dropEntryOf (projOf (R.arity i) i_1)) ⋯ f).flatten) =
entryWord (List.ofFn fun d ↦ entryWord ((fun d ↦ (dropEntrySem ![f d], takeEntrySem ![f d])) d).1).flatten ++
(R.code i ++ (List.ofFn fun d ↦ dropEntrySem ![f d]).flatten)
All goals completed! 🐙
The expression carries no smash, which is
Geb.CobhamFold.smashFree_foldOutExprV's hypothesis at this algebra.
theorem smashFreeBool_algChOf (R : RankedAlphabet) (i : Fin R.card) :
smashFreeBool (algChOf R i).1.1.1 = true :=
smashFreeBool_concatCompOf (R.arity i) _ _
(smashFreeBool_prependOf _ _
(smashFreeBool_compOf _ _ (smashFreeBool_flattenOf (R.arity i))
fun d ↦ smashFreeBool_comp1Of _ _ smashFreeBool_dropEntryOf
(smashFreeBool_projOf (R.arity i) d)))
(smashFreeBool_comp1Of _ _ smashFreeBool_entryWordOf
(smashFreeBool_compOf _ _ (smashFreeBool_flattenOf (R.arity i))
fun d ↦ smashFreeBool_comp1Of _ _ smashFreeBool_entryWordOf
(smashFreeBool_comp1Of _ _ smashFreeBool_dropEntryOf
(smashFreeBool_projOf (R.arity i) d))))
Splitting a truncation one bit past a prefix.
Geb.CobhamFold.take_succ_append_take_one is the same split at an arbitrary
index. Neither reaches for List.take_add, which SelfDelim.lean records as
Classical.choice-dependent.
private theorem take_append_length_add_one (u rest : List Bool) :
(u ++ rest).take (u.length + 1) = u ++ rest.take 1 := u:List Boolrest:List Bool⊢ List.take (u.length + 1) (u ++ rest) = u ++ List.take 1 rest
All goals completed! 🐙The presence marker is absorbed into the entry's unary prefix rather than left beside it, so the payload read from a marked value is the value's own payload followed by one further bit of what the entry leaves.
theorem takeEntrySem_cons_true (u rest : List Bool) :
takeEntrySem ![true :: (entryWord u ++ rest)] = u ++ rest.take 1 := u:List Boolrest:List Bool⊢ takeEntrySem ![true :: (entryWord u ++ rest)] = u ++ List.take 1 rest
u:List Boolrest:List Boolhshape:true :: (entryWord u ++ rest) = List.replicate (u.length + 1) true ++ false :: (u ++ rest)⊢ takeEntrySem ![true :: (entryWord u ++ rest)] = u ++ List.take 1 rest
All goals completed! 🐙The payload primitive reads nothing from a word of at most one bit.
theorem takeEntrySem_of_length_le_one : ∀ r : List Bool, r.length ≤ 1 →
takeEntrySem ![r] = []
| [], _ => takeEntrySem_nil
b:Boolt:List Boolh:(b :: t).length ≤ 1⊢ takeEntrySem ![b :: t] = [] b:Boolt:List Boolh:(b :: t).length ≤ 1⊢ takeEntrySem ![b :: t] = []
b:Boolt:List Boolh:(b :: t).length ≤ 1ht:t = []⊢ takeEntrySem ![b :: t] = []
b:Boolt:List Boolh:(b :: t).length ≤ 1ht:t = []⊢ (if b = true then takeEntrySem ![[]] ++ firstBitSem ![dropEntrySem ![[]]] else []) = []
t:List Boolht:t = []h:(false :: t).length ≤ 1⊢ (if false = true then takeEntrySem ![[]] ++ firstBitSem ![dropEntrySem ![[]]] else []) = []t:List Boolht:t = []h:(true :: t).length ≤ 1⊢ (if true = true then takeEntrySem ![[]] ++ firstBitSem ![dropEntrySem ![[]]] else []) = []
t:List Boolht:t = []h:(false :: t).length ≤ 1⊢ (if false = true then takeEntrySem ![[]] ++ firstBitSem ![dropEntrySem ![[]]] else []) = [] All goals completed! 🐙
t:List Boolht:t = []h:(true :: t).length ≤ 1⊢ (if true = true then takeEntrySem ![[]] ++ firstBitSem ![dropEntrySem ![[]]] else []) = [] t:List Boolht:t = []h:(true :: t).length ≤ 1⊢ ([] ++
match [] with
| [] => []
| b :: tail => [b]) =
[]
All goals completed! 🐙Dropping entries never lengthens a word.
theorem length_stepWord_dropEntriesOf_le : ∀ (k : ℕ) (r : List Bool),
(stepWord (dropEntriesOf k) r).length ≤ r.length :=
Nat.rec (fun r ↦ r:List Bool⊢ (stepWord (dropEntriesOf Nat.zero) r).length ≤ r.length All goals completed! 🐙)
fun k ih r ↦ k:ℕih:∀ (r : List Bool), (stepWord (dropEntriesOf k) r).length ≤ r.lengthr:List Bool⊢ (stepWord (dropEntriesOf k.succ) r).length ≤ r.length
k:ℕih:∀ (r : List Bool), (stepWord (dropEntriesOf k) r).length ≤ r.lengthr:List Bool⊢ (stepWord (dropEntriesOf k) (dropEntrySem ![r])).length ≤ r.length
All goals completed! 🐙Dropping entries composes.
theorem stepWord_dropEntriesOf_add : ∀ (n k : ℕ) (x : List Bool),
stepWord (dropEntriesOf (n + k)) x =
stepWord (dropEntriesOf k) (stepWord (dropEntriesOf n) x) :=
Nat.rec (fun k x ↦ k:ℕx:List Bool⊢ stepWord (dropEntriesOf (Nat.zero + k)) x = stepWord (dropEntriesOf k) (stepWord (dropEntriesOf Nat.zero) x) All goals completed! 🐙)
fun n ih k x ↦ n:ℕih:∀ (k : ℕ) (x : List Bool),
stepWord (dropEntriesOf (n + k)) x = stepWord (dropEntriesOf k) (stepWord (dropEntriesOf n) x)k:ℕx:List Bool⊢ stepWord (dropEntriesOf (n.succ + k)) x = stepWord (dropEntriesOf k) (stepWord (dropEntriesOf n.succ) x)
All goals completed! 🐙The fold's value at a constructed term, in the shape the entry primitives read: the children's delimited spellings as one entry, then the symbol's block and the children's spellings plain.
theorem fold_algCh_mk (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) :
Term.fold R (algCh R) (Term.mk R i ch) =
entryWord (stackWordV (List.ofFn fun d ↦ R.spell (ch d))) ++
(R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten) := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Term⊢ Term.fold R (algCh R) (Term.mk R i ch) =
entryWord (stackWordV (List.ofFn fun d ↦ R.spell (ch d))) ++ (R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten)
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Term⊢ (entryWord
(List.ofFn fun d ↦
entryWord
((fun d ↦
(dropEntrySem
![Term.fold R (algPara R fun x g ↦ (List.ofFn fun d ↦ entryWord (g d).1).flatten) (ch d)],
takeEntrySem
![Term.fold R (algPara R fun x g ↦ (List.ofFn fun d ↦ entryWord (g d).1).flatten) (ch d)]))
d).1).flatten ++
algMk R i fun d ↦
dropEntrySem ![Term.fold R (algPara R fun x g ↦ (List.ofFn fun d ↦ entryWord (g d).1).flatten) (ch d)]) =
entryWord (List.ofFn fun d ↦ entryWord (R.spell (ch d))).flatten ++
(R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten)
All goals completed! 🐙
The j-th child's spelling, read from a term's fold value.
def childSem (R : RankedAlphabet) (j : ℕ) (t : R.Term) : List Bool :=
stepWord (entryOf j) (takeEntrySem ![Term.fold R (algCh R) t])
It recovers the j-th child's spelling.
theorem childSem_mk (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) (j : ℕ) (h : j < R.arity i) :
childSem R j (Term.mk R i ch) = R.spell (ch ⟨j, h⟩) := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:j < R.arity i⊢ childSem R j (Term.mk R i ch) = R.spell (ch ⟨j, h⟩)
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:j < R.arity i⊢ ((List.ofFn fun d ↦ R.spell (ch d))[j] :: List.drop (j + 1) (List.ofFn fun d ↦ R.spell (ch d))).headD [] =
R.spell (ch ⟨j, h⟩)
All goals completed! 🐙And returns the empty word past the last child, so it is total.
theorem childSem_of_le (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) (j : ℕ) (h : R.arity i ≤ j) :
childSem R j (Term.mk R i ch) = [] := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ j⊢ childSem R j (Term.mk R i ch) = []
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ j⊢ [].headD [] = []
All goals completed! 🐙
The delimited-children fold as an expression, at its declared arity. The
multiplier is foldOutOfV's bound taken with equality, so it carries no
hypothesis of its own.
def chFoldOf (R : RankedAlphabet) : COf 1 :=
foldOutOfV R (algChOf R) (algCh R) (semAt_algChOf R) (2 * chGrowth R + 2)
(chGrowth R) (stackSize_algCh_le R) (Nat.le_refl _)
The j-th child's spelling, as an expression of Cobham's class: the
j-th entry of the fold's payload.
def childOf (R : RankedAlphabet) (j : ℕ) : COf 1 :=
comp1Of (entryOf j) (comp1Of takeEntryOf (chFoldOf R))
The fold expression's value, spelled by Geb.CobhamFold.outWordV.
theorem stepWord_chFoldOf (R : RankedAlphabet) (w : List Bool) :
stepWord (chFoldOf R) w = outWordV (foldOut R (algCh R) w) :=
foldOutSemV_eq R (algChOf R) (algCh R) (semAt_algChOf R)
(2 * chGrowth R + 2) (chGrowth R) (stackSize_algCh_le R) (Nat.le_refl _) w
The j-th child's spelling, recovered from the spelling of the term.
theorem stepWord_childOf (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) (j : ℕ) (h : j < R.arity i) :
stepWord (childOf R j) (R.spell (Term.mk R i ch)) = R.spell (ch ⟨j, h⟩) := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:j < R.arity i⊢ stepWord (childOf R j) (R.spell (Term.mk R i ch)) = R.spell (ch ⟨j, h⟩)
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:j < R.arity ihlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity i⊢ stepWord (childOf R j) (R.spell (Term.mk R i ch)) = R.spell (ch ⟨j, h⟩)
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:j < R.arity ihlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity i⊢ stepWord (entryOf j) (takeEntrySem ![outWordV (some (Term.fold R (algCh R) (Term.mk R i ch)))]) = R.spell (ch ⟨j, h⟩)
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:j < R.arity ihlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity i⊢ stepWord (entryOf j) (takeEntrySem ![true :: Term.fold R (algCh R) (Term.mk R i ch)]) = R.spell (ch ⟨j, h⟩)
All goals completed! 🐙And the empty word past the last child, so the expression is total.
theorem stepWord_childOf_of_le (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) (j : ℕ) (h : R.arity i ≤ j) :
stepWord (childOf R j) (R.spell (Term.mk R i ch)) = [] := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ j⊢ stepWord (childOf R j) (R.spell (Term.mk R i ch)) = []
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ jhlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity i⊢ stepWord (childOf R j) (R.spell (Term.mk R i ch)) = []
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ jhlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity ihshort:(List.take 1 (R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten)).length ≤ 1⊢ stepWord (childOf R j) (R.spell (Term.mk R i ch)) = []
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ jhlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity ihshort:(List.take 1 (R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten)).length ≤ 1⊢ stepWord (entryOf j) (takeEntrySem ![outWordV (some (Term.fold R (algCh R) (Term.mk R i ch)))]) = []
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ jhlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity ihshort:(List.take 1 (R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten)).length ≤ 1⊢ stepWord (entryOf j) (takeEntrySem ![true :: Term.fold R (algCh R) (Term.mk R i ch)]) = []
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termj:ℕh:R.arity i ≤ jhlen:(List.ofFn fun d ↦ R.spell (ch d)).length = R.arity ihshort:(List.take 1 (R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten)).length ≤ 1⊢ takeEntrySem
![stepWord (dropEntriesOf (j - R.arity i)) (List.take 1 (R.code i ++ (List.ofFn fun d ↦ R.spell (ch d)).flatten))] =
[]
All goals completed! 🐙
The delimited-children fold carries no smash, its algebra's own
expressions carrying none.
theorem smashFreeBool_chFoldOf (R : RankedAlphabet) :
smashFreeBool (chFoldOf R).1.1.1 = true :=
smashFree_foldOutExprV R (algChOf R) (smashFreeBool_algChOf R) (algCh R)
(semAt_algChOf R) (2 * chGrowth R + 2) (chGrowth R) (stackSize_algCh_le R)
(Nat.le_refl _)So does the child reader, so with [Strahm2003] Theorem 1(2)'s left-to-right inclusion it is computable simultaneously in polynomial time and linear space.
theorem smashFreeBool_childOf (R : RankedAlphabet) (j : ℕ) :
smashFreeBool (childOf R j).1.1.1 = true :=
smashFreeBool_comp1Of _ _ (smashFreeBool_entryOf j)
(smashFreeBool_comp1Of _ _ smashFreeBool_takeEntryOf
(smashFreeBool_chFoldOf R))
The term algebra's destructor at the RankedAlphabet.Term.mk
presentation. WType.ofSigma_toSigma is the other inverse law, which mathlib
already carries.
theorem toSigma_mk (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) :
WType.toSigma (Term.mk R i ch) = ⟨i, ch⟩ := rfl
The constructor's expression at the children's spellings is the spelling
of the term they build. Under the preorder encoding the structure map is the
identity on representations, which is what RankedAlphabet.spell_mk
states.
theorem semAt_mkOf_spell (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) :
semAt (R.arity i) (mkOf R i).1.1 (mkOf R i).2 (fun d ↦ R.spell (ch d)) =
R.spell (Term.mk R i ch) := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Term⊢ (semAt (R.arity i) ↑↑(mkOf R i) ⋯ fun d ↦ R.spell (ch d)) = R.spell (Term.mk R i ch)
All goals completed! 🐙
The constructor at the children the destructor reads returns the word.
It is stated under R.parse w = some (Term.mk R i ch) with i given rather
than read, so no dispatch over the block is needed; Geb.CobhamFold.childOf
and Geb.CobhamFold.mkOf are total and return an unspecified word off the
recognized language.
theorem semAt_mkOf_childOf (R : RankedAlphabet) (i : Fin R.card)
(ch : Fin (R.arity i) → R.Term) (w : List Bool)
(hw : R.parse w = some (Term.mk R i ch)) :
semAt (R.arity i) (mkOf R i).1.1 (mkOf R i).2
(fun d ↦ stepWord (childOf R d.val) w) = w := R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termw:List Boolhw:R.parse w = some (Term.mk R i ch)⊢ (semAt (R.arity i) ↑↑(mkOf R i) ⋯ fun d ↦ stepWord (childOf R ↑d) w) = w
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termw:List Boolhw:R.parse w = some (Term.mk R i ch)hspell:R.spell (Term.mk R i ch) = w⊢ (semAt (R.arity i) ↑↑(mkOf R i) ⋯ fun d ↦ stepWord (childOf R ↑d) w) = w
R:RankedAlphabeti:Fin R.cardch:Fin (R.arity i) → R.Termw:List Boolhw:R.parse w = some (Term.mk R i ch)hspell:R.spell (Term.mk R i ch) = whchild:(fun d ↦ stepWord (childOf R ↑d) w) = fun d ↦ R.spell (ch d)⊢ (semAt (R.arity i) ↑↑(mkOf R i) ⋯ fun d ↦ stepWord (childOf R ↑d) w) = w
All goals completed! 🐙end Geb.CobhamFoldend