agda
'No infinite descent' for (`Acc`essible elements of) `WellFounded` relations
I've added this, because it didn't obviously seem part of the existing library.
Currently in the form of a stand-alone module, but could/should be merged into Induction.WellFounded?
Includes an additional lemma for TransClosure which I first thought I needed (and then realised I could do without), but which is also itself a useful, but 'missing', lemma.
Refactoring opportunities, in addition to the above: rewrite in terms of Relation.Unary.Closure.Base, but if so, then arguably perhaps all of Induction.WellFounded should be, as well.
OK, so something seemed to have gone horribly wrong with the merge conflict resolution there (I saw, briefly 148 files changed but now there are only 4... but with a slightly weird extra commit/duplicate entry into CHANGELOG which I don't quite understand how it got there. Oh well. We'll fix it up when the time comes... and apologies for my earlier panic.
~~For info: I attempted to pull the remote branch into a fresh branch off my local copy of master (with git pull --rebase), resolve the merge conflicts there, and then push back. But that still left merge conflicts for CHANGELOG, which when I fixed on GitHub this time, suddenly replayed all the preceding commits on master. No idea how to reverse out of this, no idea how/why this happens to me, no idea what to do now. And this with a PR which was ... 'ready', and hadn't been changed for a while.~~
~~I could imagine some combination of resets and cherry-picking might save it, but I'm... peeved, to put it mildly. The content of the PR hasn't changed... only the CHANGELOG. Grrrrr. :-(~~
In addition to the evident CHANGELOG merge conflict, I realise that I never resolved the question about making a separate module, or rolling it into Induction.WellFounded...
... decided to leave it as a separate module. Fixed up the merge conflict with CHANGELOG... so good to go now!
It would be nice to merge this before it gets clobbered by another CHANGELOG merge conflict...
Left some preliminary comments, but my overall one is that the nested module structure of this module has lead to at least one major bug, and as some of my comments mention, makes it hard to check for others.
What are your thoughts about adding to the style guide that unless in exceptional circumstances, more than two levels of nested modules should be banned?
Two thoughts:
- yes, as with previous PRs, I am perhaps too enthusiastic (to the point of being careless) in my use of (nested) modules;
- I can see, again from this and previous experience, that at least as a reviewer (where it makes sense in terms of cognitive load; but correspondingly, as a developer, I find them useful, not least in trying to impose uniformity on dependencies, which otherwise might become ad hoc on a per lemma/definition basis; but you've already observed that I make mistakes with that :-()), but perhaps generally cf #2182 , you do have strong views about the use of internal modules in the library!
It seems as though, regarding your proposal about the style guide, that our recent experiences with v2.0 are each inclining us to want to mandate more stringent guidelines along various axes, according to experience, taste and perhaps pet peeves. So I'd be worried about being too authoritarian...
... that said, I do think it's a good discussion issue, either for the stdlib-admin group in Zulip, or for the issue tracker, so that others can join in?
When I find myself wanting to use "too many" levels of nested modules, I try to use that as a signal to sit back and think some more. It's a signal that maybe the current organization can be improved, or at least that it should be reconsidered.
Okay, I'll wait to see what you come up with refactoring-wise to resolve the problem of the extra dependencies, and then maybe we could make this PR a topic of the next meeting, and get everyone's opinion on use of modules?
Regarding the (global) review comment about module nesting, now the maximum nesting depth is 2...
... UPDATED but I'll go through and try a version that is 'flattened out', for comparison. I'll convert back toDRAFT for now.
Sorry I haven't returned to this for a while. I thought I might have time/brain-space to remove the nested module structure and rethink my approach generally, but then... that never happened. Thanks @MatthewDaggitt for the merge conflict resolution!
I've had a hack at it to reduce the depth of nested modules to only 1 deep. As a result the file is now about ~25 lines shorter... @jamesmckinna what do you think?
Suggested cosmetic renamings:
-
nforzfor quantifications over Nat in infinite sequences; -
satisfiable/unsatisfiableforholds/notHold(so the identifier correlates with the named definition inRelation.*) - rectify the lemma names to follow #2168 / #2206
Commit incoming...