On 28/07/2020 11:20, Chun Tian (binghe) wrote: > I would say, this is still not inline with "real" mathematics, but the > situation is slightly better than (rudely) assuming any fixed value for > `PosInf + NegInf` a priori.
Well, if you want to do it the "proper" way, you need a logic with an explicit notion of undefinedness. Or some form of dependent types, perhaps. But I think even in Coq and Lean they often go for the "let's pick a convenient dummy result" approach as opposed to the "let's restrict the function's input to a subtype" approach when it comes to questions like "what is the integral of a non-integrable function". (I don't have any hard data for that, just from anecdotes I recall from talking to people, but I'm sure someone will contradict me if the above is wrong.) In Isabelle/HOL, the current consensus seems to be that convenient dummy values are the best way to go. We've yet to encounter a situation where they are a problem (and I for one do not think there is one) and they make life much easier. For instance, if you define something like "ln x = (THE y. x = exp y)", the ln of all non-positive numbers is completely unspecified. If you add a "if x ≤ 0 then undefined else …", it's still unspecified, but you at least know that "ln x1 = ln x2" for any non-positive numbers x1, x2. That might sound silly to you, but the nice thing is that this allows you to prove that ln is measurable on the reals, whereas the other thing does not. Of course, you could do all the maths you can do with that definition also with the previous one, but things just become a lot messier because you then have to talk about measurability on a subspace and some of the automation will probably not work anymore etc. So why not make your life a bit easier? All in all, I think this fixation on defining things the "proper" way is unnecessary. But don't get me wrong, I totally understand where it is coming from, and I do think it is a legitimate view. Manuel _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
