Added properties of Heyting Commutative Ring (#1968)

CHANGELOG.md

@@ -3284,6 +3284,24 @@ This is a full list of proofs that have changed form to use irrelevant instance
  ↭-reverse : (xs : List A) → reverse xs ↭ xs
  ```
 
+* Added new functions to `Algebra.Properties.CommutativeMonoid`
+ ```agda
+ invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x
+ invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x
+ invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+ invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+ ```
+
+* Added new functions to `Algebra.Apartness.Bundles`
+ ```agda
+ invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+ invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+ x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0#
+ #-sym : Symmetric _#_
+ #-congʳ : x ≈ y → x # z → y # z
+ #-congˡ : y ≈ z → x # y → x # z
+ ```
+
 * Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties`
  and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`.
  ```agda

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -11,23 +11,98 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
  {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Data.Product.Base using (_,_; proj₂)
-open import Algebra using (CommutativeRing; RightIdentity)
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
 
 open HeytingCommutativeRing HCR
-open CommutativeRing commutativeRing using (ring)
+open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
 
-open import Algebra.Properties.Ring ring using (-0#≈0#)
+open import Algebra.Properties.Ring ring
+ using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
+open import Relation.Binary.Definitions using (Symmetric)
+import Relation.Binary.Reasoning.Setoid as ReasonSetoid
+open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
 
+private variable
+ x y z : Carrier
+
+invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
+
+invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
 
 x-0≈x : RightIdentity _≈_ 0# _-_
 x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x)
 
 1#0 : 1# # 0#
-1#0 = invertible⇒# (1# , 1*[x-0]≈x , [x-0]*1≈x)
+1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x)
  where
- 1*[x-0]≈x : ∀ {x} → 1# * (x - 0#) ≈ x
+ 1*[x-0]≈x : 1# * (x - 0#) ≈ x
  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x)
 
- [x-0]*1≈x : ∀ {x} → (x - 0#) * 1# ≈ x
- [x-0]*1≈x {x} = trans (*-comm (x - 0#) 1#) 1*[x-0]≈x
+x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0#
+x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
+ where
+
+ helper : Invertible _≈_ 1# _*_ (x - 0#) → Invertible _≈_ 1# _*_ (y - 0#) → x * y # 0#
+ helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
+ = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
+ where
+ open ReasonSetoid setoid
+
+ y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
+ y⁻¹*x⁻¹*x*y≈1 = begin
+ y⁻¹ * x⁻¹ * (x * y - 0#) ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩
+ y⁻¹ * x⁻¹ * (x * y) ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩
+ y⁻¹ * (x⁻¹ * (x * y)) ≈˘⟨ *-congˡ (*-assoc x⁻¹ x y) ⟩
+ y⁻¹ * ((x⁻¹ * x) * y) ≈˘⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟩
+ y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩
+ y⁻¹ * (1# * y) ≈⟨ *-congˡ (*-identityˡ y) ⟩
+ y⁻¹ * y ≈˘⟨ *-congˡ (x-0≈x y) ⟩
+ y⁻¹ * (y - 0#) ≈⟨ y⁻¹*y≈1 ⟩
+ 1# ∎
+
+#-sym : Symmetric _#_
+#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
+ where
+ open ReasonSetoid setoid
+ InvX-Y : Invertible _≈_ 1# _*_ (x - y)
+ InvX-Y = #⇒invertible x#y
+
+ x-y⁻¹ = InvX-Y .proj₁
+
+ y-x≈-[x-y] : y - x ≈ - (x - y)
+ y-x≈-[x-y] = begin
+ y - x ≈˘⟨ +-congʳ (-‿involutive y) ⟩
+ - - y - x ≈˘⟨ -‿anti-homo-+ x (- y) ⟩
+ - (x - y) ∎
+
+ x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
+ x-y⁻¹*y-x≈1 = begin
+ (- x-y⁻¹) * (y - x) ≈˘⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟩
+ - (x-y⁻¹ * (y - x)) ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
+ - (x-y⁻¹ * - (x - y)) ≈˘⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟩
+ - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
+ x-y⁻¹ * (x - y) ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
+ 1# ∎
+
+#-congʳ : x ≈ y → x # z → y # z
+#-congʳ {x} {y} {z} x≈y x#z = helper (#⇒invertible x#z)
+ where
+
+ helper : Invertible _≈_ 1# _*_ (x - z) → y # z
+ helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
+ = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
+ where
+ open ReasonSetoid setoid
+
+ x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
+ x-z⁻¹*y-z≈1 = begin
+ x-z⁻¹ * (y - z) ≈˘⟨ *-congˡ (+-congʳ x≈y) ⟩
+ x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩
+ 1# ∎
+
+#-congˡ : y ≈ z → x # y → x # z
+#-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y))

src/Algebra/Properties/CommutativeMonoid.agda

@@ -7,6 +7,8 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles
+open import Algebra.Definitions
+open import Data.Product using (_,_; proj₂)
 
 module Algebra.Properties.CommutativeMonoid
  {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where
@@ -23,3 +25,18 @@ open CommutativeMonoid M
  ; assoc to +-assoc
  ; comm to +-comm
  )
+
+private variable
+ x : Carrier
+
+invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x
+invertibleˡ⇒invertibleʳ {x} (-x , -x+x≈1) = -x , trans (+-comm x -x) -x+x≈1
+
+invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x
+invertibleʳ⇒invertibleˡ {x} (-x , x+-x≈1) = -x , trans (+-comm -x x) x+-x≈1
+
+invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+invertibleˡ⇒invertible left@(-x , -x+x≈1) = -x , -x+x≈1 , invertibleˡ⇒invertibleʳ left .proj₂
+
+invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+invertibleʳ⇒invertible right@(-x , x+-x≈1) = -x , invertibleʳ⇒invertibleˡ right .proj₂ , x+-x≈1