Lax Lean Archive

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

Lax916827.RegularConditional

Regular functions are closed under conditionals over regular languages

concepts/Lax916827/RegularConditional.lean · lax-916827

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    If f,g:A∗→B∗f, g : A^* \to B^* are regular and L⊆A∗L \subseteq A^* is regular, then the conditional function

    w↦{f(w)if w∈Lg(w)otherwisew \mapsto \begin{cases} f(w) & \text{if } w \in L \\ g(w) & \text{otherwise} \end{cases}

    is regular (Lemma C.2.10 of Transducers, third item): a rational function marks the input with its membership in LL, and the marked sum of Claim C.2.11 applies ff or gg according to the mark.

    Lean source view on GitHub

    1import Mathlib.Computability.DFA
    2import Lax916827.RegularFunctions
    3
    4/-!
    5---
    6title: Regular functions are closed under conditionals over regular languages
    7type: theorem
    8---
    9If f,g:A∗→B∗f, g : A^* \to B^* are regular and L⊆A∗L \subseteq A^* is regular, then the
    10conditional function
    11w↦{f(w)if w∈Lg(w)otherwisew \mapsto \begin{cases} f(w) & \text{if } w \in L \\ g(w) & \text{otherwise} \end{cases}
    12is regular (Lemma C.2.10 of *Transducers*, third item): a rational function
    13marks the input with its membership in LL, and the marked sum of Claim C.2.11
    14applies ff or gg according to the mark.
    15
    16# Formalization notes
    17
    18The conditional needs a decision of `w ∈ L`; the statement uses classical
    19decidability, since no computational content is claimed for the function. Both
    20alphabets are assumed finite, as in the book.
    21-/
    22
    23namespace Lax916827.RegularConditional
    24
    25open Lax916827.RegularFunctions
    26
    27open scoped Classical in
    28/-- The conditional of two regular functions over a regular language is regular. -/
    29axiom isRegularFun_ite {A B : Type} [Finite A] [Finite B] {f g : List A → List B}
    30 (hf : IsRegularFun f) (hg : IsRegularFun g) (L : Language A) (hL : L.IsRegular) :
    31 IsRegularFun (fun w => if w ∈ L then f w else g w)
    32
    33end Lax916827.RegularConditional
    34
    Show Proof

    Formalization notes

    The conditional needs a decision of w∈Lw ∈ L; the statement uses classical decidability, since no computational content is claimed for the function. Both alphabets are assumed finite, as in the book.

    Builds on

    Used by

    none

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…