[fix] Issue #1726: deprecates _≺_ in Data.Fin.Base plus its properties (#1868)

Author: jamesmckinna

CHANGELOG.md

@@ -888,6 +888,24 @@ Deprecated names
   raise    ↦  _↑ʳ_
   ```
 
+  Issue #1726: the relation `_≺_` and its single constructor `_≻toℕ_`
+  have been deprecated in favour of their extensional equivalent `_<_`
+  but omitting the inversion principle which pattern matching on `_≻toℕ_`
+  would achieve; this instead is proxied by the property `Data.Fin.Properties.toℕ<`.
+
+* In `Data.Fin.Induction`:
+  ```
+  ≺-Rec 
+  ≺-wellFounded
+  ≺-recBuilder
+  ≺-rec
+  ```
+
+  As with Issue #1726 above: the deprecation of relation `_≺_` means that these definitions
+  associated with wf-recursion are deprecated in favour of their `_<_` counterparts.
+  But it's not quite sensible to say that these definiton should be *renamed* to *anything*,
+  least of all those counterparts... the type confusion would be intolerable. 
+
 * In `Data.Fin.Properties`:
   ```
   toℕ-raise        ↦ toℕ-↑ʳ
@@ -898,6 +916,9 @@ Deprecated names
   eq?              ↦ inj⇒≟
   ```
 
+  Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated
+  in favour of their proxy counterparts `<⇒<′` and `<′⇒<`.
+
 * In `Data.Fin.Permutation.Components`:
   ```
   reverse            ↦ Data.Fin.Base.opposite

src/Data/Fin/Base.agda

@@ -290,9 +290,6 @@ _>_ : IRel Fin 0ℓ
 i > j = toℕ i ℕ.> toℕ j
 
 
-data _≺_ : ℕ → ℕ → Set where
-  _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n
-
 ------------------------------------------------------------------------
 -- An ordering view.
 
@@ -335,3 +332,15 @@ NB argument order has been flipped:
 the left-hand argument is the Fin m
 the right-hand is the Nat index increment."
 #-}
+
+data _≺_ : ℕ → ℕ → Set where
+  _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n
+
+{-# WARNING_ON_USAGE _≺_
+"Warning: _≺_ was deprecated in v2.0.
+Please use equivalent relation _<_ instead."
+#-}
+{-# WARNING_ON_USAGE _≻toℕ_
+"Warning: _≻toℕ_ was deprecated in v2.0.
+Please use toℕ<n from Data.Fin.Properties instead."
+#-}

src/Data/Fin/Induction.agda

@@ -5,6 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
 
 open import Data.Fin.Base
 open import Data.Fin.Properties
@@ -20,7 +21,8 @@ open import Function.Base using (flip; _$_)
 open import Induction
 open import Induction.WellFounded as WF
 open import Level using (Level)
-open import Relation.Binary using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder)
+open import Relation.Binary
+  using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder)
 import Relation.Binary.Construct.Converse as Converse
 import Relation.Binary.Construct.Flip as Flip
 import Relation.Binary.Construct.NonStrictToStrict as ToStrict
@@ -94,24 +96,6 @@ private
   ... | no  n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
     where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
-------------------------------------------------------------------------
--- Induction over _≺_
-
-≺-Rec : RecStruct ℕ ℓ ℓ
-≺-Rec = WfRec _≺_
-
-≺-wellFounded : WellFounded _≺_
-≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded
-
-module _ {ℓ} where
-  open WF.All ≺-wellFounded ℓ public
-    renaming
-    ( wfRecBuilder to ≺-recBuilder
-    ; wfRec        to ≺-rec
-    )
-    hiding (wfRec-builder)
-
-
 ------------------------------------------------------------------------
 -- Well-foundedness of other (strict) partial orders on Fin
 
