Zulip Chat Archive

Stream: new members

Topic: negative natural numbers


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:48):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:48):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 02 2020 at 07:49):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 02 2020 at 07:50):

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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:51):

(It's called nat.pred btw)

view this post on Zulip Johan Commelin (Sep 02 2020 at 07:51):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:52):

it is nat.pred up to equality

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:52):

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

view this post on Zulip Johan Commelin (Sep 02 2020 at 07:52):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Damiano Testa (Sep 02 2020 at 07:54):

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

view this post on Zulip Damiano Testa (Sep 02 2020 at 07:54):

thank you!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 02 2020 at 07:55):

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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:55):

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

view this post on Zulip Johan Commelin (Sep 02 2020 at 07:56):

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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:56):

ouch

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 07:57):

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

view this post on Zulip 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

view this post on Zulip 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 $$

view this post on Zulip Johan Commelin (Sep 02 2020 at 07:59):

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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:00):

What's happening with the coefficients below N?

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:00):

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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:01):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:01):

where () is coeff

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:02):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:04):

indeed

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:04):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:05):

you could try using N = multiplicity x f

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:05):

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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:05):

(roughly)

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:05):

I will look up multiplicity, then!

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:05):

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

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:06):

oh, enats are even more fun! :smiling_devil:

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:06):

it's a subset of fin.range n

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:06):

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

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:07):

N\mathbb{N} \cup \infty

view this post on Zulip Scott Morrison (Sep 02 2020 at 08:07):

"extended" natural numbers

view this post on Zulip Mario Carneiro (Sep 02 2020 at 08:07):

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

view this post on Zulip 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...

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:09):

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

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 08:09):

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

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 08:09):

I want to define the valuation on a discrete valuation ring

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:10):

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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 08:11):

You should buy an external mic on amazon or whatever

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 08:11):

with_zero (multiplicative \Z)

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:11):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:11):

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

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 08:14):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:16):

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

view this post on Zulip 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...

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:43):

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

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:43):

the in is part of the syntax

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:43):

btw this is polynomial.derivative

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:43):

so you can just look at how they do it

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:43):

src#polynomial.derivative

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:44):

nvm this isn't the derivative

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:45):

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

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:45):

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

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:45):

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

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:46):

including the error would be more efficient

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:46):

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

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:47):

Kenny Lau said:

including the error would be more efficient

The error was unexpected token, though...

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:48):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:49):

(coeff is underlined)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:52):

so Lean expects coeff i p : polynomial R as well

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:52):

so Lean expects p : polynomial (polynomial R)

view this post on Zulip Kenny Lau (Sep 02 2020 at 08:52):

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

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:52):

Ok, I added a C, indeed! Thanks!

view this post on Zulip Damiano Testa (Sep 02 2020 at 08:52):

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

view this post on Zulip Johan Commelin (Sep 02 2020 at 08:55):

Sorry for not testing the code...

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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