A proof that formal power series over an arbitrary commutative ring form a commutative ring, formalized in Agda using guarded coinduction.

PowerSeries.agda

{-# OPTIONS --guardedness --safe #-}

open import Data.Product
open import Function using (_$_)
open import Relation.Binary using (IsEquivalence)
open import Algebra
open import Relation.Binary.Definitions
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

open import Tactic.RingSolver using (solve-∀)
open import Tactic.RingSolver.Core.AlmostCommutativeRing
  using (AlmostCommutativeRing; fromCommutativeRing)

module PowerSeries {a ℓ} (C : CommutativeRing a ℓ) where

open CommutativeRing C using () renaming
  (Carrier to A; _≈_ to _≈ₐ_; _*_ to _*ₐ_; _+_ to _+ₐ_; -_ to -ₐ_; 0# to 0ₐ; 1# to 1ₐ)

-- Solver for equations in A
acr : AlmostCommutativeRing a ℓ
acr = fromCommutativeRing C λ _ → nothing
  where open import Data.Maybe.Base using (nothing)

-- The main carrier type: infinite sequences of A's, representing a power series
record FPS : Set a where
  coinductive
  field -- represents hd + x * tl
    hd : A
    tl : FPS

open FPS

infix 4 _≈_
record _≈_ (xs : FPS) (ys : FPS) : Set ℓ where
  coinductive
  field
    hd-≈ : hd xs ≈ₐ hd ys
    tl-≈ : tl xs ≈ tl ys

open _≈_

refl : Reflexive _≈_
refl .hd-≈ = C .CommutativeRing.refl
refl .tl-≈ = refl

sym : Symmetric _≈_
sym x≈y .hd-≈ = C .CommutativeRing.sym (x≈y .hd-≈)
sym x≈y .tl-≈ = sym (x≈y .tl-≈)

trans : Transitive _≈_
trans i≈j j≈k .hd-≈ = C .CommutativeRing.trans (i≈j .hd-≈) (j≈k .hd-≈)
trans i≈j j≈k .tl-≈ = trans (i≈j .tl-≈) (j≈k .tl-≈)

isEquivalence : IsEquivalence _≈_
isEquivalence .IsEquivalence.refl = refl
isEquivalence .IsEquivalence.sym = sym
isEquivalence .IsEquivalence.trans = trans

------------------------------------------------------------------------
-- Addition
------------------------------------------------------------------------

infixl 6 _+_

_+_ : FPS → FPS → FPS
(a + b) .hd = hd a +ₐ hd b
(a + b) .tl = tl a + tl b

+-cong : Congruent₂ _≈_ _+_
+-cong x≈y u≈v .hd-≈ = C .CommutativeRing.+-cong (hd-≈ x≈y) (hd-≈ u≈v)
+-cong x≈y u≈v .tl-≈ = +-cong (tl-≈ x≈y) (tl-≈ u≈v)

+-magma : IsMagma _≈_ _+_
+-magma .IsMagma.isEquivalence = isEquivalence
+-magma .IsMagma.∙-cong = +-cong

+-assoc : Associative _≈_ _+_
+-assoc x y z .hd-≈ = C .CommutativeRing.+-assoc (hd x) (hd y) (hd z)
+-assoc x y z .tl-≈ = +-assoc (tl x) (tl y) (tl z)

+-semigroup : IsSemigroup _≈_ _+_
+-semigroup .IsSemigroup.isMagma = +-magma
+-semigroup .IsSemigroup.assoc = +-assoc

0# : FPS
0# .hd = 0ₐ
0# .tl = 0#

+-identity : Identity _≈_ 0# _+_
+-identity .proj₁ x .hd-≈ = C .CommutativeRing.+-identity .proj₁ (hd x)
+-identity .proj₁ x .tl-≈ = +-identity .proj₁ (tl x)
+-identity .proj₂ x .hd-≈ = C .CommutativeRing.+-identity .proj₂ (hd x)
+-identity .proj₂ x .tl-≈ = +-identity .proj₂ (tl x)

+-monoid : IsMonoid _≈_ _+_ 0#
+-monoid .IsMonoid.isSemigroup = +-semigroup
+-monoid .IsMonoid.identity = +-identity

infix 8 -_
-_ : FPS → FPS
(- a) .hd = -ₐ hd a
(- a) .tl = - tl a

-‿cong : Congruent₁ _≈_ -_
-‿cong x≈y .hd-≈ = C .CommutativeRing.-‿cong (hd-≈ x≈y)
-‿cong x≈y .tl-≈ = -‿cong (tl-≈ x≈y)

-‿inverse : Inverse _≈_ 0# -_ _+_
-‿inverse .proj₁ x .hd-≈ = C .CommutativeRing.-‿inverse .proj₁ (hd x)
-‿inverse .proj₁ x .tl-≈ = -‿inverse .proj₁ (tl x)
-‿inverse .proj₂ x .hd-≈ = C .CommutativeRing.-‿inverse .proj₂ (hd x)
-‿inverse .proj₂ x .tl-≈ = -‿inverse .proj₂ (tl x)

+-group : IsGroup _≈_ _+_ 0# -_
+-group .IsGroup.isMonoid = +-monoid
+-group .IsGroup.inverse = -‿inverse
+-group .IsGroup.⁻¹-cong = -‿cong

+-comm : Commutative _≈_ _+_
+-comm x y .hd-≈ = C .CommutativeRing.+-comm (hd x) (hd y)
+-comm x y .tl-≈ = +-comm (tl x) (tl y)

+-abelian : IsAbelianGroup _≈_ _+_ 0# -_
+-abelian .IsAbelianGroup.isGroup = +-group
+-abelian .IsAbelianGroup.comm = +-comm

------------------------------------------------------------------------
-- Multiplication
------------------------------------------------------------------------

infixl 7 _*_ _*ₛ_

-- Multiplication by a scalar
_*ₛ_ : A → FPS → FPS
(a *ₛ x) .hd = a *ₐ hd x
(a *ₛ x) .tl = a *ₛ tl x

*ₛ-cong : ∀ {a₁ a₂ x₁ x₂} → a₁ ≈ₐ a₂ → x₁ ≈ x₂ → (a₁ *ₛ x₁) ≈ (a₂ *ₛ x₂)
*ₛ-cong aeq xeq .hd-≈ = C .CommutativeRing.*-cong aeq (hd-≈ xeq)
*ₛ-cong aeq xeq .tl-≈ = *ₛ-cong aeq (tl-≈ xeq)

-- Fused multiply-add: fma x y z = x + (y * z)
-- (a + bx) + (c + dx)(e + fx) = (a + ce) + (b + cf + d(e + fx))x
fma : FPS → FPS → FPS → FPS
fma x y z .hd = hd x +ₐ (hd y *ₐ hd z)
fma x y z .tl = fma (tl x + hd y *ₛ tl z) (tl y) z

_*_ : FPS → FPS → FPS
x * y = fma 0# x y

fma-cong : ∀ {x₁ x₂ y₁ y₂ z₁ z₂}
         → x₁ ≈ x₂ → y₁ ≈ y₂ → z₁ ≈ z₂
         → fma x₁ y₁ z₁ ≈ fma x₂ y₂ z₂
fma-cong xeq yeq zeq .hd-≈ = +ₐ-cong (hd-≈ xeq)
                                    (*ₐ-cong (hd-≈ yeq) (hd-≈ zeq))
  where open CommutativeRing C renaming (+-cong to +ₐ-cong; *-cong to *ₐ-cong)
fma-cong xeq yeq zeq .tl-≈ = fma-cong (+-cong (tl-≈ xeq) (*ₛ-cong (hd-≈ yeq) (tl-≈ zeq))) (tl-≈ yeq) zeq

*-cong : Congruent₂ _≈_ _*_
*-cong x≈y u≈v = fma-cong refl x≈y u≈v

*-magma : IsMagma _≈_ _*_
*-magma .IsMagma.isEquivalence = isEquivalence
*-magma .IsMagma.∙-cong = *-cong

fma-def' : ∀ {a b y z res}
  → res ≈ fma (a + b) y z
  → res ≈ (a + fma b y z)
fma-def' k .hd-≈ = tr (hd-≈ k) (+a _ _ _)
  where open CommutativeRing C using () renaming (+-assoc to +a; trans to tr)
fma-def' k .tl-≈ = fma-def' $ trans (tl-≈ k) $ fma-cong (+-assoc _ _ _) refl refl

fma-def : ∀ x y z → fma x y z ≈ (x + y * z)
fma-def x y z = begin
  fma x y z ≈˘⟨ fma-cong (+-identity .proj₂ _) refl refl ⟩
  fma (x + 0#) y z ≈⟨ fma-def' refl ⟩
  x + y * z ∎
  where open ≈-Reasoning record { isEquivalence = isEquivalence }

fma-r' : ∀ x y z res
  → fma (x + hd z *ₛ tl y) y (tl z) ≈ res
  → fma (x + hd y *ₛ tl z) (tl y) z ≈ res
fma-r' x y z res k .hd-≈ = C .CommutativeRing.trans (lemma _ _ _ _ _) (hd-≈ k)
  where lemma : ∀ x y z y' z'
          → x +ₐ y *ₐ z' +ₐ y' *ₐ z ≈ₐ x +ₐ z *ₐ y' +ₐ y *ₐ z'
        lemma = solve-∀ acr
fma-r' x y z res k .tl-≈ = fma-r' _ _ _ _ $ begin
  fma (tl x + hd y *ₛ tl (tl z) + hd z *ₛ tl (tl y)) (tl y) (tl z)
    ≈⟨ fma-cong (lemma _ _ _) refl refl ⟩
  fma (tl x + hd z *ₛ tl (tl y) + hd y *ₛ tl (tl z)) (tl y) (tl z)
    ≈⟨ tl-≈ k ⟩
  tl res ∎
  where open ≈-Reasoning record { isEquivalence = isEquivalence }
        lemma : ∀ a b c → a + b + c ≈ a + c + b
        lemma a b c = begin
          (a + b) + c ≈⟨ +-assoc _ _ _ ⟩
          a + (b + c) ≈⟨ +-cong refl (+-comm _ _) ⟩
          a + (c + b) ≈˘⟨ +-assoc _ _ _ ⟩
          (a + c) + b ∎

fma-r : ∀ {x y z}
  → fma (x + hd y *ₛ tl z) (tl y) z ≈ fma (x + hd z *ₛ tl y) y (tl z)
fma-r = fma-r' _ _ _ _ refl

fma-comm : ∀ {x y z res}
  → res ≈ fma x y z
  → res ≈ fma x z y
fma-comm k .hd-≈ = tr (hd-≈ k) (+c r (*c _ _))
  where open CommutativeRing C using ()
             renaming (refl to r; trans to tr; +-cong to +c; *-comm to *c)
fma-comm k .tl-≈ = fma-comm $ trans (tl-≈ k) fma-r

*-comm : Commutative _≈_ _*_
*-comm _ _ = fma-comm refl

*ₛ-distrib-l : ∀ {a x y} → a *ₛ (x + y) ≈ a *ₛ x + a *ₛ y
*ₛ-distrib-l .hd-≈ = C .CommutativeRing.distrib .proj₁ _ _ _
*ₛ-distrib-l .tl-≈ = *ₛ-distrib-l

*ₛ-distrib-r : ∀ {a b x} → (a +ₐ b) *ₛ x ≈ a *ₛ x + b *ₛ x
*ₛ-distrib-r .hd-≈ = C .CommutativeRing.distrib .proj₂ _ _ _
*ₛ-distrib-r .tl-≈ = *ₛ-distrib-r

fma-distrib-r' : ∀ {a b x y z res}
  → res ≈ fma (a + b) (y + z) x
  → res ≈ fma a y x + fma b z x
fma-distrib-r' k .hd-≈ = C .CommutativeRing.trans (hd-≈ k) $ lemma _ _ _ _ _
  where lemma : ∀ a b x y z → a +ₐ b +ₐ (y +ₐ z) *ₐ x ≈ₐ (a +ₐ y *ₐ x) +ₐ (b +ₐ z *ₐ x)
        lemma = solve-∀ acr
fma-distrib-r' k .tl-≈ = fma-distrib-r' $ trans (tl-≈ k) $ fma-cong (lemma _ _ _ _ _) refl refl
  where open ≈-Reasoning record { isEquivalence = isEquivalence }
        lemma : ∀ a b x y z → a + b + (y +ₐ z) *ₛ x ≈ (a + y *ₛ x) + (b + z *ₛ x)
        lemma a b x y z = begin
          a + b + (y +ₐ z) *ₛ x ≈⟨ +-cong refl *ₛ-distrib-r ⟩
          a + b + (y *ₛ x + z *ₛ x) ≈⟨ +-assoc _ _ _ ⟩
          a + (b + (y *ₛ x + z *ₛ x)) ≈⟨ +-cong refl (sym $ +-assoc _ _ _) ⟩
          a + (b + y *ₛ x + z *ₛ x) ≈⟨ +-cong refl (+-cong (+-comm _ _) refl) ⟩
          a + (y *ₛ x + b + z *ₛ x) ≈⟨ +-cong refl (+-assoc _ _ _) ⟩
          a + (y *ₛ x + (b + z *ₛ x)) ≈⟨ sym (+-assoc _ _ _) ⟩
          (a + y *ₛ x) + (b + z *ₛ x) ∎

*-distrib-+-r : ∀ x y z → (y + z) * x ≈ y * x + z * x
*-distrib-+-r _ _ _ = trans (fma-cong (sym $ +-identity .proj₁ _) refl refl)
                            (fma-distrib-r' refl)

*ₛ-assoc : ∀ {x y z} → (x *ₐ y) *ₛ z ≈ x *ₛ (y *ₛ z)
*ₛ-assoc .hd-≈ = C .CommutativeRing.*-assoc _ _ _
*ₛ-assoc .tl-≈ = *ₛ-assoc

*ₛ-assoc-distrib : ∀ a x y z res
  → res ≈ fma (x *ₛ a) (x *ₛ y) z
  → res ≈ x *ₛ fma a y z
*ₛ-assoc-distrib a x y z res k .hd-≈ = tr (hd-≈ k) $ tr (+c r (*a _ _ _)) $ s (dist .proj₁ _ _ _)
  where open CommutativeRing C using ()
             renaming (distrib to dist; trans to tr; *-assoc to *a; refl to r; sym to s; +-cong to +c)
*ₛ-assoc-distrib a x y z res k .tl-≈ = *ₛ-assoc-distrib _ _ _ _ _ $ begin
  tl res
    ≈⟨ tl-≈ k ⟩
  fma (x *ₛ tl a + x *ₐ hd y *ₛ tl z) (x *ₛ tl y) z
    ≈⟨ fma-cong (+-cong refl *ₛ-assoc) refl refl ⟩
  fma (x *ₛ tl a + x *ₛ (hd y *ₛ tl z)) (x *ₛ tl y) z
    ≈˘⟨ fma-cong *ₛ-distrib-l refl refl ⟩
  fma (x *ₛ (tl a + hd y *ₛ tl z)) (x *ₛ tl y) z ∎
  where open ≈-Reasoning record { isEquivalence = isEquivalence }

*ₛ-zero-r : ∀ {x} → x *ₛ 0# ≈ 0#
*ₛ-zero-r .hd-≈ = C .CommutativeRing.zero .proj₂ _
*ₛ-zero-r .tl-≈ = *ₛ-zero-r

*ₛ-assoc-* : ∀ {x y z}
  → x *ₛ y * z ≈ x *ₛ (y * z)
*ₛ-assoc-* {x} {y} {z} = begin
  fma 0# (x *ₛ y) z        ≈˘⟨ fma-cong *ₛ-zero-r refl refl ⟩
  fma (x *ₛ 0#) (x *ₛ y) z ≈⟨ *ₛ-assoc-distrib _ _ _ _ _ refl ⟩
  x *ₛ fma 0# y z          ∎
  where open ≈-Reasoning record { isEquivalence = isEquivalence }

fma-assoc' : ∀ a x y z res
  → res ≈ fma a (x * y) z
  → res ≈ fma a x (y * z)
fma-assoc' a x y z res k .hd-≈ = begin
  hd res                               ≈⟨ hd-≈ k ⟩
  hd a +ₐ (0ₐ +ₐ hd x *ₐ hd y) *ₐ hd z ≈⟨ +c r (*c (+-id _) r) ⟩
  hd a +ₐ hd x *ₐ hd y *ₐ hd z         ≈⟨ +c r (*a _ _ _) ⟩
  hd a +ₐ hd x *ₐ (hd y *ₐ hd z)       ≈˘⟨ +c r (*c r $ +-id _) ⟩
  hd a +ₐ hd x *ₐ (0ₐ +ₐ hd y *ₐ hd z) ∎
  where open CommutativeRing C using (setoid)
             renaming (+-identityˡ to +-id; +-cong to +c; *-cong to *c; refl to r; *-assoc to *a)
        open ≈-Reasoning setoid
fma-assoc' a x y z res k .tl-≈ = fma-assoc' _ _ _ _ _ $ begin
  tl res
    ≈⟨ tl-≈ k ⟩
  fma (tl a + hd (x * y) *ₛ tl z) (tl (x * y)) z
    ≈⟨ fma-cong (+-cong refl (*ₛ-cong (+-id _) refl)) refl refl ⟩
  fma (tl a + hd x *ₐ hd y *ₛ tl z) (tl (x * y)) z
    ≈⟨ fma-cong (+-cong refl *ₛ-assoc) refl refl ⟩
  fma (tl a + hd x *ₛ (hd y *ₛ tl z)) (fma (0# + hd x *ₛ tl y) (tl x) y) z
    ≈⟨ fma-cong refl (fma-cong (+-identity .proj₁ _) refl refl) refl ⟩
  fma (tl a + hd x *ₛ (hd y *ₛ tl z)) (fma (hd x *ₛ tl y) (tl x) y) z
    ≈⟨ fma-cong refl (fma-def _ _ _) refl ⟩
  fma (tl a + hd x *ₛ (hd y *ₛ tl z)) (hd x *ₛ tl y + tl x * y) z
    ≈⟨ fma-def _ _ _ ⟩
  tl a + hd x *ₛ (hd y *ₛ tl z) + (hd x *ₛ tl y + tl x * y) * z
    ≈⟨ +-cong refl (*-distrib-+-r _ _ _) ⟩
  tl a + hd x *ₛ (hd y *ₛ tl z) + (hd x *ₛ tl y * z + tl x * y * z)
    ≈⟨ +-cong refl (+-cong *ₛ-assoc-* refl) ⟩
  tl a + hd x *ₛ (hd y *ₛ tl z) + (hd x *ₛ (tl y * z) + tl x * y * z)
    ≈⟨ +-assoc _ _ _ ⟩
  tl a + (hd x *ₛ (hd y *ₛ tl z) + (hd x *ₛ (tl y * z) + tl x * y * z))
    ≈˘⟨ +-cong refl (+-assoc _ _ _) ⟩
  tl a + (hd x *ₛ (hd y *ₛ tl z) + hd x *ₛ (tl y * z) + tl x * y * z)
    ≈˘⟨ +-cong refl (+-cong *ₛ-distrib-l refl) ⟩
  tl a + (hd x *ₛ (hd y *ₛ tl z + tl y * z) + tl x * y * z)
    ≈˘⟨ +-assoc _ _ _ ⟩
  tl a + hd x *ₛ (hd y *ₛ tl z + tl y * z) + tl x * y * z
    ≈˘⟨ +-cong (+-cong refl (*ₛ-cong ar (+-cong (+-identity .proj₁ _) refl))) refl ⟩
  tl a + hd x *ₛ (0# + hd y *ₛ tl z + tl y * z) + tl x * y * z
    ≈˘⟨ +-cong (+-cong refl (*ₛ-cong ar (fma-def _ _ _))) refl ⟩
  tl a + hd x *ₛ fma (0# + hd y *ₛ tl z) (tl y) z + tl x * y * z
    ≈˘⟨ fma-def _ _ _ ⟩
  fma (tl a + hd x *ₛ fma (0# + hd y *ₛ tl z) (tl y) z) (tl x * y) z ∎
  where open CommutativeRing C using ()
             renaming (+-identityˡ to +-id; +-cong to +c; *-cong to *c; refl to ar; *-assoc to *a)
        open ≈-Reasoning record { isEquivalence = isEquivalence }

*-assoc : Associative _≈_ _*_
*-assoc _ _ _ = fma-assoc' _ _ _ _ _ refl

*-semigroup : IsSemigroup _≈_ _*_
*-semigroup .IsSemigroup.isMagma = *-magma
*-semigroup .IsSemigroup.assoc = *-assoc

1# : FPS
1# .hd = 1ₐ
1# .tl = 0#

*ₛ-zero-l : ∀ {x} → 0ₐ *ₛ x ≈ 0#
*ₛ-zero-l .hd-≈ = C .CommutativeRing.zero .proj₁ _
*ₛ-zero-l .tl-≈ = *ₛ-zero-l

*ₛ-identity-l : ∀ {x} → 1ₐ *ₛ x ≈ x
*ₛ-identity-l .hd-≈ = C .CommutativeRing.*-identity .proj₁ _
*ₛ-identity-l .tl-≈ = *ₛ-identity-l

fma-zero-l' : ∀ {x z res}
  → res ≈ fma x 0# z
  → res ≈ x
fma-zero-l' k .hd-≈ = tr (hd-≈ k) $ tr (+c r (z .proj₁ _)) $ +-id .proj₂ _
  where open CommutativeRing C using ()
          renaming (trans to tr; refl to r; +-cong to +c; +-identity to +-id; zero to z)
fma-zero-l' k .tl-≈ = fma-zero-l' $ trans (tl-≈ k)
  $ fma-cong (trans (+-cong refl *ₛ-zero-l) (+-identity .proj₂ _)) refl refl

*-identity : Identity _≈_ 1# _*_
*-identity .proj₁ x .hd-≈ =
  C .CommutativeRing.trans
    (C .CommutativeRing.+-identity .proj₁ _)
    (C .CommutativeRing.*-identity .proj₁ _)
*-identity .proj₁ x .tl-≈ =
  trans (fma-zero-l' refl) $ trans (+-identity .proj₁ _) $ *ₛ-identity-l
*-identity .proj₂ x = trans (*-comm _ _) (*-identity .proj₁ _)

*-monoid : IsMonoid _≈_ _*_ 1#
*-monoid .IsMonoid.isSemigroup = *-semigroup
*-monoid .IsMonoid.identity = *-identity

zero : Zero _≈_ 0# _*_
zero .proj₁ x = fma-zero-l' refl
zero .proj₂ x = trans (*-comm _ _) $ zero .proj₁ _

distrib : _DistributesOver_ _≈_ _*_ _+_
distrib .proj₁ x y z = trans (*-comm _ _)
    $ trans (*-distrib-+-r _ _ _) $ +-cong (*-comm _ _) (*-comm _ _)
distrib .proj₂ = *-distrib-+-r

------------------------------------------------------------------------
-- The whole ring!
------------------------------------------------------------------------

ring : IsRing _≈_ _+_ _*_ -_ 0# 1#
ring .IsRing.+-isAbelianGroup = +-abelian
ring .IsRing.*-isMonoid = *-monoid
ring .IsRing.distrib = distrib
ring .IsRing.zero = zero

commutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
commutativeRing .IsCommutativeRing.isRing = ring
commutativeRing .IsCommutativeRing.*-comm = *-comm

-- Yay! Finally
FormalPowerSeries : CommutativeRing a ℓ
FormalPowerSeries = record { isCommutativeRing = commutativeRing }

-- TODO prove: if the first term is invertable, then the series is invertable
-- Maybe composing power series, too?

-- TODO use it to show an explicit formula for a linear recursive sequence