Add new Bool action on a RawMonoid plus properties

CHANGELOG.md

@@ -48,6 +48,19 @@ 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
+  ```
+
+* In `Algebra.Properties.Monoid.Mult` 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 : b ∧′ x ∙ y ≈ (b ∧ x) + y
+ ```
+
 * In `Data.List.Relation.Unary.All`:
   ```agda
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs

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

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 _ = refl
+
+∧-assocˡ : ∀ b b′ x → b ∧ (b′ ∧ x) ≈ (b Bool.∧ 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)