module Problem10 where

open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

infixl 15 _⋆_

postulate
  C : Set
  _⋆_ : C → C → C
  _ᵒ : C → C
  assoc : ∀ a b c → (a ⋆ b) ⋆ c ≡ a ⋆ (b ⋆ c)
  ᵒ-prop : ∀ a → a ⋆ a ᵒ ⋆ a ≡ a

_ᶜ : C → C
x ᶜ = x ᵒ ⋆ x ⋆ x ᵒ

prop₁ : ∀ a → a ⋆ a ᶜ ⋆ a ≡ a
prop₁ a = begin
  a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ⋆ a ≡˘⟨ cong (_⋆ a) (assoc a (a ᵒ ⋆ a) (a ᵒ)) ⟩
  a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ≡˘⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (assoc a (a ᵒ) a) ⟩
  a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a   ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (ᵒ-prop a) ⟩
  a ⋆ a ᵒ ⋆ a             ≡⟨ ᵒ-prop a ⟩
  a                       ∎
prop₂ : ∀ a → a ᶜ ⋆ a ⋆ a ᶜ ≡ a ᶜ
prop₂ a = begin
  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ≡˘⟨ assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ ⋆ a) (a ᵒ) ⟩
  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ) a) ⟩
  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ   ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩
  a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩
  a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (ᵒ-prop a) ⟩
  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ             ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩
  a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ           ≡⟨ cong (_⋆ (a ᵒ)) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩
  a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ           ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) (ᵒ-prop a) ⟩
  a ᵒ ⋆ a ⋆ a ᵒ                       ∎

postulate
  commute : ∀ a b → a ⋆ a ≡ a → b ⋆ b ≡ b → a ⋆ b ≡ b ⋆ a

uniqueness : ∀ a z →  a ⋆ z ⋆ a ≡ a
                   →  z ⋆ a ⋆ z ≡ z
                   →  z ≡ a ᶜ
uniqueness a z aza≡a zaz≡z = begin
  z                         ≡˘⟨ zaz≡z ⟩
  z ⋆ a ⋆ z                 ≡˘⟨ cong (λ - → z ⋆ - ⋆ z) (ᵒ-prop a) ⟩
  z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ z     ≡˘⟨ cong (_⋆ z) (assoc z (a ⋆ a ᵒ) a) ⟩
  z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ z     ≡⟨ assoc (z ⋆ (a ⋆ a ᵒ)) a z ⟩
  z ⋆ (a ⋆ a ᵒ) ⋆ (a ⋆ z)   ≡⟨ assoc z (a ⋆ a ᵒ) (a ⋆ z) ⟩
  z ⋆ ((a ⋆ a ᵒ) ⋆ (a ⋆ z)) ≡⟨ cong (z ⋆_) (commute (a ⋆ a ᵒ) (a ⋆ z) aaᵒaaᵒ≡aaᵒ azaz≡az) ⟩
  z ⋆ ((a ⋆ z) ⋆ (a ⋆ a ᵒ)) ≡˘⟨ assoc z (a ⋆ z) (a ⋆ a ᵒ) ⟩
  z ⋆ (a ⋆ z) ⋆ (a ⋆ a ᵒ)   ≡˘⟨ cong (_⋆ (a ⋆ a ᵒ)) (assoc z a z) ⟩
  z ⋆ a ⋆ z ⋆ (a ⋆ a ᵒ)     ≡⟨ cong (_⋆ (a ⋆ a ᵒ)) zaz≡z ⟩
  z ⋆ (a ⋆ a ᵒ)             ≡˘⟨ assoc z a (a ᵒ) ⟩
  z ⋆ a ⋆ a ᵒ               ≡˘⟨ cong (λ - → z ⋆ - ⋆ (a ᵒ)) (ᵒ-prop a) ⟩
  z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ   ≡˘⟨ cong (_⋆ a ᵒ) (assoc z (a ⋆ a ᵒ) a) ⟩
  z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ   ≡˘⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc z a (a ᵒ)) ⟩
  z ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ     ≡⟨ cong (_⋆ a ᵒ) (assoc (z ⋆ a) (a ᵒ) a) ⟩
  z ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ   ≡⟨ cong (_⋆ a ᵒ) (commute (z ⋆ a) (a ᵒ ⋆ a) zaza≡za aᵒaaᵒa≡aᵒa) ⟩
  a ᵒ ⋆ a ⋆ (z ⋆ a) ⋆ a ᵒ   ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a) z a) ⟩
  a ᵒ ⋆ a ⋆ z ⋆ a ⋆ a ᵒ     ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a z) ⟩
  a ᵒ ⋆ (a ⋆ z) ⋆ a ⋆ a ᵒ   ≡⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ z) a) ⟩
  a ᵒ ⋆ (a ⋆ z ⋆ a) ⋆ a ᵒ   ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) aza≡a ⟩
  a ᵒ ⋆ a ⋆ a ᵒ             ∎
  where
  zaza≡za : z ⋆ a ⋆ (z ⋆ a) ≡ z ⋆ a
  zaza≡za = begin
    z ⋆ a ⋆ (z ⋆ a) ≡˘⟨ assoc (z ⋆ a) z a ⟩
    z ⋆ a ⋆ z ⋆ a   ≡⟨ cong (_⋆ a) zaz≡z ⟩
    z ⋆ a           ∎

  azaz≡az : a ⋆ z ⋆ (a ⋆ z) ≡ a ⋆ z
  azaz≡az = begin
    a ⋆ z ⋆ (a ⋆ z) ≡˘⟨ assoc (a ⋆ z) a z ⟩
    a ⋆ z ⋆ a ⋆ z   ≡⟨ cong (_⋆ z) aza≡a ⟩
    a ⋆ z           ∎

  aᵒaaᵒa≡aᵒa : a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ≡ a ᵒ ⋆ a
  aᵒaaᵒa≡aᵒa = begin
    a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a)   ≡⟨ assoc (a ᵒ) a (a ᵒ ⋆ a) ⟩
    a ᵒ ⋆ (a ⋆ (a ᵒ ⋆ a)) ≡˘⟨ cong (a ᵒ ⋆_) (assoc a (a ᵒ) a) ⟩
    a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a)   ≡⟨ cong (a ᵒ ⋆_) (ᵒ-prop a) ⟩
    a ᵒ ⋆ a               ∎

  aaᵒaaᵒ≡aaᵒ : a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡ a ⋆ a ᵒ
  aaᵒaaᵒ≡aaᵒ = begin
    a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡˘⟨ assoc (a ⋆ a ᵒ) a (a ᵒ) ⟩
    a ⋆ a ᵒ ⋆ a ⋆ a ᵒ   ≡⟨ cong (_⋆ a ᵒ) (ᵒ-prop a) ⟩
    a ⋆ a ᵒ             ∎