[ add ] Bool action on a RawMonoid plus properties (#2450)

* Add new `Bool` action on a `RawMonoid` plus properties

* response to review comments on draft

* reset: `CHANGELOG`

* restore: new `CHANGELOG` entries

* change: notation

* refactor: use new notation, plus add new lemma

* refactor: tweak notation

* refactor: proof following Jacques' suggestion

Author: jamesmckinna

CHANGELOG.md

@@ -172,6 +172,12 @@ Additions to existing modules
   Central : Op₂ A → A → Set _
   ```
 
+* In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid:
+  ```agda
+  _?>₀_  : Bool → Carrier → Carrier
+  _?>_∙_ : Bool → Carrier → Carrier → Carrier
+  ```
+
 * In `Algebra.Lattice.Properties.BooleanAlgebra.XorRing`:
   ```agda
   ⊕-∧-isBooleanRing : IsBooleanRing _⊕_ _∧_ id ⊥ ⊤
@@ -192,6 +198,14 @@ Additions to existing modules
   -ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r)
   ```
 
+* In `Algebra.Properties.Monoid.Mult` properties of the Boolean action on a RawMonoid:
+  ```agda
+  ?>₀-homo-true  : true ?>₀ x ≈ x
+  ?>₀-assocˡ     : b ?>₀ b′ ?>₀ x ≈ (b ∧ b′) ?>₀ x
+  b?>x∙y≈b?>₀x+y : b ?> x ∙ y ≈ (b ?>₀ x) + y
+  b?>₀x≈b?>x∙0   : b ?>₀ x ≈ b ?> x ∙ 0#
+   ```
+
 * In `Algebra.Properties.RingWithoutOne`:
   ```agda
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y

src/Algebra/Definitions/RawMonoid.agda

@@ -10,8 +10,10 @@ open import Algebra.Bundles using (RawMonoid)
 
 module Algebra.Definitions.RawMonoid {a ℓ} (M : RawMonoid a ℓ) where
 
+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)
+
 open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
 
 ------------------------------------------------------------------------
@@ -21,7 +23,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 +67,18 @@ suc n ×′ x = n ×′ x + x
 
 sum : ∀ {n} → Vector Carrier n → Carrier
 sum = Vector.foldr _+_ 0#
+
+------------------------------------------------------------------------
+-- 'Guard' with a Boolean: action of the Boolean (true,∧)-rawMonoid
+------------------------------------------------------------------------
+
+infixr 8 _?>₀_
+
+_?>₀_ : Bool → Carrier → Carrier
+b ?>₀ x = if b then x else 0#
+
+-- accumulator optimisation
+infixl 8 _?>_∙_
+
+_?>_∙_ : Bool → Carrier → Carrier → Carrier
+b ?> x ∙ y = if b then x + y else y

src/Algebra/Properties/Monoid/Mult.agda

@@ -7,12 +7,14 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
+
+module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where
+
+open import Data.Bool.Base as Bool using (true; false; _∧_)
 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 (_≡_)
 
-module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where
-
 -- View of the monoid operator as addition
 open Monoid M
   renaming
@@ -26,15 +28,15 @@ open Monoid M
   ; ε         to 0#
   )
 
-open import Relation.Binary.Reasoning.Setoid setoid
-
 open import Algebra.Definitions _≈_
+open import Algebra.Properties.Semigroup semigroup
+open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
 -- Definition
 
 open import Algebra.Definitions.RawMonoid rawMonoid public
-  using (_×_)
+  using (_×_; _?>₀_; _?>_∙_)
 
 ------------------------------------------------------------------------
 -- Properties of _×_
@@ -59,10 +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 × x + n × x)  ≈⟨ sym (+-assoc x (m × x) (n × x)) ⟩
-  x + m × x + n × x    ∎
+×-homo-+ x (suc m) n = sym (uv≈w⇒xu∙v≈xw (sym (×-homo-+ x m n)) x)
 
 ×-idem : ∀ {c} → _+_ IdempotentOn c →
          ∀ n → .{{_ : NonZero n}} → n × c ≈ c
@@ -78,3 +77,20 @@ 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 _ = refl
+
+?>₀-assocˡ : ∀ b b′ x → b ?>₀ b′ ?>₀ x ≈ (b ∧ b′) ?>₀ x
+?>₀-assocˡ false _ _ = refl
+?>₀-assocˡ true  _ _ = refl
+
+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)
+
+b?>₀x≈b?>x∙0 : ∀ b x → b ?>₀ x ≈ b ?> x ∙ 0#
+b?>₀x≈b?>x∙0 true  _ = sym (+-identityʳ _)
+b?>₀x≈b?>x∙0 false x = refl