Cleaning up dependencies on Data.Fin and Data.Nat ahead of a first attempt to fix Issue1686

[jamesmckinna]

Along the lines of the 'worker/wrapper' distinction I made in the discussion of the issue.

Outstanding task(s):

• CHANGELOG, as ever;
• Algebra.Properties.CommutativeMonoid.Sum
• Data.Fin.Base
• Data.Fin.Properties
• Data.List.Properties
• Data.Vec.Base
• Data.Vec.Functional
• Data.Vec.Properties
• Data.Vec.Recursive
• Data.Vec.Relation.Unary.All
• Data.Vec.Relation.Unary.Any
• Data.Vec.Relation.Unary.Linked.Properties

EDITED: These are now both pending, given Matthew's comments below.
UPDATED: the above task list shows all (at least) the files needing to be touched by the PR
I'd like to merge the existing changes first before proceeding to working on them.

[jamesmckinna]

Hmmm. I think that this is now OK, but I am slightly worried that the previous commits to agda/master which needed to have their merge conflicts resolved, are now part of this PR? Ooops, if so, and I'll try again later.

Otherwise, this PR is the 'part I' alluded to above: namely groundwork preparation (mostly dependency thinning; and no (?) new functions or deprecations) ahead of the more controversial part II, where NonZero-bracketed functions and their properties get propagated throughout. Towards such a move, all the imports of Data.Nat{.Base} now explicitly import NonZero and pred, ahead of their eventual (heavy) use to implement Matthew's proposal. But further discussion of that required, it would seem.

[jamesmckinna]

Following f2f discussion with @MatthewDaggitt today, my revised proposal is to:

• retain existing functionality as 'worker' functions, with their existing names, reflecting that they are the 'more dependent' (because their types involve inhomogeneous telescopes eg {n : ℕ} (i : Fin (suc n)))
• in place of the original, ugly, NZ prefix to the above, write 'wrapper' functions with the same names, but primed, for the corresponding homogeneous operations prefixed on a {{NonZero n} instance (because 'less dependent' here = homogeneously telescoped)

I'll push those commits another day, once this proposed naming convention has settled (?).

[MatthewDaggitt]

Difficult to judge the utility of this without the context that it is being used. Any chance we could keep this and nℕ-suci<n to the follow up PR?

[jamesmckinna]

Matthew,
this function is not currently used, but since at various points in the library there are uses of its (grotesque) definitional equivalent n ∸ suc (toℕ i) I thought it worth lifting out as something in its own right; but admittedly in obscure corners:

• Data.Fin.Properties.opposite-prop, Data.Fin.Properties.opposite-suc
• Data.List.Properties.lookup-applyDownFrom, Data.List.Properties.lookup-downFrom

So very easy to prune this, and its properties, back. But it is an example of a 'naturally'-occurring homogeneously-telescoped function on Fin n, so in the spirit of this PR.

[MatthewDaggitt]

Okay, in which case could you make use of it in this PR to simplify the code that you mention?

My deepest apologies if this was previously in this PR before and you have to add it back in. I'm just playing the part of Goldilocks. Previously the PR was too big to review, but now it contains too small in that it contains this partial change that doesn't stand on its own. In general, we tend to like each PR to stand on its own as people (including me!) promise to do things, but don't actually come back and do it! Not implying that you will, but as a general rule these things happen! Therefore we like each PR to be an obvious standalone improvement over the existing code. Adding a function that is never used doesn't quite pass this test.

[jamesmckinna]

Ha! No, it wasn't, more that I had been laying the groundwork for it... much as I had been enriching the imports of Data.Nat with NonZero and pred.

But you make a good point. When I reinstate it, I'll also use it! Or did you want this to happen now, as opposed to later as part of the whole head/head' etc. enrichment?

[MatthewDaggitt]

Don't mind, happy either way. Whichever you'd prefer!

[jamesmckinna]

Some more tidying up possible: don't push yet!