Refactor/deprecate Data.Nat.Base._≤‴_ and its properties

[jamesmckinna]

@tsung-ju 's recent #2503 drew my attention to two things:

• the relation is, in fact, never used in stdlib, so is a good candidate for deprecation; cf. Deprecate _≺_ in Data.Fin.Base #1726
• failing that (maybe someone out there does, in fact, use it? UPDATED: @tsung-ju in fact!), the constructor ≤‴-refl : ∀{m} → m ≤‴ m, with its repeated occurrence of the m, in fact gives rise to unification problems for the typechecker under the ambient options without-K or cubical-compatible, requiring in the open PR a circumlocution via a lemma which cuts in an explicit appeal to equality...

If we opt to deprecate the relation, then all well and good as to the first point... but the second suggests a wider library-design issue/pattern that we might wish to more systematically deploy: avoid repeated arguments in data constructors... unless with-K is in operation?

Eg. replacing the current definition with

data _≤‴_ (m n : ℕ) : Set

_<‴_ : (m n : ℕ) → Set
m <‴ n = suc m ≤‴ n

data _≤‴_ m n where
  ≤‴-reflexive : m ≡ n → m ≤‴ n
  ≤‴-step : m <‴ n → m ≤‴ n

pattern ≤‴-refl = ≤‴-reflexive refl

(and hence a possible additional refactoring in terms of Relation.Binary.Construct.Closure.Reflexive etc.)

UPDATED: the above definition moreover admits (much?) more direct proofs of ≤‴⇒≤ and ≤⇒≤‴ (aah... but with bad complexity, cf. #2440 #2442 )

≤‴⇒≤ : m ≤‴ n → m ≤ n
≤‴⇒≤ (≤‴-reflexive eq) = ≤-reflexive eq
≤‴⇒≤ (≤‴-step m<n) = <⇒≤ (≤‴⇒≤ m<n)

s≤‴s : m ≤‴ n → suc m ≤‴ suc n
s≤‴s (≤‴-reflexive m≡n) = ≤‴-refl $ cong suc m≡n
s≤‴s (≤‴-step m<n) = ≤‴-step (s≤‴s m<n)

0≤‴n : ∀ n → 0 ≤‴ n
0≤‴n zero    = ≤‴-refl
0≤‴n (suc n) = ≤‴-step (s≤‴s (0≤‴n n))

≤⇒≤‴ : _≤_ ⇒ _≤‴_
≤⇒≤‴ z≤n       = 0≤‴n _
≤⇒≤‴ (s≤s m≤n) = s≤‴s $ ≤⇒≤‴ m≤n

But with cleaner proofs of

≤‴⇒≤″ : m ≤‴ n → m ≤″ n
≤‴⇒≤″  ≤‴-refl      = _ , +-identityʳ _
≤‴⇒≤″ (≤‴-step m≤n) = _ , trans (+-suc _ _) (≤″-proof (≤‴⇒≤″ m≤n))

m≤‴m+k : m + k ≡ n → m ≤‴ n
m≤‴m+k {k = zero}  = ≤‴-reflexive ∘ trans (sym (+-identityʳ _))
m≤‴m+k {k = suc _} = ≤‴-step ∘ m≤‴m+k ∘ trans (sym (+-suc _ _))

and from #2503

≤‴-irrelevant : Irrelevant _≤‴_
≤‴-irrelevant (≤‴-reflexive eq₁) (≤‴-reflexive eq₂) = cong ≤‴-reflexive (≡-irrelevant eq₁ eq₂)
≤‴-irrelevant (≤‴-reflexive eq₁) (≤‴-step q)        with () ← <‴-irrefl eq₁ q
≤‴-irrelevant (≤‴-step p)        (≤‴-reflexive eq₂) with () ← <‴-irrefl eq₂ p
≤‴-irrelevant (≤‴-step p)        (≤‴-step q)        = cong ≤‴-step (≤‴-irrelevant p q)

[MatthewDaggitt]

Hmm I don't really have much to add to this, except that the names of these relations are getting more and more ridiculous! I agree with @JacquesCarette that eventually we should have smaller Data.Nat.Relation.Binary (or ideally Data.Nat.Order, see #1763) files for each of them.

[jamesmckinna]

As to the "ridiculous" names, these have been there already for a long time (before my time!), but I am sympathetic to your general point (and that of #1763 ) about trying to 'manage' this state of affairs.

My only contribution here is to try to streamline this one better, now that someone (for better or worse) is actually using it in anger!

[MatthewDaggitt]

Yup agreed! Sorry for the off-topic rant!

[JacquesCarette]

If we were in "full maintenance" mode, then all the suggestions in the issue itself make sense. Deprecating this probably makes even more sense.

[jamesmckinna]

If we were in "full maintenance" mode, then all the suggestions in the issue itself make sense.

I'm not familiar with what you intend by this term-of-art. Can you say more?

Deprecating this probably makes even more sense.

Well, I thought so, too, but I'm rethinking that ... on the basis of symmetry with _≤′_

And as for Matthew's comments on names, any hypothetical-rewrite would surely want to choose 'better' ones!

[JacquesCarette]

What I mean by "full maintenance" is if all we were doing were point releases with bug fixes and small additions and nothing else.

We're still (re)designing stdlib, as well as hoping to add significant functionality!

[jamesmckinna]

What I mean by "full maintenance" is if all we were doing were point releases with bug fixes and small additions and nothing else.

Thanks for the clarification!

We're still (re)designing stdlib, as well as hoping to add significant functionality!

Agreed, and really the only reasons to lift this issue out explicitly were:

• Agda issue Problem supplying infix parameters to data declaration? agda#7620
• the library-design aspect of (recommending) non-duplicated parameters/indices in data under --without-K The type of a data constructor should *not* have repeated indices unless defined within the scope of with-K #2519

The former as a horrible UX failure; the latter as part of a 'better' re-design philosophy?

[JacquesCarette]

On the last point, agree: we shouldn't repeat parameters/indices, we should ask for a witness of that fact instead.

[jamesmckinna]

What I mean by "full maintenance" is if all we were doing were point releases with bug fixes and small additions and nothing else.

Well, we do have an as-yet not-really discussed question as to whether we continue with v2.x point releases in the short-term, while planning for a great leap forward to v3.0, and, absent such discussions (#2352 hasn't been revisited for a while, nor its principal suggestion as to how to organise such discussion...), perhaps point releases are the way to go for now?

For my money, the above provides 'easy' fixes to the current situation, but at the same time at the cost (in Data.Nat.Base) of introducing a pattern synonym which would/might need to be subsequently deprecated. Otherwise I'd raise a PR now to knock this one off. Previously we've frowned on introducing too many pattern synonyms on Base (also because of a refactoring of an ordering relation on Nat!!!), because of potential ambiguity problems, but here I don't think such an objection applies?

Accordingly, have changed this to v2.2, but that's up for discussion!

[JacquesCarette]

The pattern is unlikely to clash with other things (name is too obscure for that), true enough. But this is Data.Nat.Base we're talking about, I think the bar should be higher!

[jamesmckinna]

Re: high bars

I think the 'right' way to raise that bar would eventually be to break these relations out under Data.Nat.<something> (interestingly, none of those proposals suggest the *.Relation.Binary.* subhierarchy we have under Data.List etc...?), but in the meantime, we're in the incremental improvement business?

So the 'cost'/'value' of each such increment does need to be weighed up, for sure.