Lighten dependencies of Data.Nat.Induction

[MatthewDaggitt]

Removed a bunch of unused imports. Would really really like to get rid of the last remaining dependency on Data.Nat.Properties...

[jamesmckinna]

There's an potential alternative proof using m≤n⇒m<n∨m≡n also from Data.Nat.Properties ... for the cost of an import of Data.Sum. Potayto, potahto.

Part of the issue seems to be how much Data.Nat.Properties covers everything and isn't factored into properties of the order, properties of the operations...

... and the fact that m≤n⇒m<n∨m≡n itself is a property, not a definition (which would then eliminate the dependency entirely). I guess that's a separate can of worms.

[jamesmckinna]

And indeed... the lemma above doesn't really belong, as now, in

-- Properties of _+_ and _≤_/_<_

but rather in

-- Other properties of _<_

in that vast collection...

[jamesmckinna]

So the thing that surprised me is that in Agda.Builtin.Nat, the strict ordering is defined as _<_ (renamed to to _<ᵇ_ in Data.Nat.Base), with the 'obvious' definitional rules (as counterparts to the constructors were it to be defined inductively) , and then defines _≤ᵇ_ /_≤_ in terms of it (in the highly Nat-specific way in terms of successor), whereas Data.Nat.Base defines _≤_ inductively and then defines _<_ in the highly Nat-specific way in terms of _≤_ and successor, rather than what I might have expected, namely defining _≤_ as the reflexive closure of the strict relation (however defined).

As you have observed many times before, there are no right answers here, so my comment/question is really about trying to understanding why certain design decisions have been made in stdlib, and specifically here, why the preorder relation/structure is considered conceptually prior to the strict order, when the builtin version appears to make the 'opposite' choice...

[JacquesCarette]

If I had to guess: accident of history. Various pieces of code evolving independently, and only later clashing by using opposite conventions. As you say, there's no right/wrong here, just lack of harmony.

[jamesmckinna]

Indeed, I can imagine. The curiosity, such as it is, about the, viz. Matthew's, issue/PR, is that judicious choices, congruent with certain others in the stdlib, would/could remove the dependence on Data.Nat.Properties entirely... but that alone is not, perhaps, a hill large enough on which to take a stand...

[JacquesCarette]

I've been on a bit of a simplify-the-dependency graph kick (actively so some months ago, on pause right now mostly for lack of time.) Weird dependencies, in my opinion, will have a real effect down the road when growth becomes increasingly difficult because of cycles.

Axiom went down the route to allow cycles... and ended up with cycles with over 150 modules needing to be type-checked "as one" !

[jamesmckinna]

Hmmm. Maybe I spoke too soon. The lemma one actually requires for _<_ would/should be
m<1+n⇒m<n∨m≡n, which isn't in the library, except as an accident of being definitionally equal to the above lemma, for the particular choices made. But it probably should be a thing in its own right, as an 'intrinsic' property of _<_. And it isn't definitionally the case, for any of the choices made in Data.Nat.Base, so some dependency might still be required @MatthewDaggitt . Ah well.

If interested, I made a branch, pr1698 on my fork, for comparison, but I won't open a competing PR (yet ;-)).

[MatthewDaggitt]

Thanks for the investigations! Yes I agree, the way that the orders are defined in Data.Nat.Base is not very pleasing. Indeed see #1179 for a proposal to get round some of the problems that are caused. As you guessed and @JacquesCarette confirmed, the reasons are indeed historical and long pre-date my involvement with the library. The dependency on Data.Sum wouldn't be a problem, as sums are considered "more primitive" than natural numbers in the library in terms of dependecies. I'm not sure it's something we can change at this point though, as so much code relies on the way it's setup currently.

The lemma one actually requires for < would/should be
m<1+n⇒m<n∨m≡n, which isn't in the library,

That's a curious lemma. I've currently broken my installation of Agda, but will have a look at your branch once I've got it running again.

[jamesmckinna]

So... the 'curious' lemma indeed has the identical proof structure to m≤n⇒m<n∨m≡n (which is then a trivial corollary, modulo a constructor), but is (deliberately) phrased purely in terms of _<_, and mutatis mutandis would exhibit the analogous relationship between _<_ and _<'_ (were they to be given inductively) as between _≤_ and _≤'_ currently exploited in Induction.WF. So it's more, perhaps, a question of "Six of one, ..." but I find it odd to have WF proofs (about _<_) phrased in terms of properties of _≤_

[jamesmckinna]

So... there's a discussion perhaps to take offline, until I can get my ideas straight in advance of raising an issue/PR (but see below). Some points, more or less in dependency order:

1. Data.Nat.Properties, as previously observed, is both heavily dependent on particular choices of definitions in Data.Nat.Base, but also on redundant repetition of what could otherwise be reified smart constructors associated with those choices, eg

z<s : ∀ {n} → zero < suc n
z<s = s≤s z≤n

s<s : ∀ {m n} (m<n : m < n) → suc m < suc n
s<s = s≤s

Such smart constructors could usefully be put in Data.Nat.Properties.Core?
EDITED 2022-02-07 No, these can now better be put in Data.Nat.Base, as per 2 and @MatthewDaggitt 's comments below.

2. After @MatthewDaggitt 's pushing of NonZero instances everywhere, these now appear in Data.Nat.Base, even though they are entirely self-contained... EDITED and yet their properties, esp. wrt the ordering relations, do rely on the particular choices made... which seems like an abstraction failure, albeit within the same module, but for the cost of not yet being able to establish the more abstract properties of the orderings first?
3. There is also Data.Nat.Properties.Core, now containing only a single definition, which once upon a time was needed to resolve a dependency issue (I haven't chased the history of this module (**)); this definition can be eliminated entirely, changing lemmas in 3 places to in-line the pattern match... EDITED and elsewhere (*), but these can be (reasonably) sensibly accommodated.

So there are (at least) two possible directions to take this towards one (or more) PRs:

• minimalist: eliminate Data.Nat.Properties.Core entirely (modulo a deprecation warning... and moving the single definition back into Data.Nat.Properties?); (*),(**)
• maximalist: enrich Data.Nat.Properties.Core to incorporate the smart constructors for _<_ etc. and the NonZero instance, and its properties (I'm not clear whether the philosophy regarding NonZero instances is to declare them in *.Base, but build up their properties elsewhere, or lump them all together; in any case, the proofs of these properties, too, could benefit from the smart constructors...?), and then make that a public import in either Data.Nat.Base or Data.Nat.Properties
• a middle way, but in some ways more drastic: break up Data.Nat.Properties into those of the ordering relations, and then those of the operations, and then those concerning their interactions... (and regarding the NonZero work as somehow a 'preview' of such factorisation... either inlined, or as Core properties)

Matthew's concerns about dependency on the existing 'fat' module which prompted this PR suggests that, sooner or later, it is this size issue which needs dealing with, rather than isolating the actual dependencies on which Induction, Induction.WF might depend. Of course, some isolation of properties of the ordering relations, separated out from Data.Nat.Properties, seems the way to go... But I'm interested in what the/a 'best' way forward is/might be?

EDITED (*) there would be knock-on viscosity to this proposal, concerning Data.Fin.Base and Data.Fin.Properties, but both of these modules import Data.Nat with the constructors of _≤_, so the replacement pattern-matches would be admissible; but also in Data.Vec.Properties, but that's also eliminable, for the same reasons... In general, we seem to have the problem that we either export a (bad?) definition with its defining patterns from a module, and take the knock-on hit downstream in client modules, or try to encapsulate the exported pattern matches as destructors in the desire for a more abstract module boundary... and I don't (yet) see how the library designers really expected such a choice to cash out, or to have formalised the choice in the style guide? @MatthewDaggitt is there now a YouTube feed for the WITS workshop, or else your slides available, to see what you might have said about such issues there?
(**) oh, ... I have now looked at issues #1487, #1225 , #1033, #619, #153, #60, oh man!
There is now an extended version of the pr1698 branch, imaginatively called pr1698-extended which pursues some of the rabbit holes opened by the above.

[jamesmckinna]

@MatthewDaggitt if I take your hint from earlier... is it the case that certain functions in Data.Fin.Base are supposed to have erasable _≤_, (or _<_) arguments, and for that the single destructor form ≤-pred from Data.Nat.Properties.Core was needed? If so, we can ignore the minimalist approach, which then gives me ammunition to argue for the more maximalist approach which builds into that sub-module enough of the theory of order to solve your Induction.WF problem... or not?

[MatthewDaggitt]

Hmm so we have the original issue discussing why Data.Fin.Base depends on Data.Nat.Properties.Core here: #675

And the original PR that implemented it, along the discussion of irrelevance here: 1690f69#r34691463

In my memory there were much stronger reasons for implementing it, but it looks like I've been getting confused with cast in more ways than one. Looking back at it now with the benefit of hindsight, I'm really not convinced that @xekoukou's stated reason that the pattern matching on the < proof prevents reduction is very convincing. One produces far more robust code by preventing reduction and relying on actual explicit proofs to do the work. And that's all without even mentioning the benefit of eliminating the nasty dependency cycle.

So in answer I think we should open a PR with your minimalist approach to change the definitions of inject<= and fromN< back to pattern matching explicitly.

As I've mentioned the middle-way would result in an (unacceptable?) hit to searchability of the library, and I'm still hoping that with a smart design, we can avoid the maximalist approach as it feels... unprincipled somehow, as I'm unsure how it would generalise, e.g. what would go in Data.List.Properties.Core.

I don't (yet) see how the library designers really expected such a choice to cash out, or to have formalised the choice in the style guide?

To be honest I'm not aware of anyone has ever really thought about it in those terms before, so no it's not formalised anywhere.

@MatthewDaggitt is there now a YouTube feed for the WITS workshop, or else your slides available, to see what you might have said about such issues there?

Unfortunately I can't find any link to my talk. It certainly didn't go into this amount of depth however...

[xekoukou]

I am not currently using the agda-stdlib, so it is up to you.

In general though, I believe that I have spent too much effort to make agda happy, by understanding its quirks. Instead we should spend time on the mathematical problem at hand.

For example, take + of naturals, from @jespercockx 's taming of the rew .
It is unnatural that the way we split the arguments determines which equality is definitional or propositional.

I have spent so much time optimizing this. So maybe the solution is extensive use of rewrite rules everywhere.

edit : The other solution being cubical type theory.

[jamesmckinna]

Thanks @xekoukou for the comment, and with sympathy over the trials and tribulations (and development costs) of library development vs. application of such a library to "mathematical problem"s.

My current version doesn't fundamentally change what was already there; rather, it simplifies one anomalous dependency in favour of a (more) deliberate use of the choices of constructors/admissible pattern-matches already present. The cost seems to be that some definitions/proofs (in Data.Fin.Base, Data.Fin.Properties) now ostensibly use 'relevant' arguments of the ordering relation, but my understanding (limited as it is) of the evolution of the Irrelevant analysis is that the present proofs of the irrelevance of those relations would also devolve to the erasability of such arguments (If this analysis is incorrect, it might be good to have that explained somewhere).

The new versions, such as they are, also pave the way (I hope) to support removing (some of) the dependency of properties of Nat on the slightly mismatched choices of definitions of the orderings, which I find as unnatural as you do (and with good reason!) the choices regarding _+_ indicated above. Supporting additional rewrites to mitigate biases in representation is one potential part of the solution; supporting more flexible programmer-definable eliminations/pattern matches ('views') on such representations is the/an other side of that story, as Conor and I first advanced a long time ago.

[gallais]

I'm unsure how it would generalise, e.g. what would go in Data.List.Properties.Core.

To compare equals for equals we would need to move the comparison relations
to Data.Nat.Relation.Binary.Comparison just like we have Data.List.Relation.Binary.Prefix.

The numeric types are a bit special in that we include way more in Base than for other types.

[JacquesCarette]

My feeling is that the module sub-hierarchy has gone a little crazy. Data.Nat.Relation makes sense to me (instead of Data.Nat.Properties.Core). Splitting it up by arity and then 'kind' (aka Comparison - I'd love a better descriptor than 'kind' here) seems over-zealous? It does please my minimalist heart, but for this particular library, seems a bit much.

Minimalist me would certainly be happy with a meta-rule along the lines: non-fat modules can't have more than 20 definitions in them (type, data types, properties, what have you; basically 20 exported names). Fat modules should then go crazy in the opposite direction.

But as to @xekoukou tribulations: in theory, we know what to do. Define Nat whichever way you want, prove the basic properties that make it a rig / ordered rig / lattice / etc, then prove everything else on top of that. Don't allow "proofs by induction" on Nat for properties that are provable from that core. That 'core' becomes the interface to Nat. In theory, we could then change Nat's definition without altering anything else. In practice, I seriously doubt we're ready for that. I do think it is something worth aiming for.

[jamesmckinna]

Re @JacquesCarette 's last comment (with which I broadly agree, modulo... history, stdlib as it now is): why is there no distinction made in the library between zero and suc as constructors, and their values as ordinary terms? I could imagine better encapsulation of quite a lot reasoning with Nat if, instead of cong suc, one used cong 1+_ for example.

[jamesmckinna]

Just doing a last make test then should be able to open a PR from pr1698-extended. But you could always look at the comparisons first... my 'solution' is to expand the range of 'constructors' of the various relations with pattern synonyms, and then aggressively deploy those, under nevertheless quite controlled conditions. Isolating eg the equivalence of _<_ and _<′_ in some submodule of Data.Nat.* or other would then yield @MatthewDaggitt 's holy grail of Data.Nat.Induction without appealing to Data.Nat.Properties. But I'm open to (further) discussion.

[MatthewDaggitt]

Merging this in as it still zaps a few unused dependencies.