Computable version of ^-1 for ℝ

Stream: mathlib4

[Linuxmetel]

I found that Mathlib doesn't seem to have a computable version of ^-1 for ℝ, so I wrote one myself. If I make it into a pull request, would such a trivial (and probably unnecessary) contribution be welcomed?
(It's my first post here, so if I've sent it to the wrong place, please let me know)

[Linuxmetel]

I don't know how much the people involved in Mathlib development care about computability.

[Kenny Lau]

@Linuxmetel first of all, welcome to lean, and well done on writing the code, so please don't let the following deter you:

1. as you've observed you have a partial function here because you need the input to be nonzero, while in Mathlib we've adopted the convention that the inverse function in a field should be total and send 0 to 0, this is to prevent the statements from blowing up in complexity because you would have to write a proof every time you want to say the inverse
2. and as you might know it's impossible to extend it to a total function computably because all computable functions are continuous
3. and as you've observed, mathlib doesn't particularly care about computability, and this isn't a trivial replacement (because of it being a partial function)

[Kenny Lau]

(i'm not affiliated to mathlib officially, but i'm reasonably confident that that would be the opinion of mathlib)

[Linuxmetel]

@Kenny Lau Thank you for your reply. So when I use Lean, don't I need to hesitate to mark definitions as uncomputable?

The case I came across is some function I was writing that uses the value of x / ‖x‖ for x ≠ 0 in some normed space. The Lean processor said it should be marked uncomputable, but I believed it is computable. But I couldn't find such a version of inversion in Mathlib, so I was wondering why that is.

[Kenny Lau]

that's because we like total functions over removing the noncomputability tag

[Kenny Lau]

to make / total it has to be noncomputable

[Kevin Buzzard]

I don't think they observed "mathlib doesn't particularly care about computability", I think they're asking how much the mathlib devs care about computability, but the answer is that this is not a high priority issue in mathlib and your PR is unlikely to be merged.

[Linuxmetel]

Thank you for your replies. I know total functions are better when you do normal analysis or algebra, but I might care about it too much when I write some codes that I intend to use in multiple places.

[Kenny Lau]

@Linuxmetel computability matters if you want to #reduce or #eval it, which I argue is the wrong thing to do (the correct thing to do is to set up simp lemmas and tactics such as norm_num)

[Kenny Lau]

import Mathlib

example : ((3 + 3 / 7) * 6 : ℝ) = sorry := by
  norm_num

[Kenny Lau]

for example, the tactic norm_num can compute 144/7 here without ever needing computability

[Aaron Liu]

I think a computable implementation for partial division on reals is already in mathlib

[Aaron Liu]

the just put a noncomputable check for zero in front of it and mark the whole thing noncomputable

[Linuxmetel]

computability matters if you want to #reduce or #eval it,

I think computability matters because it guarantees constructivity, rather than because you actually want to evaluate it. But I know some people care about it while others don't.

[Linuxmetel]

Aaron Liu said:

I think a computable implementation for partial division on reals is already in mathlib

I couldn't find one. Mathlib includes that for CauSeq (CauSeq.inv), but it seems not for CauSeq.Completion.Cauchy and Real.

[Aaron Liu]

If you look at src#CauSeq.Completion.instInvCauchy it's computable except for the part where it tests zero

[Linuxmetel]

You may be able to "extract" computable part from it, but I think it is a little troublesome in that such a function need to receive the proof of x ≠ 0 after lift along the equivalence relation. Still I wrote my version from scratch using CauSeq.inv rather than extract from it.

[Kenny Lau]

@Linuxmetel could you share a little bit more context? what did you "intend to use" with this computable partial inverse?

[Linuxmetel]

@Kenny Lau I wanted to construct the natural homeomorphism

$$S^n \times \mathbf{R}_{> 0} \to \mathbf{R}^{n+1} \setminus \{0\},$$

and I just hesitated to mark such a simple mapping as uncomputable. However, it is something I don't need to worry about in Lean, I am ok to mark it.

[Kenny Lau]

the forward direction you sent should be computable

[Kenny Lau]

Linuxmetel said:

I think computability matters because it guarantees constructivity

also, computable functions can (and do) still use Classical.choice

[Ruben Van de Velde]

Is there not also #norm_num?

[Linuxmetel]

Homeomorph requires to construct InvFun, so ...

[Patrick Massot]

If you care about constructivity then you should forget Mathlib completely and you'll live a happier life.

[Violeta Hernández]

It should be possible to computably define the inverse with domain {x : ℝ // x ≠ 0}. I'm somewhat skeptical that this would be accepted into Mathlib, however.

[Violeta Hernández]

Oh, this is what you did! I thought that people were saying that you made a partial def.

[Yury G. Kudryashov]

See also docs#divp

[Eric Wieser]

I think it would be totally reasonable to accept a PR to mathlib that split out the computable part of https://github.com/leanprover-community/mathlib4/blob/aa1b475dc183aa4e2f541bea5bff747c5963fec2/Mathlib/Algebra/Order/CauSeq/Completion.lean#L194-L206 into Cauchy.inv0 or similar if that's useful to you, especially as the this wouldn't really affect the complexity of the code.

[Eric Wieser]

But certainly mathlib (rightly) doesn't care enough about computability of Reals (which is mostly useless in it's current form anyway) to change how division works elsewhere

[Eric Wieser]

(such an def inv0 would be a nice place to park a docstring explaining why we don't attempt to propagate the computability to Real)

[Alex Meiburg]

Yeah, invertibility of reals /as cauchy sequences/ is "useless" in a mathematically precise way: the only computable predicates of reals are the constants True and False, sort of a Rice's theorem for numerics. So there is, in a strict sense, nothing gained by making an operation computable or not. (Nothing besides not writing "noncomputable", or maybe scratching a philosophical itch.)

If reals are built from sequences of intervals / Dedekind cuts (as Rat -> Bool) / Cauchy sequences with some guarantee on convergence rate, then some things are computable, so then this could have a material benefit.