Remove all external use of less-than-or-equal beyond Data.Nat.*

[jamesmckinna]

Following up on #2216 / #2217 (and #2250 ) with a 'pure' refactoring PR (so: no CHANGELOG entry required at this stage) which localises all uses of the retained-for-backwards-compatibility pattern synonym less-than-or-equal to Data.Nat.Base, Data.Nat.Properties, Data.Nat.Properties/WithK.

Outstanding issues (maybe):

• deprecation of the pattern synonym (in Data.Nat? or elsewhere?), which would require a CHANGELOG entry;
• the fix-up of the various Vec lengths in padRight, padBoth etc. at present use rewrite, but it might be cleaner to use Vec.cast with the appropriate equality (shoutout to @JacquesCarette for this);
• the ubiquity (now) of the 'pattern' of definition

f : ... (as : Vec≤ A n) ... 
f ... as@record { length = m ; vec = vs ; bound = m≤n } ...
  with ≤″-offset k ← recompute (_ ℕ.≤″? _) (ℕ.≤⇒≤″ m≤n) = ...

suggests that the design of the datatype might be revisited, to optimise for computing the offset k?

[jamesmckinna]

Re: revising the design

On reflection, I think the proof pattern alluded to above could be improved off-the-bat by:

• adding to Data.Nat.Properties, replacing these proofs, with

≤⇒≤″ : _≤_ ⇒ _≤″_
≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n

-- corollary

≤-proof : ∀ {m n} (le : m ≤ n) → ∃[ k ] m + k ≡ n
≤-proof le = _ , ≤″-proof (≤⇒≤″ le)

pattern ≤-offset k = k , refl
pattern <-offset k = ≤-offset k

-- equivalence to _≤_

≤″⇒≤ : _≤″_ ⇒ _≤_
≤″⇒≤ (≤″-offset k) = m≤m+n _ k

• and then rewriting the above proof pattern in Data.Vec.Bounded.Base as

  with ℕₚ.≤-offset k ← ℕₚ.≤-proof (recompute (_ ℕₚ.≤? _) m≤n)

thereby encapsulating all mention even of _≤″_ itself... not merely that of its smart constructor...

[JacquesCarette]

I would be a definite fan of doing this in two stages, i.e. first pull this in, and then your further improvements later, when they land.

[jamesmckinna]

OK, so let's merge this as it stands, and then I'll file a followup? Are you happy for me to hit 'merge'?

[JacquesCarette]

Well, I still think it shouldn't be the author who merges - but I'm happy to do it.

[jamesmckinna]

I agree re: self-merging, so I hadn't done so... ;-)