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
.
Free nonabelian additive monoid over a given alphabet
Equations
- FreeAddMonoid α = List α
Free monoid over a given alphabet.
Equations
- FreeMonoid α = List α
The identity equivalence between FreeAddMonoid α
and List α
.
Equations
- FreeAddMonoid.toList = Equiv.refl (FreeAddMonoid α)
The identity equivalence between FreeMonoid α
and List α
.
Equations
- FreeMonoid.toList = Equiv.refl (FreeMonoid α)
The identity equivalence between List α
and FreeAddMonoid α
.
Equations
- FreeAddMonoid.ofList = Equiv.refl (List α)
The identity equivalence between List α
and FreeMonoid α
.
Equations
- FreeMonoid.ofList = Equiv.refl (List α)
Equations
- FreeAddMonoid.instAddCancelMonoid = AddCancelMonoid.mk ⋯
Equations
- FreeMonoid.instCancelMonoid = CancelMonoid.mk ⋯
Equations
- FreeAddMonoid.instInhabited = { default := 0 }
Equations
- FreeMonoid.instInhabited = { default := 1 }
Equations
- FreeAddMonoid.instUniqueOfIsEmpty = inferInstanceAs (Unique (List α))
Equations
- FreeMonoid.instUniqueOfIsEmpty = inferInstanceAs (Unique (List α))
Embeds an element of α
into FreeAddMonoid α
as a singleton list.
Equations
- FreeAddMonoid.of x = FreeAddMonoid.ofList [x]
Embeds an element of α
into FreeMonoid α
as a singleton list.
Equations
- FreeMonoid.of x = FreeMonoid.ofList [x]
Length #
The length of an additive free monoid element: 1.length = 0 and (a + b).length = a.length + b.length
Equations
- a.length = List.length a
The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length
Equations
- a.length = List.length a
Membership in a free monoid element
Membership in a free monoid element
Equations
- FreeAddMonoid.instMembership = { mem := FreeAddMonoid.mem }
Equations
- FreeMonoid.instMembership = { mem := FreeMonoid.mem }
Recursor for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xsinstead of
[]and
x :: xs`.
Recursor for FreeMonoid
using 1
and FreeMonoid.of x * xs
instead of []
and x :: xs
.
Induction #
An induction principle on free monoids, with cases for 0
, FreeAddMonoid.of
and +
.
An induction principle on free monoids, with cases for 1
, FreeMonoid.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.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 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 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
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
Equivalence between maps α → A
and additive monoid homomorphisms
FreeAddMonoid α →+ A
.
Equations
- One or more equations did not get rendered due to their size.
Equivalence between maps α → M
and monoid homomorphisms FreeMonoid α →* M
.
Equations
- One or more equations did not get rendered due to their size.
Define an additive action of FreeAddMonoid α
on β
.
Equations
Define a multiplicative action of FreeMonoid α
on β
.
Equations
map #
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 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' := ⋯ }
Equations
- FreeAddMonoid.uniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }
The only invertible element of the free monoid is 1; this instance enables units_eq_one
.
Equations
- FreeMonoid.uniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }
reverse #
reverses the symbols in an additive free monoid element
Equations
- FreeAddMonoid.reverse = List.reverse
reverses the symbols in a free monoid element
Equations
- FreeMonoid.reverse = List.reverse