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

CHANGELOG.md

@@ -50,6 +50,10 @@ Highlights
 Bug-fixes
 ---------
 
+* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation`
+  to `#-sym` in order to avoid overloaded projection. The field names
+  `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
+
 * Removed unnecessary parameter `zero : Zero 0# *` from
   `Algebra.Structures.IsNonAssociativeRing`.
 
@@ -72,6 +76,21 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The definitions of `Algebra.Structures.IsHeyting*` and
+  `Algebra.Bundles.Heyting*` have been refactored, together
+  with that of `Relation.Binary.Definitions.Tight` on which they depend.
+  Specifically:
+  - `Tight _≈_ _#_` has been redefined as `∀ x y → ¬ x # y → x ≈ y`,
+    dropping the redundant second conjunct, because it is equivalent to
+    `Irreflexive _≈_ _#_`.
+  - new definitions: `(Is)TightApartnessRelation` structure/bundle, exploiting
+    the above redefinition.
+  - the definition of `HeytingCommutativeRing` now drops the properties of
+    invertibility, in favour of moving them to `HeytingField`.
+  - both `Heyting*` algebraic structure/bundles have been redefined to base
+    off an underlying `TightApartnessRelation`.
+  - both also further require `_+_`/`_*_` to be `StronglyExtensional` wrt `_#_`.
+
 * A major overhaul of the `Function` hierarchy sees the systematic development
   and use of the theory of the left inverse `from` to a given `Surjective` function
   `to`, as a consequence of which we can achieve full symmetry of `Bijection`, in
@@ -177,6 +196,12 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Apartness.Properties.HeytingCommutativeRing`:
+  ```agda
+  x-0≈x  ↦   Algebra.Properties.Ring.x-0#≈x
+  #-sym  ↦   Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym
+  ```
+
 * In `Algebra.Definitions`:
   ```agda
   StarLeftExpansive     ↦  Relation.Binary.Definitions.KleeneAlgebra.StarLeftExpansive
@@ -277,6 +302,15 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Apartness.Consequences`, relationships between definitions, given
+  properties of a given apartness relation, notably `Cotransitive _#_`.
+
+* `Algebra.Apartness.Definitions`, properties of algebraic operations wrt
+  a given apartness relation `_#_`.
+
+* `Algebra.Apartness.Properties.HeytingField`, refactoring the existing
+  `Algebra.Apartness.Properties.HeytingCommutativeRing`.
+
 * `Algebra.Properties.KleeneAlgebra` has been completely rewritten.
 
 * `Codata.Guarded.Stream.Relation.Unary.Linked` for a proof that each pair
@@ -317,6 +351,18 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Apartness.Bundles.HeytingCommutativeRing`:
+  ```agda
+  TightApartnessRelation c ℓ₁ ℓ₂ : Set _
+  ```
+
+* In `Algebra.Apartness.Structures.IsHeytingCommutativeRing`:
+  ```agda
+  IsTightApartnessRelation _≈_ _#_ : Set _
+  +-stronglyExtensional : StronglyExtensional _#_ _+_
+  *-stronglyExtensional : StronglyExtensional _#_ _*_
+  ```
+
 * In `Algebra.Consequences.Base`:
   ```agda
   almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ →
@@ -347,6 +393,21 @@ Additions to existing modules
   Except_RightCancellative_    : (P : Pred A p) → Op₂ A → Set _
   ```
 
+* In `Algebra.Properties.AbelianGroup`:
+  ```agda
+  x-ε≈x : RightIdentity ε _-_
+  ```
+
+* In `Algebra.Properties.RingWithoutOne`:
+  ```agda
+  x-0#≈x : RightIdentity 0# _-_
+  ```
+
+* In `Algebra.Structures.IsKleeneAlgebra`:
+  ```agda
+  _≤_            : Rel A _
+  ```
+
 * In `Algebra.Properties.KleeneAlgebra`:
   ```agda
   ≤-reflexive    : _≈_ ⇒ _≤_
@@ -359,11 +420,6 @@ Additions to existing modules
   poset          : Poset _ _
   ```
 
-* In `Algebra.Structures.IsKleeneAlgebra`:
-  ```agda
-  _≤_            : Rel A _
-  ```
-
 * In `Data.Bool.Properties`:
   ```agda
   ∨-monoid : Monoid 0ℓ 0ℓ
@@ -478,6 +534,29 @@ Additions to existing modules
                 (q ℤ.* + p) / (r ℕ.* p) ≡ q / r
   i/n+j/n≡[i+j]/n : ∀ (i j : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n }} →
                     i / n + j / n ≡ (i ℤ.+ j) / n
