Rename preorder ~ relation reasoning combinators (#2156)

Author: MatthewDaggitt

src/Codata/Musical/Colist.agda

@@ -190,10 +190,12 @@ module ⊑-Reasoning {a} {A : Set a} where
 module ⊆-Reasoning {A : Set a} where
   private module Base = PreR (⊆-Preorder A)
 
-  open Base public hiding (step-∼)
+  open Base public
+    hiding (step-≲; step-∼)
+    renaming (≲-go to ⊆-go)
 
   open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x)
-  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
 
 
 -- take returns a prefix.

src/Data/Integer/Divisibility/Signed.agda

@@ -121,9 +121,11 @@ open _∣_ using (quotient) public
 module ∣-Reasoning where
   private module Base = PreorderReasoning ∣-preorder
 
-  open Base public hiding (step-∼; step-≈; step-≈˘)
+  open Base public
+    hiding (step-≲; step-∼; step-≈; step-≈˘)
+    renaming (≲-go to ∣-go)
 
-  open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public
+  open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∣-go public
 
 ------------------------------------------------------------------------
 -- Other properties of _∣_

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -96,8 +96,8 @@ module ⊆-Reasoning {A : Set a} where
   private module Base = PreorderReasoning (⊆-preorder A)
 
   open Base public
-    hiding (step-≈; step-≈˘; step-∼)
-    renaming (∼-go to ⊆-go)
+    hiding (step-≈; step-≈˘; step-∼; step-≲)
+    renaming (≲-go to ⊆-go)
 
   open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x) public
   open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

@@ -117,11 +117,13 @@ module ⊆-Reasoning (S : Setoid a ℓ) where
 
   private module Base = PreorderReasoning (⊆-preorder S)
 
-  open Base public hiding (step-∼; step-≈; step-≈˘)
+  open Base public
+    hiding (step-≲; step-≈; step-≈˘; step-∼)
+    renaming (≲-go to ⊆-go; ≈-go to ≋-go)
 
   open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → Base.begin x) public
-  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public
-  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ Base.≈-go public
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
+  open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go public
 
 ------------------------------------------------------------------------
 -- Relationship with other binary relations

src/Data/Nat/Divisibility.agda

@@ -120,9 +120,11 @@ suc n ∣? m      = Dec.map (m%n≡0⇔n∣m m (suc n)) (m % suc n ≟ 0)
 module ∣-Reasoning where
   private module Base = PreorderReasoning ∣-preorder
 
-  open Base public hiding (step-≈; step-≈˘; step-∼)
+  open Base public
+    hiding (step-≈; step-≈˘; step-∼; step-≲)
+    renaming (≲-go to ∣-go)
 
-  open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public
+  open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∣-go public
 
 ------------------------------------------------------------------------
 -- Simple properties of _∣_

src/Data/Rational/Properties.agda

@@ -164,7 +164,7 @@ drop-*≡* (*≡* eq) = eq
   ...   | refl = refl
 
 ≃-sym : Symmetric _≃_
-≃-sym = ≡⇒≃ ∘′ sym ∘′ ≃⇒≡ 
+≃-sym = ≡⇒≃ ∘′ sym ∘′ ≃⇒≡
 
 ------------------------------------------------------------------------
 -- Properties of ↥
@@ -753,7 +753,7 @@ module ≤-Reasoning where
 
   ≃-go : Trans _≃_ _IsRelatedTo_ _IsRelatedTo_
   ≃-go = Triple.≈-go ∘′ ≃⇒≡
-  
+
   open ≃-syntax _IsRelatedTo_ _IsRelatedTo_ ≃-go (λ {x y} → ≃-sym {x} {y}) public
 
 ------------------------------------------------------------------------

src/Data/Rational/Unnormalised/Properties.agda

@@ -164,7 +164,7 @@ p≃0⇒↥p≡0 p (*≡* eq) = begin
   ↥ p ℤ.* 1ℤ  ≡⟨ eq ⟩
   0ℤ           ∎
   where open ≡-Reasoning
-  
+
 ↥p≡↥q≡0⇒p≃q : ∀ p q → ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≃ q
 ↥p≡↥q≡0⇒p≃q p q ↥p≡0 ↥q≡0 = ≃-trans (↥p≡0⇒p≃0 p ↥p≡0) (≃-sym (↥p≡0⇒p≃0 _ ↥q≡0))
 

src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda

@@ -115,7 +115,9 @@ module _ {i t} {I : Set i} (T : Rel I t) where
 module StarReasoning {i t} {I : Set i} (T : Rel I t) where
   private module Base = PreorderReasoning (preorder T)
 
-  open Base public hiding (step-≈; step-∼)
+  open Base public
+    hiding (step-≈; step-∼; step-≲)
+    renaming (≲-go to ⟶-go)
 
-  open ⟶-syntax _IsRelatedTo_ _IsRelatedTo_ (Base.∼-go ∘ (_◅ ε)) public
-  open ⟶*-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public
+  open ⟶-syntax _IsRelatedTo_ _IsRelatedTo_ (⟶-go ∘ (_◅ ε)) public
+  open ⟶*-syntax _IsRelatedTo_ _IsRelatedTo_ ⟶-go public

src/Relation/Binary/Reasoning/Base/Double.agda

@@ -21,7 +21,7 @@ open import Relation.Binary.Reasoning.Syntax
 
 
 module Relation.Binary.Reasoning.Base.Double {a ℓ₁ ℓ₂} {A : Set a}
-  {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} (isPreorder : IsPreorder _≈_ _∼_)
+  {_≈_ : Rel A ℓ₁} {_≲_ : Rel A ℓ₂} (isPreorder : IsPreorder _≈_ _≲_)
   where
 
 open IsPreorder isPreorder
@@ -32,24 +32,24 @@ open IsPreorder isPreorder
 infix 4 _IsRelatedTo_
 
 data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
-  nonstrict : (x∼y : x ∼ y) → x IsRelatedTo y
+  nonstrict : (x≲y : x ≲ y) → x IsRelatedTo y
   equals    : (x≈y : x ≈ y) → x IsRelatedTo y
 
-start : _IsRelatedTo_ ⇒ _∼_
+start : _IsRelatedTo_ ⇒ _≲_
 start (equals x≈y) = reflexive x≈y
-start (nonstrict x∼y) = x∼y
+start (nonstrict x≲y) = x≲y
 
 ≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_
 ≡-go x≡y (equals y≈z) = equals (case x≡y of λ where P.refl → y≈z)
 ≡-go x≡y (nonstrict y≤z) = nonstrict (case x≡y of λ where P.refl → y≤z)
 
-∼-go : Trans _∼_ _IsRelatedTo_ _IsRelatedTo_
-∼-go x∼y (equals y≈z) = nonstrict (∼-respʳ-≈ y≈z x∼y)
-∼-go x∼y (nonstrict y∼z) = nonstrict (trans x∼y y∼z)
+≲-go : Trans _≲_ _IsRelatedTo_ _IsRelatedTo_
+≲-go x≲y (equals y≈z) = nonstrict (∼-respʳ-≈ y≈z x≲y)
+≲-go x≲y (nonstrict y≲z) = nonstrict (trans x≲y y≲z)
 
 ≈-go : Trans _≈_ _IsRelatedTo_ _IsRelatedTo_
 ≈-go x≈y (equals y≈z) = equals (Eq.trans x≈y y≈z)
-≈-go x≈y (nonstrict y∼z) = nonstrict (∼-respˡ-≈ (Eq.sym x≈y) y∼z)
+≈-go x≈y (nonstrict y≲z) = nonstrict (∼-respˡ-≈ (Eq.sym x≈y) y≲z)
 
 stop : Reflexive _IsRelatedTo_
 stop = equals Eq.refl
@@ -81,6 +81,21 @@ equalitySubRelation = record
 open begin-syntax  _IsRelatedTo_ start public
 open begin-equality-syntax  _IsRelatedTo_ equalitySubRelation public
 open ≡-syntax _IsRelatedTo_ ≡-go public
-open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public
 open ≈-syntax _IsRelatedTo_ _IsRelatedTo_ ≈-go Eq.sym public
+open ≲-syntax _IsRelatedTo_ _IsRelatedTo_ ≲-go public
 open end-syntax _IsRelatedTo_ stop public
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ≲-go public
+{-# WARNING_ON_USAGE step-∼
+"Warning: step-∼ and _∼⟨_⟩_ syntax was deprecated in v2.0.
+Please use step-≲ and _≲⟨_⟩_ instead. "
+#-}

src/Relation/Binary/Reasoning/Syntax.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Syntax for the building blocks of equational reasoning modules 
+-- Syntax for the building blocks of equational reasoning modules
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -26,7 +26,7 @@ open import Relation.Binary.PropositionalEquality.Core as P
 --   Codata/Guarded/Stream/Relation/Binary/Pointwise
 --   Codata/Sized/Stream/Bisimilarity
 --   Function/Reasoning
- 
+
 module Relation.Binary.Reasoning.Syntax where
 
 private
@@ -170,14 +170,20 @@ module _
   forward : ∀ (x : A) {y z} → S y z → R x y → T x z
   forward x yRz x∼y = step {x} x∼y yRz
 
-
-  -- Preorder syntax
+  -- Arbitrary relation syntax
   module ∼-syntax where
     infixr 2 step-∼
     step-∼ = forward
     syntax step-∼ x yRz x∼y = x ∼⟨ x∼y ⟩ yRz
 
 
+  -- Preorder syntax
+  module ≲-syntax where
+    infixr 2 step-≲
+    step-≲ = forward
+    syntax step-≲ x yRz x≲y = x ≲⟨ x≲y ⟩ yRz
+
+
   -- Partial order syntax
   module ≤-syntax where
     infixr 2 step-≤