Skip to content

Instantly share code, notes, and snippets.

@Rotsor
Last active May 24, 2017 23:02
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Rotsor/021b532e5828ac2fd8af57654fc96bf8 to your computer and use it in GitHub Desktop.
Save Rotsor/021b532e5828ac2fd8af57654fc96bf8 to your computer and use it in GitHub Desktop.
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ʳ
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment