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?

Sadly Andrei Popescu is not on Zulip (https://andreipopescu.uk/), he knows this kind of things.

I cannot answer your question, but dependent types don't have anything to do with Isar ;-)

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)

@Josh Chen worked on dependent types, https://github.com/jaycech3n/Isabelle-HoTT and see the #new projects stream

Paper https://arxiv.org/abs/2002.09282

Small warning: that arXiv paper has a couple of mistakes, is a bit outdated and will be updated soon.

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: Dec 07 2023 at 08:19 UTC