Tidying up in Relation.Binary.Construct.Closure (#1315)

* Use variables
* Deprecate non-standard closure names and proofs

Author: MatthewDaggitt

CHANGELOG.md

@@ -9,7 +9,9 @@ Highlights
 Bug-fixes
 ---------
 
-* Fixed List.Relation.Unary.All.Properties.map-id, which was abstracted over
+* The example module `Maybe` in `Relation.Binary.Construct.Closure.Reflexive` was accidentally exposed publicly. It has been made private.
+
+* Fixed the type of the proof `map-id` in `List.Relation.Unary.All.Properties`, which was incorrectly abstracted over
   unused module parameters.
 
 Non-backwards compatible changes
@@ -22,9 +24,21 @@ Non-backwards compatible changes
 Deprecated modules
 ------------------
 
+* The module `TransitiveClosure` in `Induction.WellFounded` has been deprecated. You should instead use the standard definition of transitive closure and the accompanying proof of well-foundness defined in `Relation.Binary.Construct.Closure.Transitive`.
+
 Deprecated names
 ----------------
 
+* In `Relation.Binary.Construct.Closure.Reflexive`:
+  ```agda
+  Refl ↦ ReflClosure
+  ```
+
+* In `Relation.Binary.Construct.Closure.Transitive`:
+  ```agda
+  Plus′ ↦ TransClosure
+  ```
+
 New modules
 -----------
 
@@ -67,6 +81,13 @@ Other minor additions
   IsLatticeIsomorphism   (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
   ```
 
+* Added new proofs to `Relation.Binary.Construct.Closure.Transitive`:
+  ```agda
+  reflexive   : Reflexive _∼_ → Reflexive _∼⁺_
+  symmetric   : Symmetric _∼_ → Symmetric _∼⁺_
+  transitive  : Transitive _∼⁺_
+  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
+
 * Added new definitions to `Algebra.Definitions`:
   ```agda
   AlmostLeftCancellative  e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z

src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda

@@ -201,7 +201,7 @@ private
   ix∙⁺jz : IPointwise (Plus _R_) ix jz
   ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ []
 
-  ¬ix⁺∙jz : ¬ Plus′ (IPointwise _R_) ix jz
+  ¬ix⁺∙jz : ¬ TransClosure (IPointwise _R_) ix jz
   ¬ix⁺∙jz [ iRj ∷ () ∷ [] ]
   ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ])
   ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _)

src/Induction/WellFounded.agda

@@ -39,10 +39,6 @@ WfRec _<_ P x = ∀ y → y < x → P y
 data Acc {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where
   acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x
 
-acc-inverse : ∀ {_<_ : Rel A ℓ} {x : A} (q : Acc _<_ x) →
-              (y : A) → y < x → Acc _<_ y
-acc-inverse (acc rs) y y<x = rs y y<x
-
 -- The accessibility predicate encodes what it means to be
 -- well-founded; if all elements are accessible, then _<_ is
 -- well-founded.
@@ -59,6 +55,10 @@ Please use WellFounded instead."
 ------------------------------------------------------------------------
 -- Basic properties
 
+acc-inverse : ∀ {_<_ : Rel A ℓ} {x : A} (q : Acc _<_ x) →
+              (y : A) → y < x → Acc _<_ y
+acc-inverse (acc rs) y y<x = rs y y<x
+
 Acc-resp-≈ : {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} → Symmetric _≈_ →
              _<_ Respectsʳ _≈_ → (Acc _<_) Respects _≈_
 Acc-resp-≈ sym respʳ x≈y (acc rec) =
@@ -146,6 +146,9 @@ module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
 \ \Please use wellFounded instead."
   #-}
 
+
+-- DEPRECATED in v1.4.
+-- Please use proofs in `Relation.Binary.Construct.On` instead.
 module InverseImage {_<_ : Rel B ℓ} (f : A → B) where
 
   accessible : ∀ {x} → Acc _<_ (f x) → Acc (_<_ on f) x
@@ -168,6 +171,9 @@ module InverseImage {_<_ : Rel B ℓ} (f : A → B) where
 \ \Please use wellFounded from `Relation.Binary.Construct.On` instead."
   #-}
 
+
+-- DEPRECATED in v1.5.
+-- Please use `TransClosure` from `Relation.Binary.Construct.Closure.Transitive` instead.
 module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where
 
   infix 4 _<⁺_
@@ -192,15 +198,17 @@ module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where
   wellFounded : WellFounded _<_ → WellFounded _<⁺_
   wellFounded wf = λ x → accessible (wf x)
 
+  {-# WARNING_ON_USAGE _<⁺_
+  "Warning: _<⁺_ was deprecated in v1.5.
+\ \Please use TransClosure from Relation.Binary.Construct.Closure.Transitive instead."
+  #-}
   downwards-closed = downwardsClosed
   {-# WARNING_ON_USAGE downwards-closed
-  "Warning: downwards-closed was deprecated in v0.15.
-\ \Please use downwardsClosed instead."
+  "Warning: downwards-closed was deprecated in v0.15."
   #-}
   well-founded     = wellFounded
   {-# WARNING_ON_USAGE well-founded
-  "Warning: well-founded was deprecated in v0.15.
-\ \Please use wellFounded instead."
+  "Warning: well-founded was deprecated in v0.15."
   #-}
 
 

src/Relation/Binary/Construct/Closure/Equivalence.agda

@@ -10,22 +10,40 @@
 module Relation.Binary.Construct.Closure.Equivalence where
 
 open import Function using (flip; id; _∘_)
-open import Level using (_⊔_)
+open import Level using (Level; _⊔_)
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive as Star
   using (Star; ε; _◅◅_; reverse)
-open import Relation.Binary.Construct.Closure.Symmetric as SC using (SymClosure)
+open import Relation.Binary.Construct.Closure.Symmetric as SC
+  using (SymClosure)
+
+private
+  variable
+    a ℓ ℓ₁ ℓ₂ : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- Definition
 
-EqClosure : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Rel A (a ⊔ ℓ)
+EqClosure : {A : Set a} → Rel A ℓ → Rel A (a ⊔ ℓ)
 EqClosure _∼_ = Star (SymClosure _∼_)
 
 ------------------------------------------------------------------------
--- Equivalence closures are equivalences.
+-- Operations
 
-module _ {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) where
+-- A generalised variant of map which allows the index type to change.
+gmap : {P : Rel A ℓ₁} {Q : Rel B ℓ₂} →
+       (f : A → B) → P =[ f ]⇒ Q → EqClosure P =[ f ]⇒ EqClosure Q
+gmap {Q = Q} f = Star.gmap f ∘ SC.gmap {Q = Q} f
+
+map : ∀ {P : Rel A ℓ₁} {Q : Rel A ℓ₂} →
+      P ⇒ Q → EqClosure P ⇒ EqClosure Q
+map = gmap id
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (_∼_ : Rel A ℓ) where
 
   reflexive : Reflexive (EqClosure _∼_)
   reflexive = ε
@@ -43,23 +61,8 @@ module _ {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) where
     ; trans = transitive
     }
 
-  setoid : Setoid a (a ⊔ ℓ)
-  setoid = record
-    { _≈_           = EqClosure _∼_
-    ; isEquivalence = isEquivalence
-    }
-
-------------------------------------------------------------------------
--- Operations
-
-module _ {a ℓ₁ ℓ₂} {A : Set a} where
-
-  -- A generalised variant of map which allows the index type to change.
-
-  gmap : ∀ {b} {B : Set b} {P : Rel A ℓ₁} {Q : Rel B ℓ₂} →
-         (f : A → B) → P =[ f ]⇒ Q → EqClosure P =[ f ]⇒ EqClosure Q
-  gmap {Q = Q} f = Star.gmap f ∘ SC.gmap {Q = Q} f
-
-  map : ∀ {P : Rel A ℓ₁} {Q : Rel A ℓ₂} →
-        P ⇒ Q → EqClosure P ⇒ EqClosure Q
-  map = gmap id
+setoid : {A : Set a} (_∼_ : Rel A ℓ) → Setoid a (a ⊔ ℓ)
+setoid _∼_ = record
+  { _≈_           = EqClosure _∼_
+  ; isEquivalence = isEquivalence _∼_
+  }

src/Relation/Binary/Construct/Closure/Reflexive.agda

@@ -15,42 +15,65 @@ open import Relation.Binary
 open import Relation.Binary.Construct.Constant using (Const)
 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
 
+private
+  variable
+    a ℓ ℓ₁ ℓ₂ : Level
+    A B : Set a
+
 ------------------------------------------------------------------------
--- Reflexive closure
+-- Definition
 
-data Refl {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
-  [_]  : ∀ {x y} (x∼y : x ∼ y) → Refl _∼_ x y
-  refl : Reflexive (Refl _∼_)
+data ReflClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
+  refl : Reflexive (ReflClosure _∼_)
+  [_]  : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _∼_ x y
 
-[]-injective : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} {x y p q} →
-               (Refl _∼_ x y ∋ [ p ]) ≡ [ q ] → p ≡ q
-[]-injective refl = refl
+------------------------------------------------------------------------
+-- Operations
 
--- Map.
+map : ∀ {R : Rel A ℓ₁} {S : Rel B ℓ₂} {f : A → B} →
+      R =[ f ]⇒ S → ReflClosure R =[ f ]⇒ ReflClosure S
+map R⇒S [ xRy ] = [ R⇒S xRy ]
+map R⇒S refl    = refl
 
-map : ∀ {a a′ ℓ ℓ′} {A : Set a} {A′ : Set a′}
-        {_R_ : Rel A ℓ} {_R′_ : Rel A′ ℓ′} {f : A → A′} →
-      _R_ =[ f ]⇒ _R′_ → Refl _R_ =[ f ]⇒ Refl _R′_
-map R⇒R′ [ xRy ] = [ R⇒R′ xRy ]
-map R⇒R′ refl    = refl
+------------------------------------------------------------------------
+-- Properties
 
 -- The reflexive closure has no effect on reflexive relations.
-
-drop-refl : ∀ {a ℓ} {A : Set a} {_R_ : Rel A ℓ} →
-            Reflexive _R_ → Refl _R_ ⇒ _R_
-drop-refl rfl [ x∼y ] = x∼y
+drop-refl : {R : Rel A ℓ} → Reflexive R → ReflClosure R ⇒ R
+drop-refl rfl [ xRy ] = xRy
 drop-refl rfl refl    = rfl
 
+[]-injective : {R : Rel A ℓ} → ∀ {x y p q} →
+               (ReflClosure R x y ∋ [ p ]) ≡ [ q ] → p ≡ q
+[]-injective refl = refl
+
 ------------------------------------------------------------------------
--- Example: Maybe
+-- Example usage
 
-module Maybe where
+private
+  module Maybe where
+    Maybe : Set a → Set a
+    Maybe A = ReflClosure (Const A) tt tt
+
+    nothing : Maybe A
+    nothing = refl
+
+    just : A → Maybe A
+    just = [_]
+
+
+
+------------------------------------------------------------------------
+-- Deprecations
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
 
-  Maybe : ∀ {ℓ} → Set ℓ → Set ℓ
-  Maybe A = Refl (Const A) tt tt
+-- v1.5
 
-  nothing : ∀ {a} {A : Set a} → Maybe A
-  nothing = refl
+Refl = ReflClosure
+{-# WARNING_ON_USAGE Refl
+"Warning: Refl was deprecated in v1.5.
+Please use ReflClosure instead."
+#-}
 
-  just : ∀ {a} {A : Set a} → A → Maybe A
-  just = [_]