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

open import Algebra
import Algebra.Operations
open import Relation.Nullary

module Algebra.RingSolver.Natural-coefficients
         {r₁ r₂}
         (R : CommutativeSemiring r₁ r₂)
         (dec : let open CommutativeSemiring R
                    open Algebra.Operations semiring in
                ∀ m n → Dec (m × 1# ≈ n × 1#)) where

import Algebra.RingSolver
open import Algebra.RingSolver.AlmostCommutativeRing
open import Data.Nat as ℕ
open import Data.Product using (module Σ)
open import Function
import Relation.Binary.EqReasoning
import Relation.Nullary.Decidable as Dec

open CommutativeSemiring R
open Algebra.Operations semiring
open Relation.Binary.EqReasoning setoid

private

  -- The coefficient "ring".

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

  -- There is a homomorphism from ℕ to R.
  --
  -- Note that _×′_ is used rather than _×_. 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 → Dec (m ×′ 1# ≈ n ×′ 1#)
  dec′ m n = Dec.map′ to from (dec m n)
    where
    to : m × 1# ≈ n × 1# → m ×′ 1# ≈ n ×′ 1#
    to m≈n = begin
      m ×′ 1#  ≈⟨ sym $ ×≈×′ m 1# ⟩
      m ×  1#  ≈⟨ m≈n ⟩
      n ×  1#  ≈⟨ ×≈×′ n 1# ⟩
      n ×′ 1#  ∎

    from : m ×′ 1# ≈ n ×′ 1# → m × 1# ≈ n × 1#
    from m≈n = begin
      m ×  1#  ≈⟨ ×≈×′ m 1# ⟩
      m ×′ 1#  ≈⟨ m≈n ⟩
      n ×′ 1#  ≈⟨ sym $ ×≈×′ n 1# ⟩
      n ×  1#  ∎

-- The instantiation.

open Algebra.RingSolver _ _ homomorphism dec′ public