Rings characterized by a fused multiply-add operator and negative one

Fumula.agda

{-# OPTIONS --cubical-compatible --safe --postfix-projections #-}
module Fumula where
open import Level renaming (suc to ℓsuc; zero to ℓzero)
open import Function using (id)
open import Data.Product
open import Algebra
open import Algebra.Morphism
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
import Algebra.Properties.Ring as RingProperties

{-
  Structure:
  C : Set
  □ : C
  - ⟪ - ⟫ - : C × C × C → C

  Convenience definitions:
  -ˢ ≝ □ ⟪ - ⟫ □
  ◆ ≝ □ˢ
  ◯ ≝ ◆ˢ

  Axioms:
  □ ⟪ a ⟫ b = b ⟪ a ⟫ □
  ◆ ⟪ a ⟫ b = b ⟪ a ⟫ ◆ = a
  ◯ ⟪ a ⟫ b = b ⟪ a ⟫ ◯ = ◯ ⟪ b ⟫ a = a ⟪ b ⟫ ◯
  ◯ ⟪ ◆ ⟫ a = a ⟪ ◆ ⟫ ◯ = a
  □ ⟪ a ⟫ a = a ⟪ a ⟫ □ = ◆
  a ⟪ b ⟪ c ⟫ d ⟫ e = b ⟪ a ⟪ c ⟫ e ⟫ d
  (a ⟪ b ⟫ c) ⟪ d ⟫ e = (a ⟪ ◆ ⟫ c) ⟪ b ⟪ d ⟫ e ⟫ e
  a ⟪ b ⟫ (c ⟪ d ⟫ e) = a ⟪ a ⟪ b ⟫ d ⟫ (c ⟪ ◆ ⟫ e)
  (a ⟪ ◆ ⟫ b) ⟪ c ⟫ d = a ⟪ c ⟫ (b ⟪ ◆ ⟫ d)

  Theorems:
  ◯ ⟪ a ⟫ (◯ ⟪ b ⟫ c) = ◯ ⟪ ◯ ⟪ a ⟫ b ⟫ c
  ◯ ⟪ a ⟫ (b ⟪ c ⟫ d) = ◯ ⟪ c ⟫ (b ⟪ a ⟫ d)
  ◯ ⟪ a ⟫ (b ⟪ ◆ ⟫ c) = b ⟪ a ⟫ c

  Conventional representation:
  a ∙ b ≝ a ⟪ ◆ ⟫ b
  a + b ≝ ◯ ⟪ a ⟫ b
  -a ≝ □ ⟪ ◆ ⟫ a
  a - b ≝ □ ⟪ a ⟫ b
  1 ≝ ◯
  0 ≝ ◆
  -1 ≝ □
-}

record RawFumula c ℓ : Set (ℓsuc (c ⊔ ℓ)) where
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    -1# : Carrier -- -1# ≈ - 1#
    fma : Carrier → Carrier → Carrier → Carrier -- "fused multiply-add", fma x y z ≈ (x * y) + z

  0# : Carrier
  0# = fma -1# -1# -1#

  1# : Carrier
  1# = fma -1# -1# 0#

  rawRing : RawRing c ℓ
  rawRing .RawRing.Carrier = Carrier
  rawRing .RawRing._≈_ = _≈_
  rawRing .RawRing._+_ x y = fma 1# x y
  rawRing .RawRing._*_ x y = fma x y 0#
  rawRing .RawRing.-_ x = fma -1# x 0#
  rawRing .RawRing.0# = 0#
  rawRing .RawRing.1# = 1#
  open RawRing rawRing public hiding (Carrier; _≈_; 0#; 1#)

  fms : Carrier → Carrier → Carrier → Carrier -- "fused multiply-subtract" (note the inverted convention)
  fms x y z = - fma x y (- z)

  nfma : Carrier → Carrier → Carrier → Carrier -- "negated fused multiply-add"
  nfma x y z = - fma x y z

  nfms : Carrier → Carrier → Carrier → Carrier -- "negated fused multiply-subtract" (note the inverted convention)
  nfms x y z = fma x y (- z)

module _ {c ℓ} (rawRing : RawRing c ℓ) where
  open RawRing rawRing

  RawRing→RawFumula : RawFumula c ℓ
  RawRing→RawFumula .RawFumula.Carrier = Carrier
  RawRing→RawFumula .RawFumula._≈_ = _≈_
  RawRing→RawFumula .RawFumula.-1# = - 1#
  RawRing→RawFumula .RawFumula.fma x y z = x * y + z

record IsFumula {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (-1# : A) (fma : A → A → A → A) : Set (a ⊔ ℓ) where
  private
    0# = fma -1# -1# -1#
    1# = fma -1# -1# 0#
  field
    isEquivalence : IsEquivalence _≈_
    fma-cong : ∀{x y u v r s} → x ≈ y → u ≈ v → r ≈ s → fma x u r ≈ fma y v s
    fma-distrib₁ : ∀ v w x y z → fma (fma v w x) y z ≈ fma (fma v w 0#) y (fma x y z) -- (v * w + x) * y + z ≈ (v * w + 0) * y + (x * y + z)
    fma-distrib₂ : ∀ v w x y z → fma v (fma w x y) z ≈ fma v (fma w x 0#) (fma v y z) -- v * (w * x + y) + z ≈ v * (w * x + 0) + (v * y + z)
    fma-distrib₃ : ∀ v w x y z → fma v w (fma x y z) ≈ fma x y (fma v w z) -- v * w + (x * y + z) ≈ x * y + (v * w + z)
    fma-1#-comm₁₂ : ∀ x y → fma 1# x y ≈ fma x 1# y -- 1 * x + y ≈ x * 1 + y
    fma-identityˡ : ∀ x → fma 1# x 0# ≈ x -- 1 * x + 0 ≈ x
    fma-annihilateˡ : ∀ x y → fma 0# x y ≈ y -- 0 * x + y ≈ y
    fma-annihilateʳ : ∀ x y → fma x 0# y ≈ y -- x * 0 + y ≈ y
    fma-comm₂₃ : ∀ x y → fma 1# x y ≈ fma 1# y x -- 1 * x + y ≈ 1 * y + x
    fma‿-1#-collapse : ∀ x → fma -1# x x ≈ 0# -- -1 * x + x ≈ 0#
    fma-assoc₁₂₂ : ∀ w x y z → fma (fma w x 0#) y z ≈ fma w (fma x y 0#) z -- (w * x + 0) * y + z ≈ w * (x * y + 0) + z

  open IsEquivalence isEquivalence
  open SetoidReasoning (record { isEquivalence = isEquivalence })

  fma-assoc₁₁₂ : ∀ w x y z → fma w (fma x y 0#) z ≈ fma (fma w x 0#) y z -- w * (x * y + 0) + z ≈ (w * x + 0) * y + z
  fma-assoc₁₁₂ w x y z =
    sym (fma-assoc₁₂₂ w x y z)

  fma-0#-comm₁₂ : ∀ x y → fma 0# x y ≈ fma x 0# y -- 0 * x + y ≈ x * 0 + y
  fma-0#-comm₁₂ x y =
    begin fma 0# x y ≈⟨ fma-annihilateˡ x y ⟩ y ≈⟨ sym (fma-annihilateʳ x y) ⟩ fma x 0# y ∎

  fma-identityʳ : ∀ x  → fma x 1# 0# ≈ x -- x * 1 + 0 ≈ x
  fma-identityʳ x =
    begin fma x 1# 0# ≈⟨ sym (fma-1#-comm₁₂ x 0#) ⟩ fma 1# x 0# ≈⟨ fma-identityˡ x ⟩ x ∎

  fma-comm₁₃ : ∀ x y → fma x 1# y ≈ fma y 1# x -- x * 1 + y ≈ y * 1 + x
  fma-comm₁₃ x y =
    begin fma x 1# y ≈⟨ sym (fma-1#-comm₁₂ x y) ⟩ fma 1# x y ≈⟨ fma-comm₂₃ x y ⟩ fma 1# y x ≈⟨ fma-1#-comm₁₂ y x ⟩ fma y 1# x ∎

  fma-assoc₂₂₃ : ∀ x y z → fma 1# x (fma 1# y z) ≈ fma 1# (fma 1# x y) z -- 1 * x + (1 * y + z) = 1 * (1 * x + y) + z
  fma-assoc₂₂₃ x y z =
    begin
      fma 1# x (fma 1# y z)
    ≈⟨ fma-comm₂₃ x (fma 1# y z) ⟩
      fma 1# (fma 1# y z) x
    ≈⟨ fma-distrib₂ 1# 1# y z x ⟩
      fma 1# (fma 1# y 0#) (fma 1# z x)
    ≈⟨ fma-cong refl (fma-identityˡ y) refl ⟩
      fma 1# y (fma 1# z x)
    ≈⟨ fma-distrib₃ 1# y 1# z x ⟩
      fma 1# z (fma 1# y x)
    ≈⟨ fma-comm₂₃ z (fma 1# y x) ⟩
      fma 1# (fma 1# y x) z
    ≈⟨ fma-cong refl (fma-comm₂₃ y x) refl ⟩
      fma 1# (fma 1# x y) z
    ∎

  fma-assoc₂₁₃ : ∀ x y z → fma 1# x (fma y 1# z) ≈ fma 1# (fma x 1# y) z -- 1 * x + (y * 1 + z) = 1 * (x * 1 + y) + z
  fma-assoc₂₁₃ x y z =
    begin
      fma 1# x (fma y 1# z)
    ≈⟨ fma-cong refl refl (sym (fma-1#-comm₁₂ y z)) ⟩
      fma 1# x (fma 1# y z)
    ≈⟨ fma-assoc₂₂₃ x y z ⟩
      fma 1# (fma 1# x y) z
    ≈⟨ fma-cong refl (fma-1#-comm₁₂ x y) refl ⟩
      fma 1# (fma x 1# y) z
    ∎

  fma-assoc₁₂₃ : ∀ x y z → fma x 1# (fma 1# y z) ≈ fma (fma 1# x y) 1# z -- x * 1 + (1 * y + z) = (1 * x + y) * 1 + z
  fma-assoc₁₂₃ x y z =
    begin
      fma x 1# (fma 1# y z)
    ≈⟨ sym (fma-1#-comm₁₂ x (fma 1# y z)) ⟩
      fma 1# x (fma 1# y z)
    ≈⟨ fma-assoc₂₂₃ x y z ⟩
      fma 1# (fma 1# x y) z
    ≈⟨ fma-1#-comm₁₂ (fma 1# x y) z ⟩
      fma (fma 1# x y) 1# z
    ∎

  fma-assoc₁₁₃ : ∀ x y z → fma x 1# (fma y 1# z) ≈ fma (fma x 1# y) 1# z -- x * 1 + (y * 1 + z) = (x * 1 + y) * 1 + z
  fma-assoc₁₁₃ x y z =
    begin
      fma x 1# (fma y 1# z)
    ≈⟨ sym (fma-1#-comm₁₂ x (fma y 1# z)) ⟩
      fma 1# x (fma y 1# z)
    ≈⟨ fma-cong refl refl (sym (fma-1#-comm₁₂ y z)) ⟩
      fma 1# x (fma 1# y z)
    ≈⟨ fma-assoc₂₂₃ x y z ⟩
      fma 1# (fma 1# x y) z
    ≈⟨ fma-cong refl (fma-1#-comm₁₂ x y) refl ⟩
      fma 1# (fma x 1# y) z
    ≈⟨ fma-1#-comm₁₂ (fma x 1# y) z ⟩
      fma (fma x 1# y) 1# z
    ∎

  fma-comm-inner₃ : ∀ w x y z → fma 1# (fma w x y) z ≈ fma 1# (fma w x z) y -- 1 * (w * x + y) + z ≈ 1 * (w * x + z) + y
  fma-comm-inner₃ w x y z =
    begin
      fma 1# (fma w x y) z
    ≈⟨ fma-distrib₂ 1# w x y z ⟩
      fma 1# (fma w x 0#) (fma 1# y z)
    ≈⟨ fma-cong refl refl (fma-comm₂₃ y z) ⟩
      fma 1# (fma w x 0#) (fma 1# z y)
    ≈⟨ sym (fma-distrib₂ 1# w x z y) ⟩
      fma 1# (fma w x z) y
    ∎

  fma-fuse : ∀ x y z → fma 1# (fma x y 0#) z ≈ fma x y z -- 1 * (x * y + 0) + z ≈ x * y + z
  fma-fuse x y z =
    begin
      fma 1# (fma x y 0#) z
    ≈⟨ fma-comm-inner₃ x y 0# z ⟩
      fma 1# (fma x y z) 0#
    ≈⟨ fma-identityˡ (fma x y z) ⟩
      fma x y z
    ∎

  private
    rawFumula : RawFumula a ℓ
    rawFumula = record { _≈_ = _≈_; -1# = -1#; fma = fma }
  open RawFumula rawFumula using (_+_; _*_; -_; fms)

  isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.isMonoid
    .IsMonoid.isSemigroup
    .IsSemigroup.isMagma
    .IsMagma.isEquivalence =
      isEquivalence
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.isMonoid
    .IsMonoid.isSemigroup
    .IsSemigroup.isMagma
    .IsMagma.∙-cong x≈y u≈v =
      fma-cong refl x≈y u≈v
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.isMonoid
    .IsMonoid.isSemigroup
    .IsSemigroup.assoc x y z =
      begin
        fma 1# (fma 1# x y) z
      ≈⟨ sym (fma-assoc₂₂₃ x y z) ⟩
        fma 1# x (fma 1# y z)
      ∎
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.isMonoid
    .IsMonoid.identity
    .proj₁ x =
      begin
        fma 1# 0# x
      ≈⟨ fma-annihilateʳ 1# x ⟩
        x
      ∎
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.isMonoid
    .IsMonoid.identity
    .proj₂ x =
      begin
        fma 1# x 0#
      ≈⟨ fma-identityˡ x ⟩
        x
      ∎
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.inverse
    .proj₁ x =
      begin
        fma 1# (fma -1# x 0#) x
      ≈⟨ fma-fuse -1# x x ⟩
        fma -1# x x
      ≈⟨ fma‿-1#-collapse x ⟩
        0#
      ∎
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.inverse
    .proj₂ x =
      begin
        fma 1# x (fma -1# x 0#)
      ≈⟨ fma-comm₂₃ x (fma -1# x 0#) ⟩
        fma 1# (fma -1# x 0#) x
      ≈⟨ fma-fuse -1# x x ⟩
        fma -1# x x
      ≈⟨ fma‿-1#-collapse x ⟩
        0#
      ∎
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.isGroup
    .IsGroup.⁻¹-cong x≈y =
      fma-cong refl x≈y refl
  isRing
    .IsRing.+-isAbelianGroup
    .IsAbelianGroup.comm x y =
      begin
        fma 1# x y
      ≈⟨ fma-comm₂₃ x y ⟩
        fma 1# y x
      ∎
  isRing
    .IsRing.*-isMonoid
    .IsMonoid.isSemigroup
    .IsSemigroup.isMagma
    .IsMagma.isEquivalence =
      isEquivalence
  isRing
    .IsRing.*-isMonoid
    .IsMonoid.isSemigroup
    .IsSemigroup.isMagma
    .IsMagma.∙-cong x≈y u≈v =
      fma-cong x≈y u≈v refl
  isRing
    .IsRing.*-isMonoid
    .IsMonoid.isSemigroup
    .IsSemigroup.assoc x y z =
      begin
        fma (fma x y 0#) z 0#
      ≈⟨ fma-assoc₁₂₂ x y z 0# ⟩
        fma x (fma y z 0#) 0#
      ∎
  isRing
    .IsRing.*-isMonoid
    .IsMonoid.identity
    .proj₁ x =
      begin
        fma 1# x 0#
      ≈⟨ fma-identityˡ x ⟩
        x
      ∎
  isRing
    .IsRing.*-isMonoid
    .IsMonoid.identity
    .proj₂ x =
      begin
        fma x 1# 0#
      ≈⟨ fma-identityʳ x ⟩
        x
      ∎
  isRing
    .IsRing.distrib
    .proj₁ x y z =
      begin
        fma x (fma 1# y z) 0#
      ≈⟨ fma-distrib₂ x 1# y z 0# ⟩
        fma x (fma 1# y 0#) (fma x z 0#)
      ≈⟨ fma-cong refl (fma-identityˡ y) refl ⟩
        fma x y (fma x z 0#)
      ≈⟨ sym (fma-fuse x y (fma x z 0#)) ⟩
        fma 1# (fma x y 0#) (fma x z 0#)
      ∎
  isRing
    .IsRing.distrib
    .proj₂ x y z =
      begin
        fma (fma 1# y z) x 0#
      ≈⟨ fma-distrib₁ 1# y z x 0# ⟩
        fma (fma 1# y 0#) x (fma z x 0#)
      ≈⟨ fma-cong (fma-identityˡ y) refl refl ⟩
        fma y x (fma z x 0#)
      ≈⟨ sym (fma-fuse y x (fma z x 0#)) ⟩
        fma 1# (fma y x 0#) (fma z x 0#)
      ∎
  isRing
    .IsRing.zero
    .proj₁ x =
      begin
        fma 0# x 0#
      ≈⟨ fma-annihilateˡ x 0# ⟩
        0#
      ∎
  isRing
    .IsRing.zero
    .proj₂ x =
      begin
        fma x 0# 0#
      ≈⟨ fma-annihilateʳ x 0# ⟩
        0#
      ∎

  open IsRing isRing public hiding (isEquivalence; refl; sym; trans)
  open RingProperties (record { isRing = isRing }) public

  -‿1#≈-1# : -1# ≈ (- 1#)
  -‿1#≈-1# =
    sym (fma-identityʳ -1#)


  x*-1#≈-x : ∀{x} → (x * -1#) ≈ (- x)
  x*-1#≈-x {x} =
    begin
      (x * -1#)
    ≈⟨ *-cong refl -‿1#≈-1# ⟩
       (x * (- 1#))
    ≈⟨ sym (-‿distribʳ-* x 1#) ⟩
       (- (x * 1#))
    ≈⟨ -‿cong (*-identityʳ x) ⟩
       (- x)
    ∎

  fma‿-1#-comm₁₂ : ∀ x y → fma -1# x y ≈ fma x -1# y -- -1 * x + y ≈ x * -1 + y
  fma‿-1#-comm₁₂ x y =
    begin
      fma -1# x y
    ≈⟨ sym (fma-fuse -1# x y) ⟩
      ((- x) + y)
    ≈⟨ +-cong (sym x*-1#≈-x) refl ⟩
      ((x * -1#) + y)
    ≈⟨ fma-fuse x -1# y ⟩
      fma x -1# y
    ∎

  fms-rearrangeˡ : ∀ x y z → fms x y z ≈ fma (- x) y z
  fms-rearrangeˡ x y z =
    begin
      fms x y z
    ≈⟨ fma-distrib₂ -1# x y (- z) 0# ⟩
      fma -1# (x * y) (- (- z))
    ≈⟨ fma-cong refl refl (-‿involutive z) ⟩
      fma -1# (x * y) z
    ≈⟨ fma-assoc₁₁₂ -1# x y z ⟩
      fma (- x) y z
    ∎

  fms-rearrangeʳ : ∀ x y z → fms x y z ≈ fma x (- y) z
  fms-rearrangeʳ x y z =
    begin
      fms x y z
    ≈⟨ fms-rearrangeˡ x y z ⟩
      fma (- x) y z
    ≈⟨ fma-cong (fma‿-1#-comm₁₂ x 0#) refl refl ⟩
      fma (x * -1#) y z
    ≈⟨ fma-assoc₁₂₂ x -1# y z ⟩
      fma x (- y) z
    ∎

module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} {_+_ _*_ : Op₂ A} { -_ : Op₁ A} {0# 1# : A} (isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) where
  open IsRing isRing

  private
    rawRing : RawRing a ℓ
    rawRing .RawRing.Carrier = A
    rawRing .RawRing._≈_ = _≈_
    rawRing .RawRing._+_ = _+_
    rawRing .RawRing._*_ = _*_
    rawRing .RawRing.-_ = -_
    rawRing .RawRing.0# = 0#
    rawRing .RawRing.1# = 1#

    rawFumula : RawFumula a ℓ
    rawFumula = RawRing→RawFumula rawRing

  open RawFumula rawFumula using (-1#; fma)
  open SetoidReasoning setoid
  open RingProperties (record { isRing = isRing })

  private
    -1#*x≈-x : ∀{x} → (-1# * x) ≈ (- x)
    -1#*x≈-x {x} =
      begin
        ((- 1#) * x)
      ≈⟨ sym (-‿distribˡ-* 1# x) ⟩
        (- (1# * x))
      ≈⟨ -‿cong (*-identityˡ x) ⟩
        (- x)
      ∎

    -1#*-1#≈1# : (-1# * -1#) ≈ 1#
    -1#*-1#≈1# =
      begin
        ((- 1#) * (- 1#))
      ≈⟨ -1#*x≈-x ⟩
        (- (- 1#))
      ≈⟨ -‿involutive 1# ⟩
        1#
      ∎

    0#-fma-defined : fma -1# -1# -1# ≈ 0#
    0#-fma-defined =
      begin
        (((- 1#) * (- 1#)) + (- 1#))
      ≈⟨ +-cong -1#*-1#≈1# refl ⟩
        (1# + (- 1#))
      ≈⟨ -‿inverseʳ 1# ⟩
        0#
      ∎

    1#-fma-defined-partial : fma -1# -1# 0# ≈ 1#
    1#-fma-defined-partial =
      begin
        (((- 1#) * (- 1#)) + 0#)
      ≈⟨ +-cong -1#*-1#≈1# refl ⟩
        (1# + 0#)
      ≈⟨ +-identityʳ 1# ⟩
        1#
      ∎

    1#-fma-defined : fma -1# -1# (fma -1# -1# -1#) ≈ 1#
    1#-fma-defined =
      begin
        (((- 1#) * (- 1#)) + (((- 1#) * (- 1#)) + (- 1#)))
      ≈⟨ +-cong refl 0#-fma-defined ⟩
        (((- 1#) * (- 1#)) + 0#)
      ≈⟨ 1#-fma-defined-partial ⟩
        1#
      ∎

    fma-cong : ∀{x y u v r s} → x ≈ y → u ≈ v → r ≈ s → fma x u r ≈ fma y v s
    fma-cong x≈y u≈v r≈s = +-cong (*-cong x≈y u≈v) r≈s

  IsRing→IsFumula : IsFumula _≈_ -1# fma
  IsRing→IsFumula .IsFumula.isEquivalence =
    isEquivalence
  IsRing→IsFumula .IsFumula.fma-cong =
    fma-cong
  IsRing→IsFumula .IsFumula.fma-distrib₁ v w x y z =
    begin
      fma (fma v w x) y z
    ≈⟨ +-cong (distribʳ y (v * w) x) refl ⟩
      (fma (v * w) y (x * y) + z)
    ≈⟨ +-assoc ((v * w) * y) (x * y) z ⟩
      fma (v * w) y (fma x y z)
    ≈⟨ fma-cong (sym (+-identityʳ (v * w))) refl refl ⟩
      fma (fma v w 0#) y (fma x y z)
    ≈⟨ fma-cong (fma-cong refl refl (sym 0#-fma-defined)) refl refl ⟩
      fma (fma v w (fma -1# -1# -1#)) y (fma x y z)
    ∎
  IsRing→IsFumula .IsFumula.fma-distrib₂ v w x y z =
    begin
      fma v (fma w x y) z
    ≈⟨ +-cong (distribˡ v (w * x) y) refl ⟩
      (fma v (w * x) (v * y) + z)
    ≈⟨ +-assoc (v * (w * x)) (v * y) z ⟩
      fma v (w * x) (fma v y z)
    ≈⟨ fma-cong refl (sym (+-identityʳ (w * x))) refl ⟩
      fma v (fma w x 0#) (fma v y z)
    ≈⟨ fma-cong refl (fma-cong refl refl (sym 0#-fma-defined)) refl ⟩
      fma v (fma w x (fma -1# -1# -1#)) (fma v y z)
    ∎
  IsRing→IsFumula .IsFumula.fma-distrib₃ v w x y z =
    begin
      fma v w (fma x y z)
    ≈⟨ sym (+-assoc (v * w) (x * y) z) ⟩
      (fma v w (x * y) + z)
    ≈⟨ +-cong (+-comm (v * w) (x * y)) refl ⟩
      (fma x y (v * w) + z)
    ≈⟨ +-assoc (x * y) (v * w) z ⟩
      fma x y (fma v w z)
    ∎
  IsRing→IsFumula .IsFumula.fma-1#-comm₁₂ x y =
    begin
      fma (fma -1# -1# (fma -1# -1# -1#)) x y
    ≈⟨ fma-cong 1#-fma-defined refl refl ⟩
      fma 1# x y
    ≈⟨ +-cong (*-identityˡ x) refl ⟩
      (x + y)
    ≈⟨ +-cong (sym (*-identityʳ x)) refl ⟩
      fma x 1# y
    ≈⟨ fma-cong refl (sym 1#-fma-defined) refl ⟩
      fma x (fma -1# -1# (fma -1# -1# -1#)) y
    ∎
  IsRing→IsFumula .IsFumula.fma-identityˡ x =
    begin
      fma (fma -1# -1# (fma -1# -1# -1#)) x (fma -1# -1# -1#)
    ≈⟨ fma-cong 1#-fma-defined refl 0#-fma-defined ⟩
      fma 1# x 0#
    ≈⟨ +-identityʳ (1# * x) ⟩
      (1# * x)
    ≈⟨ *-identityˡ x ⟩
      x
    ∎
  IsRing→IsFumula .IsFumula.fma-annihilateˡ x y =
    begin
      fma (fma -1# -1# -1#) x y
    ≈⟨ fma-cong 0#-fma-defined refl refl ⟩
      fma 0# x y
    ≈⟨ +-cong (zeroˡ x) refl ⟩
      (0# + y)
    ≈⟨ +-identityˡ y ⟩
      y
    ∎
  IsRing→IsFumula .IsFumula.fma-annihilateʳ x y =
    begin
      fma x (fma -1# -1# -1#) y
    ≈⟨ fma-cong refl 0#-fma-defined refl ⟩
      fma x 0# y
    ≈⟨ +-cong (zeroʳ x) refl ⟩
      (0# + y)
    ≈⟨ +-identityˡ y ⟩
      y
    ∎
  IsRing→IsFumula .IsFumula.fma-comm₂₃ x y =
    begin
      fma (fma -1# -1# (fma -1# -1# -1#)) x y
    ≈⟨ fma-cong 1#-fma-defined refl refl ⟩
      fma 1# x y
    ≈⟨ +-cong (*-identityˡ x) refl ⟩
      (x + y)
    ≈⟨ +-comm x y ⟩
      (y + x)
    ≈⟨ +-cong (sym (*-identityˡ y)) refl ⟩
      fma 1# y x
    ≈⟨ fma-cong (sym 1#-fma-defined) refl refl ⟩
      fma (fma -1# -1# (fma -1# -1# -1#)) y x
    ∎
  IsRing→IsFumula .IsFumula.fma‿-1#-collapse x =
    begin
      fma -1# x x
    ≈⟨ +-cong -1#*x≈-x refl ⟩
      ((- x) + x)
    ≈⟨ -‿inverseˡ x ⟩
      0#
    ≈⟨ sym 0#-fma-defined ⟩
      fma -1# -1# -1#
    ∎
  IsRing→IsFumula .IsFumula.fma-assoc₁₂₂ w x y z =
    begin
      fma (fma w x (fma -1# -1# -1#)) y z
    ≈⟨ fma-cong (fma-cong refl refl 0#-fma-defined) refl refl ⟩
      fma (fma w x 0#) y z
    ≈⟨ fma-cong (+-identityʳ (w * x)) refl refl ⟩
      fma (w * x) y z
    ≈⟨ +-cong (*-assoc w x y) refl ⟩
      fma w (x * y) z
    ≈⟨ fma-cong refl (sym (+-identityʳ (x * y))) refl ⟩
      fma w (fma x y 0#) z
    ≈⟨ fma-cong refl (fma-cong refl refl (sym 0#-fma-defined)) refl ⟩
      fma w (fma x y (fma -1# -1# -1#)) z
    ∎

record Fumula c ℓ : Set (ℓsuc (c ⊔ ℓ)) where
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    -1# : Carrier
    fma : Carrier → Carrier → Carrier → Carrier
    isFumula : IsFumula _≈_ -1# fma

  rawFumula : RawFumula c ℓ
  rawFumula = record { _≈_ = _≈_; -1# = -1#; fma = fma }
  open RawFumula rawFumula public hiding (Carrier; _≈_; -1#; fma)
  open IsFumula isFumula public

  ring : Ring c ℓ
  ring = record { isRing = isRing }
  open Ring ring public using
    ( +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup; +-group; +-abelianGroup
    ; *-magma; *-semigroup
    ; +-monoid ; +-commutativeMonoid
    ; *-monoid
    ; nearSemiring; semiringWithoutOne; semiringWithoutAnnihilatingZero; semiring
    )

Ring→Fumula : ∀{c ℓ} → Ring c ℓ → Fumula c ℓ
Ring→Fumula ring = record { isFumula = IsRing→IsFumula isRing }
  where open Ring ring

module _ {c ℓ} (ring : Ring c ℓ) where
  private
    ringFromFumula : Ring c ℓ
    ringFromFumula = Fumula.ring (Ring→Fumula ring)

    module FromFumula = Ring ringFromFumula

  open Ring ring
  open RingProperties ring
  open SetoidReasoning setoid

  private
    -1# : Carrier
    -1# = - 1#

    -1#*-1#≈1# : -1# * -1# ≈ 1#
    -1#*-1#≈1# =
      begin
        (-1# * -1#)
      ≈⟨ sym (-‿distribˡ-* 1# -1#) ⟩
        (- (1# * -1#))
      ≈⟨ -‿cong (*-identityˡ -1#) ⟩
        (- -1#)
      ≈⟨ -‿involutive 1# ⟩
        1#
      ∎

    fma‿-1#‿-1#‿-1#≈0# : (-1# * -1#) + -1# ≈ 0#
    fma‿-1#‿-1#‿-1#≈0# =
      begin
        ((-1# * -1#) + -1#)
      ≈⟨ +-cong -1#*-1#≈1# refl ⟩
        (1# + -1#)
      ≈⟨ -‿inverseʳ 1# ⟩
        0#
      ∎

    fma‿-1#‿-1#‿0#≈1# : (-1# * -1#) + 0# ≈ 1#
    fma‿-1#‿-1#‿0#≈1# =
      begin
        ((-1# * -1#) + 0#)
      ≈⟨ +-cong -1#*-1#≈1# refl ⟩
        (1# + 0#)
      ≈⟨ +-identityʳ 1# ⟩
        1#
      ∎

    fma‿-1#‿-1#‿fma‿-1#‿-1#‿-1#≈1# : (-1# * -1#) + ((-1# * -1#) + -1#) ≈ 1#
    fma‿-1#‿-1#‿fma‿-1#‿-1#‿-1#≈1# =
      begin
        ((-1# * -1#) + ((-1# * -1#) + -1#))
      ≈⟨ +-cong refl fma‿-1#‿-1#‿-1#≈0# ⟩
        ((-1# * -1#) + 0#)
      ≈⟨ fma‿-1#‿-1#‿0#≈1# ⟩
        1#
      ∎

  ring∘Ring→Fumula-isRingIsomorphism : IsRingIsomorphism rawRing FromFumula.rawRing id
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.+-isGroupHomomorphism
    .IsGroupHomomorphism.isMonoidHomomorphism
    .IsMonoidHomomorphism.isMagmaHomomorphism
    .IsMagmaHomomorphism.isRelHomomorphism =
      record { cong = id }
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.+-isGroupHomomorphism
    .IsGroupHomomorphism.isMonoidHomomorphism
    .IsMonoidHomomorphism.isMagmaHomomorphism
    .IsMagmaHomomorphism.homo x y =
      begin
        (x + y)
      ≈⟨ +-cong (sym (*-identityˡ x)) refl ⟩
        ((1# * x) + y)
      ≈⟨ +-cong (*-cong (sym fma‿-1#‿-1#‿fma‿-1#‿-1#‿-1#≈1#) refl) refl ⟩
        ((((-1# * -1#) + ((-1# * -1#) + -1#)) * x) + y)
      ≈⟨ refl ⟩
        (x FromFumula.+ y)
      ∎
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.+-isGroupHomomorphism
    .IsGroupHomomorphism.isMonoidHomomorphism
    .IsMonoidHomomorphism.ε-homo =
      begin
        0#
      ≈⟨ sym fma‿-1#‿-1#‿-1#≈0# ⟩
        ((-1# * -1#) + -1#)
      ≈⟨ refl ⟩
        FromFumula.0#
      ∎
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.+-isGroupHomomorphism
    .IsGroupHomomorphism.⁻¹-homo x =
      begin
        (- x)
      ≈⟨ -‿cong (sym (*-identityˡ x)) ⟩
        (- (1# * x))
      ≈⟨ sym (+-identityʳ (- (1# * x))) ⟩
        (- (1# * x) + 0#)
      ≈⟨ +-cong (-‿distribˡ-* 1# x) (sym fma‿-1#‿-1#‿-1#≈0#) ⟩
        ((-1# * x) + ((-1# * -1#) + -1#))
      ≈⟨ refl ⟩
        (FromFumula.- x)
      ∎
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.*-isMonoidHomomorphism
    .IsMonoidHomomorphism.isMagmaHomomorphism
    .IsMagmaHomomorphism.isRelHomomorphism =
      record { cong = id }
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.*-isMonoidHomomorphism
    .IsMonoidHomomorphism.isMagmaHomomorphism
    .IsMagmaHomomorphism.homo x y =
      begin
        (x * y)
      ≈⟨ sym (+-identityʳ (x * y)) ⟩
        ((x * y) + 0#)
      ≈⟨ +-cong refl (sym fma‿-1#‿-1#‿-1#≈0#) ⟩
        ((x * y) + ((-1# * -1#) + -1#))
      ≈⟨ refl ⟩
        (x FromFumula.* y)
      ∎
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.isRingHomomorphism
    .IsRingHomomorphism.*-isMonoidHomomorphism
    .IsMonoidHomomorphism.ε-homo =
      begin
        1#
      ≈⟨ sym fma‿-1#‿-1#‿fma‿-1#‿-1#‿-1#≈1# ⟩
        ((-1# * -1#) + ((-1# * -1#) + -1#))
      ≈⟨ refl ⟩
        FromFumula.1#
      ∎
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.isRingMonomorphism
    .IsRingMonomorphism.injective =
      id
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.surjective x
    .proj₁ =
      x
  ring∘Ring→Fumula-isRingIsomorphism
    .IsRingIsomorphism.surjective _
    .proj₂ =
      refl

ReversibleFumula.agda

{-# OPTIONS --cubical-compatible --safe --postfix-projections #-}
module ReversibleFumula where
open import Level renaming (suc to ℓsuc; zero to ℓzero)
open import Function using (id)
open import Data.Product
open import Algebra
open import Algebra.Morphism
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Fumula as _

{-
  Additional axiom:
    a ⟪ b ⟫ c = c ⟪ b ⟫ a
-}

record IsReversibleFumula {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (-1# : A) (fma : A → A → A → A) : Set (a ⊔ ℓ) where
  private
    0# = fma -1# -1# -1#
    1# = fma -1# -1# 0#
  field
    isEquivalence : IsEquivalence _≈_
    fma-cong : ∀{x y u v r s} → x ≈ y → u ≈ v → r ≈ s → fma x u r ≈ fma y v s
    fma-distrib₁ : ∀ v w x y z → fma (fma v w x) y z ≈ fma (fma v w 0#) y (fma x y z) -- (v * w + x) * y + z ≈ (v * w + 0) * y + (x * y + z)
    fma-distrib₃ : ∀ v w x y z → fma v w (fma x y z) ≈ fma x y (fma v w z) -- v * w + (x * y + z) ≈ x * y + (v * w + z)
    fma-identityˡ : ∀ x → fma 1# x 0# ≈ x -- 1 * x + 0 ≈ x
    fma-annihilateˡ : ∀ x y → fma 0# x y ≈ y -- 0 * x + y ≈ y
    fma-comm₂₃ : ∀ x y → fma 1# x y ≈ fma 1# y x -- 1 * x + y ≈ 1 * y + x
    fma‿-1#-collapse : ∀ x → fma -1# x x ≈ 0# -- -1 * x + x ≈ x
    fma-assoc₁₂₂ : ∀ w x y z → fma (fma w x 0#) y z ≈ fma w (fma x y 0#) z -- (w * x + 0) * y + z ≈ w * (x * y + 0) + z
    fma-comm₁₂ : ∀ x y z → fma x y z ≈ fma y x z -- x * y + z ≈ y * x + z

  open IsEquivalence isEquivalence
  open SetoidReasoning (record { isEquivalence = isEquivalence })

  isFumula : IsFumula _≈_ -1# fma
  isFumula .IsFumula.isEquivalence =
    isEquivalence
  isFumula .IsFumula.fma-cong =
    fma-cong
  isFumula .IsFumula.fma-distrib₁ =
    fma-distrib₁
  isFumula .IsFumula.fma-distrib₂ v w x y z =
    begin
      fma v (fma w x y) z
    ≈⟨ fma-comm₁₂ v (fma w x y) z ⟩
      fma (fma w x y) v z
    ≈⟨ fma-distrib₁ w x y v z ⟩
      fma (fma w x 0#) v (fma y v z)
    ≈⟨ fma-cong refl refl (fma-comm₁₂ y v z) ⟩
      fma (fma w x 0#) v (fma v y z)
    ≈⟨ fma-comm₁₂ (fma w x 0#) v (fma v y z) ⟩
      fma v (fma w x 0#) (fma v y z)
    ∎
  isFumula .IsFumula.fma-distrib₃ =
    fma-distrib₃
  isFumula .IsFumula.fma-1#-comm₁₂ =
    fma-comm₁₂ 1#
  isFumula .IsFumula.fma-identityˡ =
    fma-identityˡ
  isFumula .IsFumula.fma-annihilateˡ =
    fma-annihilateˡ
  isFumula .IsFumula.fma-annihilateʳ x y =
    begin
      fma x 0# y
    ≈⟨ fma-comm₁₂ x 0# y ⟩
      fma 0# x y
    ≈⟨ fma-annihilateˡ x y ⟩
      y
    ∎
  isFumula .IsFumula.fma-comm₂₃ =
    fma-comm₂₃
  isFumula .IsFumula.fma‿-1#-collapse =
    fma‿-1#-collapse
  isFumula .IsFumula.fma-assoc₁₂₂ =
    fma-assoc₁₂₂
  open IsFumula isFumula public hiding
    ( isEquivalence
    ; fma-cong
    ; fma-distrib₁
    ; fma-distrib₃
    ; fma-identityˡ
    ; fma-annihilateˡ
    ; fma-comm₂₃
    ; fma‿-1#-collapse
    ; fma-assoc₁₂₂
    )

  private
    rawFumula : RawFumula a ℓ
    rawFumula = record { _≈_ = _≈_; -1# = -1#; fma = fma }
  open RawFumula rawFumula using (_+_; _*_; -_)

  isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
  isCommutativeRing .IsCommutativeRing.isRing =
    isRing
  isCommutativeRing .IsCommutativeRing.*-comm x y =
    fma-comm₁₂ x y 0#

  open IsCommutativeRing isCommutativeRing public using
    ( *-isCommutativeMagma; *-isCommutativeSemigroup; *-isCommutativeMonoid
    ; isCommutativeSemiringWithoutOne; isCommutativeSemiring
    )

module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} {_+_ _*_ : Op₂ A} { -_ : Op₁ A} {0# 1# : A} (isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#) where
  open IsCommutativeRing isCommutativeRing

  private
    -1# : A
    -1# = - 1#

    fma : A → A → A → A
    fma x y z = (x * y) + z

    isFumula : IsFumula _≈_ -1# fma
    isFumula = IsRing→IsFumula isRing

  IsCommutativeRing→IsReversibleFumula : IsReversibleFumula _≈_ -1# fma
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.isEquivalence =
    isFumula .IsFumula.isEquivalence
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-cong =
    isFumula .IsFumula.fma-cong
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-distrib₁ =
    isFumula .IsFumula.fma-distrib₁
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-distrib₃ =
    isFumula .IsFumula.fma-distrib₃
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-identityˡ =
    isFumula .IsFumula.fma-identityˡ
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-annihilateˡ =
    isFumula .IsFumula.fma-annihilateˡ
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-comm₂₃ =
    isFumula .IsFumula.fma-comm₂₃
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma‿-1#-collapse =
    isFumula .IsFumula.fma‿-1#-collapse
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-assoc₁₂₂ =
    isFumula .IsFumula.fma-assoc₁₂₂
  IsCommutativeRing→IsReversibleFumula .IsReversibleFumula.fma-comm₁₂ x y _ =
    +-cong (*-comm x y) refl

record ReversibleFumula c ℓ : Set (ℓsuc (c ⊔ ℓ)) where
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    -1# : Carrier
    fma : Carrier → Carrier → Carrier → Carrier
    isReversibleFumula : IsReversibleFumula _≈_ -1# fma

  rawFumula : RawFumula c ℓ
  rawFumula = record { _≈_ = _≈_; -1# = -1#; fma = fma }
  open RawFumula rawFumula public hiding (Carrier; _≈_; -1#; fma)
  open IsReversibleFumula isReversibleFumula public

  fumula : Fumula c ℓ
  fumula = record { isFumula = isFumula }
  open Fumula fumula public using (ring)

  commutativeRing : CommutativeRing c ℓ
  commutativeRing = record { isCommutativeRing = isCommutativeRing }
  open CommutativeRing commutativeRing public using
    ( +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne; semiringWithoutAnnihilatingZero; semiring; commutativeSemiring
    )

CommutativeRing→ReversibleFumula : ∀{c ℓ} → CommutativeRing c ℓ → ReversibleFumula c ℓ
CommutativeRing→ReversibleFumula commutativeRing = record { isReversibleFumula = IsCommutativeRing→IsReversibleFumula isCommutativeRing }
  where open CommutativeRing commutativeRing

module _ {c ℓ} (commutativeRing : CommutativeRing c ℓ) where
  private
    commutativeRingFromReversibleFumula : CommutativeRing c ℓ
    commutativeRingFromReversibleFumula = ReversibleFumula.commutativeRing (CommutativeRing→ReversibleFumula commutativeRing)

    module FromReversibleFumula = CommutativeRing commutativeRingFromReversibleFumula

  open CommutativeRing commutativeRing

  commutativeRing∘CommutativeRing→ReversibleFumula-isRingIsomorphism : IsRingIsomorphism rawRing FromReversibleFumula.rawRing id
  commutativeRing∘CommutativeRing→ReversibleFumula-isRingIsomorphism = ring∘Ring→Fumula-isRingIsomorphism ring