## Stream: new members

### Topic: negative natural numbers

#### Damiano Testa (Sep 02 2020 at 07:42):

Dear All,

every once in a while, I am confronted with Lean accepting and working with functions that I thought would not have to exist. Here is a simple example

def shift1 : ℕ → ℕ := λ i : ℕ , i-1
#eval shift1 0  --- 0
#eval shift1 1  --- 0
#eval shift1 0 - shift1 1  --- 0


I gather than Lean considers "negative natural numbers" as equal to 0. I always feel a little worried by this.

1. Why does Lean not ask me to prove that the codomain of shift1 is ℕ?
2. Assuming that Lean is being lazy about it, why does Lean not complain when I apply shift1 at 0?
3. Does this not cause consistency issues with proof checking?

#### Mario Carneiro (Sep 02 2020 at 07:45):

When you use - and the domain is natural numbers, you get the function nat.sub : nat -> nat -> nat, which is truncated subtraction

#### Mario Carneiro (Sep 02 2020 at 07:45):

there is no inference of alternatives, and this can sometimes cause surprises, but there is no consistency concern, it's just a weird function

#### Bryan Gin-ge Chen (Sep 02 2020 at 07:45):

As Mario says, 1+2 might be cleared up if you inspect the definition of natural number subtraction in Lean. This blog post of @Kevin Buzzard is related too.

#### Mario Carneiro (Sep 02 2020 at 07:47):

If you want "proper subtraction", you should write (a - b : int) (even if a and b have type nat). Then it will infer int.sub instead (which is sensible) and coerce a and b to integers

#### Mario Carneiro (Sep 02 2020 at 07:48):

Of course, if you do this lean will complain about the type you have given shift1

#### Damiano Testa (Sep 02 2020 at 07:48):

Ok, so you are saying that what Lean checks is correct, but it is on me to check that I am not using - where I should not?

#### Mario Carneiro (Sep 02 2020 at 07:48):

well, if you wanted truncated subtraction then it might be the right thing

#### Johan Commelin (Sep 02 2020 at 07:49):

@Damiano Testa You cannot prove that a function (or any term, for that matter) has a certain type. It has only one type, Lean can try to check it for you, but from a proving point of view, it's inaccesible.

#### Scott Morrison (Sep 02 2020 at 07:49):

Yes, just like it's on you to put parentheses in the right places!

#### Damiano Testa (Sep 02 2020 at 07:49):

Mario Carneiro said:

If you want "proper subtraction", you should write (a - b : int) (even if a and b have type nat). Then it will infer int.sub instead (which is sensible) and coerce a and b to integers

I see, so, to be safe, I should be using "integer subtraction" and prove that I land in the naturals in my applications

#### Mario Carneiro (Sep 02 2020 at 07:49):

but usually yes, you should just always use it when you have a hypothesis saying it is sensible

#### Johan Commelin (Sep 02 2020 at 07:49):

So if you write def shift1 : ℕ → ℕ := then what ever comes afterwards must be a function that has a well-defined nat value when you stick in 0.

#### Johan Commelin (Sep 02 2020 at 07:50):

You could also define shift1 : pnat -> nat... and then you cannot evaluate it on 0, but only on terms of type pnat, which consist of nat + a proof of positivity.

#### Johan Commelin (Sep 02 2020 at 07:50):

In practice however, it is easier to use the shift1 that you defined.

#### Mario Carneiro (Sep 02 2020 at 07:51):

