Skip to content

Examples.Classical.CommutativeRing

Worked example: (ℤ, +, *, 0, 1, -) as a commutative ring

This is the Examples.Classical.CommutativeRing module of the Agda Universal Algebra Library.

The integers are the canonical commutative ring; built directly from stdlib's additive abelian-group laws, multiplicative monoid laws, commutativity, and the two distributivity laws. This module discharges the M3-8 acceptance criteria: the worked example ℤ-commutativeRing type-checks, and the bridge to stdlib's CommutativeRing round-trips on ℤ.

The ring's curried accessors are opened under fresh names (_⊕_, _⊗_, ⊝_, e₀, e₁) so they do not clash with Data.Integer's own _+_, _*_, -_.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Examples.Classical.CommutativeRing where

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Integer             using ( ℤ ; _+_ ; _*_ ; 0ℤ ; 1ℤ ; -_ )
open import Data.Integer.Properties  using ( +-assoc ; +-identityˡ ; +-identityʳ
                                           ; +-inverseˡ ; +-inverseʳ ; +-comm
                                           ; *-assoc ; *-identityˡ ; *-identityʳ ; *-comm
                                           ; *-distribˡ-+ ; *-distribʳ-+ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Bundles.CommutativeRing using ( ⟨_⟩ᶜʳᵍ ; ⟪_⟫ᶜʳᵍ )
open import Classical.Small.Structures.CommutativeRing
  using ( CommutativeRing ; eqsToCommutativeRing )

import Classical.Structures.CommutativeRing as Polymorphic

The commutative ring (ℤ, +, *, 0, 1, -)

ℤ-commutativeRing : CommutativeRing
ℤ-commutativeRing =
  eqsToCommutativeRing ℤ _+_ 0ℤ -_ _*_ 1ℤ
    +-assoc +-identityˡ +-identityʳ +-inverseˡ +-inverseʳ +-comm
    *-assoc *-identityˡ *-identityʳ *-comm
    *-distribˡ-+ *-distribʳ-+

open Polymorphic.CommutativeRing-Op ℤ-commutativeRing using ()
  renaming ( _+_ to _⊕_ ; _·_ to _⊗_ ; 0R to e₀ ; 1R to e₁ ; -_ to ⊝_ )

Acceptance checks

The curried accessors compute to the underlying integer operations.

⊕-is-+-cr : ∀ (a b : ℤ) → a ⊕ b ≡ a + b
⊕-is-+-cr a b = refl

⊗-is-*-cr : ∀ (a b : ℤ) → a ⊗ b ≡ a * b
⊗-is-*-cr a b = refl

e₀-is-0ℤ-cr : e₀ ≡ 0ℤ
e₀-is-0ℤ-cr = refl

e₁-is-1ℤ-cr : e₁ ≡ 1ℤ
e₁-is-1ℤ-cr = refl

⊝-is-neg-cr : ∀ (a : ℤ) → ⊝ a ≡ - a
⊝-is-neg-cr a = refl

The bridge to stdlib's CommutativeRing round-trips pointwise on every operation.

open Polymorphic.CommutativeRing-Op ⟪ ⟨ ℤ-commutativeRing ⟩ᶜʳᵍ ⟫ᶜʳᵍ using ()
  renaming ( _+_ to _⊕'_ ; _·_ to _⊗'_ ; 0R to e₀' ; 1R to e₁' ; -_ to ⊝'_ )

roundtrip-⊕-cr : ∀ (a b : ℤ) → a ⊕' b ≡ a + b
roundtrip-⊕-cr a b = refl

roundtrip-⊗-cr : ∀ (a b : ℤ) → a ⊗' b ≡ a * b
roundtrip-⊗-cr a b = refl

roundtrip-e₀-cr : e₀' ≡ 0ℤ
roundtrip-e₀-cr = refl

roundtrip-e₁-cr : e₁' ≡ 1ℤ
roundtrip-e₁-cr = refl

roundtrip-⊝-cr : ∀ (a : ℤ) → ⊝' a ≡ - a
roundtrip-⊝-cr a = refl