problem3.agda

module problem3 where

-- see:
-- https://www.reddit.com/r/DailyProver/comments/6d4oct/finite_cancellative_semigroups/
-- https://coq-math-problems.github.io/Problem3/

open import Relation.Binary.PropositionalEquality
open import Data.Product

Injective : {A B : Set} → (f : A → B) → Set
Injective f = ∀ x y → f x ≡ f y → x ≡ y

Surjective : {A B : Set} → (f : A → B) → Set
Surjective f = ∀ fx → ∃ (λ x → f x ≡ fx)

Dedekind-finite : Set → Set
Dedekind-finite X = ∀ {f : X → X} → Injective f → Surjective f

record Assumptions : Set₁ where
 field
  A : Set
  finite : Dedekind-finite A
  add : A → A → A
  assoc : ∀ a b c → add (add a b) c ≡ add a (add b c)
  cancellationʳ : ∀ x a b → add a x ≡ add b x → a ≡ b
  cancellationˡ : ∀ x a b → add x a ≡ add x b → a ≡ b
  nonempty : A
  
record Result (AA : Assumptions) : Set where
 open Assumptions AA
 field
  identity : A
  inverse : A → A
  identityˡ : ∀ x → add identity x ≡ x
  identityʳ : ∀ x → add x identity ≡ x
  inverseˡ : ∀ x → add (inverse x) x ≡ identity
  inverseʳ : ∀ x → add x (inverse x) ≡ identity

module _ (AA : Assumptions) where
  open Assumptions AA

  example = nonempty

  subtract : A → A → A
  subtract a b = proj₁ (finite (cancellationʳ b) a)

  subtract-law : ∀ a b → add (subtract a b) b ≡ a
  subtract-law a b = proj₂ (finite (cancellationʳ b) a)

  identity = subtract example example

  identityʳ : ∀ x → add x identity ≡ x
  identityʳ x = cancellationʳ example _ _ (
    trans
      (assoc _ _ _)
      (cong (add x)
         (subtract-law example example)))

  identityˡ : ∀ x → add identity x ≡ x
  identityˡ x =
    cancellationˡ example _ _ (trans
      (sym (assoc example identity x))
      (cong (λ z → add z x) (identityʳ example)))

  inverse = λ x → subtract identity x

  inverseˡ : ∀ x → add (inverse x) x ≡ identity
  inverseˡ = subtract-law identity
  
  inverseʳ : ∀ x → add x (inverse x) ≡ identity
  inverseʳ x =
    cancellationʳ x _ _
      (trans
        (trans (assoc _ _ _) (trans (cong (add x) (inverseˡ x))
        ((identityʳ _)))) (sym (identityˡ _)))

  result : Result AA
  result = record
             { identity = identity
             ; inverse = inverse
             ; identityˡ = identityˡ
             ; identityʳ = identityʳ
             ; inverseˡ = inverseˡ
             ; inverseʳ = inverseʳ
             }