Playing with monoids in Lean 4

Monoids.lean

/-
  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 : (in₁ in₂ : In) → map (monoidIn.append in₁ in₂) = 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 in₁ in₂ => by
    induction in₁ with
      | 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