Unsatisfying conventions?

Stream: new members

[Linus Tang]

According to Mathematics in Lean, the inverse function is defined to be an arbitrary element when an inverse doesn't exist, and the pointwise derivative of a function not differentiable at said point is defined to be 0. Are these conventions as unsatisfying as they seem? Or is there a reason why they're actually alright? Is there a good reason not to instead say e.g. that the derivative of an $\mathbb R\to\mathbb R$ function is a function $\mathbb R\to\mathbb R\cup\{\text{undefined}\}$?

[Michael Rothgang]

Well, working with such a definition would be rather unsatisfying in practice :-)

[Jireh Loreaux]

Yes, there's a good reason. If you make that definition, all of a sudden you can't take the derivative of the derivative, because it has the wrong type. It's similar to why we define x/0 := 0. It's more convenient this way. You shift the burden away from writing the expression to using/proving things about it.

[Michael Rothgang]

https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ has some of this spelled out in more detail.

[Michael Rothgang]

I think of the mathlib notion for limit more as a limit' --- which takes the value you expect when it exists, and a "junk value" otherwise. Because the junk value has the same type, that makes working with it much more pleasant. For almost any reasonable theorem, your limit' is in fact on the well-defined domain, and you get the result you expect.

[Michael Rothgang]

There is some thought to choosing junk values well: if done correctly, some theorems about (e.g.) limit' become true without e.g. convergence assumptions --- because they are true in paper mathematics, and also true in the degenerate case. In practice, that means you have one fewer assumption to check... and such well-definedness assumptions would otherwise crop up over and over and over and over, not just once.

[Jireh Loreaux]

To be clear, what I mean is this: if you define def deriv (f : ℝ → ℝ) : (ℝ → Option ℝ), then you will want another definition def actualDeriv (f : ℝ → ℝ) (hf : Differentiable f) : ℝ → ℝ which extracts the value out of the Option so that you can still access the underlying function when f is differentiable (so that, for example, you can take the derivative twice). But then this amounts to passing around proofs in the same way Kevin's post describes passing around proofs of nonzeroness.

[Linus Tang]

You shift the burden away from writing the expression to using/proving things about it.

This is very helpful, thank you!

[Michael Rothgang]

As an example: I formalise a lot of differential geometry, which means working with charts of a manifold. These map a subset of your space to a subset of Euclidean space (we don't need to be more precise here). In practice, proving lemmas in DG means you're spending time proving over and over "this point lies in my subset where things are well-defined". On paper, you don't do that (or much much less)... it changes the feeling of formalisaing in that area quite a bit.
Doing that more would be really painful.