Lax Lean Archive

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

Proof of `The snake lemma: the output of a snake graph is a regular function`

groundedproofs/Lax916827Proofs/Results.lean · lax-916827

What this proof establishes

no assumptions

thm✓Lax916827.SnakeLemma

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

The snake lemma (Lemma C.2.12): the output of a snake graph of width at most kk, read off its string representation, is a regular function (Transducers.SnakeGraph.snakeOutisRegularTransducers.SnakeGraph.snakeOut_isRegular).

Proof strategy

The source reads the snake letters through the two-way transducer snakeTranssnakeTrans that walks along a snake graph (PartC/SnakeAlph∗.leanPartC/SnakeAlph*.lean) and applies the general snake lemma Transducers.boundedWidthisRegularTransducers.boundedWidth_isRegular for the width-kk output function of a two-way transducer on the regular language of strings representing a snake graph of width at most kk. The concept's snake graphs are defined by the same formulas as the source's; snakeOuteqsnakeOut_eq of the bridge identifies the two output functions.

Attribution

Lemma C.2.12 of Transducers, Part C; formalised by Aristotle (Harmonic).