@@ -159,3 +143,43 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
                   WellFounded (flip (ToStrict._<_ _≈_ _⊑_))
   po-noetherian isPO =
     spo-noetherian (ToStrict.<-isStrictPartialOrder _≈_ _ isPO)
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+≺-Rec : RecStruct ℕ ℓ ℓ
+≺-Rec = WfRec _≺_
+
+≺-wellFounded : WellFounded _≺_
+≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded
+
+module _ {ℓ} where
+  open WF.All ≺-wellFounded ℓ public
+    renaming
+    ( wfRecBuilder to ≺-recBuilder
+    ; wfRec        to ≺-rec
+    )
+    hiding (wfRec-builder)
+
+{-# WARNING_ON_USAGE ≺-Rec
+"Warning: ≺-Rec was deprecated in v2.0.
+Please use <-Rec instead."
+#-}
+{-# WARNING_ON_USAGE ≺-wellFounded
+"Warning: ≺-wellFounded was deprecated in v2.0.
+Please use <-wellFounded instead."
+#-}
+{-# WARNING_ON_USAGE ≺-recBuilder
+"Warning: ≺-recBuilder was deprecated in v2.0.
+Please use <-recBuilder instead."
+#-}
+{-# WARNING_ON_USAGE ≺-rec
+"Warning: ≺-rec was deprecated in v2.0.
+Please use <-rec instead."
+#-}
+

src/Data/Fin/Properties.agda

@@ -6,6 +6,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
 
 module Data.Fin.Properties where
 
@@ -166,7 +167,7 @@ toℕ≤n : ∀ (i : Fin n) → toℕ i ℕ.≤ n
 toℕ≤n {suc n} i = ℕₚ.m≤n⇒m≤1+n (toℕ≤pred[n] i)
 
 toℕ<n : ∀ (i : Fin n) → toℕ i ℕ.< n
-toℕ<n {suc n} i = s≤s (toℕ≤pred[n] i)
+toℕ<n {suc n} i = s<s (toℕ≤pred[n] i)
 
 -- A simpler implementation of toℕ≤pred[n],
 -- however, with a different reduction behavior.
@@ -758,18 +759,6 @@ lift-injective f inj (suc k) {zero}  {zero}  eq = refl
 lift-injective f inj (suc k) {suc _} {suc _} eq =
   cong suc (lift-injective f inj k (suc-injective eq))
 
-------------------------------------------------------------------------
--- _≺_
-------------------------------------------------------------------------
-
-≺⇒<′ : _≺_ ⇒ ℕ._<′_
-≺⇒<′ (n ≻toℕ i) = ℕₚ.≤⇒≤′ (toℕ<n i)
-
-<′⇒≺ : ℕ._<′_ ⇒ _≺_
-<′⇒≺ {n} ℕ.≤′-refl = subst (_≺ suc n) (toℕ-fromℕ n) (suc n ≻toℕ fromℕ n)
-<′⇒≺ (ℕ.≤′-step m≤′n) with <′⇒≺ m≤′n
-... | n ≻toℕ i = subst (_≺ suc n) (toℕ-inject₁ i) (suc n ≻toℕ _)
-
 ------------------------------------------------------------------------
 -- pred
 ------------------------------------------------------------------------
@@ -1133,3 +1122,33 @@ eq? = inj⇒≟
 "Warning: eq? was deprecated in v2.0.
 Please use inj⇒≟ instead."
 #-}
+
+private
+
+  z≺s : ∀ {n} → zero ≺ suc n
+  z≺s = _ ≻toℕ zero
+
+  s≺s : ∀ {m n} → m ≺ n → suc m ≺ suc n
+  s≺s (n ≻toℕ i) = (suc n) ≻toℕ (suc i)
+
+  <⇒≺ : ℕ._<_ ⇒ _≺_
+  <⇒≺ {zero}  z<s      = z≺s
+  <⇒≺ {suc m} (s<s lt) = s≺s (<⇒≺ lt)
+
+  ≺⇒< : _≺_ ⇒ ℕ._<_
+  ≺⇒< (n ≻toℕ i) = toℕ<n i
+
+≺⇒<′ : _≺_ ⇒ ℕ._<′_
+≺⇒<′ lt = ℕₚ.<⇒<′ (≺⇒< lt)
+{-# WARNING_ON_USAGE ≺⇒<′
+"Warning: ≺⇒<′ was deprecated in v2.0.
+Please use <⇒<′ instead."
+#-}
+
+<′⇒≺ : ℕ._<′_ ⇒ _≺_
+<′⇒≺ lt = <⇒≺ (ℕₚ.<′⇒< lt)
+{-# WARNING_ON_USAGE <′⇒≺
+"Warning: <′⇒≺ was deprecated in v2.0.
+Please use <′⇒< instead."
+#-}
+