The equational theory

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

definition

Loading review…

Natural Language Statement

Definition

Section 4 introduces an equivalence relation $f \equiv g$ on rational terms of the same type, called provable equivalence. It is the least equivalence relation on rational terms that contains the following sixteen axioms and is preserved by the four combinators of Definition 3.1 (composition and functoriality of products, co-products and lists).

Category axioms: composition is associative and the identity is neutral.
Functoriality: the combinators $\times$ , $+$ and $(-)^*$ preserve identities and composition.
Naturality: every atomic function except prefix multiplication is a natural transformation.
Isomorphisms: ten pairs of mutually inverse terms — the units and $\mathsf{fst}$ , $\mathsf{snd}$ ; $\mathsf{assocL}$ and $\mathsf{assocR}$ ; $\mathsf{distL}$ and $\mathsf{undistL}$ ; $\mathsf{distR}$ and $\mathsf{undistR}$ ; $\mathsf{cons}$ and $\mathsf{uncons}$ ; $\mathsf{snoc}$ and $\mathsf{unsnoc}$ ; $\mathsf{split}$ and $\mathsf{unsplit}$ ; $\mathsf{pref}$ and $\mathsf{unpref}$ ; $\mathsf{shiftL}$ and $\mathsf{shiftR}$ .
The unit type is terminal: any two terms $A \to 1$ are equivalent.
The co-diagonal: $\mathsf{Left} \mathbin{;} \mathsf{codiag} \equiv \mathrm{id}$ , $\mathsf{Right} \mathbin{;} \mathsf{codiag} \equiv \mathrm{id}$ and $(\mathsf{Left} + \mathsf{Right}) \mathbin{;} \mathsf{codiag} \equiv \mathrm{id}$ .
Mac Lane's pentagon for $\mathsf{assocL}$ .
Mac Lane's triangle for $\mathsf{assocL}$ and the unit.
The notation based on $\mathsf{snoc}$ agrees with the notation based on $\mathsf{cons}$ : for the empty list, for singleton lists, and for concatenation.
$A^*$ is a monoid under $\mathsf{binconcat}$ with unit $[\,]$ .
$\mathsf{concat}$ is a monoid homomorphism.
$A^*$ is a monad with unit $\mathsf{pure}$ and multiplication $\mathsf{concat}$ .
$\mathsf{prepend}$ and $\mathsf{append}$ are expressed by $\mathsf{binconcat}$ .
Concatenating a list of empty lists gives the empty list.
$\mathsf{shiftR}$ does not change the content of a list: it commutes with the concatenation maps into $(A + B)^*$ .
The window axiom: the bundle term $\mathsf{bundle} : (2^*)^* \to (2^* \times 2^*)^* \times (1 + 2^*)$ , which splits a list into consecutive pairs followed by a remainder of at most one element, is undone by the concatenation map: $\mathsf{bundle} \mathbin{;} \mathsf{concat} \equiv \mathrm{id}$ . Here $2 = 1 + 1$ .

The bundle term (Definition H.5) is, for a type $A$ and a value $w : 1 \to A$ , the composition

((\mathrm{id}, 1) \mathbin{;} (\mathrm{id} \times \mathsf{Right}))^* \mathbin{;} \mathsf{pref}_{\mathbb{Z}_2} \mathbin{;} (\mathsf{distR} \mathbin{;} \langle \mathsf{fst} \mathbin{;} \mathsf{Right}, \mathsf{fst} \mathbin{;} \mathsf{Left} \rangle)^* \mathbin{;} \mathsf{split} \mathbin{;} \mathsf{shiftL} \mathbin{;} ((\mathsf{head}_w \times \mathrm{id})^* \times (\mathsf{uncons} \mathbin{;} (\mathrm{id} + \mathsf{fst}))),

where $\mathbb{Z}_2$ is the cyclic group of order two on $2 = 1 + 1$ , with identity $\mathsf{Left}$ . The window axiom uses it for $A = 2^*$ and $w = [\,]$ .

Concept map

4 concepts

100%

DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Lean source view on GitHub

Show types on hover

