natural numbers

Stream: new members

[Massimiliano Gubinelli]

Hi, I'm new to Lean/mathlib and trying to undestand the conceptual framework. Every time I've seen defined natural numbers they are an inductive type. I still haven't tried but seems to me possible to define them as a typeclass (e.g. is_nat (a: Type)) parametrised over a generic type. Peano axioms then become proofs that this particular type satisfy the properties of natural numbers (i.e. one has a specific embedding). This would allow to treat \ZZ as an instance of \NN. Actually also \ZZ and all the other mathematical structures could be type classes. Is there any obvious problem with this approach (before I try it out...) ?

[Scott Morrison]

What is the payoff?

This would allow to treat \ZZ as an instance of \NN.

sounds like a bad thing rather than a good thing. :-)

[Eric Wieser]

How does your proposed typeclass for $\mathbb{N}$ differ from docs#add_comm_monoid?

[Johan Commelin]

@Massimiliano Gubinelli We already get a canonical coercion from nat to every type that has instances of has_zero, has_one, and has_add.

[Massimiliano Gubinelli]

Eric Wieser said:

How does your proposed typeclass for $\mathbb{N}$ differ from docs#add_comm_monoid?

it is a comm_monoid + more properties, like that S n \neq n. Also before I made a mistake I was meaning that I wanted to have a class is_nat and then a class is_int and every instance of is_nat can also be made an instance of is_int (for example). Of course the inductive type will be an instance of the is_nat class, but one can prove theorems just on the class without needing the explicit representation.

@Johan Commelin I guess I want a typeclass is_nat for which every instance can be coerced into nat (not only the other way around). This would express the idea that anything with the right properties can be a model for nat.

[Kevin Buzzard]

You're proposing a structure such that an instance of that structure is uniquely isomorphic to the naturals. You could then in theory take every theorem proved about the naturals and then reprove it for your structure. Sure this is possible. And it's also kind of beautiful. But it's not clear whether it actually helps us to do things like e.g. develop MSc level commutative algebra in Lean, which is one direction where I personally would like the maths library to go next.

[Johan Commelin]

Massimiliano Gubinelli said:

I guess I want a typeclass is_nat for which every instance can be coerced into nat (not only the other way around). This would express the idea that anything with the right properties can be a model for nat.

So then $\Z$ would not be an instance.

[Scott Morrison]

Note that is_nat is not a very good name for this, because it is very much _structure_, not _property_, that the typeclass is carrying around.

[Kevin Buzzard]

We do have this framework already for various other types, e.g. as well as the rationals we have a predicate saying "this ring is a field of fractions of the integers" so variants of (my understanding of) your proposal already exist. But I don't understand why you keep saying that the naturals are the integers, or the integers are the naturals.

[Scott Morrison]

any countable type "is the naturals" in the sense that you can define a zero and a successor function...

[Scott Morrison]

just by picking an arbitrary bijection with nat and transporting its structure across...

[Eric Wieser]

In a sense, looking for a typeclass that unifies the naturals with the integers is working in the wrong direction. A better thing to do is start with proofs of the "same thing" about ints and nats, and ask yourself "what typeclass would I need to write a single proof for both". Because if you go in that direction, you'll likely find:

• The typeclass you want already exists, or almost does
• You'll find other types your typeclass applies to

[Massimiliano Gubinelli]

@Kevin Buzzard @Johan Commelin , what i wanted to say is that something that is_nat can be made an instance of is_int . This would express the fact that the naturals can be faithfully embedded in the integers (maybe one can say this better).
@Scott Morrison indeed, one could use lists as a model (i.e. concrete instance) of is_nat or (as in lambda calculus) some particular class of functions. But you need a "good" (i.e. large enough) structure.
My point is that I do not see reasons to use a particular model as definition of integers (in OO programming one would consider them in interface). In this context I tend to think to natural numbers just some bunch of objects satisfying some axioms (like all the other math structures). I just wanted to understand if there are reasons to not treat any mathematical structure as a class.

[Kevin Buzzard]