(It's called nat.pred btw)

#### Johan Commelin (Sep 02 2020 at 07:51):

And then put the possitivity assumptions in the theorems that you want to prove.

#### Damiano Testa (Sep 02 2020 at 07:51):

Ok, these answers clarified my doubts and confirmed my fears! I am glad to hear that Lean is acting consistently, I am less happy about having to now check that when I use - is really should make sure that - is the function that I think it is!

#### Johan Commelin (Sep 02 2020 at 07:51):

Mario Carneiro said:

(It's called nat.pred btw)

But that one has syntactic issues... because i - 1 looks a lot better.

#### Mario Carneiro (Sep 02 2020 at 07:52):

it is nat.pred up to equality

#### Mario Carneiro (Sep 02 2020 at 07:52):

Kevin will tell you to just avoid ever using - on naturals

#### Johan Commelin (Sep 02 2020 at 07:52):

But you can't avoid using 1/x on the rationals...

#### Johan Commelin (Sep 02 2020 at 07:53):

Damiano Testa said:

Ok, these answers clarified my doubts and confirmed my fears! I am glad to hear that Lean is acting consistently, I am less happy about having to now check that when I use - is really should make sure that - is the function that I think it is!

There will be a theorem that says that it is the function you think it is for all sensible inputs.

#### Mario Carneiro (Sep 02 2020 at 07:53):

If you prove a good selection of theorems about your definitions, you will very likely notice if you have missed a hypothesis

#### Damiano Testa (Sep 02 2020 at 07:53):

So, just to make it completely explicit: a-b in Lean means what I would write on a board as max 0 (a-b)
Lean takes care of checking that with this definition, everything follows

#### Johan Commelin (Sep 02 2020 at 07:53):

1/0 = 0, but for all nonzero x, we have a theorem that says x * (1/x) = 1

#### Damiano Testa (Sep 02 2020 at 07:54):

Alright, my doubts have dissolved, my fears have crystallized!

thank you!

#### Mario Carneiro (Sep 02 2020 at 07:54):

similarly, we have a theorem that says a-b means what you would write on a board as a-b whenever it could possibly land in the type you have ascribed to it

#### Johan Commelin (Sep 02 2020 at 07:55):

Of course def shift1' : int -> int := \lam i, i - 1 is mathematically pure

#### Mario Carneiro (Sep 02 2020 at 07:55):

otherwise it yields "garbage"and we quietly ignore that case

#### Johan Commelin (Sep 02 2020 at 07:56):

@Damiano Testa Have you ever tried #eval 7.3/2.5?

ouch

#### Damiano Testa (Sep 02 2020 at 07:56):

Right, except that if I am trying to shift the coefficients of a polynomial, then I am assigning the constant term to lots of coefficients that should be getting a coefficient of 0

#### Mario Carneiro (Sep 02 2020 at 07:57):

shouldn't the coefficient map be going the other direction?

#### Damiano Testa (Sep 02 2020 at 07:57):

Johan Commelin said:

Damiano Testa Have you ever tried #eval 7.3/2.5?

are you trying to discourage me from using Lean?!?! Ahahaha

#### Johan Commelin (Sep 02 2020 at 07:57):

What exactly are you trying to do? Can you write down the function in maths $\latex here$

#### Johan Commelin (Sep 02 2020 at 07:59):

@Damiano Testa Is it $\sum_i a_i X^i \mapsto \sum_i a_i X^{i-1}$, or what kind of map do you want?

#### Damiano Testa (Sep 02 2020 at 07:59):

Mario Carneiro said:

shouldn't the coefficient map be going the other direction?

In my mind, I have a polynomial f and I want to write is as x^N*g, where g is not divisible by x. For this, I shift coefficients by N...

#### Mario Carneiro (Sep 02 2020 at 08:00):

What's happening with the coefficients below N?

#### Damiano Testa (Sep 02 2020 at 08:00):

the polynomial f has coefficients below N equal to 0...

#### Mario Carneiro (Sep 02 2020 at 08:01):

In that situation you can define g(i) = f(i+N)

#### Johan Commelin (Sep 02 2020 at 08:01):

I wish multiplicity would be easier to use... but I'm scared of sending you in that direction. It is what should be used here.

#### Mario Carneiro (Sep 02 2020 at 08:01):

where () is coeff

#### Damiano Testa (Sep 02 2020 at 08:02):

but in order to construct the support for g i need to do the opposite shift, no?

#### Johan Commelin (Sep 02 2020 at 08:02):

I don't think you should construct the polynomial by hand.

#### Damiano Testa (Sep 02 2020 at 08:02):

Johan Commelin said:

I don't think you should construct the polynomial by hand.

Ok, but I know of no other way...

#### Mario Carneiro (Sep 02 2020 at 08:03):

You could say N is the largest integer such that there exists g such that f = x^N*g

#### Damiano Testa (Sep 02 2020 at 08:03):

(to be clear, in this specific case, I do not think that there is a problem with using Lean's -, but the proof checker in my mind was having some difficult times reconciling the two notions!)

#### Johan Commelin (Sep 02 2020 at 08:03):

\lam poly, \sum i in range (nat_degree poly), coeff i poly * X ^ (i - N) is one definition... but I don't think it's the best.

#### Johan Commelin (Sep 02 2020 at 08:04):

Mario Carneiro said:

You could say N is the largest integer such that there exists g such that f = x^N*g

This is multiplicity

indeed

#### Johan Commelin (Sep 02 2020 at 08:04):

@Damiano Testa Do you already have a proof that your poly is nonzero?

#### Damiano Testa (Sep 02 2020 at 08:04):

Johan Commelin said:

Damiano Testa Do you already have a proof that your poly is nonzero?

yes

#### Mario Carneiro (Sep 02 2020 at 08:05):

you could try using N = multiplicity x f

#### Johan Commelin (Sep 02 2020 at 08:05):

Great... then multiplicity might not be too bad.

(roughly)

#### Damiano Testa (Sep 02 2020 at 08:05):

I will look up multiplicity, then!

#### Damiano Testa (Sep 02 2020 at 08:05):

(and use it carefully: I am fed up of finsets)

#### Mario Carneiro (Sep 02 2020 at 08:06):

oh, enats are even more fun! :smiling_devil:

#### Damiano Testa (Sep 02 2020 at 08:06):

i had to write a lemma to show that a bounded subset of the naturals is a finset and i do not want to think about finsets again, if possible!

#### Mario Carneiro (Sep 02 2020 at 08:06):

it's a subset of fin.range n

#### Damiano Testa (Sep 02 2020 at 08:06):

enats?! I am not sure that I want to know what those are

#### Johan Commelin (Sep 02 2020 at 08:07):

$\mathbb{N} \cup \infty$

#### Scott Morrison (Sep 02 2020 at 08:07):

"extended" natural numbers

#### Mario Carneiro (Sep 02 2020 at 08:07):

you will be getting acquainted with them because that's the type of multiplicity

#### Damiano Testa (Sep 02 2020 at 08:08):

oooh no! at least, I also produced many lemmas proving that a polynomial is non-zero, so hopefully I can steer away from enats! for finsets the bad guy was nonempty...

#### Damiano Testa (Sep 02 2020 at 08:09):

it looks like the "good" non-zero saves you from the evil of enats and nonempty

#### Kevin Buzzard (Sep 02 2020 at 08:09):

@Damiano Testa I was going to be using multiplicity in about an hour on the Discord.

#### Kevin Buzzard (Sep 02 2020 at 08:09):

I want to define the valuation on a discrete valuation ring

#### Johan Commelin (Sep 02 2020 at 08:10):

let N := enat.get (multiplicity X f) _
obtain \<g, hg\> : X ^ N \| f := pow_multiplicity_dvd _,


#### Damiano Testa (Sep 02 2020 at 08:10):

Kevin Buzzard said:

Damiano Testa I was going to be using multiplicity in about an hour on the Discord.

I see! I will try to work with it a little first and if I am still having problems, I will come to discord. i feel a little awkward on the discord: I am listening in on the conversation, but not able to talk. I feel like I am eavesdropping...

#### Johan Commelin (Sep 02 2020 at 08:10):

Kevin Buzzard said:

I want to define the valuation on a discrete valuation ring

Where will it take values?

#### Kevin Buzzard (Sep 02 2020 at 08:11):

You should buy an external mic on amazon or whatever

#### Kevin Buzzard (Sep 02 2020 at 08:11):

with_zero (multiplicative \Z)

#### Johan Commelin (Sep 02 2020 at 08:11):

Note that (factors x).card is also very useful. See the dvr.lean file

#### Damiano Testa (Sep 02 2020 at 08:11):

Kevin Buzzard said:

You should buy an external mic on amazon or whatever

Yes, I am going to, I just have not gotten around to doing it, yet

#### Johan Commelin (Sep 02 2020 at 08:11):

I've used it as a "pseudo" valuation already

#### Kevin Buzzard (Sep 02 2020 at 08:14):

The issue with DVRs will be proving v(xy)=v(x)v(y).

#### Damiano Testa (Sep 02 2020 at 08:14):

Ok, I have made a note of all the commands that you suggested wrt multiplicities and also made a mental note that - in Lean is not the - in my mind, at least when it comes to the naturals!

I feel kind of strange that in my mind, shift1 does not compile as a function from nat to nat, while for Lean it does, although now I understand the reason behind it!

#### Kevin Buzzard (Sep 02 2020 at 08:16):

To find "all of the commands for multiplicity" you should #check the definition, right click to find it in the source code, and then read the statements of the theorems that come immediately after the definition.

#### Johan Commelin (Sep 02 2020 at 08:16):

@Damiano Testa But like I said... multiplicity API needs quite a bit of love

#### Damiano Testa (Sep 02 2020 at 08:17):

Johan Commelin said:

Damiano Testa But like I said... multiplicity API needs quite a bit of love

that is ok: i feel like I have not really taken advantage of the existing API's of almost all the definitions that I have been using so far...

#### Damiano Testa (Sep 02 2020 at 08:20):

Kevin Buzzard said:

To find "all of the commands for multiplicity" you should #check the definition, right click to find it in the source code, and then read the statements of the theorems that come immediately after the definition.

I know that you mentioned this many times and I am making progress with this!

1. I am getting better at reading Lean code, so I can actually understand the statements (although the proof escape me, usually, but, by proof irrelevance, I can work with the one in my head and I am happy!)
2. I am starting to realize that files are not so long, so "reading the whole file" is actually not a daunting task!
3. I am also understanding how to convert these statement into commands that I can use.

Probably, these 3 points above are clear to everyone else, but I am trying to internalize them, albeit slowly!

#### Kevin Buzzard (Sep 02 2020 at 08:33):

For me this was a key point. I remember thinking "I need to use finite sets, so I should carefully read all of data.finset so I should probably also read all of data.multiset" and these files are (or were -- maybe now they have been split up a bit) gigantic, and the proofs were incomprehensible. I thought I was in trouble! I tried to work through some of the early proofs but they were in term mode and I found it extremely difficult.

I later on realised that I was doing the wrong thing. The key things to do are: (1) isolate the key definitions in the file (which nowadays should be easy because they should be in the module documentation at the top of the file) and (2) for each definition which you want to use, get to know its interface by reading the statements of the theorems proved about it; often some of the important ones are proved in the code directly after the definition is made. Don't worry about the proofs. Just figure out what you can do with the definition. Then you can use it in your own work.

#### Damiano Testa (Sep 02 2020 at 08:42):

Johan Commelin said:

\lam poly, \sum i in range (nat_degree poly), coeff i poly * X ^ (i - N) is one definition... but I don't think it's the best.

Johan, when you write \sum, I imagine that you are telling Lean that you want to sum over the set. What is the syntax? I am using

λ p : polynomial R , (∑ ( i in range (nat_degree p)), coeff i p * X ^ (nat_degree p - i))


and Lean does not like it...

#### Kenny Lau (Sep 02 2020 at 08:43):

it's ∑ i in range (nat_degree p) not ∑ ( i in range (nat_degree p))

#### Kenny Lau (Sep 02 2020 at 08:43):

the in is part of the syntax

#### Kenny Lau (Sep 02 2020 at 08:43):

btw this is polynomial.derivative

#### Kenny Lau (Sep 02 2020 at 08:43):

so you can just look at how they do it

#### Kenny Lau (Sep 02 2020 at 08:43):

src#polynomial.derivative

#### Kenny Lau (Sep 02 2020 at 08:44):

nvm this isn't the derivative

#### Damiano Testa (Sep 02 2020 at 08:44):

with

λ p : polynomial R , (∑ i in range (nat_degree p) , coeff i p * X ^ (nat_degree p - i))


I still get an unexpected token and a red underlined \Sigma

#### Kenny Lau (Sep 02 2020 at 08:45):

you need to open_locale big_operators at the top of the file after the imports

#### Damiano Testa (Sep 02 2020 at 08:45):

Kenny Lau said:

nvm this isn't the derivative

That is ok, they probably do something similar to what I want: I will take a look!

#### Kenny Lau (Sep 02 2020 at 08:45):

you'll find that "Lean does not like it" doesn't tell much

#### Kenny Lau (Sep 02 2020 at 08:45):

it's like people saying that some code "doesn't work"

#### Kenny Lau (Sep 02 2020 at 08:46):

including the error would be more efficient

#### Damiano Testa (Sep 02 2020 at 08:46):

Now "Lean does not like range"! Wow Progress!!

#### Damiano Testa (Sep 02 2020 at 08:47):

Kenny Lau said:

including the error would be more efficient

The error was unexpected token, though...

#### Kenny Lau (Sep 02 2020 at 08:48):

yes, and that's more helpful than "Lean doesn't like it"

#### Kenny Lau (Sep 02 2020 at 08:48):

so Lean doesn't like range because it's finset.range, so you either type the full name or open finset

#### Damiano Testa (Sep 02 2020 at 08:49):

yes, I added the finset. Still...

type mismatch at application
p.coeff
term
p
has type
polynomial R
but is expected to have type
polynomial (polynomial R)


#### Damiano Testa (Sep 02 2020 at 08:49):

(coeff is underlined)

#### Kenny Lau (Sep 02 2020 at 08:52):

Lean sees coeff i p * X ^ (nat_degree p - i)) and knows that X ^ (nat_degree p - i)) : polynomial R

#### Kenny Lau (Sep 02 2020 at 08:52):

so Lean expects coeff i p : polynomial R as well

#### Kenny Lau (Sep 02 2020 at 08:52):

so Lean expects p : polynomial (polynomial R)

#### Kenny Lau (Sep 02 2020 at 08:52):

because you need C (coeff i p) instead of coeff i p

#### Damiano Testa (Sep 02 2020 at 08:52):

Ok, I added a C, indeed! Thanks!

#### Damiano Testa (Sep 02 2020 at 08:52):

(also, the i and the p are flipped, but I got as far!)

#### Johan Commelin (Sep 02 2020 at 08:55):

Sorry for not testing the code...

#### Damiano Testa (Sep 02 2020 at 08:57):

Johan Commelin said:

Sorry for not testing the code...

No problem: it is more helpful when I also have to do some work to understand how to use it!

#### Damiano Testa (Sep 02 2020 at 11:11):

Johan Commelin said:

\lam poly, \sum i in range (nat_degree poly), coeff i poly * X ^ (i - N) is one definition... but I don't think it's the best.

Dear Johan,

as I am making progress in unwrapping the definitions, I think that the range should be nat_degree p + 1, rather than nat_degree p, if I understand correctly.

lemma larger_range {R : Type*} [comm_ring R] {f : polynomial R} : f = ∑ i in finset.range (nat_degree f + 1) , (polynomial.C (coeff f i)) * X ^i :=
begin
exact as_sum f,
end


#### Kevin Buzzard (Sep 02 2020 at 12:06):

There was no point proving that lemma; it is best if you delete it and just use as_sum. The more functions there are, the more the chances are that Lean will get confused.

#### Damiano Testa (Sep 02 2020 at 12:09):

I agree, although I would like to use the "reversal of coefficients", which I am not sure is already defined:

noncomputable def at_infty {R : Type*} [comm_ring R] : polynomial R → polynomial R :=
λ p : polynomial R , ∑ i in finset.range (nat_degree p + 1) , (polynomial.C (coeff p i)) * X ^ (nat_degree p - i)


#### Damiano Testa (Sep 02 2020 at 12:10):

(and now I am struggling to prove that the coefficients satisfy the identity

coeff f a = coeff (at_infty f) (nat_degree f - a)


)

#### Reid Barton (Sep 02 2020 at 12:17):

This operation was actually discussed here but I don't know whether a PR was ever made

#### Damiano Testa (Sep 02 2020 at 12:21):

Reid Barton said:

This operation was actually discussed here but I don't know whether a PR was ever made

Thank you! I tried

#check polynomial.reverse


but there is not hit, unfortunately.

#### Johan Commelin (Sep 02 2020 at 12:55):

@Damiano Testa oops, you are right about the nat.degree f + 1

Last updated: May 17 2021 at 21:12 UTC