Skip to content

Instantly share code, notes, and snippets.

@mb64
Last active April 7, 2021 23:00
Show Gist options
  • Save mb64/24b62fa36d942550b8eeea871322e446 to your computer and use it in GitHub Desktop.
Save mb64/24b62fa36d942550b8eeea871322e446 to your computer and use it in GitHub Desktop.
A proof that formal power series over an arbitrary commutative ring form a commutative ring, formalized in Agda using guarded coinduction.
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment