[ refactor ] (Re)define (Is)TightApartness and (Is)HeytingCommutativeRing/(Is)HeytingField

CHANGELOG.md

@@ -17,6 +17,10 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
+* The definitions of `Algebra.Structures.IsHeyting*` and
+  `Algebra.Structures.IsHeyting*` have been refactored, together
+  with that of `Relation.Binary.Definitions.Tight` on which they depend.
+
 Minor improvements
 ------------------
 
@@ -91,13 +95,26 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Apartness.Properties.HeytingField`, refactoring the existing
+  `Algebra.Apartness.Properties.HeytingCommutativeRing`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Apartness.Bundles`:
+  ```agda
+  TightApartnessRelation c ℓ₁ ℓ₂ : Set _
+  ```
+
+* In `Algebra.Apartness.Structures`:
+  ```agda
+  IsTightApartnessRelation _≈_ _#_ : Set _
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →
@@ -126,3 +143,10 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* In `Relation.Binary.Properties.DecSetoid`:
+  ```agda
+  ≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
+  ≉-tightApartnessRelation   : TightApartnessRelation _ _ _
+  ```
+

src/Algebra/Apartness/Bundles.agda

@@ -10,7 +10,7 @@ module Algebra.Apartness.Bundles where
 
 open import Level using (_⊔_; suc)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (ApartnessRelation)
+open import Relation.Binary.Bundles using (TightApartnessRelation)
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles using (CommutativeRing)
 open import Algebra.Apartness.Structures
@@ -36,8 +36,8 @@ record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ
   commutativeRing : CommutativeRing c ℓ₁
   commutativeRing = record { isCommutativeRing = isCommutativeRing }
 
-  apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
-  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+  tightApartnessRelation : TightApartnessRelation c ℓ₁ ℓ₂
+  tightApartnessRelation = record { isTightApartnessRelation = isTightApartnessRelation }
 
 
 record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -61,5 +61,5 @@ record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   heytingCommutativeRing : HeytingCommutativeRing c ℓ₁ ℓ₂
   heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing }
 
-  apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
-  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+  open HeytingCommutativeRing heytingCommutativeRing public
+    using (commutativeRing; tightApartnessRelation)

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -11,98 +11,14 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
   {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Function.Base using (_∘_)
-open import Data.Product.Base using (_,_; proj₁; proj₂)
-open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
+open import Algebra using (CommutativeRing; RightIdentity)
 
 open HeytingCommutativeRing HCR
-open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
-
-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 ≈-Reasoning
-open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
+open CommutativeRing commutativeRing using (ring)
+open import Algebra.Properties.Ring ring using (-0#≈0#)
 
 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 : Carrier
 
 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)
-  where
-  1*[x-0]≈x : 1# * (x - 0#) ≈ x
-  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x 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 ≈-Reasoning 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 ≈-Reasoning 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 ≈-Reasoning 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/Apartness/Properties/HeytingField.agda

@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of Heyting Commutative Rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Apartness.Bundles using (HeytingCommutativeRing; HeytingField)
+
+module Algebra.Apartness.Properties.HeytingField
+  {c ℓ₁ ℓ₂} (HF : HeytingField c ℓ₁ ℓ₂) where
+
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
+
+open HeytingField HF
+open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
+
+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 ≈-Reasoning
+open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
+
+private variable
+  x y z : Carrier
+
+
+open import Algebra.Apartness.Properties.HeytingCommutativeRing heytingCommutativeRing public
+
+invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
+
+invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
+
+1#0 : 1# # 0#
+1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x)
+  where
+  1*[x-0]≈x : 1# * (x - 0#) ≈ x
+  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x 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 ≈-Reasoning 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 ≈-Reasoning 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 ≈-Reasoning 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/Apartness/Structures.agda

@@ -17,27 +17,21 @@ module Algebra.Apartness.Structures
   where
 
 open import Level using (_⊔_; suc)
-open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
 open import Algebra.Definitions _≈_ using (Invertible)
 open import Algebra.Structures _≈_ using (IsCommutativeRing)
-open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
-open import Relation.Binary.Definitions using (Tight)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Binary.Structures
+  using (IsEquivalence; IsApartnessRelation; IsTightApartnessRelation)
 import Relation.Binary.Properties.ApartnessRelation as AR
 
 
 record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
-    isCommutativeRing   : IsCommutativeRing _+_ _*_ -_ 0# 1#
-    isApartnessRelation : IsApartnessRelation _≈_ _#_
+    isCommutativeRing        : IsCommutativeRing _+_ _*_ -_ 0# 1#
+    isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
 
   open IsCommutativeRing isCommutativeRing public
-  open IsApartnessRelation isApartnessRelation public
-
-  field
-    #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
-    invertible⇒# : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
+  open IsTightApartnessRelation isTightApartnessRelation public
 
   ¬#-isEquivalence : IsEquivalence _¬#_
   ¬#-isEquivalence = AR.¬#-isEquivalence refl isApartnessRelation
@@ -47,6 +41,10 @@ record IsHeytingField : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
     isHeytingCommutativeRing : IsHeytingCommutativeRing
-    tight                    : Tight _≈_ _#_
 
   open IsHeytingCommutativeRing isHeytingCommutativeRing public
+
+  field
+    #⇒invertible             : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
+    invertible⇒#             : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
+

src/Data/Rational/Properties.agda

@@ -1299,15 +1299,14 @@ module _ where
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
-    ; isApartnessRelation = ≉-isApartnessRelation
-    ; #⇒invertible = #⇒invertible
-    ; invertible⇒# = invertible⇒#
+    ; isTightApartnessRelation = ≉-isTightApartnessRelation
     }
 
   isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingField = record
     { isHeytingCommutativeRing = isHeytingCommutativeRing
-    ; tight = ≉-tight
+    ; #⇒invertible = #⇒invertible
+    ; invertible⇒# = invertible⇒#
     }
 
   heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ

src/Data/Rational/Unnormalised/Properties.agda

@@ -35,7 +35,7 @@ open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; DenseLinearOrder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
+  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTightApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
 import Relation.Binary.Consequences as BC
@@ -139,8 +139,13 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   }
 
 ≄-tight : Tight _≃_ _≄_
-proj₁ (≄-tight p q) ¬p≄q = Dec.decidable-stable (p ≃? q) ¬p≄q
-proj₂ (≄-tight p q) p≃q p≄q = p≄q p≃q
+≄-tight p q = Dec.decidable-stable (p ≃? q)
+
+≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
+≄-isTightApartnessRelation = record
+  { isApartnessRelation = ≄-isApartnessRelation
+  ; tight = ≄-tight
+  }
 
 ≃-setoid : Setoid 0ℓ 0ℓ
 ≃-setoid = record
@@ -1399,15 +1404,14 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
 +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingCommutativeRing = record
   { isCommutativeRing   = +-*-isCommutativeRing
-  ; isApartnessRelation = ≄-isApartnessRelation
-  ; #⇒invertible        = ≄⇒invertible
-  ; invertible⇒#        = invertible⇒≄
+  ; isTightApartnessRelation = ≄-isTightApartnessRelation
   }
 
 +-*-isHeytingField : IsHeytingField _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingField = record
   { isHeytingCommutativeRing = +-*-isHeytingCommutativeRing
-  ; tight                    = ≄-tight
+  ; #⇒invertible        = ≄⇒invertible
+  ; invertible⇒#        = invertible⇒≄
   }
 
 ------------------------------------------------------------------------