+  +-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≢_ (p +_)
+  +-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≢_ (_+ r)
+  +-stronglyCongruent   : StronglyCongruent₂ _≢_ _+_
+  +-stronglyExtensional : StronglyExtensional _≢_ _+_
+  *-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≢_ (p *_)
+  *-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≢_ (_* r)
+  *-stronglyCongruent   : StronglyCongruent₂ _≢_ _*_
+  *-stronglyExtensional : StronglyExtensional _≢_ _*_
+  ```
+
+* In `Data.Rational.Unnormalised.Properties`:
+  ```agda
+  ≄-apartnessRelation        : ApartnessRelation _ _ _
+  ≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
+  ≄-tightApartnessRelation   : TightApartnessRelation _ _ _
+  +-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≄_ (p +_)
+  +-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≄_ (_+ r)
+  +-stronglyCongruent   : StronglyCongruent₂ _≄_ _+_
+  +-stronglyExtensional : StronglyExtensional _≄_ _+_
+  *-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≄_ (p *_)
+  *-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≄_ (_* r)
+  *-stronglyCongruent   : StronglyCongruent₂ _≄_ _*_
+  *-stronglyExtensional : StronglyExtensional _≄_ _*_
   ```
 
 * In `Data.Vec.Properties`:
@@ -596,6 +675,7 @@ Additions to existing modules
 
   HalfRightAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
   HalfRightAdjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y)
+
   module KleeneAlgebra (_≤_ : Rel A ℓ₁) where
     StarLeftExpansive     : ∀ (e : A) (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
     StarRightExpansive    : ∀ (e : A) (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
@@ -605,6 +685,17 @@ Additions to existing modules
     StarDestructive       : ∀ (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
   ```
 
+* In `Relation.Binary.Properties.DecSetoid`:
+  ```agda
+  ≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
+  ≉-tightApartnessRelation   : TightApartnessRelation _ _ _
+  ```
+  Additionally,
+  ```agda
+  ≉-tight : Tight _≈_ _≉_
+  ```
+  has been redefined to reflect the change in the definition of `Tight`.
+
 * In `Relation.Unary`:
   ```agda
   Unique         : Rel A ℓ₁ → Pred A ℓ₂ → Pred A _

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 using (IsHeytingCommutativeRing; IsHeytingField)
@@ -36,8 +36,11 @@ 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 }
+
+  open TightApartnessRelation tightApartnessRelation public
+    using (apartnessRelation)
 
 
 record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -61,5 +64,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; apartnessRelation)

src/Algebra/Apartness/Consequences.agda

@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Lemmas relating algebraic definitions wrt an apartness.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Algebra.Apartness.Consequences
+  {a ℓ} {A : Set a} (_#_ : Rel A ℓ) where
+
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Apartness.Definitions _#_
+open import Data.Product.Base using (_,_)
+import Data.Sum.Base as Sum
+open import Level using (Level)
+open import Relation.Binary.Definitions
+  using (Cotransitive)
+
+private
+  variable
+    r : Level
+    f : Op₁ A
+    _∙_ : Op₂ A
+
+
+------------------------------------------------------------------------
+-- Cotransitive plus StronglyCongruent₂ implies StronglyExtensional
+
+cotransitive∧congruent⇒extensional : Cotransitive _#_ →
+  StronglyCongruent₂ _∙_ → StronglyExtensional _∙_
+cotransitive∧congruent⇒extensional
+  {_∙_ = _∙_} cotrans cong@(congˡ , congʳ) {y = y} {w = w} xy#wz
+  = Sum.map (congʳ y) (congˡ w) (cotrans xy#wz (w ∙ y))

src/Algebra/Apartness/Definitions.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of operations, relative to an apartness relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel; _⇒_)
+
+module Algebra.Apartness.Definitions
+  {a ℓ} {A : Set a}   -- The underlying set
+  (_#_ : Rel A ℓ)     -- The underlying apartness
+  where
+
+open import Algebra.Core using (Op₁; Op₂)
+open import Data.Product.Base using (_×_)
+open import Data.Sum.Base using (_⊎_)
+open import Function.Base using (_on_)
+
+
+------------------------------------------------------------------------
+-- Properties of operations
+
+module _ (f : Op₁ A) where
+
+  StronglyCongruent₁  : Set _
+  StronglyCongruent₁  = (_#_ on f) ⇒ _#_
+
+module _ (_∙_ : Op₂ A) where
+
+  StronglyCongruent₂ : Set _
+  StronglyCongruent₂ =
+    (∀ x → StronglyCongruent₁ (x ∙_)) × (∀ z → StronglyCongruent₁ (_∙ z))
+
+  StronglyExtensional : Set _
+  StronglyExtensional = ∀ {x y w z} → (x ∙ y) # (w ∙ z) → x # w ⊎ y # z
+

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -9,76 +9,31 @@
 open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 
 module Algebra.Apartness.Properties.HeytingCommutativeRing
-  {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
+  {c ℓ₁ ℓ₂} (heytingCommutativeRing : 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.Bundles using (CommutativeRing)
 
-open HeytingCommutativeRing HCR
-open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
+open HeytingCommutativeRing heytingCommutativeRing using (commutativeRing)
+open CommutativeRing commutativeRing using (ring)
+open import Algebra.Properties.Ring ring using (x-0#≈x)
 
-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
-
-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)
-  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# ∎
-
-#-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))
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 3.0
+
+x-0≈x = x-0#≈x
+{-# WARNING_ON_USAGE x-0≈x
+"Warning: x-0≈x was deprecated in v3.0.
+Please use Algebra.Properties.Ring.x-0#≈x instead."
+#-}
+
+open HeytingCommutativeRing heytingCommutativeRing public using (#-sym)
+{-# WARNING_ON_USAGE #-sym
+"Warning: #-sym was deprecated in v3.0.
+Please use Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym instead."
+#-}