Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `For-transducers are closed under composition`

groundedproofs/Lax194892Proofs/Results.lean · lax-194892

What this proof establishes

no assumptions

thm✓Lax194892.ForComposition

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

Description

Functions computed by for-transducers are closed under composition (Lemma D.1.4), Transducers.forTransducercompTransducers.forTransducer_comp.

Proof strategy

The source simulates the second program on the output of the first: each position variable of the second program ranging over the output is replaced by the tuple of loop variables of the first program at which that output letter is produced, and the tests on output positions become tests on these tuples, evaluated by re-running the first program (PartD/ForComp∗.leanPartD/ForComp*.lean, PartD/ForResim.leanPartD/ForResim.lean, PartD/ForTrace.leanPartD/ForTrace.lean). isForTransduceriffisForTransducer_iff transports both hypotheses and the conclusion.

Attribution

Lemma D.1.4 of Transducers, Part D; formalised by Aristotle (Harmonic).