Right now the philosophy of mathlib seems to be that even though things like the naturals and the reals can be characterised up to unique isomorphism by some structure and axioms, and so in theory every proof that we have about the real numbers could have been generalised to be a proof about any structure satisfying the axioms of the real numbers, it is not clear to me how this benefits us in practice. It sounds more like a theoretical type-theory exercise. However I do envisage that sometimes we will run into situations where we have proved theorems about X and want to apply these theorems to objects isomorphic to X. My plan for when these situations arise is to write tactics to transport the theorems along the isomorphism, rather than refactoring the theorems themselves so they're proved for all X-like objects. This proposal seems like a better idea than the one suggested for nats, because (a) it is more widely applicable (in particular I cannot envisage _any_ situation in actual mathematics where one comes up with something which is isomorphic to nat but where one needs a non-trivial theorem about nat to be pulled back to this structure, whereas I can envisage it for other objects), and (b) it even works in situations where objects are not classified up to unique isomorphism, but more generally where one has an isomorphism of structures X and Y and one wants to pull theorems about X back to Y. It is also worth adding that whilst a couple of years ago I was convinced that this sort of thing would show up all the time in mathematics, it has thus far been rather rare that we've had to make these kinds of pullback constructions.

[Kevin Buzzard]

Your comments about is_nat -> is_int make no sense to me. If is_int X means "I am isomorphic to the integers" and is_nat Y means "I am canonically isomorphic to the naturals" then there is no is_int Y or is_nat X.

[Massimiliano Gubinelli]

Eric Wieser said:

In a sense, looking for a typeclass that unifies the naturals with the integers is working in the wrong direction. A better thing to do is start with proofs of the "same thing" about ints and nats, and ask yourself "what typeclass would I need to write a single proof for both". Because if you go in that direction, you'll likely find:

• The typeclass you want already exists, or almost does
• You'll find other types your typeclass applies to

Well if I have a structure which behaves like natural numbers, then I want to say that is_nat, so that I can use the theorems I already proved for that. I have difficulty to see why one consider the notion of monoid a good class but the notion of natural number not a good class (both are defined just via a bunch of axioms, no?).

[Scott Morrison]

Because there are lots of interesting monoids, but only one interesting natural numbers?

[Eric Wieser]

If your proof doesn't use anything about multiplication, then why assume is_nat N when you only needed to assume add_comm_monoid N (for example).

[Scott Morrison]

