Define middleBolLoop and add proofs (#1809)

Author: Akshobhya1234

CHANGELOG.md

@@ -1400,6 +1400,15 @@ New modules
   ```
   Algebra.Properties.Quasigroup
   ```
+  
+* Properties of MiddleBolLoop
+  ```
+  Algebra.Properties.MiddleBolLoop
+  ```
+
+* Properties of Loop
+  ```
+  Algebra.Properties.Loop
 
 * Some n-ary functions manipulating lists
   ```
@@ -1441,6 +1450,7 @@ Other minor changes
   record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ))
   record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ))
   record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ))
+  record MiddleBolLoop c ℓ : Set (suc (c ⊔ ℓ))
   ```
   and the existing record `Lattice` now provides
   ```agda
@@ -1528,6 +1538,7 @@ Other minor changes
   Semimedial _∙_ = (LeftSemimedial _∙_) × (RightSemimedial _∙_)
   LeftBol _∙_ = ∀ x y z → (x ∙ (y ∙ (x ∙ z))) ≈ ((x ∙ (y ∙ z)) ∙ z )
   RightBol _∙_ = ∀ x y z → (((z ∙ x) ∙ y) ∙ x) ≈ (z ∙ ((x ∙ y) ∙ x))
+  MiddleBol _∙_ _\\_ _//_ = ∀ x y z → (x ∙ ((y ∙ z) \\ x)) ≈ ((x // z) ∙ (y \\ x))
   ```
 
 * Added new functions to `Algebra.Definitions.RawSemiring`:
@@ -1582,6 +1593,7 @@ Other minor changes
   record IsRightBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
   record IsMoufangLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
   record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ)
+  record IsMiddleBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ)
   ```
   and the existing record `IsLattice` now provides
   ```

src/Algebra/Bundles.agda

@@ -1136,3 +1136,25 @@ record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open LeftBolLoop leftBolLoop public
     using (loop)
+
+record MiddleBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infixl 7 _\\_
+  infixl 7 _//_
+  infix  4 _≈_
+  field
+    Carrier         : Set c
+    _≈_             : Rel Carrier ℓ
+    _∙_             : Op₂ Carrier
+    _\\_            : Op₂ Carrier
+    _//_            : Op₂ Carrier
+    ε               : Carrier
+    isMiddleBolLoop : IsMiddleBolLoop  _≈_ _∙_ _\\_ _//_ ε
+
+  open IsMiddleBolLoop isMiddleBolLoop public
+
+  loop : Loop _ _
+  loop = record { isLoop = isLoop }
+
+  open Loop loop public
+    using (quasigroup)

src/Algebra/Definitions.agda

@@ -216,5 +216,8 @@ LeftBol _∙_ = ∀ x y z → (x ∙ (y ∙ (x ∙ z))) ≈ ((x ∙ (y ∙ x)) 
 RightBol : Op₂ A → Set _
 RightBol _∙_ = ∀ x y z → (((z ∙ x) ∙ y) ∙ x) ≈ (z ∙ ((x ∙ y) ∙ x))
 
+MiddleBol : Op₂ A → Op₂ A  → Op₂ A  → Set _
+MiddleBol _∙_ _\\_ _//_ = ∀ x y z → (x ∙ ((y ∙ z) \\ x)) ≈ ((x // z) ∙ (y \\ x))
+
 Identical : Op₂ A → Set _
 Identical _∙_ = ∀ x y z → ((z ∙ x) ∙ (y ∙ z)) ≈ (z ∙ ((x ∙ y) ∙ z))

src/Algebra/Properties/Loop.agda

@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Quasigroup
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (Loop)
+
+module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where
+
+open Loop L
+open import Algebra.Definitions _≈_
+open import Relation.Binary.Reasoning.Setoid setoid
+open import Data.Product
+open import Algebra.Properties.Quasigroup
+
+x//x≈ε : ∀ x → x // x ≈ ε
+x//x≈ε x = begin
+  x // x       ≈⟨ //-congʳ (sym (identityˡ x)) ⟩
+  (ε ∙ x) // x ≈⟨ rightDividesʳ x ε ⟩
+  ε            ∎
+
+x\\x≈ε : ∀ x → x \\ x ≈ ε
+x\\x≈ε x = begin
+  x \\ x       ≈⟨ \\-congˡ (sym (identityʳ x )) ⟩
+  x \\ (x ∙ ε) ≈⟨ leftDividesʳ x ε ⟩
+  ε            ∎
+
+ε\\x≈x : ∀ x → ε \\ x ≈ x
+ε\\x≈x x = begin
+  ε \\ x       ≈⟨ sym (identityˡ (ε \\ x)) ⟩
+  ε ∙ (ε \\ x) ≈⟨ leftDividesˡ ε x ⟩
+  x            ∎
+
+x//ε≈x : ∀ x → x // ε ≈ x
+x//ε≈x x = begin
+ x // ε       ≈⟨ sym (identityʳ (x // ε)) ⟩
+ (x // ε) ∙ ε ≈⟨ rightDividesˡ ε x ⟩
+ x            ∎

src/Algebra/Properties/MiddleBolLoop.agda

@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Quasigroup
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (MiddleBolLoop)
+
+module Algebra.Properties.MiddleBolLoop {m₁ m₂} (M : MiddleBolLoop m₁ m₂) where
+
+open MiddleBolLoop M
+open import Algebra.Definitions _≈_
+open import Relation.Binary.Reasoning.Setoid setoid
+open import Data.Product
+import Algebra.Properties.Loop as LoopProperties
+open LoopProperties loop public
+
+xyx\\x≈y\\x : ∀ x y → x ∙ ((y ∙ x) \\ x) ≈ y \\ x
+xyx\\x≈y\\x x y = begin
+  x ∙ ((y ∙ x) \\ x)  ≈⟨ middleBol x y x ⟩
+  (x // x) ∙ (y \\ x) ≈⟨ ∙-congʳ (x//x≈ε x) ⟩
+  ε ∙ (y \\ x)        ≈⟨ identityˡ ((y \\ x)) ⟩
+  y \\ x              ∎
+
+xxz\\x≈x//z : ∀ x z → x ∙ ((x ∙ z) \\ x) ≈ x // z
+xxz\\x≈x//z x z = begin
+  x ∙ ((x ∙ z) \\ x)  ≈⟨ middleBol x x z ⟩
+  (x // z) ∙ (x \\ x) ≈⟨ ∙-congˡ (x\\x≈ε x) ⟩
+  (x // z) ∙ ε        ≈⟨ identityʳ ((x // z)) ⟩
+  x // z              ∎
+
+xz\\x≈x//zx : ∀ x z → x ∙ (z \\ x) ≈ (x // z) ∙ x
+xz\\x≈x//zx x z = begin
+  x ∙ (z \\ x)       ≈⟨ ∙-congˡ (\\-congʳ( sym (identityˡ z))) ⟩
+  x ∙ ((ε ∙ z) \\ x) ≈⟨ middleBol x ε z ⟩
+  x // z ∙ (ε \\ x)  ≈⟨ ∙-congˡ (ε\\x≈x x) ⟩
+  x // z ∙ x         ∎
+
+x//yzx≈x//zy\\x : ∀ x y z → (x // (y ∙ z)) ∙ x ≈ (x // z) ∙ (y \\ x)
+x//yzx≈x//zy\\x x y z = begin
+ (x // (y ∙ z)) ∙ x  ≈⟨ sym (xz\\x≈x//zx x ((y ∙ z))) ⟩
+ x ∙ ((y ∙ z) \\ x)  ≈⟨ middleBol x y z ⟩
+ (x // z) ∙ (y \\ x) ∎
+
+x//yxx≈y\\x : ∀ x y → (x // (y ∙ x)) ∙ x ≈ y \\ x
+x//yxx≈y\\x x y = begin
+  (x // (y ∙ x)) ∙ x  ≈⟨ x//yzx≈x//zy\\x  x y x ⟩
+  (x // x) ∙ (y \\ x) ≈⟨ ∙-congʳ (x//x≈ε x) ⟩
+  ε ∙ (y \\ x)        ≈⟨ identityˡ ((y \\ x)) ⟩
+  y \\ x              ∎
+
+x//xzx≈x//z : ∀ x z → (x // (x ∙ z)) ∙ x ≈ x // z
+x//xzx≈x//z x z = begin
+  (x // (x ∙ z)) ∙ x  ≈⟨ x//yzx≈x//zy\\x x x z ⟩
+  (x // z) ∙ (x \\ x) ≈⟨ ∙-congˡ (x\\x≈ε x) ⟩
+  (x // z) ∙ ε        ≈⟨ identityʳ (x // z) ⟩
+  x // z              ∎

src/Algebra/Properties/Quasigroup.agda

@@ -31,3 +31,15 @@ cancelʳ x y z eq = begin
 
 cancel : Cancellative _∙_
 cancel = cancelˡ , cancelʳ
+
+y≈x\\z : ∀ x y z → x ∙ y ≈ z → y ≈ x \\ z
+y≈x\\z x y z eq = begin
+  y            ≈⟨ sym (leftDividesʳ x y) ⟩
+  x \\ (x ∙ y) ≈⟨ \\-congˡ eq ⟩
+  x \\ z       ∎
+
+x≈z//y : ∀ x y z → x ∙ y ≈ z → x ≈ z // y
+x≈z//y x y z eq = begin
+  x            ≈⟨ sym (rightDividesʳ y x) ⟩
+  (x ∙ y) // y ≈⟨ //-congʳ eq ⟩
+  z // y       ∎

src/Algebra/Structures.agda

@@ -936,3 +936,10 @@ record IsMoufangLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
     identical      : Identical ∙
 
   open IsLeftBolLoop isLeftBolLoop public
+
+record IsMiddleBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
+  field
+    isLoop    : IsLoop ∙ \\ //  ε
+    middleBol : MiddleBol ∙ \\ //
+
+  open IsLoop isLoop public