Deprecating `Num`

Stream: mathlib4

[Jeremy Tan]

In Data.Num.* we define natural number types Num, ZNum, etc. through binary representation rather than our preferred standard Peano axioms. A note in Data.Num.Basic reads

Note: Unlike in Coq, where this representation is preferred because of
the reliance on kernel reduction, in Lean this representation is discouraged
in favor of the "Peano" natural numbers `Nat`, and the purpose of this
collection of theorems is to show the equivalence of the different approaches.

A check shows that the Data.Num.* files are also not used anywhere else in mathlib. Given these, can we just deprecate everything in Data.Num.* by moving them to Deprecated?

[Michael Rothgang]

I do think mathlib should have a notion of representing natural/rational/real numbers in positional system. See e.g. #PR reviews > representation of reals in [0, 1] in positional system

[Michael Rothgang]

Are you advocating for merely moving Data.Num, or also for removing them in the medium term?

[Jeremy Tan]

I want to eventually remove everything in Data.Num; besides the note on preferred representation in Lean, the files are ancient

[Jeremy Tan]

For Nat at least, we already have Nat.digits

[Niels Voss]

One extremely minor note is that if I remember correctly, external type checkers are not required to implement custom reduction for Nat, and can do it the Peano Arithmetic way if they so please. So, using Num could in theory speed up proofs for external checkers. (I don't consider this to be important, but I thought it might be worth mentioning.)

[Kyle Miller]

It's worth pinging @Mario Carneiro about deprecation, he's the primary author of Data.Num

[Mario Carneiro]

Num is already "deprecated" in the sense that you should use Nat instead if you don't have a good reason. But I don't see a reason to put it on the deletion pipeline

[Ruben Van de Velde]

What would be the benefit of removing it?

[Jeremy Tan]

For me Num and relatives are like the CGT material that was downstreamed – unlikely to be used anywhere else in mathlib, or even in a downstream project – but unlike CGT it isn't even interesting in its own right

[Jeremy Tan]

I got the idea while depriming induction'. Some of the uses of induction' in the Num files are very involved

[Jeremy Tan]

At best Num and relatives should be relegated to Archive because they are alternative representations of core types that – as practice has shown – makes proving theorems about them much harder

[Jeremy Tan]

As for the benefit of deleting Num? It would be the best way of communicating our design choice around Nat and Int