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
Instances For
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
Instances For
Equations
Equations
Equations
Length #
The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length
Equations
Instances For
The length of an additive free monoid element: 1.length = 0 and (a + b).length = a.length + b.length
Equations
Instances For
Membership in a free monoid element
Equations
Instances For
Membership in a free monoid element
Equations
Instances For
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
.
Equations
Instances For
Recursor for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xsinstead of
[]and
x :: xs`.
Equations
Instances For
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
Instances For
A version of List.casesOn
for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xs
instead of []
and x :: xs
.
Equations
Instances For
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
Instances For
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
Instances For
Equivalence between maps α → A
and additive monoid homomorphisms
FreeAddMonoid α →+ A
.
Equations
Instances For
Define a multiplicative action of FreeMonoid α
on β
.
Equations
Instances For
Define an additive action of FreeAddMonoid α
on β
.
Equations
Instances For
map #
The unique monoid homomorphism FreeMonoid α →* FreeMonoid β
that sends
each of x
to of (f x)
.
Equations
Instances For
The unique additive monoid homomorphism FreeAddMonoid α →+ FreeAddMonoid β
that sends each of x
to of (f x)
.
Equations
Instances For
The only invertible element of the free monoid is 1; this instance enables units_eq_one
.
Equations
Equations
reverse #
reverses the symbols in a free monoid element
Equations
Instances For
reverses the symbols in an additive free monoid element
Equations
Instances For
free monoids over isomorphic types are isomorphic
Equations
Instances For
if two types are isomorphic, the additive free monoids over those types are isomorphic