From d666858d9f8d00efd1effcd2770eab926367a320 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 31 Jul 2024 15:22:54 +0100
Subject: [PATCH 1/2] Add new `Bool` action on a `RawMonoid` plus properties
---
CHANGELOG.md | 13 +++++++++++++
src/Algebra/Definitions/RawMonoid.agda | 18 +++++++++++++++++-
src/Algebra/Properties/Monoid/Mult.agda | 18 ++++++++++++++++--
3 files changed, 46 insertions(+), 3 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 80da9ee48e..a9aee06faa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,3 +26,16 @@ New modules
Additions to existing modules
-----------------------------
+
+* In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid:
+ ```agda
+ _∧_ : Bool → Carrier → Carrier
+ _∧′_∙_ : Bool → Carrier → Carrier → Carrier
+ ```
+
+* Properties of the Boolean action on a RawMonoid:
+ ```agda
+ ∧-homo-true : true ∧ x ≈ x
+ -assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x
+ ∧∙-≗∧+ : b ∧′ x ∙ y ≈ (b ∧ x) + y
+ ```
diff --git a/src/Algebra/Definitions/RawMonoid.agda b/src/Algebra/Definitions/RawMonoid.agda
index cbb095ab40..478671627c 100644
--- a/src/Algebra/Definitions/RawMonoid.agda
+++ b/src/Algebra/Definitions/RawMonoid.agda
@@ -7,6 +7,7 @@
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (RawMonoid)
+open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Vec.Functional as Vector using (Vector)
@@ -21,7 +22,7 @@ open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
open import Algebra.Definitions.RawMagma rawMagma public
------------------------------------------------------------------------
--- Multiplication by natural number
+-- Multiplication by natural number: action of the (0,+)-rawMonoid
------------------------------------------------------------------------
-- Standard definition
@@ -65,3 +66,18 @@ suc n ×′ x = n ×′ x + x
sum : ∀ {n} → Vector Carrier n → Carrier
sum = Vector.foldr _+_ 0#
+
+------------------------------------------------------------------------
+-- 'Conjunction' with a Boolean: action of the Boolean (true,∧)-rawMonoid
+------------------------------------------------------------------------
+
+infixr 8 _∧_
+
+_∧_ : Bool → Carrier → Carrier
+b ∧ x = if b then x else 0#
+
+-- tail-recursive optimisation
+infixl 8 _∧′_∙_
+
+_∧′_∙_ : Bool → Carrier → Carrier → Carrier
+b ∧′ x ∙ y = if b then x + y else y
diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda
index ce837c8134..320b2c4ef4 100644
--- a/src/Algebra/Properties/Monoid/Mult.agda
+++ b/src/Algebra/Properties/Monoid/Mult.agda
@@ -7,6 +7,7 @@
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Monoid)
+open import Data.Bool.Base as Bool using (Bool; true; false; if_then_else_)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
@@ -34,7 +35,7 @@ open import Algebra.Definitions _≈_
-- Definition
open import Algebra.Definitions.RawMonoid rawMonoid public
- using (_×_)
+ using (_×_; _∧_; _∧′_∙_)
------------------------------------------------------------------------
-- Properties of _×_
@@ -60,7 +61,7 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
×-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
- x + (m ℕ.+ n) × x ≈⟨ +-cong refl (×-homo-+ x m n) ⟩
+ x + (m ℕ.+ n) × x ≈⟨ +-congˡ (×-homo-+ x m n) ⟩
x + (m × x + n × x) ≈⟨ sym (+-assoc x (m × x) (n × x)) ⟩
x + m × x + n × x ∎
@@ -78,3 +79,16 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
n × x + m × n × x ≈⟨ +-congˡ (×-assocˡ x m n) ⟩
n × x + (m ℕ.* n) × x ≈⟨ ×-homo-+ x n (m ℕ.* n) ⟨
(suc m ℕ.* n) × x ∎
+
+-- _∧_ is homomorphic with respect to _Bool∧_.
+
+∧-homo-true : ∀ x → true ∧ x ≈ x
+∧-homo-true x = refl
+
+∧-assocˡ : ∀ b b′ x → b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x
+∧-assocˡ false b x = refl
+∧-assocˡ true b x = refl
+
+∧∙-≗∧+ : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y
+∧∙-≗∧+ true x y = refl
+∧∙-≗∧+ false x y = sym (+-identityˡ y)
From 7d4d3a0db19ae1c5faeb30ae946edbfbe050577b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 16 Aug 2024 07:53:40 +0100
Subject: [PATCH 2/2] response to review comments on draft
---
CHANGELOG.md | 4 ++--
src/Algebra/Properties/Monoid/Mult.agda | 14 +++++++-------
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a9aee06faa..57bafa0b0b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,6 @@ Additions to existing modules
* Properties of the Boolean action on a RawMonoid:
```agda
∧-homo-true : true ∧ x ≈ x
- -assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x
- ∧∙-≗∧+ : b ∧′ x ∙ y ≈ (b ∧ x) + y
+ ∧-assocˡ : b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x
+ b∧x∙y≈b∧x+y : b ∧′ x ∙ y ≈ (b ∧ x) + y
```
diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda
index 320b2c4ef4..4f824b087f 100644
--- a/src/Algebra/Properties/Monoid/Mult.agda
+++ b/src/Algebra/Properties/Monoid/Mult.agda
@@ -80,15 +80,15 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
n × x + (m ℕ.* n) × x ≈⟨ ×-homo-+ x n (m ℕ.* n) ⟨
(suc m ℕ.* n) × x ∎
--- _∧_ is homomorphic with respect to _Bool∧_.
+-- _∧_ is homomorphic with respect to Bool._∧_.
∧-homo-true : ∀ x → true ∧ x ≈ x
-∧-homo-true x = refl
+∧-homo-true _ = refl
∧-assocˡ : ∀ b b′ x → b ∧ (b′ ∧ x) ≈ (b Bool.∧ b′) ∧ x
-∧-assocˡ false b x = refl
-∧-assocˡ true b x = refl
+∧-assocˡ false _ _ = refl
+∧-assocˡ true _ _ = refl
-∧∙-≗∧+ : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y
-∧∙-≗∧+ true x y = refl
-∧∙-≗∧+ false x y = sym (+-identityˡ y)
+b∧x∙y≈b∧x+y : ∀ b x y → b ∧′ x ∙ y ≈ (b ∧ x) + y
+b∧x∙y≈b∧x+y true _ _ = refl
+b∧x∙y≈b∧x+y false _ y = sym (+-identityˡ y)