negative natural numbers

Stream: new members

[Damiano Testa]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Damiano Testa]

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]

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

[Johan Commelin]

@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]

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

[Damiano Testa]

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]

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

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

(It's called nat.pred btw)

[Johan Commelin]

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

[Damiano Testa]

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]

Mario Carneiro said:

(It's called nat.pred btw)

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

[Mario Carneiro]

it is nat.pred up to equality

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

thank you!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

ouch

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Johan Commelin]

@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]

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]

What's happening with the coefficients below N?

[Damiano Testa]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

where () is coeff

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

Johan Commelin said:

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

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

[Mario Carneiro]

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

[Damiano Testa]

(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]

\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]

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

[Mario Carneiro]

indeed

[Johan Commelin]

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

[Damiano Testa]

Johan Commelin said:

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

yes

[Mario Carneiro]

you could try using N = multiplicity x f

[Johan Commelin]

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

[Mario Carneiro]

(roughly)

[Damiano Testa]

I will look up multiplicity, then!

[Damiano Testa]

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

[Mario Carneiro]

oh, enats are even more fun! :smiling_devil:

[Damiano Testa]

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]

it's a subset of fin.range n

[Damiano Testa]

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

[Johan Commelin]

$\mathbb{N} \cup \infty$

[Scott Morrison]

"extended" natural numbers

[Mario Carneiro]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I want to define the valuation on a discrete valuation ring

[Johan Commelin]

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

[Damiano Testa]

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]

Kevin Buzzard said:

I want to define the valuation on a discrete valuation ring

Where will it take values?

[Kevin Buzzard]

You should buy an external mic on amazon or whatever

[Kevin Buzzard]

with_zero (multiplicative \Z)

[Johan Commelin]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

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]

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]

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]

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

[Kenny Lau]

the in is part of the syntax

[Kenny Lau]

btw this is polynomial.derivative

[Kenny Lau]

so you can just look at how they do it

[Kenny Lau]

src#polynomial.derivative

[Kenny Lau]

nvm this isn't the derivative

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Kenny Lau]

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

[Kenny Lau]

including the error would be more efficient

[Damiano Testa]

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

[Damiano Testa]

Kenny Lau said:

including the error would be more efficient

The error was unexpected token, though...

[Kenny Lau]

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

[Kenny Lau]

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

[Damiano Testa]

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]

(coeff is underlined)

[Kenny Lau]

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

[Kenny Lau]

so Lean expects coeff i p : polynomial R as well

[Kenny Lau]

so Lean expects p : polynomial (polynomial R)

[Kenny Lau]

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

[Damiano Testa]

Ok, I added a C, indeed! Thanks!

[Damiano Testa]

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

[Johan Commelin]

Sorry for not testing the code...

[Damiano Testa]

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]

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]

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]

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]

(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]

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

[Damiano Testa]

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]

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