1	import Lax149335.DerivedTerms
2
3	/-!
4	---
5	title: The equational theory
6	type: definition
7	---
8	Section 4 introduces an equivalence relation $f \equiv g$ on rational terms of the same type,
9	called provable equivalence. It is the least equivalence relation on rational terms that
10	contains the following sixteen axioms and is preserved by the four combinators of
11	Definition 3.1 (composition and functoriality of products, co-products and lists).
12
13	1. Category axioms: composition is associative and the identity is neutral.
14	2. Functoriality: the combinators $\times$ , $+$ and $(-)^*$ preserve identities and
15	composition.
16	3. Naturality: every atomic function except prefix multiplication is a natural
17	transformation.
18	4. Isomorphisms: ten pairs of mutually inverse terms — the units and $\mathsf{fst}$ ,
19	$\mathsf{snd}$ ; $\mathsf{assocL}$ and $\mathsf{assocR}$ ; $\mathsf{distL}$ and
20	$\mathsf{undistL}$ ; $\mathsf{distR}$ and $\mathsf{undistR}$ ; $\mathsf{cons}$ and
21	$\mathsf{uncons}$ ; $\mathsf{snoc}$ and $\mathsf{unsnoc}$ ; $\mathsf{split}$ and
22	$\mathsf{unsplit}$ ; $\mathsf{pref}$ and $\mathsf{unpref}$ ; $\mathsf{shiftL}$ and
23	$\mathsf{shiftR}$ .
24	5. The unit type is terminal: any two terms $A \to 1$ are equivalent.
25	6. The co-diagonal: $\mathsf{Left} \mathbin{;} \mathsf{codiag} \equiv \mathrm{id}$ ,
26	$\mathsf{Right} \mathbin{;} \mathsf{codiag} \equiv \mathrm{id}$ and
27	$(\mathsf{Left} + \mathsf{Right}) \mathbin{;} \mathsf{codiag} \equiv \mathrm{id}$ .
28	7. Mac Lane's pentagon for $\mathsf{assocL}$ .
29	8. Mac Lane's triangle for $\mathsf{assocL}$ and the unit.
30	9. The notation based on $\mathsf{snoc}$ agrees with the notation based on
31	$\mathsf{cons}$ : for the empty list, for singleton lists, and for concatenation.
32	10. $A^*$ is a monoid under $\mathsf{binconcat}$ with unit $[\,]$ .
33	11. $\mathsf{concat}$ is a monoid homomorphism.
34	12. $A^*$ is a monad with unit $\mathsf{pure}$ and multiplication $\mathsf{concat}$ .
35	13. $\mathsf{prepend}$ and $\mathsf{append}$ are expressed by $\mathsf{binconcat}$ .
36	14. Concatenating a list of empty lists gives the empty list.
37	15. $\mathsf{shiftR}$ does not change the content of a list: it commutes with the
38	concatenation maps into $(A + B)^*$ .
39	16. The window axiom: the bundle term
40	$\mathsf{bundle} : (2^)^ \to (2^* \times 2^)^ \times (1 + 2^*)$ , which splits a
41	list into consecutive pairs followed by a remainder of at most one element, is undone by
42	the concatenation map: $\mathsf{bundle} \mathbin{;} \mathsf{concat} \equiv \mathrm{id}$
43	. Here $2 = 1 + 1$ .
44
45	The bundle term (Definition H.5) is, for a type $A$ and a value $w : 1 \to A$ , the
46	composition
47
48	$((\mathrm{id}, 1) \mathbin{;} (\mathrm{id} \times \mathsf{Right}))^* \mathbin{;} \mathsf{pref}_{\mathbb{Z}_2} \mathbin{;} (\mathsf{distR} \mathbin{;} \langle \mathsf{fst} \mathbin{;} \mathsf{Right}, \mathsf{fst} \mathbin{;} \mathsf{Left} \rangle)^* \mathbin{;} \mathsf{split} \mathbin{;} \mathsf{shiftL} \mathbin{;} ((\mathsf{head}_w \times \mathrm{id})^* \times (\mathsf{uncons} \mathbin{;} (\mathrm{id} + \mathsf{fst}))),$
49
50
51
52
53
54
55	where $\mathbb{Z}_2$ is the cyclic group of order two on $2 = 1 + 1$ , with identity
56	$\mathsf{Left}$ . The window axiom uses it for $A = 2^*$ and $w = [\,]$ .
57
58	# Formalization notes
59
60	Naturality of prefix multiplication is not an axiom: as observed in footnote 5 of the paper,
61	it is derivable. The axioms are listed in full in the constructors of `PEq` below.
62	-/
63
64	namespace Lax149335.EquationalTheory
65
66	open Lax149335.Types Lax149335.Terms Lax149335.DerivedTerms
67
68	namespace Term
69
70	open Lax149335.Terms.Term Lax149335.DerivedTerms.Term
71
72	/-- The cyclic group `ℤ₂` of order two, with the two letter alphabet `2 = 1 + 1` as its
73	underlying set: the group identity is the first letter `Left`, and the second letter `Right`
74	is the generator. -/
75	def cyclicTwo : Group ⟦Ty.finAlph 1⟧ where
76	mul x y := match x, y with
77	\| .inl _, y => y
78	\| x, .inl _ => x
79	\| .inr _, .inr _ => .inl ()
80	one := .inl ()
81	inv x := x
82	mul_assoc := by intro x y z; cases x <;> cases y <;> cases z <;> rfl
83	one_mul := by intro x; cases x <;> rfl
84	mul_one := by intro x; cases x <;> rfl
85	inv_mul_cancel := by intro x; cases x <;> rfl
86
87	/-- The generator `Right` of the cyclic group of order two. -/
88	def cyclicTwoGen : ⟦Ty.finAlph 1⟧ := Sum.inr ()
89
90	/-- Step 3 of the bundle term, for a single element: `distR ; either (fst ; Right)
91	(fst ; Left) : A × 2 → A + A`. An element annotated with the generator `Right` goes to the
92	left copy of `A`, and an element annotated with the identity `Left` goes to the right
93	copy. -/
94	def bundleTag (A : Ty) : Term (A ⊗ Ty.finAlph 1) (A ⊕' A) :=
95	distR A Ty.unit (Ty.finAlph 0) ⨟ either (fst A Ty.unit ⨟ inr A A) (fst A Ty.unit ⨟ inl A A)
96
97	/-- Definition H.5 (the bundle term) `A* → (A × A)* × (1 + A)`, for a type `A` and a value
98	`w : 1 → A`:
99
100	`((id,1) ; (id × Right))* ; pref_{ℤ₂} ; (distR ; either (fst ; Right) (fst ; Left))* ;
101	split ; shiftL ; ((head_w × id)* × (uncons ; (id + fst)))`.
102
103	The window axiom (Axiom 16) says that, for `A = 2*` and `w = []`, it is a one-sided inverse
104	of the concatenation map `(A × A)* × (1 + A) ↣ A*`. -/
105	def bundle (A : Ty) (w : Value A) : Term A⋆ ((A ⊗ A)⋆ ⊗ (Ty.unit ⊕' A)) :=
106	listF (unitR A ⨟ prodF (Term.id A) (inr Ty.unit (Ty.finAlph 0))) ⨟
107	pref A cyclicTwo ⨟
108	listF (bundleTag A) ⨟
109	split A A ⨟
110	shiftL A⋆ A ⨟
111	prodF (listF (prodF (headT w) (Term.id A))) (uncons A ⨟ sumF (Term.id Ty.unit) (fst A A⋆))
112
113	/-- The type constructor `A ↦ (A × A)* × (1 + A)` of the window axiom. -/
114	def TyF.window : TyF := .prod (.list (.prod .param .param)) (.sum .unit .param)
115
116	end Term
117
118	open Lax149335.Terms.Term Lax149335.DerivedTerms.Term
119
120	/-- Provable equality of rational terms: the least equivalence relation containing
121	Axioms 1-16 of Section 4 and stable under the combinators of the system. -/
122	inductive PEq : {A B : Ty} → Term A B → Term A B → Prop
123	-- rules of equational reasoning: `≡` is an equivalence relation, stable under the
124	-- four combinators of the system
125	\| refl {A B : Ty} (f : Term A B) : PEq f f
126	\| symm {A B : Ty} {f g : Term A B} : PEq f g → PEq g f
127	\| trans {A B : Ty} {f g h : Term A B} : PEq f g → PEq g h → PEq f h
128	\| congr_comp {A B C : Ty} {f f' : Term A B} {g g' : Term B C} :
129	PEq f f' → PEq g g' → PEq (f ⨟ g) (f' ⨟ g')
130	\| congr_prodF {A₁ A₂ B₁ B₂ : Ty} {f f' : Term A₁ B₁} {g g' : Term A₂ B₂} :
131	PEq f f' → PEq g g' → PEq (prodF f g) (prodF f' g')
132	\| congr_sumF {A₁ A₂ B₁ B₂ : Ty} {f f' : Term A₁ B₁} {g g' : Term A₂ B₂} :
133	PEq f f' → PEq g g' → PEq (sumF f g) (sumF f' g')
134	\| congr_listF {A B : Ty} {f f' : Term A B} : PEq f f' → PEq (listF f) (listF f')
135	-- ## Axiom 1 (category axioms)
136	\| comp_assoc {A B C D : Ty} (f : Term A B) (g : Term B C) (h : Term C D) :
137	PEq ((f ⨟ g) ⨟ h) (f ⨟ (g ⨟ h))
138	\| id_comp {A B : Ty} (f : Term A B) : PEq (Term.id A ⨟ f) f
139	\| comp_id {A B : Ty} (f : Term A B) : PEq (f ⨟ Term.id B) f
140	-- ## Axiom 2 (functoriality), first part: the functors preserve the identity
141	\| prod_id (A B : Ty) : PEq (prodF (Term.id A) (Term.id B)) (Term.id (A ⊗ B))
142	\| sum_id (A B : Ty) : PEq (sumF (Term.id A) (Term.id B)) (Term.id (A ⊕' B))
143	\| list_id (A : Ty) : PEq (listF (Term.id A)) (Term.id A⋆)
144	-- ## Axiom 2 (functoriality), second part: the functors preserve composition
145	\| prod_comp {A₁ A₂ B₁ B₂ C₁ C₂ : Ty} (f₁ : Term A₁ B₁) (f₂ : Term A₂ B₂)
146	(g₁ : Term B₁ C₁) (g₂ : Term B₂ C₂) :
147	PEq (prodF f₁ f₂ ⨟ prodF g₁ g₂) (prodF (f₁ ⨟ g₁) (f₂ ⨟ g₂))
148	\| sum_comp {A₁ A₂ B₁ B₂ C₁ C₂ : Ty} (f₁ : Term A₁ B₁) (f₂ : Term A₂ B₂)
149	(g₁ : Term B₁ C₁) (g₂ : Term B₂ C₂) :
150	PEq (sumF f₁ f₂ ⨟ sumF g₁ g₂) (sumF (f₁ ⨟ g₁) (f₂ ⨟ g₂))
151	\| list_comp {A B C : Ty} (f : Term A B) (g : Term B C) :
152	PEq (listF f ⨟ listF g) (listF (f ⨟ g))
153	-- ## Axiom 3 (each atomic function is a natural transformation)
154	\| nat_inl {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
155	PEq (inl A B ⨟ sumF f g) (f ⨟ inl A' B')
156	\| nat_inr {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
157	PEq (inr A B ⨟ sumF f g) (g ⨟ inr A' B')
158	\| nat_codiag {A A' : Ty} (f : Term A A') :
159	PEq (sumF f f ⨟ codiag A') (codiag A ⨟ f)
160	\| nat_fst {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
161	PEq (prodF f g ⨟ fst A' B') (fst A B ⨟ f)
162	\| nat_snd {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
163	PEq (prodF f g ⨟ snd A' B') (snd A B ⨟ g)
164	\| nat_unitR {A A' : Ty} (f : Term A A') :
165	PEq (f ⨟ unitR A') (unitR A ⨟ prodF f (Term.id Ty.unit))
166	\| nat_unitL {A A' : Ty} (f : Term A A') :
167	PEq (f ⨟ unitL A') (unitL A ⨟ prodF (Term.id Ty.unit) f)
168	\| nat_assocL {A A' B B' C C' : Ty} (f₁ : Term A A') (f₂ : Term B B') (f₃ : Term C C') :
169	PEq (prodF f₁ (prodF f₂ f₃) ⨟ assocL A' B' C') (assocL A B C ⨟ prodF (prodF f₁ f₂) f₃)
170	\| nat_assocR {A A' B B' C C' : Ty} (f₁ : Term A A') (f₂ : Term B B') (f₃ : Term C C') :
171	PEq (prodF (prodF f₁ f₂) f₃ ⨟ assocR A' B' C') (assocR A B C ⨟ prodF f₁ (prodF f₂ f₃))
172	\| nat_distR {A A' B B' C C' : Ty} (f : Term A A') (g : Term B B') (h : Term C C') :
173	PEq (prodF f (sumF g h) ⨟ distR A' B' C') (distR A B C ⨟ sumF (prodF f g) (prodF f h))
174	\| nat_distL {A A' B B' C C' : Ty} (f : Term A A') (g : Term B B') (h : Term C C') :
175	PEq (prodF (sumF f g) h ⨟ distL A' B' C') (distL A B C ⨟ sumF (prodF f h) (prodF g h))
176	\| nat_cons {A B : Ty} (f : Term A B) :
177	PEq (sumF (Term.id Ty.unit) (prodF f (listF f)) ⨟ cons B) (cons A ⨟ listF f)
178	\| nat_uncons {A B : Ty} (f : Term A B) :
179	PEq (listF f ⨟ uncons B) (uncons A ⨟ sumF (Term.id Ty.unit) (prodF f (listF f)))
180	\| nat_snoc {A B : Ty} (f : Term A B) :
181	PEq (sumF (Term.id Ty.unit) (prodF (listF f) f) ⨟ snoc B) (snoc A ⨟ listF f)
182	\| nat_unsnoc {A B : Ty} (f : Term A B) :
183	PEq (listF f ⨟ unsnoc B) (unsnoc A ⨟ sumF (Term.id Ty.unit) (prodF (listF f) f))
184	\| nat_concat {A B : Ty} (f : Term A B) :
185	PEq (listF (listF f) ⨟ concat B) (concat A ⨟ listF f)
186	\| nat_split {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
187	PEq (listF (sumF f g) ⨟ split A' B')
188	(split A B ⨟ prodF (listF f) (listF (prodF g (listF f))))
189	\| nat_shiftR {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
190	PEq (prodF (listF (prodF f g)) f ⨟ shiftR A' B')
191	(shiftR A B ⨟ prodF f (listF (prodF g f)))
192	\| nat_shiftL {A A' B B' : Ty} (f : Term A A') (g : Term B B') :
193	PEq (prodF f (listF (prodF g f)) ⨟ shiftL A' B')
194	(shiftL A B ⨟ prodF (listF (prodF f g)) f)
195	-- (Naturality of the group prefix multiplication need not be postulated: it is derivable,
196	-- see footnote 5 of the paper.)
197	-- ## Axiom 4 (ten pairs of mutually inverse functions)
198	\| unitR_fst (A : Ty) : PEq (unitR A ⨟ fst A Ty.unit) (Term.id A)
199	\| fst_unitR (A : Ty) : PEq (fst A Ty.unit ⨟ unitR A) (Term.id (A ⊗ Ty.unit))
200	\| unitL_snd (A : Ty) : PEq (unitL A ⨟ snd Ty.unit A) (Term.id A)
201	\| snd_unitL (A : Ty) : PEq (snd Ty.unit A ⨟ unitL A) (Term.id (Ty.unit ⊗ A))
202	\| assocL_assocR (A B C : Ty) :
203	PEq (assocL A B C ⨟ assocR A B C) (Term.id (A ⊗ (B ⊗ C)))
204	\| assocR_assocL (A B C : Ty) :
205	PEq (assocR A B C ⨟ assocL A B C) (Term.id ((A ⊗ B) ⊗ C))
206	\| distL_undistL (A B C : Ty) :
207	PEq (distL A B C ⨟ undistL A B C) (Term.id ((A ⊕' B) ⊗ C))
208	\| undistL_distL (A B C : Ty) :
209	PEq (undistL A B C ⨟ distL A B C) (Term.id ((A ⊗ C) ⊕' (B ⊗ C)))
210	\| distR_undistR (A B C : Ty) :
211	PEq (distR A B C ⨟ undistR A B C) (Term.id (A ⊗ (B ⊕' C)))
212	\| undistR_distR (A B C : Ty) :
213	PEq (undistR A B C ⨟ distR A B C) (Term.id ((A ⊗ B) ⊕' (A ⊗ C)))
214	\| cons_uncons (A : Ty) : PEq (cons A ⨟ uncons A) (Term.id (Ty.unit ⊕' (A ⊗ A⋆)))
215	\| uncons_cons (A : Ty) : PEq (uncons A ⨟ cons A) (Term.id A⋆)
216	\| snoc_unsnoc (A : Ty) : PEq (snoc A ⨟ unsnoc A) (Term.id (Ty.unit ⊕' (A⋆ ⊗ A)))
217	\| unsnoc_snoc (A : Ty) : PEq (unsnoc A ⨟ snoc A) (Term.id A⋆)
218	\| split_unsplit (A B : Ty) : PEq (split A B ⨟ unsplit A B) (Term.id (A ⊕' B)⋆)
219	\| unsplit_split (A B : Ty) : PEq (unsplit A B ⨟ split A B) (Term.id (A⋆ ⊗ (B ⊗ A⋆)⋆))
220	\| pref_unpref (A : Ty) {n : ℕ} (G : Group ⟦Ty.finAlph n⟧) :
221	PEq (pref A G ⨟ unpref A G) (Term.id ((A ⊗ Ty.finAlph n)⋆))
222	\| unpref_pref (A : Ty) {n : ℕ} (G : Group ⟦Ty.finAlph n⟧) :
223	PEq (unpref A G ⨟ pref A G) (Term.id ((A ⊗ Ty.finAlph n)⋆))
224	\| shiftL_shiftR (A B : Ty) : PEq (shiftL A B ⨟ shiftR A B) (Term.id (A ⊗ (B ⊗ A)⋆))
225	\| shiftR_shiftL (A B : Ty) : PEq (shiftR A B ⨟ shiftL A B) (Term.id ((A ⊗ B)⋆ ⊗ A))
226	-- ## Axiom 5 (the unit type is terminal)
227	\| unit_unique {A : Ty} (f g : Term A Ty.unit) : PEq f g
228	-- ## Axiom 6 (the co-diagonal)
229	\| inl_codiag (A : Ty) : PEq (inl A A ⨟ codiag A) (Term.id A)
230	\| inr_codiag (A : Ty) : PEq (inr A A ⨟ codiag A) (Term.id A)
231	\| sum_inl_inr_codiag (A B : Ty) :
232	PEq (sumF (inl A B) (inr A B) ⨟ codiag (A ⊕' B)) (Term.id (A ⊕' B))
233	-- ## Axiom 7 (Mac Lane's pentagon)
234	\| pentagon (A B C D : Ty) :
235	PEq (prodF (Term.id A) (assocL B C D) ⨟ assocL A (B ⊗ C) D ⨟
236	prodF (assocL A B C) (Term.id D))
237	(assocL A B (C ⊗ D) ⨟ assocL (A ⊗ B) C D)
238	-- ## Axiom 8 (Mac Lane's triangle)
239	\| triangle (A C : Ty) :
240	PEq (assocL A Ty.unit C ⨟ prodF (fst A Ty.unit) (Term.id C))
241	(prodF (Term.id A) (snd Ty.unit C))
242	-- ## Axiom 9 (`snoc`-based notation agrees with `cons`-based notation)
243	\| inl_snoc_cons (A : Ty) :
244	PEq (inl Ty.unit (A⋆ ⊗ A) ⨟ snoc A) (inl Ty.unit (A ⊗ A⋆) ⨟ cons A)
245	\| append_nil_prepend_nil (A : Ty) :
246	PEq (unitL A ⨟ prodF (nilT A) (Term.id A) ⨟ append A)
247	(unitR A ⨟ prodF (Term.id A) (nilT A) ⨟ prepend A)
248	\| append_concat_prepend_concat (A : Ty) :
249	PEq (prodF (pureT A⋆) (Term.id A⋆) ⨟ append A⋆ ⨟ concat A)
250	(prodF (Term.id A⋆) (pureT A⋆) ⨟ prepend A⋆ ⨟ concat A)
251	-- ## Axiom 10 (`A*` is a monoid)
252	\| binconcat_assoc (A : Ty) :
253	PEq (prodF (binconcat A) (Term.id A⋆) ⨟ binconcat A)
254	(assocR A⋆ A⋆ A⋆ ⨟ prodF (Term.id A⋆) (binconcat A) ⨟ binconcat A)
255	\| binconcat_unitR (A : Ty) :
256	PEq (unitR A⋆ ⨟ prodF (Term.id A⋆) (nilT A) ⨟ binconcat A) (Term.id A⋆)
257	\| binconcat_unitL (A : Ty) :
258	PEq (unitL A⋆ ⨟ prodF (nilT A) (Term.id A⋆) ⨟ binconcat A) (Term.id A⋆)
259	-- ## Axiom 11 (`concat` is a monoid homomorphism)
260	\| nil_concat (A : Ty) : PEq (nilT A⋆ ⨟ concat A) (nilT A)
261	\| binconcat_concat (A : Ty) :
262	PEq (binconcat A⋆ ⨟ concat A) (prodF (concat A) (concat A) ⨟ binconcat A)
263	-- ## Axiom 12 (`A*` is a monad)
264	\| concat_concat (A : Ty) : PEq (listF (concat A) ⨟ concat A) (concat A⋆ ⨟ concat A)
265	\| pure_concat (A : Ty) : PEq (pureT A⋆ ⨟ concat A) (Term.id A⋆)
266	\| listF_pure_concat (A : Ty) : PEq (listF (pureT A) ⨟ concat A) (Term.id A⋆)
267	-- ## Axiom 13 (the inductive structure in terms of the monoid structure)
268	\| prepend_def (A : Ty) :
269	PEq (prepend A) (prodF (pureT A) (Term.id A⋆) ⨟ binconcat A)
270	\| append_def (A : Ty) :
271	PEq (append A) (prodF (Term.id A⋆) (pureT A) ⨟ binconcat A)
272	-- ## Axiom 14 (concatenating a list of empty lists)
273	\| nil_map_concat (A : Ty) :
274	PEq (listF (nilT A) ⨟ concat A) (toUnit Ty.unit ⋆ ⨟ nilT A)
275	-- ## Axiom 15 (`shiftR` does not change the content of the list)
276	\| shiftR_content (A B : Ty) :
277	PEq (shiftR A B ⨟ TyF2.concatMap (.prod .p1 (.list (.prod .p2 .p1))) A B)
278	(TyF2.concatMap (.prod (.list (.prod .p1 .p2)) .p1) A B)
279	-- ## Axiom 16 (the window axiom: the bundle term undoes the concatenation map of bundles
280	-- of size two over binary strings)
281	--
282	-- The bundle term `bundle_{2} : (2)* → (2* × 2) × (1 + 2*)` of Definition H.5,
283	-- formalised as `Term.bundle` with the value `w = []`, splits a list into bundles
284	-- of two consecutive entries followed by a remainder of at most one entry. The axiom says
285	-- that this splitting is undone by the concatenation map
286	--
287	-- `(2* × 2) × (1 + 2) ↣ (2)*`,
288	--
289	-- i.e. that `bundle ; concat ≡ id`.
290	\| window :
291	PEq (Term.bundle ((Ty.finAlph 1)⋆) (nilT (Ty.finAlph 1)) ⨟
292	TyF.concatMap Term.TyF.window ((Ty.finAlph 1)⋆))
293	(Term.id (((Ty.finAlph 1)⋆)⋆))
294
295	/-- Notation `f ≡ₜ g` for provable equivalence of rational terms. -/
296	infix:50 " ≡ₜ " => PEq
297
298	end Lax149335.EquationalTheory
299

Formalization notes

Naturality of prefix multiplication is not an axiom: as observed in footnote 5 of the paper, it is derivable. The axioms are listed in full in the constructors of $PEq$ below.

Builds on

Lax149335.DerivedTerms

Used by

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

The equational theory

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments