    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Almost commutative rings
    ------------------------------------------------------------------------

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

    module Tactic.RingSolver.Core.AlmostCommutativeRing where

    open import Level
    open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
    open import Algebra.Core using (Op₁; Op₂)
    open import Algebra.Structures using (IsCommutativeSemiring)
    open import Algebra.Definitions
    open import Algebra.Bundles using (RawRing; CommutativeRing; CommutativeSemiring)
    import Algebra.Morphism as Morphism
    open import Function.Base using (id)
    open import Level
    open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)

    record IsAlmostCommutativeRing
             {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
             (_+_ _*_ : A → A → A) (-_ : A → A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
        -‿cong                : -_ Preserves _≈_ ⟶ _≈_
        -‿*-distribˡ          : ∀ x y → ((- x) * y)     ≈ (- (x * y))
        -‿+-comm              : ∀ x y → ((- x) + (- y)) ≈ (- (x + y))

      open IsCommutativeSemiring isCommutativeSemiring public

    import Algebra.Definitions.RawSemiring as Exp

    record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
      infix  8 -_
      infixl 7 _*_
      infixl 6 _+_
      infix  4 _≈_
      infixr 8 _^_
      field
        Carrier                 : Set c
        _≈_                     : Rel Carrier ℓ
        _+_                     : Op₂ Carrier
        _*_                     : Op₂ Carrier
        -_                      : Op₁ Carrier
        0#                      : Carrier
        0≟_                     : (x : Carrier) → Maybe (0# ≈ x)
        1#                      : Carrier
        isAlmostCommutativeRing :
          IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

      open IsAlmostCommutativeRing isAlmostCommutativeRing hiding (refl) public
      open import Data.Nat.Base as ℕ using (ℕ)

      commutativeSemiring : CommutativeSemiring _ _
      commutativeSemiring = record
        { isCommutativeSemiring = isCommutativeSemiring
        }

      open CommutativeSemiring commutativeSemiring public
        using
        ( +-semigroup; +-monoid; +-commutativeMonoid
        ; *-semigroup; *-monoid; *-commutativeMonoid
        ; rawSemiring; semiring
        )

      rawRing : RawRing _ _
      rawRing = record
        { _≈_ = _≈_
        ; _+_ = _+_
        ; _*_ = _*_
        ; -_  = -_
        ; 0#  = 0#
        ; 1#  = 1#
        }

      _^_ : Carrier → ℕ → Carrier
      _^_ = Exp._^′_ rawSemiring
      {-# NOINLINE _^_ #-}

      _-_ : Carrier → Carrier → Carrier
      _-_ x y = x + (- y)

      refl : ∀ {x} → x ≈ x
      refl = IsAlmostCommutativeRing.refl isAlmostCommutativeRing

    record _-Raw-AlmostCommutative⟶_
             {r₁ r₂ r₃ r₄}
             (From : RawRing r₁ r₂)
             (To : AlmostCommutativeRing r₃ r₄) : Set (r₁ ⊔ r₂ ⊔ r₃ ⊔ r₄) where
      private
        module F = RawRing From
        module T = AlmostCommutativeRing To
      open Morphism.Definitions F.Carrier T.Carrier T._≈_
      field
        ⟦_⟧    : Morphism
        +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
        *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
        -‿homo : Homomorphic₁ ⟦_⟧ (F.-_)  (T.-_)
        0-homo : Homomorphic₀ ⟦_⟧ F.0#  T.0#
        1-homo : Homomorphic₀ ⟦_⟧ F.1#  T.1#

    -raw-almostCommutative⟶
      : ∀ {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) →
        AlmostCommutativeRing.rawRing R -Raw-AlmostCommutative⟶ R
    -raw-almostCommutative⟶ R = record
      { ⟦_⟧    = id
      ; +-homo = λ _ _ → refl
      ; *-homo = λ _ _ → refl
      ; -‿homo = λ _ → refl
      ; 0-homo = refl
      ; 1-homo = refl
      }
      where open AlmostCommutativeRing R

    -- A homomorphism induces a notion of equivalence on the raw ring.

    Induced-equivalence :
      ∀ {c₁ c₂ c₃ ℓ} {Coeff : RawRing c₁ c₂} {R : AlmostCommutativeRing c₃ ℓ} →
      Coeff -Raw-AlmostCommutative⟶ R → Rel (RawRing.Carrier Coeff) ℓ
    Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧
      where
      open AlmostCommutativeRing R
      open _-Raw-AlmostCommutative⟶_ morphism

    ------------------------------------------------------------------------
    -- Conversions

    -- Commutative rings are almost commutative rings.

    fromCommutativeRing : ∀ {r₁ r₂} (CR : CommutativeRing r₁ r₂) →
                          (open CommutativeRing CR) →
                          (∀ x → Maybe (0# ≈ x)) →
                          AlmostCommutativeRing _ _
    fromCommutativeRing CR 0≟_ = record
      { isAlmostCommutativeRing = record
          { isCommutativeSemiring = isCommutativeSemiring
          ; -‿cong                = -‿cong
          ; -‿*-distribˡ          = λ x y → sym (-‿distribˡ-* x y)
          ; -‿+-comm              = ⁻¹-∙-comm
          }
      ; 0≟_ = 0≟_
      }
      where
      open CommutativeRing CR
      open import Algebra.Properties.Ring ring
      open import Algebra.Properties.AbelianGroup +-abelianGroup

    fromCommutativeSemiring : ∀ {r₁ r₂} (CS : CommutativeSemiring r₁ r₂)
                              (open CommutativeSemiring CS) →
                              (∀ x → Maybe (0# ≈ x)) →
                              AlmostCommutativeRing _ _
    fromCommutativeSemiring CS 0≟_ = record
      { -_                      = id
      ; isAlmostCommutativeRing = record
          { isCommutativeSemiring = isCommutativeSemiring
          ; -‿cong                = id
          ; -‿*-distribˡ          = λ _ _ → refl
          ; -‿+-comm              = λ _ _ → refl
          }
      ; 0≟_ = 0≟_
      }
      where open CommutativeSemiring CS