Jakub Kądziołka (Feb 08 2021 at 01:54): Jakub Kądziołka (Feb 08 2021 at 01:54):I'm thinking about what a marriage of Isar and dependant types could look like. If I understand correctly Coq/Lean tend to handle partial functions like division, nat subtraction or cardinality of a potentially infinite set like we do - with default values and careful thinking - even though they have the alternative of having the functions take a proof of the arguments' correctness.
The latter approach has the downside of essentially having to prove that your terms are valid before considering a proposition, which isn't ideal. However, I feel like it could help with some automation sore spots that I often observe in Isabelle.
I would like to ask you about any previous work in this area - are there any systems that take full advantage of dependent types? Do they have any interesting syntax or mechanisms for handling the proof arguments of functions?
Mathias Fleury (Feb 08 2021 at 05:53):Sadly Andrei Popescu is not on Zulip (https://andreipopescu.uk/), he knows this kind of things.
Mathias Fleury (Feb 08 2021 at 05:54):I cannot answer your question, but dependent types don't have anything to do with Isar ;-)
Mathias Fleury (Feb 08 2021 at 06:35):From my understanding Coq and Lean considered having division by 0 undefined, but it is annoying and you don't get or loose anything compared to defining it as 0. (For Coq, IIRC from some talks, it depends on the math library you use)
maximilian p.l. haslbeck (Feb 08 2021 at 08:28):@Josh Chen worked on dependent types, https://github.com/jaycech3n/Isabelle-HoTT and see the #new projects stream
Lukas Stevens (Feb 08 2021 at 10:13):Paper https://arxiv.org/abs/2002.09282
Josh Chen (Feb 08 2021 at 12:34):Small warning: that arXiv paper has a couple of mistakes, is a bit outdated and will be updated soon.
Manuel Eberl (Feb 08 2021 at 13:14):Mathias Fleury said:
From my understanding Coq and Lean considered having division by 0 undefined, but it is annoying and you don't get or loose anything compared to defining it as 0. (For Coq, IIRC from some talks, it depends on the math library you use)
If you define division by zero as 0, you do gain the usual discussion on the mailing list where e.g. some external person comes along and claims that this is unsound/evil/etc. :grinning_face_with_smiling_eyes:
Last updated: Apr 19 2024 at 16:20 UTC