(where of course we're making sure to do the Goldilocks level of identification of isomorphic structures :-)

[Kevin Buzzard]

The reason to have a particular definition of integers is that this is the way that mathematicians have proceeded classically, so what we have now does not look intimidating to working mathematicians. To a working mathematician your idea looks like a needless obfuscation with no clear practical benefits. We (working mathematicians) don't want to say "Take some type Z which is the integers", we want to see $\mathbb{Z}$. As part of the story it's not just a case of showing that any two instances of the class are isomorphic, it's also crucial that one proves that instances of the class exist. And then when one does do this, one has $\mathbb{Z}$, which mathematicians have been proving theorems about for centuries, without ever caring that their proofs also work for any object canonically isomorphic to $\mathbb{Z}$.

[Eric Wieser]

When definining "canonicity" - are there any properties of $\mathbb{Z}$ not captured by some existing typeclass?

[Kevin Buzzard]

I totally agree that from a theoretical CS point of view the class approach looks like an appealing idea. However it does not seem to bring any practical benefits to the modern working mathematician.

[Kevin Buzzard]

Eric Wieser said:

When definining "canonicity" - are there any properties of $\mathbb{Z}$ not captured by some existing typeclass?

Sure, the set of its prime ideals are a smooth 1-dimensional scheme.

[Eric Wieser]

I should be more wary of asking questions I won't understand the answer to... Is that statement formalized in lean yet?

[Kevin Buzzard]

no, that's why this is an answer to your question. In fact we haven't even defined smooth schemes yet.

[Kevin Buzzard]

It's a regular ring, a Cohen-Macauley ring, a complete intersection ring.

[Kevin Buzzard]

It's Japanese and universally catenary. https://stacks.math.columbia.edu/tag/032F https://stacks.math.columbia.edu/tag/00NL

[Eric Wieser]

Is it actually possible to fully state the properties of N in a typeclass such that nat.rec can be recovered without universe issues?

[Mario Carneiro]

Yes, but only because nat exists

[Mario Carneiro]

The proof that X with is_nat X satisfies the same recursor as nat is to show that X ~= nat and then pull back the property

[Mario Carneiro]

If you were working in some kind of weak MLTT theory without nat then it wouldn't be possible to prove that X eliminates to all universes

[Eric Wieser]

Here ~= is some monstrous "ring equiv and order iso and ..." equivalence that we don't have a strucutre for?

[Mario Carneiro]

No, I mean equiv

[Mario Carneiro]

well, I suppose you want an equiv that preserves 0 and S

[Eric Wieser]

I was going to say, I can construct an equiv between int and nat - but maybe that is still enough for the recursor

[Mario Carneiro]

By the way, regarding the puzzling claims about int being is_nat, I think Massimiliano is suggesting a typeclass which doesn't have a recursor clause, it's just a type, an element 0 and an injective endomorphism S such that 0 is not in the range of S

[Mario Carneiro]

I suppose we would call this typeclass infinite

[Mario Carneiro]

If we mean is_nat to include the recursor, then it is provable exactly when the type is denumerable, i.e. X ~= nat with a regular equiv

[Mario Carneiro]

in fact docs#denumerable is probably the closest existing definition to what @Massimiliano Gubinelli is looking for

[Mario Carneiro]

and incidentally we do have a proof that int is denumerable

[Massimiliano Gubinelli]

@Mario Carneiro is right, I was confused myself about this point. Indeed I was thinking to is_nat without implying isomorphism but only an injection. And I agree that if one require also isomorphism one falls into denumerable. If I understand the definition it uses the concrete type nat to enforce that a denumerable type is a type of natural numbers. What I had in mind was more a typeclass which packages the basic axioms (e.g. Peano's?). It uses a concrete type to enforce structural informations.
@Kevin Buzzard My question was coming from doing the Natural number game. I'm a "general" mathematician but indeed in mathematics one defines natural numbers as some set with some properties, not as an inductive type, so I was feeling that a typeclass would be "nearer" to the way I was taught the foundations. I understand the objection that makes the "implementation" a bit more awkward, because all will depend on a type variable which is never fixed. On the other hand this is a matter of syntax (one could probably hide the low-level implementation from the user, as it is already done with other aspects).
Anyway, thanks for all these answers. I think things are (a bit) clearer now. If I come up with a meaningful example where such idea could be useful I will let you know :)

[Mario Carneiro]

My point to Eric above is that it's not really possible to do everything without ever using a "canonical" version of the class; the existence of inductive types is needed to prove some theorems that pure axiomatic classes won't help with. Basically, you eventually have to show that your axiomatic class is not vacuous

[Massimiliano Gubinelli]

@Mario Carneiro yes I think understand this: the axioms could be contradictory so you need a model to show that they do not cause problems.

[Kevin Buzzard]

The naturals are defined as a set with some properties, but those properties are precisely the construtors of the inductive type. In set theory there is this artificial construction involving {{},{{}},...}={0,1,...} but again it is a concrete model rather than "a thing satisfying some axioms".

[Mario Carneiro]

How would you state derived definitions avoiding the concrete definition? For example, a first countable topology needs a prior definition of some nat-like type, unless you quantify (universally or existentially) over a nat-like type

[Kevin Buzzard]

We do have situations where we end up proving things about e.g. "natural numbers, but regarded as real numbers". That's a pretty good example of a thing which is isomorphic to the naturals but not literally equal to them. But we have tactics which pull back statements about natural real numbers to $\mathbb{N}$.

[Mario Carneiro]

and no matter what quantifier you use you will eventually have to prove forall implies exists or something along those lines and then you need to know that some nat-like type exists

[Massimiliano Gubinelli]

@Mario Carneiro I'm clueless :) I will try to write down some actual code to clarify my ideas. I'm just starting looking over these matters. (I know some Haskell but that's all)
@Kevin Buzzard as a general mathematician who likes programming I'm interested in formalization also because I have a vague hope that it could allow to "think" (research level) mathematics differently. Usually I find that a computer could be used in new ways to do math, not only as a "better" way to do old stuff (e.g. like when we go into a lot of trouble to use it as a support on which to write with a pen....). For example: non-standard analysis has never worked quite well in the "real world" of everyday math, but somehow was an attempt to put a different "API" on the concepts of analysis.

[Massimiliano Gubinelli]

Mario Carneiro said:

How would you state derived definitions avoiding the concrete definition? For example, a first countable topology needs a prior definition of some nat-like type, unless you quantify (universally or existentially) over a nat-like type

I think I had in mind to quantify universally. The proposal was really: every time you see nat you should really have is_nat a for an arbitrary type a. I have hard time to see at which point you need "a model" when you prove things. Of course if your axioms are contradictory your proofs means nothing, so instantiate the abstract theory on a concrete model is a way to reduce the axioms of the abstract theory to that of the model and carry the burden of coherence to that of the model (which being simpler is less risky).

[Bryan Gin-ge Chen]

The idea behind #3292 (@Alex J. Best and @Jalex Stark 's PR for "conditionally_complete_linear_ordered_field, aka the reals") is similar, right?

[Kevin Buzzard]

You can probably do everything with some is_nat class. But you have to ask at the end of the day whether a mathematician wants to see

∀ a b c n : ℕ, n > 2 ∧ a > 0 ∧ b > 0 → a^n + b^n ≠ c^n

or

∀ (N : Type) [is_nat N] (a b c n : N), n > 2 ∧ a > 0 ∧ b > 0 → a^n + b^n ≠ c^n

and I definitely prefer the former. So whilst the class version does have some kind of pleasing "more general" appeal to it, another point of view is that it is obfuscating for no practical gain.

[Massimiliano Gubinelli]

@Bryan Gin-ge Chen for what I understand seems so. They give a class which wraps the relevant axioms. I would be interested to know what prompted this PR.
@Kevin Buzzard I could guess with appropriate support from the parser, support this kind of style would not be more difficult that support notations like a * b. The real question indeed is whether it is useful or opens new way of working with mathematical structures, this I do not know. My reason for asking in the first place was to check my understating of how Lean works.
Thanks for the feedback!

[Massimiliano Gubinelli]

@Kevin Buzzard (btw, I'm going thru the material on youtube from last summer, it is very helpful to see how things work and how to set up e.g. topology in the elementary way, thanks for sharing it)

[Alex J. Best]

Massimiliano Gubinelli said:

Bryan Gin-ge Chen for what I understand seems so. They give a class which wraps the relevant axioms. I would be interested to know what prompted this PR.
Kevin Buzzard I could guess with appropriate support from the parser, support this kind of style would not be more difficult that support notations like a * b. The real question indeed is whether it is useful or opens new way of working with mathematical structures, this I do not know. My reason for asking in the first place was to check my understating of how Lean works.
Thanks for the feedback!

At least with the reals there are several very distinct construction (cauchy sequences, dedekind cuts, eudoxus reals) so aligning them seemed important. Also interesting is the fact that the definition of the isomorphism between such fields gives you unique embeddings of any linear ordered field (e.g. the rationals) into the reals, so you get some nice results as a side effect. One actual motivation for me was that @Mario Carneiro produced a lean proof of the prime number theorem that was automatically translated from a proof in metamath, the problem is that the definitions were also autogenerated from metamath and so do not align completely with the mathlib ones. So in order to start getting the real PNT (pun intended) you need either to relate the definitions manually, or some theorem like this that lets you just check some properties of metamath reals hold to get the isomorphism for free.

[Massimiliano Gubinelli]

I took nat as an example. Indeed the same arguments apply to all mathematical structures. Is more evident if the structure does not have a "preferred" representation. However if you come from lambda calculus then naturals are represented via lambda abstractions, not inductive types. I was thinking if I have an example where could be useful. The only thing which was coming to my mind was that one could have a function on nat which want to prove to be increasing, a strategy familiar to me (I'm an analyst/probabilist) is to extend it (arbitrarily) to the reals so that I can use calculus and prove that the derivative is positive. So in this case a model of nat based on the reals seems to help in the job.

It is interesting however to know that the same mechanism could help to bridge the gap between different systems.

[Kevin Buzzard]

Aah, this is a nice example! So here is what the proof would look like in Lean:

import data.real.basic

example (f : ℕ → ℝ) (g : ℝ → ℝ) (hfg : ∀ n : ℕ, f n = g n)
  (g_mono : ∀ a b : ℝ, a ≤ b → g a ≤ g b) : ∀ m n : ℕ, m ≤ n → f m ≤ f n :=
begin
  intros,
  rw [hfg, hfg],
  apply g_mono,
  assumption_mod_cast,
end

After apply g_mono we have two naturals m and n, a proof that m <= n, and our goal is to prove that (m : real) <= (n : real). The proof is one line long though, assumption_mod_cast, which is a tactic specifically written to move proofs between the naturals and the reals.

[Kevin Buzzard]

So you are saying "why not prove all theorems for any model of the naturals", and I am saying "in Lean we prove things for our one model, and in practice the only other models which show up are things like the copy of the naturals in the reals / rationals / complexes / integers / p-adic numbers, where we have a specific tactic for doing this".

[Kevin Buzzard]

And the observation is that in practice this approach has worked really really well.

[Kevin Buzzard]

However sometimes we do use your approach, for example when doing localisation of rings, and in this case we had to think hard about precisely how to classify such things by a list of axioms, because there are several equivalent characterisations. Strickland came up with a list which was really practical to use in practice, and this was the big change between versions 1 and 2 of schemes as described in this paper: https://arxiv.org/abs/2101.02602 . Here we have both the concrete model and the abstract class parametrised by Strickland's axioms, and some key intermediate theorems were proved for the abstract class because it turned out that there were examples of rings in the literature which mathematicians were treating as the same but which actually were set-theoretically not quite equal. I say more about this in this part of this talk here https://youtu.be/g2--VL2SkMo?t=2267 which I gave to an undergraduate maths society last month. So your phenomenon really does show up, and we are dealing with it in different ways depending on the circumstances.

[Mario Carneiro]

Massimiliano Gubinelli said:

Mario Carneiro said:

How would you state derived definitions avoiding the concrete definition? For example, a first countable topology needs a prior definition of some nat-like type, unless you quantify (universally or existentially) over a nat-like type

I think I had in mind to quantify universally. The proposal was really: every time you see nat you should really have is_nat a for an arbitrary type a. I have hard time to see at which point you need "a model" when you prove things. Of course if your axioms are contradictory your proofs means nothing, so instantiate the abstract theory on a concrete model is a way to reduce the axioms of the abstract theory to that of the model and carry the burden of coherence to that of the model (which being simpler is less risky).

If you quantify universally, then the problem comes when you want to discharge assumptions local to a proof. Let's say we want to prove A -> B where A and B make no mention of natural numbers (perhaps the idea that you would even need natural numbers isn't on the radar - for a less trivial example consider that the statement of Fermat's last theorem does not invoke the existence of modular forms in any way). However the proof goes via an intermediate statement P(nat) where nat is any reasonable definition of natural numbers. That is, we can prove A -> P(nat) and P(nat) -> B. If nat is some concrete structure then we can just chain these together and we get a proof of A -> B, but if we had been universally quantifying over is_nats, we would have proved ∀ X, is_nat X -> A -> P(X) and ∀ X, is_nat X -> P(X) -> B, and if you put those two together you get ∀ X, is_nat X -> A -> B, or (∃ X, is_nat X) -> A -> B if you prefer. In order to finish the proof and prove the original A -> B goal we need ∃ X, is_nat X.

[Massimiliano Gubinelli]

I see. Your observation clarifies to me at which point you need a proof that the axioms for is_nat are not incoherent in the Lean system, that's nice. Can the second statement be $\exists X, (is_nat X -> P(X) -> B)$ and still be able to conclude? I think so, no? (or even the first one existential and the second universal? or do we really need both to be universal?) That would leave the freedom to choose a particular model for certain computations.

[Mario Carneiro]

Yes, if one of the statements was universal and the other existential, then you could conclude as desired. But then you are somehow "coloring" the library with red and blue theorems and which should be which? What's worse, while two universal theorems get along just fine, two existential theorems don't, because they might have two different choices of X and then you have to have coherence theorems that show that if is_nat X and is_nat Y and P(X) then P(Y), where P is a property of interest. If is_nat determines X up to isomorphism this is probably possible to prove, but it's not automatic and making everything work together gets a lot harder.

[Massimiliano Gubinelli]

I can imagine. For the moment I'm even stuck at the complex number game ... :)

[Eric Wieser]

Does mathlib have a linter for "this typeclass has no instances"?

[Damiano Testa]

Isn't that the inhabited instance? I have been asked by the linter to produce inhabitedinstances when defining a new type.