Free monoid over a given alphabet #
Main definitions #
FreeMonoid α
: free monoid over alphabetα
; defined as a synonym forList α
with multiplication given by(++)
.FreeMonoid.of
: embeddingα → FreeMonoid α
sending each elementx
to[x]
;FreeMonoid.lift
: natural equivalence betweenα → M
andFreeMonoid α →* M
FreeMonoid.map
: embedding ofα → β
intoFreeMonoid α →* FreeMonoid β
given byList.map
.
If α
is a type, then FreeMonoid α
is the free monoid generated by α
.
This is a monoid equipped with a function FreeMonoid.of : α → FreeMonoid α
which has
the following universal property: if M
is any monoid, and f : α → M
is any function,
then this function is the composite of FreeMonoid.of
and a unique monoid homomorphism
FreeMonoid.lift f : FreeMonoid α →* M
.
A typical element of FreeMonoid α
is a formal product of elements of α
.
For example if x
and y
are terms of type α
then x * y * y * x
is a
"typical" element of FreeMonoid α
. In particular if α
is empty
then FreeMonoid α
is isomorphic to the trivial monoid, and if α
has one term
then FreeMonoid α
is isomorphic to Multiplicative ℕ
.
If α
has two or more terms then FreeMonoid α
is not commutative.
One can think of FreeMonoid α
as the type of lists of α
, with multiplication
given by concatenation.
Equations
- FreeMonoid α = List α
If α
is a type, then FreeAddMonoid α
is the free additive monoid generated by α
.
This is a monoid equipped with a function FreeAddMonoid.of : α → FreeAddMonoid α
which has
the following universal property: if M
is any monoid, and f : α → M
is any function,
then this function is the composite of FreeAddMonoid.of
and a unique monoid homomorphism
FreeAddMonoid.lift f : FreeAddMonoid α →+ M
.
A typical element of FreeAddMonoid α
is a formal sum of elements of α
.
For example if x
and y
are terms of type α
then x + y + y + x
is a
"typical" element of FreeAddMonoid α
. In particular if α
is empty
then FreeAddMonoid α
is isomorphic to the trivial monoid, and if α
has one term
then FreeAddMonoid α
is isomorphic to ℕ
.
If α
has two or more terms then FreeAddMonoid α
is not commutative.
One can think of FreeAddMonoid α
as the type of lists of α
, with addition
given by concatenation.
Equations
- FreeAddMonoid α = List α
The identity equivalence between FreeMonoid α
and List α
.
Equations
The identity equivalence between FreeAddMonoid α
and List α
.
Equations
The identity equivalence between List α
and FreeMonoid α
.
Equations
The identity equivalence between List α
and FreeAddMonoid α
.
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- FreeMonoid.instInhabited = { default := 1 }
Equations
- FreeAddMonoid.instInhabited = { default := 0 }
Equations
Equations
Embeds an element of α
into FreeMonoid α
as a singleton list.
Equations
Embeds an element of α
into FreeAddMonoid α
as a singleton list.
Equations
Length #
The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length
Equations
- a.length = (FreeMonoid.toList a).length
The length of an additive free monoid element: 1.length = 0 and (a + b).length = a.length + b.length
Equations
- a.length = (FreeAddMonoid.toList a).length
Membership in a free monoid element
Equations
- a.mem m = (m ∈ FreeMonoid.toList a)
Membership in a free monoid element
Equations
- a.mem m = (m ∈ FreeAddMonoid.toList a)
Equations
- FreeMonoid.instMembership = { mem := FreeMonoid.mem }
Equations
Alias of FreeAddMonoid.notMem_zero
.
Alias of FreeMonoid.notMem_one
.
Recursor for FreeMonoid
using 1
and FreeMonoid.of x * xs
instead of []
and x :: xs
.
Recursor for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xsinstead of
[]and
x :: xs`.
Induction #
An induction principle on free monoids, with cases for 1
, FreeMonoid.of
and *
.
An induction principle on free monoids, with cases for 0
, FreeAddMonoid.of
and +
.
An induction principle for free monoids which mirrors induction on lists, with cases analogous to the empty list and cons
An induction principle for free monoids which mirrors induction on lists, with cases analogous to the empty list and cons
A version of List.cases_on
for FreeMonoid
using 1
and FreeMonoid.of x * xs
instead of
[]
and x :: xs
.
Equations
- xs.casesOn h0 ih = List.casesOn xs h0 ih
A version of List.casesOn
for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xs
instead of []
and x :: xs
.
Equations
- xs.casesOn h0 ih = List.casesOn xs h0 ih
A variant of List.prod
that has [x].prod = x
true definitionally.
The purpose is to make FreeMonoid.lift_eval_of
true by rfl
.
Equations
- FreeMonoid.prodAux [] = 1
- FreeMonoid.prodAux (x_1 :: xs) = List.foldl (fun (x1 x2 : M) => x1 * x2) x_1 xs
A variant of List.sum
that has [x].sum = x
true definitionally.
The purpose is to make FreeAddMonoid.lift_eval_of
true by rfl
.
Equations
- FreeAddMonoid.sumAux [] = 0
- FreeAddMonoid.sumAux (x_1 :: xs) = List.foldl (fun (x1 x2 : M) => x1 + x2) x_1 xs
Equivalence between maps α → M
and monoid homomorphisms FreeMonoid α →* M
.
Equations
- One or more equations did not get rendered due to their size.
Equivalence between maps α → A
and additive monoid homomorphisms
FreeAddMonoid α →+ A
.
Equations
- One or more equations did not get rendered due to their size.
Define a multiplicative action of FreeMonoid α
on β
.
Equations
- FreeMonoid.mkMulAction f = { smul := fun (l : FreeMonoid α) (b : β) => List.foldr f b (FreeMonoid.toList l), one_smul := ⋯, mul_smul := ⋯ }
Define an additive action of FreeAddMonoid α
on β
.
Equations
- FreeAddMonoid.mkAddAction f = { vadd := fun (l : FreeAddMonoid α) (b : β) => List.foldr f b (FreeAddMonoid.toList l), zero_vadd := ⋯, add_vadd := ⋯ }
map #
The unique monoid homomorphism FreeMonoid α →* FreeMonoid β
that sends
each of x
to of (f x)
.
Equations
- FreeMonoid.map f = { toFun := fun (l : FreeMonoid α) => FreeMonoid.ofList (List.map f (FreeMonoid.toList l)), map_one' := ⋯, map_mul' := ⋯ }
The unique additive monoid homomorphism FreeAddMonoid α →+ FreeAddMonoid β
that sends each of x
to of (f x)
.
Equations
- FreeAddMonoid.map f = { toFun := fun (l : FreeAddMonoid α) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ }
The only invertible element of the free monoid is 1; this instance enables units_eq_one
.
Equations
- FreeMonoid.uniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }
Equations
- FreeAddMonoid.uniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }
reverse #
reverses the symbols in a free monoid element
Equations
reverses the symbols in an additive free monoid element
Equations
free monoids over isomorphic types are isomorphic
Equations
- FreeMonoid.freeMonoidCongr e = { toFun := ⇑(FreeMonoid.map ⇑e), invFun := ⇑(FreeMonoid.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
if two types are isomorphic, the additive free monoids over those types are isomorphic
Equations
- FreeAddMonoid.freeAddMonoidCongr e = { toFun := ⇑(FreeAddMonoid.map ⇑e), invFun := ⇑(FreeAddMonoid.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }