search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

Simpler speed-up and cosmetics #41

Closed Columbus240 closed 2 years ago

Columbus240 commented 2 years ago

I found some simpler ways to speed-up Structure/Monoidal/Internal/Product.v and some other files, which I'd like to share. The resulting proofs are still quite long, but compilation is a lot quicker. The proofs could probably be generated by sufficiently clever Ltac...

I also recovered some comments and minor clean-up work from the previous branch. Besides the comments, I included a "forward" in the Makefile which would make it easier for me to build (and time) single files. And the definition of equivalence for natural transformations is wrongly generated. Coq used strict equality instead of pointwise equivalence. It doesn't really matter, because it is never used.

Last, I recovered the generalized definition of Unique so it works for arbitrary Setoid and not just for hom-sets. This makes it possible to write "an object exists, uniquely up to isomorphism" etc.

Because some changes are quite small, I bundled them together in a single PR. (Edit: please veto on any part which you don't want.) I'll keep back most of the new definitions I added last time until they are necessary for some greater theorem, whatever that may be. Until then they can collect dust in my repo.

jwiegley commented 2 years ago

Thanks! I'll go through it soon.

Columbus240 commented 2 years ago

Thanks for merging. It is useful to me, if the library builds quickly and makes it easier to try small changes.

Could you please use the tools of GitHub to request changes to my branch if you like to do some before merging? Or merge the branch and do the changes afterwards? Currently I can't simply do git rebase Cosmetics jwiegley/master because small differences in formatting and wording you made create conflicts. For example between my commit 41ee28 and your dafe57b4. Fixing these conflicts (especially for all my branches that build upon the Cosmetics branch) takes quite a bit of work.

jwiegley commented 2 years ago

@Columbus240 Btw, my e-mail is jwiegley@gmail.com, if we don't want all conversations to be through GitHub. :)

Your request that I suggest changes to your PR via GitHub is a difficult one. The last PR in question was a very large PR with several unrelated changes in it. Had they been smaller, I could have tried to simply modify them, but in these cases my workflow generally is:

Your Cosmetic PR ended up becoming something on the order of 5-6 PRs by the time I was done. And I wasn't certain at the beginning that I would want all of them, so the idea of submitting change requests to a large PR where I may only intend to accept part of it -- this is too much overhead for the time I have available to work on these things.

Also, I'm not sure you want to work against multiple branches at once, since you are moving an aggregate state forward on your side as well. The old TopGit tool used to be tuned for just this scenario: work on multiple branches in parallel, but do your testing on a synthesis. But even those tools were too cumbersome to be truly practical.

So the best I can suggest is that the smaller and more focused the PR is, the more likely I can merge first and then change after, or submit changes against it myself on your side. Anything larger than that, and I'll have to just work with the code independently, rather than the commits.

Thanks for all your efforts, and I'm very interested to see how some of your development branches come along. I had also started working on indexed constructions a couple of years ago, but later abandoned it.