Lax916827.RegularSum

The sum of two regular functions on disjoint alphabets

concepts/Lax916827/RegularSum.lean · lax-916827

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax916827.RegularSum

⊢Lax916827Proofs.Results.exists_isRegularFun_sum

In the paper

page 99 of the paper of lax-157538, Transducers

Theorem

For regular functions $f_1 : A_1^* \to B_1^*$ and $f_2 : A_2^* \to B_2^*$ with disjoint input and output alphabets, the function $f_1 + f_2$ on $(A_1 + A_2)^*$ is regular (Claim C.2.11 of Transducers): it applies $f_1$ to the inputs using only letters of $A_1$ , $f_2$ to those using only letters of $A_2$ , and returns a fixed string $\bot$ using both output alphabets otherwise. The claim is what the closure properties of Lemma C.2.10 rest on.

Lean source view on GitHub

1	import Lax916827.RegularFunctions
2
3	/-!
4	---
5	title: The sum of two regular functions on disjoint alphabets
6	type: theorem
7	---
8	For regular functions $f_1 : A_1^* \to B_1^$ and $f_2 : A_2^ \to B_2^*$
9	with disjoint input and output alphabets, the function $f_1 + f_2$ on
10	$(A_1 + A_2)^$ is regular (Claim C.2.11 of Transducers*): it applies $f_1$
11	to the inputs using only letters of $A_1$ , $f_2$ to those using only letters of
12	$A_2$ , and returns a fixed string $\bot$ using both output alphabets otherwise.
13	The claim is what the closure properties of Lemma C.2.10 rest on.
14
15	# Formalization notes
16
17	The claim as printed is false on the empty input: the empty string uses only
18	letters of $A_1$ and, at the same time, only letters of $A_2$ , so the first two
19	requirements conflict unless $f_1(\varepsilon)$ and $f_2(\varepsilon)$ are both
20	empty. The statement therefore imposes the two requirements on nonempty
21	inputs only and leaves the value on the empty input unspecified, which is
22	harmless for the use the book makes of the claim, where the blocks are always
23	nonempty. The disjoint union of alphabets is `A₁ ⊕ A₂`, and the output
24	alphabets are assumed nonempty so that $\bot$ exists.
25	-/
26
27	namespace Lax916827.RegularSum
28
29	open Lax916827.RegularFunctions
30
31	/-- The sum `f₁ + f₂` of two regular functions on disjoint alphabets is regular,
32	with a bottom value on mixed inputs (and the two clauses required on nonempty
33	inputs). -/
34	axiom exists_isRegularFun_sum {A₁ A₂ B₁ B₂ : Type} [Finite A₁] [Finite A₂] [Finite B₁] [Finite B₂]
35	[Nonempty B₁] [Nonempty B₂] {f₁ : List A₁ → List B₁} {f₂ : List A₂ → List B₂}
36	(hf₁ : IsRegularFun f₁) (hf₂ : IsRegularFun f₂) :
37	∃ (bot : List (B₁ ⊕ B₂)) (F : List (A₁ ⊕ A₂) → List (B₁ ⊕ B₂)),
38	(∃ b₁, Sum.inl b₁ ∈ bot) ∧ (∃ b₂, Sum.inr b₂ ∈ bot) ∧
39	IsRegularFun F ∧
40	(∀ u : List A₁, u ≠ [] → F (u.map Sum.inl) = (f₁ u).map Sum.inl) ∧
41	(∀ u : List A₂, u ≠ [] → F (u.map Sum.inr) = (f₂ u).map Sum.inr) ∧
42	(∀ w, (¬ ∃ u : List A₁, w = u.map Sum.inl) → (¬ ∃ u : List A₂, w = u.map Sum.inr) →
43	F w = bot)
44
45	end Lax916827.RegularSum
46

Show Proof

Formalization notes

The claim as printed is false on the empty input: the empty string uses only letters of $A_1$ and, at the same time, only letters of $A_2$ , so the first two requirements conflict unless $f_1(\varepsilon)$ and $f_2(\varepsilon)$ are both empty. The statement therefore imposes the two requirements on nonempty inputs only and leaves the value on the empty input unspecified, which is harmless for the use the book makes of the claim, where the blocks are always nonempty. The disjoint union of alphabets is $A₁ ⊕ A₂$ , and the output alphabets are assumed nonempty so that $\bot$ exists.

Builds on

Lax916827.RegularFunctions

Used by

none

From Mathlib

none

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…

Lax Lean Archive