    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Instantiates the ring solver, using the natural numbers as the
    -- coefficient "ring"
    ------------------------------------------------------------------------

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

    open import Algebra using (RawRing; CommutativeSemiring )
    import Algebra.Properties.Semiring.Mult as SemiringMultiplication
    open import Data.Maybe.Base using (Maybe; just; nothing; map)

    module Algebra.Solver.Ring.NaturalCoefficients
      {r₁ r₂} (R : CommutativeSemiring r₁ r₂)
      (open CommutativeSemiring R)
      (open SemiringMultiplication semiring using () renaming (_×_ to _×ᵤ_))
      (dec : ∀ m n → Maybe (m ×ᵤ 1# ≈ n ×ᵤ 1#)) where

    open import Algebra.Solver.Ring.AlmostCommutativeRing
    open import Data.Nat.Base as ℕ using (ℕ; _+_; _*_)
    open import Data.Product.Base using (module Σ)
    open import Function.Base using (id)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_)

    open import Algebra.Properties.Semiring.Mult.TCOptimised semiring
    open import Relation.Binary.Reasoning.Setoid setoid

    private

      -- The coefficient "ring".

      ℕ-ring : RawRing _ _
      ℕ-ring = record
        { Carrier = ℕ
        ; _≈_     = _≡_
        ; _+_     = ℕ._+_
        ; _*_     = ℕ._*_
        ; -_      = id
        ; 0#      = 0
        ; 1#      = 1
        }

      -- There is a homomorphism from ℕ to R.
      --
      -- Note that the optimised _×_ is used rather than unoptimised _×ᵤ_.
      -- If _×ᵤ_ were used, then Function.Related.TypeIsomorphisms.test
      -- would fail to type-check.

      homomorphism : ℕ-ring -Raw-AlmostCommutative⟶ fromCommutativeSemiring R
      homomorphism = record
        { ⟦_⟧    = λ n → n × 1#
        ; +-homo = ×-homo-+ 1#
        ; *-homo = ×1-homo-*
        ; -‿homo = λ _ → refl
        ; 0-homo = refl
        ; 1-homo = refl
        }

      -- Equality of certain expressions can be decided.

      dec′ : ∀ m n → Maybe (m × 1# ≈ n × 1#)
      dec′ m n = map to (dec m n)
        where
        to : m ×ᵤ 1# ≈ n ×ᵤ 1# → m × 1# ≈ n × 1#
        to m≈n = begin
          m ×  1#  ≈⟨ ×ᵤ≈× m 1# ⟨
          m ×ᵤ 1#  ≈⟨  m≈n ⟩
          n ×ᵤ 1#  ≈⟨  ×ᵤ≈× n 1# ⟩
          n ×  1#  ∎

    -- The instantiation.

    open import Algebra.Solver.Ring _ _ homomorphism dec′ public