We need algorithms to prove these things. The example I usually use is being a noetherian local ring. If A and B are isomorphic rings and A is Noetherian local then so is B but currently this has to be proved manually. Morrison is working on a tactic. It's harder than it looks
Conversation
Why do you need a tactic? I'd assume that you'd need to state and prove the theorem only once.
1
yes but there are 1000 theorems like this
1
If your notion of iso fits into the TT transport then you can just use it, right?
1
I so don't understand Twitter conversations, sorry for the short delat. The whole issue of transport is a very broad one; we don't yet have a tactic broad enough to push an arbitrary interesting mathematical thing along an isomorphism. Mathematicians do this all the time :-)
1
1
Thanks for the reply! So far indeed it is a bit of manual process and requires quite a bit of discipline so things fit, but IMO it is not as bad as it looks.
Things like effective iso transport are IMO tooling issues so indeed mathematics will depend on CS to provide solutions.
1
This always surprises me as a plus for Lean since transport is so much more natural in HoTT, and UIP is incompatible with univalence. UIP gets you some help but it is still ad-hoc compared to, say, cubical. But Leo is amazing at tools for this kind of thing.
1
OTOH Leo had to hack around the lack of univalence to define congruence, and and his student recently showed that congruence is way more natural in cubical. From this you get e-graphs, from e-graphs you get type-directed search for transport.
1
1
The problem is the overlap of people who understand both cubical and e-graphs is like, one or two people. I've been trying to get Anders on board with this.
In vanilla Coq though you have my work, and you have univalent parametricity, and so on. Just all are external tools.
1
2
I've noticed that it is extremely hard to get people to use external tools. I have a few users but that's it. I tried to use UP and I struggled a lot. I think we need more of this in the standard library.
2
1
Replying to
I guess I hope that at some point Coq can see better forwards compatibility, and more reproducible, easy to use package management tooling.🤞This is one of the big things that keeps me out of investing time in working with Agda, Coq, OCaml, and Haskell. 😔
I do realise this stuff is really hard though, and the funding for this kind of tooling stuff is scarce, and each community is doing the best they can. Just hoping it gets better. Brittle tools are scary!
1
Hoping that stuff like what you are working on could help with upgrading dependencies? Like, even in languages where semver is pervasive, versioning is *hard*! Would be cool if libraries could help you 'upgrade' your existing code at a more fine grained level! 🤩
2
2
Show replies