------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the natural coefficients ring solver, using coefficient
-- equality induced by ℕ.
--
-- This is sufficient for proving equalities that are independent of the
-- characteristic.  In particular, this is enough for equalities in
-- rings of characteristic 0.
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Solver.Ring.NaturalCoefficients.Default
  {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where

import Algebra.Properties.Semiring.Mult as SemiringMultiplication
open import Data.Maybe.Base using (Maybe; map)
open import Data.Nat using (_≟_)
open import Relation.Binary.Consequences using (dec⇒weaklyDec)
import Relation.Binary.PropositionalEquality.Core as ≡

open CommutativeSemiring R
open SemiringMultiplication semiring

private
  dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)
  dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≟_ m n)

open import Algebra.Solver.Ring.NaturalCoefficients R dec public