Skip to content

Instantly share code, notes, and snippets.

@brendanzab

brendanzab/Monoids.lean

Last active Mar 5, 2021
Embed
What would you like to do?
Playing with monoids in Lean 4
/-
Playing with monoids in Lean 4
```
$ lean -v
Lean (version 4.0.0-nightly-2021-02-28, commit 6a6f68f6ccc8, Release)
```
-/
namespace Monoids
class Monoid (A : Type) where
append : A → A → A
empty : A
append_assoc : (a₁ a₂ a₃ : A) → append (append a₁ a₂) a₃ = append a₁ (append a₂ a₃)
append_empty : (a : A) → append a empty = a
instance Nat.addMonoid : Monoid Nat := {
append := Nat.add
empty := 0
append_assoc := Nat.add_assoc
append_empty := Nat.add_zero
}
instance Nat.mulMonoid : Monoid Nat := {
append := Nat.mul
empty := 1
append_assoc := Nat.mul_assoc
append_empty := Nat.mul_one
}
instance Bool.andMonoid : Monoid Bool := {
append := and
empty := true
append_assoc := fun
| false, _, _ => rfl
| true, _, _ => rfl
append_empty := fun
| false => rfl
| true => rfl
}
instance Bool.orMonoid : Monoid Bool := {
append := or
empty := false
append_assoc := fun
| false, _, _ => rfl
| true, _, _ => rfl
append_empty := fun
| false => rfl
| true => rfl
}
inductive Ordering
| lt
| eq
| gt
instance : Monoid Ordering := {
append := fun
| Ordering.lt, _ => Ordering.lt
| Ordering.gt, _ => Ordering.gt
| Ordering.eq, ord => ord
empty := Ordering.eq
append_assoc := fun
| Ordering.lt, _, _ => rfl
| Ordering.gt, _, _ => rfl
| Ordering.eq, _, _ => rfl
append_empty := fun
| Ordering.lt => rfl
| Ordering.gt => rfl
| Ordering.eq => rfl
}
instance {A : Type} : Monoid (List A) := {
append := List.append
empty := List.nil
append_assoc := List.append_assoc
append_empty := List.append_nil
}
instance {Fst Snd : Type} [monoidFst : Monoid Fst] [monoidSnd : Monoid Snd] : Monoid (Fst × Snd) := {
append := fun (fst₁, snd₁) (fst₂, snd₂) =>
(monoidFst.append fst₁ fst₂, monoidSnd.append snd₁ snd₂)
empty := (monoidFst.empty, monoidSnd.empty)
append_assoc := fun (fst₁, snd₁) (fst₂, snd₂) (fst₃, snd₃) => by
simp
rw [monoidFst.append_assoc fst₁ fst₂ fst₃]
rw [monoidSnd.append_assoc snd₁ snd₂ snd₃]
append_empty := fun (fst, snd) => by
simp
rw [monoidFst.append_empty fst]
rw [monoidSnd.append_empty snd]
}
instance Function.endomorphismMonoid {A : Type} : Monoid (A → A) := {
append := Function.comp
empty := id
append_assoc := fun _ _ _ => rfl
append_empty := fun _ => rfl
}
instance Function.codomainMonoid {In Out : Type} [monoidOut : Monoid Out] : Monoid (In → Out) := {
append := fun f₁ f₂ x => monoidOut.append (f₁ x) (f₂ x)
empty := fun _ => monoidOut.empty
append_assoc := fun f₁ f₂ f₃ => by
simp
funext x
rw [monoidOut.append_assoc (f₁ x) (f₂ x) (f₃ x)]
append_empty := fun f => by
simp
funext x
rw [monoidOut.append_empty (f x)]
}
/- Monoid Homomorphisms -/
structure MonoidHom (In Out : Type) where
map : In → Out
monoidIn : Monoid In
monoidOut : Monoid Out
preserve_append : (inin₂ : In) → map (monoidIn.append inin₂) = monoidOut.append (map in₁) (map in₂)
preserve_empty : map monoidIn.empty = monoidOut.empty
def lengthHom {A} : MonoidHom (List A) Nat := {
map := List.length
monoidIn := inferInstanceAs (Monoid (List A))
monoidOut := Nat.addMonoid
preserve_append := fun inin₂ => by
induction inwith
| nil => simp [Monoid.append]
| cons _ tail₁ ih₁ =>
simp [Monoid.append]
simp [Monoid.append] at ih₁
rw [Nat.succ_add]
rw [ih₁]
preserve_empty := rfl
}
end Monoids
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment