Synchronised output lengths

Lax149335.SynchronisedLengths · concepts/Lax149335/SynchronisedLengths.lean · lax-149335

proven

Loading review…

Natural Language Statement

Claim

Claim 2.7. This claim arises in the induction step for products in the proof of Theorem 2.6. Consider two simple rational terms with input type $A_1^* \times \cdots \times A_n^*$ of the form

f = w_0 \cdot (\mathrm{hom}\, f_1 \cdot w_1) \odot \cdots \odot (\mathrm{hom}\, f_n \cdot w_n) \qquad g = v_0 \cdot (\mathrm{hom}\, g_1 \cdot v_1) \odot \cdots \odot (\mathrm{hom}\, g_n \cdot v_n)

that define the same function. Then for every $i \in \{1, \ldots, n\}$ and every $a \in A_i$ , the strings $f_i(a)$ and $g_i(a)$ have the same length.

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

cla✓Lax149335.SynchronisedLengths

⊢Lax149335Proofs.Results.claim_same_lengths

Lean source view on GitHub

Show types on hover

1	import Lax149335.SimpleRationalTerms
2
3	/-!
4	---
5	title: Synchronised output lengths
6	type: claim
7	---
8	Claim 2.7. This claim arises in the induction step for products in the proof of
9	Theorem 2.6. Consider two simple rational terms with input type
10	$A_1^* \times \cdots \times A_n^*$ of the form
11
12	$f = w_0 \cdot (\mathrm{hom}\, f_1 \cdot w_1) \odot \cdots \odot (\mathrm{hom}\, f_n \cdot w_n) \qquad g = v_0 \cdot (\mathrm{hom}\, g_1 \cdot v_1) \odot \cdots \odot (\mathrm{hom}\, g_n \cdot v_n)$
13
14
15
16	that define the same function. Then for every $i \in \{1, \ldots, n\}$ and every
17	$a \in A_i$ , the strings $f_i(a)$ and $g_i(a)$ have the same length.
18
19	# Formalization notes
20
21	The input type is $A_1^* \times (A_2^* \times \cdots \times (A_n^* \times 1))$ , and the
22	components $(f_i, w_i)$ are given as a list (`HomList`).
23	-/
24
25	namespace Lax149335.SynchronisedLengths
26
27	open Lax149335.Types Lax149335.SimpleRationalTerms
28
29	namespace SimpleTerm
30
31	variable {Bs : Type}
32
33	/-- The type `A₁* × (A₂* × ⋯ × (Aₙ* × 1))`. -/
34	def prodListTy : List Ty → Ty
35	\| [] => Ty.unit
36	\| A :: As => Ty.prod A⋆ (prodListTy As)
37
38	/-- A list of pairs `(fᵢ, wᵢ)` of a simple rational term `fᵢ : Aᵢ → Bs*` and a string `wᵢ`. -/
39	inductive HomList (Bs : Type) : List Ty → Type
40	\| nil : HomList Bs []
41	\| cons {A : Ty} {As : List Ty} : SimpleTerm Bs A → List Bs → HomList Bs As →
42	HomList Bs (A :: As)
43
44	/-- The term `(hom f₁ · w₁) ⊙ ⋯ ⊙ (hom fₙ · wₙ)` of a list of pairs. -/
45	def HomList.term : {As : List Ty} → HomList Bs As → SimpleTerm Bs (prodListTy As)
46	\| _, .nil => .empty
47	\| _, .cons f w rest => .conc (.post (.hom f) w) rest.term
48
49	/-- Two lists of pairs whose terms `fᵢ` and `gᵢ` produce outputs of the same length on every
50	input. -/
51	def HomList.SameLengths : {As : List Ty} → HomList Bs As → HomList Bs As → Prop
52	\| _, .nil, .nil => True
53	\| _, .cons f _ F, .cons g _ G =>
54	(∀ a, (f.den a).length = (g.den a).length) ∧ HomList.SameLengths F G
55
56	end SimpleTerm
57
58	open SimpleTerm
59
60	/-- Claim 2.7. If `w₀ · (hom f₁ · w₁) ⊙ ⋯ ⊙ (hom fₙ · wₙ)` and
61	`v₀ · (hom g₁ · v₁) ⊙ ⋯ ⊙ (hom gₙ · vₙ)` define the same function, then `fᵢ` and `gᵢ` produce
62	outputs of the same length on every input. -/
63	axiom claim_same_lengths {Bs : Type} {As : List Ty} (F G : HomList Bs As) (w₀ v₀ : List Bs) :
64	(SimpleRationalTerms.SimpleTerm.pre w₀ F.term).den =
65	(SimpleRationalTerms.SimpleTerm.pre v₀ G.term).den →
66	F.SameLengths G
67
68	end Lax149335.SynchronisedLengths
69

Show Proof

Formalization notes

The input type is $A_1^* \times (A_2^* \times \cdots \times (A_n^* \times 1))$ , and the components $(f_i, w_i)$ are given as a list ( $HomList$ ).

Builds on

Lax149335.SimpleRationalTerms

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Synchronised output lengths

Flags

Flag this concept

Natural Language Statement

Claim

Lean source view on GitHub

Discussion

Settings

Your comments