From d7e9ffefb7671446a86914eb50245e101c4ae47c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 2 Feb 2024 08:04:30 +0000 Subject: [PATCH 1/8] =?UTF-8?q?tidying=20up=20proofs=20of,=20and=20using,?= =?UTF-8?q?=20semiring=20structure=20induced=20by=20`=5F=C3=97=20x`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 16 ++++++++++++ src/Algebra/Properties/Monoid/Mult.agda | 3 +++ src/Algebra/Properties/Semiring/Binomial.agda | 2 +- src/Algebra/Properties/Semiring/Mult.agda | 25 +++++++++++++++---- 4 files changed, 40 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e8f0a568f2..2506d9d538 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,11 @@ Deprecated modules Deprecated names ---------------- +* In `Algebra.Properties.Semiring.Mult`: + ```agda + 1×-identityʳ ↦ Algebra.Properties.Monoid.Mult.×-homo-1 + ``` + * In `Data.Nat.Divisibility.Core`: ```agda *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ @@ -84,6 +89,17 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` +* In `Algebra.Properties.Monoid.Mult`: + ```agda + ×-homo-0 : ∀ x → 0 × x ≈ 0# + ×-homo-1 : ∀ x → 1 × x ≈ x + ``` + +* In `Algebra.Properties.Semiring.Mult`: + ```agda + ×-homo-0 : ∀ x → 0 × x ≈ 0# * x + ``` + * In `Data.Fin.Properties`: ```agda nonZeroIndex : Fin n → ℕ.NonZero n diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index 88c4258fcb..4a3b0df2f0 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -51,6 +51,9 @@ open import Algebra.Definitions.RawMonoid rawMonoid public -- _×_ is homomorphic with respect to _ℕ+_/_+_. +×-homo-1 : ∀ x → 1 × x ≈ x +×-homo-1 = +-identityʳ + ×-homo-+ : ∀ x m n → (m ℕ.+ n) × x ≈ m × x + n × x ×-homo-+ x 0 n = sym (+-identityˡ (n × x)) ×-homo-+ x (suc m) n = begin diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda index 6731018af6..e04b1094de 100644 --- a/src/Algebra/Properties/Semiring/Binomial.agda +++ b/src/Algebra/Properties/Semiring/Binomial.agda @@ -216,7 +216,7 @@ term₁+term₂≈term x*y≈y*x n (suc i) with view i theorem : x * y ≈ y * x → ∀ n → (x + y) ^ n ≈ binomialExpansion n theorem x*y≈y*x zero = begin (x + y) ^ 0 ≡⟨⟩ - 1# ≈⟨ 1×-identityʳ 1# ⟨ + 1# ≈⟨ +-identityʳ 1# ⟨ 1 × 1# ≈⟨ *-identityʳ (1 × 1#) ⟨ (1 × 1#) * 1# ≈⟨ ×-assoc-* 1 1# 1# ⟩ 1 × (1# * 1#) ≡⟨⟩ diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda index 801e4f1966..ac42fe82f1 100644 --- a/src/Algebra/Properties/Semiring/Mult.agda +++ b/src/Algebra/Properties/Semiring/Mult.agda @@ -28,16 +28,16 @@ open import Algebra.Properties.Monoid.Mult +-monoid public ×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#) ×1-homo-* 0 n = sym (zeroˡ (n × 1#)) ×1-homo-* (suc m) n = begin - (n ℕ.+ m ℕ.* n) × 1# ≈⟨ ×-homo-+ 1# n (m ℕ.* n) ⟩ - n × 1# + (m ℕ.* n) × 1# ≈⟨ +-congˡ (×1-homo-* m n) ⟩ + (n ℕ.+ m ℕ.* n) × 1# ≈⟨ ×-homo-+ 1# n (m ℕ.* n) ⟩ + n × 1# + (m ℕ.* n) × 1# ≈⟨ +-congˡ (×1-homo-* m n) ⟩ n × 1# + (m × 1#) * (n × 1#) ≈⟨ +-congʳ (*-identityˡ _) ⟨ 1# * (n × 1#) + (m × 1#) * (n × 1#) ≈⟨ distribʳ (n × 1#) 1# (m × 1#) ⟨ (1# + m × 1#) * (n × 1#) ∎ --- (1 ×_) is the identity +-- (0 ×_) is (0# *_) -1×-identityʳ : ∀ x → 1 × x ≈ x -1×-identityʳ = +-identityʳ +×-homo-0 : ∀ x → 0 × x ≈ 0# * x +×-homo-0 x = sym (zeroˡ x) -- (n ×_) commutes with _*_ @@ -60,3 +60,18 @@ open import Algebra.Properties.Monoid.Mult +-monoid public x * y + (n × x) * y ≈⟨ +-congˡ (×-assoc-* n _ _) ⟩ x * y + n × (x * y) ≡⟨⟩ suc n × (x * y) ∎ + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.1 + +1×-identityʳ = ×-homo-1 + +{-# WARNING_ON_USAGE 1×-identityʳ +"Warning: 1×-identityʳ was deprecated in v2.1. +Please use Algebra.Properties.Monoid.Mult.×-homo-1 instead. " +#-} From d6cd9f91c25ec79818a86e919b23adabdf478278 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 2 Feb 2024 08:55:15 +0000 Subject: [PATCH 2/8] reinstated lemma about `0#` --- src/Algebra/Properties/Monoid/Mult.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda index 4a3b0df2f0..2963523b77 100644 --- a/src/Algebra/Properties/Monoid/Mult.agda +++ b/src/Algebra/Properties/Monoid/Mult.agda @@ -51,6 +51,9 @@ open import Algebra.Definitions.RawMonoid rawMonoid public -- _×_ is homomorphic with respect to _ℕ+_/_+_. +×-homo-0 : ∀ x → 0 × x ≈ 0# +×-homo-0 x = refl + ×-homo-1 : ∀ x → 1 × x ≈ x ×-homo-1 = +-identityʳ From 98e8363141d138c43807dd2104ac078b6fe6481d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 2 Feb 2024 09:47:11 +0000 Subject: [PATCH 3/8] fixed name clash --- CHANGELOG.md | 2 +- src/Algebra/Properties/Semiring/Mult.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2506d9d538..b0e8b595d5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -97,7 +97,7 @@ Additions to existing modules * In `Algebra.Properties.Semiring.Mult`: ```agda - ×-homo-0 : ∀ x → 0 × x ≈ 0# * x + ×-homo-0# : ∀ x → 0 × x ≈ 0# * x ``` * In `Data.Fin.Properties`: diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda index ac42fe82f1..fd4b06c259 100644 --- a/src/Algebra/Properties/Semiring/Mult.agda +++ b/src/Algebra/Properties/Semiring/Mult.agda @@ -36,8 +36,8 @@ open import Algebra.Properties.Monoid.Mult +-monoid public -- (0 ×_) is (0# *_) -×-homo-0 : ∀ x → 0 × x ≈ 0# * x -×-homo-0 x = sym (zeroˡ x) +×-homo-0# : ∀ x → 0 × x ≈ 0# * x +×-homo-0# x = sym (zeroˡ x) -- (n ×_) commutes with _*_ From be06f2917514b28642f7275a6e19feafb460fa8c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 2 Feb 2024 10:00:00 +0000 Subject: [PATCH 4/8] added companion lemma for `1#` --- CHANGELOG.md | 1 + src/Algebra/Properties/Semiring/Mult.agda | 15 ++++++++++----- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b0e8b595d5..99e0ffcd72 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -98,6 +98,7 @@ Additions to existing modules * In `Algebra.Properties.Semiring.Mult`: ```agda ×-homo-0# : ∀ x → 0 × x ≈ 0# * x + ×-homo-1# : ∀ x → 1 × x ≈ 1# * x ``` * In `Data.Fin.Properties`: diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda index fd4b06c259..ee2bab944f 100644 --- a/src/Algebra/Properties/Semiring/Mult.agda +++ b/src/Algebra/Properties/Semiring/Mult.agda @@ -23,6 +23,16 @@ open import Algebra.Properties.Monoid.Mult +-monoid public ------------------------------------------------------------------------ -- Properties of _×_ +-- (0 ×_) is (0# *_) + +×-homo-0# : ∀ x → 0 × x ≈ 0# * x +×-homo-0# x = sym (zeroˡ x) + +-- (1 ×_) is (1# *_) + +×-homo-1# : ∀ x → 1 × x ≈ 1# * x +×-homo-1# x = trans (×-homo-1 x) (sym (*-identityˡ x)) + -- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_. ×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#) @@ -34,11 +44,6 @@ open import Algebra.Properties.Monoid.Mult +-monoid public 1# * (n × 1#) + (m × 1#) * (n × 1#) ≈⟨ distribʳ (n × 1#) 1# (m × 1#) ⟨ (1# + m × 1#) * (n × 1#) ∎ --- (0 ×_) is (0# *_) - -×-homo-0# : ∀ x → 0 × x ≈ 0# * x -×-homo-0# x = sym (zeroˡ x) - -- (n ×_) commutes with _*_ ×-comm-* : ∀ n x y → x * (n × y) ≈ n × (x * y) From ec09e102d78d620d991ffd73e6930879bd37bba8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 2 Feb 2024 11:37:59 +0000 Subject: [PATCH 5/8] new lemma, plus refactoring --- CHANGELOG.md | 5 ++-- src/Algebra/Properties/Semiring/Mult.agda | 32 ++++++++++++++--------- 2 files changed, 22 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 99e0ffcd72..635cc21238 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -97,8 +97,9 @@ Additions to existing modules * In `Algebra.Properties.Semiring.Mult`: ```agda - ×-homo-0# : ∀ x → 0 × x ≈ 0# * x - ×-homo-1# : ∀ x → 1 × x ≈ 1# * x + ×-homo-0# : ∀ x → 0 × x ≈ 0# * x + ×-homo-1# : ∀ x → 1 × x ≈ 1# * x + idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x ``` * In `Data.Fin.Properties`: diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda index ee2bab944f..05b8513bd1 100644 --- a/src/Algebra/Properties/Semiring/Mult.agda +++ b/src/Algebra/Properties/Semiring/Mult.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra +open import Algebra.Bundles using (Semiring) open import Data.Nat.Base as ℕ using (zero; suc) module Algebra.Properties.Semiring.Mult @@ -14,6 +14,7 @@ module Algebra.Properties.Semiring.Mult open Semiring S renaming (zero to *-zero) open import Relation.Binary.Reasoning.Setoid setoid +open import Algebra.Definitions _≈_ using (_IdempotentOn_) ------------------------------------------------------------------------ -- Re-export definition from the monoid @@ -33,17 +34,6 @@ open import Algebra.Properties.Monoid.Mult +-monoid public ×-homo-1# : ∀ x → 1 × x ≈ 1# * x ×-homo-1# x = trans (×-homo-1 x) (sym (*-identityˡ x)) --- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_. - -×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#) -×1-homo-* 0 n = sym (zeroˡ (n × 1#)) -×1-homo-* (suc m) n = begin - (n ℕ.+ m ℕ.* n) × 1# ≈⟨ ×-homo-+ 1# n (m ℕ.* n) ⟩ - n × 1# + (m ℕ.* n) × 1# ≈⟨ +-congˡ (×1-homo-* m n) ⟩ - n × 1# + (m × 1#) * (n × 1#) ≈⟨ +-congʳ (*-identityˡ _) ⟨ - 1# * (n × 1#) + (m × 1#) * (n × 1#) ≈⟨ distribʳ (n × 1#) 1# (m × 1#) ⟨ - (1# + m × 1#) * (n × 1#) ∎ - -- (n ×_) commutes with _*_ ×-comm-* : ∀ n x y → x * (n × y) ≈ n × (x * y) @@ -66,6 +56,23 @@ open import Algebra.Properties.Monoid.Mult +-monoid public x * y + n × (x * y) ≡⟨⟩ suc n × (x * y) ∎ +-- (_× x) is homomorphic with respect to _ℕ.*_/_*_ for idempotent x. + +module _ {x} (idem : _*_ IdempotentOn x) where + + idem-×-homo-* : ∀ m n → (m × x) * (n × x) ≈ (m ℕ.* n) × x + idem-×-homo-* m n = begin + (m × x) * (n × x) ≈⟨ ×-assoc-* m x (n × x) ⟩ + m × (x * (n × x)) ≈⟨ ×-congʳ m (×-comm-* n x x) ⟩ + m × (n × (x * x)) ≈⟨ ×-assocˡ _ m n ⟩ + (m ℕ.* n) × (x * x) ≈⟨ ×-congʳ (m ℕ.* n) idem ⟩ + (m ℕ.* n) × x ∎ + +-- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_. + +×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#) +×1-homo-* m n = sym (idem-×-homo-* (*-identityʳ 1#) m n) + ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ @@ -75,7 +82,6 @@ open import Algebra.Properties.Monoid.Mult +-monoid public -- Version 2.1 1×-identityʳ = ×-homo-1 - {-# WARNING_ON_USAGE 1×-identityʳ "Warning: 1×-identityʳ was deprecated in v2.1. Please use Algebra.Properties.Monoid.Mult.×-homo-1 instead. " From ec20b29965d89fe954f2b22f0fa534f4fa9c08eb Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 2 Feb 2024 12:26:06 +0000 Subject: [PATCH 6/8] removed anonymous `module` --- src/Algebra/Properties/Semiring/Mult.agda | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda index 05b8513bd1..6d363835a6 100644 --- a/src/Algebra/Properties/Semiring/Mult.agda +++ b/src/Algebra/Properties/Semiring/Mult.agda @@ -58,20 +58,18 @@ open import Algebra.Properties.Monoid.Mult +-monoid public -- (_× x) is homomorphic with respect to _ℕ.*_/_*_ for idempotent x. -module _ {x} (idem : _*_ IdempotentOn x) where - - idem-×-homo-* : ∀ m n → (m × x) * (n × x) ≈ (m ℕ.* n) × x - idem-×-homo-* m n = begin - (m × x) * (n × x) ≈⟨ ×-assoc-* m x (n × x) ⟩ - m × (x * (n × x)) ≈⟨ ×-congʳ m (×-comm-* n x x) ⟩ - m × (n × (x * x)) ≈⟨ ×-assocˡ _ m n ⟩ - (m ℕ.* n) × (x * x) ≈⟨ ×-congʳ (m ℕ.* n) idem ⟩ - (m ℕ.* n) × x ∎ +idem-×-homo-* : ∀ m n {x} → (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x +idem-×-homo-* m n {x} idem = begin + (m × x) * (n × x) ≈⟨ ×-assoc-* m x (n × x) ⟩ + m × (x * (n × x)) ≈⟨ ×-congʳ m (×-comm-* n x x) ⟩ + m × (n × (x * x)) ≈⟨ ×-assocˡ _ m n ⟩ + (m ℕ.* n) × (x * x) ≈⟨ ×-congʳ (m ℕ.* n) idem ⟩ + (m ℕ.* n) × x ∎ -- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_. ×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#) -×1-homo-* m n = sym (idem-×-homo-* (*-identityʳ 1#) m n) +×1-homo-* m n = sym (idem-×-homo-* m n (*-identityʳ 1#)) ------------------------------------------------------------------------ -- DEPRECATED NAMES From a06eef589c48f7ffd323a9dace46cd4c3afe97e0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 3 Feb 2024 09:19:54 +0000 Subject: [PATCH 7/8] don't inline use of the lemma --- src/Algebra/Properties/Semiring/Binomial.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda index e04b1094de..28ea35a8e8 100644 --- a/src/Algebra/Properties/Semiring/Binomial.agda +++ b/src/Algebra/Properties/Semiring/Binomial.agda @@ -216,7 +216,7 @@ term₁+term₂≈term x*y≈y*x n (suc i) with view i theorem : x * y ≈ y * x → ∀ n → (x + y) ^ n ≈ binomialExpansion n theorem x*y≈y*x zero = begin (x + y) ^ 0 ≡⟨⟩ - 1# ≈⟨ +-identityʳ 1# ⟨ + 1# ≈⟨ ×-homo-1 1# ⟨ 1 × 1# ≈⟨ *-identityʳ (1 × 1#) ⟨ (1 × 1#) * 1# ≈⟨ ×-assoc-* 1 1# 1# ⟩ 1 × (1# * 1#) ≡⟨⟩ From 78a3600b764b4cf2679b6c581d108cf3cf1cfcac Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 5 Feb 2024 05:32:25 +0000 Subject: [PATCH 8/8] revised deprecation warning --- CHANGELOG.md | 2 +- src/Algebra/Properties/Semiring/Mult.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 635cc21238..8d2eb6f009 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -35,7 +35,7 @@ Deprecated names * In `Algebra.Properties.Semiring.Mult`: ```agda - 1×-identityʳ ↦ Algebra.Properties.Monoid.Mult.×-homo-1 + 1×-identityʳ ↦ ×-homo-1 ``` * In `Data.Nat.Divisibility.Core`: diff --git a/src/Algebra/Properties/Semiring/Mult.agda b/src/Algebra/Properties/Semiring/Mult.agda index 6d363835a6..6301d274c6 100644 --- a/src/Algebra/Properties/Semiring/Mult.agda +++ b/src/Algebra/Properties/Semiring/Mult.agda @@ -82,5 +82,5 @@ idem-×-homo-* m n {x} idem = begin 1×-identityʳ = ×-homo-1 {-# WARNING_ON_USAGE 1×-identityʳ "Warning: 1×-identityʳ was deprecated in v2.1. -Please use Algebra.Properties.Monoid.Mult.×-homo-1 instead. " +Please use ×-homo-1 instead. " #-}