https://golem.ph.utexas.edu/category/2015/06/semigroup_puzzles.html

SemigroupPuzzles.agda

module SemigroupPuzzles where

open import Algebra
open import Function

module _ {c ℓ} (S : Semigroup c ℓ)
       (open Semigroup S)
       (assumption : (e f : Carrier) → e ∙ f ∙ e ≈ e)
       where

  open import Relation.Binary.EqReasoning setoid

  puzzle₁ : (x y z : Carrier) → x ∙ y ∙ z ≈ x ∙ z
  puzzle₁ x y z =
    begin
    x ∙ y ∙ z             ≈⟨ ∙-cong refl (sym $ assumption z x) ⟩
    x ∙ y ∙ (z ∙ x ∙ z)   ≈⟨ lemma ⟩
    (x ∙ (y ∙ z) ∙ x) ∙ z ≈⟨ ∙-cong (assumption x (y ∙ z)) refl ⟩
    x ∙ z
    ∎ where
    
    lemma : x ∙ y ∙ (z ∙ x ∙ z) ≈ (x ∙ (y ∙ z) ∙ x) ∙ z
    lemma =
      begin
      x ∙ y ∙ (z ∙ x ∙ z)     ≈⟨ assoc x y (z ∙ x ∙ z) ⟩
      x ∙ (y ∙ (z ∙ x ∙ z))   ≈⟨ ∙-cong refl (∙-cong refl (assoc z x z)) ⟩
      x ∙ (y ∙ (z ∙ (x ∙ z))) ≈⟨ ∙-cong refl (sym $ assoc y z (x ∙ z)) ⟩
      x ∙ (y ∙ z ∙ (x ∙ z))   ≈⟨ sym $ assoc x (y ∙ z) (x ∙ z) ⟩
      x ∙ (y ∙ z) ∙ (x ∙ z)   ≈⟨ sym $ assoc (x ∙ (y ∙ z)) x z ⟩
      (x ∙ (y ∙ z) ∙ x) ∙ z
      ∎

  puzzle₂ : (x : Carrier) → x ∙ x ≈ x
  puzzle₂ x =
    begin
    x ∙ x           ≈⟨ ∙-cong refl (sym $ assumption x x) ⟩
    x ∙ (x ∙ x ∙ x) ≈⟨ sym $ assoc x (x ∙ x) x ⟩
    x ∙ (x ∙ x) ∙ x ≈⟨ assumption x (x ∙ x) ⟩
    x
    ∎