Zulip Chat Archive

Stream: maths

Topic: nat and pnat


view this post on Zulip Kevin Buzzard (May 27 2018 at 15:42):

Should I not be using these functions:

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:42):

definition plus_to_nat (n : ℕ+) := (n : )
definition nat_to_plus (n : ) := (n : ℕ+)

-- example (n : ℕ+) : nat_to_plus (plus_to_nat n) = n := by simp -- fails

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:42):

Not only are we no longer refl, we are not even simp apparently

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:42):

Is that because simp won't unfold my definition by default?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:43):

I am trying to make working with pnat easier. Nobody like a subtype.

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:43):

But I really want it to be easy to work with

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:45):

@[reducible] definition plus_to_nat (n : ℕ+) := (n : )
@[reducible] definition nat_to_plus (n : ) := (n : ℕ+)

example (n : ℕ+) : nat_to_plus (plus_to_nat n) = n := begin
unfold nat_to_plus plus_to_nat, -- still need to do this
simp,
end

What am I doing wrong? Should those functions not have names and I am expected to always use coercion?

view this post on Zulip Mario Carneiro (May 27 2018 at 15:45):

The functions have names

view this post on Zulip Mario Carneiro (May 27 2018 at 15:45):

Have you looked at pnat.lean?

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:58):

I have

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:58):

Oh I see, you're saying don't make new names for old functions

view this post on Zulip Kevin Buzzard (May 27 2018 at 15:58):

because the old ones will have been made better

view this post on Zulip Mario Carneiro (May 27 2018 at 15:59):

By the way I'm revising pnat right now

view this post on Zulip Mario Carneiro (May 27 2018 at 15:59):

to remove that funny coercion

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:00):

So am I supposed to refer to these functions as coe_nat_pnat and coe_pnat_nat if I ever talk about them?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:01):

wait those aren't the functions

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:02):

nat.to_pnat' and subtype.val are the rather unsexy names of the functions

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:02):

Is the idea behind coercion that I do not ever mention these names?

view this post on Zulip Mario Carneiro (May 27 2018 at 16:02):

yes

view this post on Zulip Mario Carneiro (May 27 2018 at 16:02):

nat.to_pnat' is going to be used instead of the coercion

view this post on Zulip Mario Carneiro (May 27 2018 at 16:02):

but the other coercion will stay

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:03):

and what happens when I end up with ↑↑↑↑↑n?

view this post on Zulip Mario Carneiro (May 27 2018 at 16:03):

what are those coercions?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:03):

Oh -- you're removing the instance?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:03):

the coercion from nat to pnat?

view this post on Zulip Mario Carneiro (May 27 2018 at 16:03):

yes

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:03):

Oh great

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:04):

you will really break Reid's code which I'm trying to maintain :-)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:04):

I can't help but think that this is good though

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:05):

So you'll replace it with a dependent coercion which typechecks but when it actually runs it will ask the type class resolution system for a proof that n > 0?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:06):

and then the coercion from pnat to nat to pnat will become refl

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:06):

or some other cool new system

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:07):

I don't know if the typeclass resolution system will be the right thing

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:07):

I want it to check the properties of all the pnats it can see :-)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:07):

and then use known lemmas like a>0 and b>0 implies a+b>0

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:08):

Can it work like that? That's how it works in a mathematician's head

view this post on Zulip Mario Carneiro (May 27 2018 at 16:08):

that is not at all what I'm suggesting :)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:08):

thought not

view this post on Zulip Mario Carneiro (May 27 2018 at 16:08):

I'm just removing the nat_pnat coercion, that's it

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:08):

less ambitious

view this post on Zulip Mario Carneiro (May 27 2018 at 16:09):

there is a coercion that asks dec_trivial for the positivity proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

What is stopping my idea above being built into Lean 7?

view this post on Zulip Mario Carneiro (May 27 2018 at 16:09):

that's nat.to_pnat

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

Oh yeah I saw that

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

you fill in the hole with a tactic

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

I see

view this post on Zulip Mario Carneiro (May 27 2018 at 16:09):

it could ask some other tactic, like simp

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

so at some point you might want to get hold of a proof

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

and you have loads of options

view this post on Zulip Mario Carneiro (May 27 2018 at 16:09):

and then it would do some kind of a+b>0 thing

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:09):

you could ask the type class dude

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:10):

or a tactic

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:10):

or you could pester the user

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:10):

But I'm a busy guy and I don't want to be pestered

view this post on Zulip Mario Carneiro (May 27 2018 at 16:10):

But I hope that people provide a positivity proof of a+b just by adding a b : pnat

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:10):

Yes

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:10):

so in some sense my example was not good

view this post on Zulip Mario Carneiro (May 27 2018 at 16:11):

as long as you stay in pnat world it's all good

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:11):

but how about "n^2 + 1 : pnat"

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:11):

if n is a nat

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:11):

A mathematician would be able to do that

view this post on Zulip Mario Carneiro (May 27 2018 at 16:11):

that's succ_pnat

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:11):

damn you

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:11):

What about (n + 4 + n : pnat)

view this post on Zulip Mario Carneiro (May 27 2018 at 16:12):

but I think there is space for add_pnat_left : N -> N+ -> N+

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:12):

A mathematician could do that

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:12):

what about (4 + n : pnat)

view this post on Zulip Mario Carneiro (May 27 2018 at 16:12):

that would cover your example

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:12):

I see

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:12):

But can we get the coercion to do it?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:12):

Why is the coercion system part of type class resolution?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:12):

could it be its own system?

view this post on Zulip Mario Carneiro (May 27 2018 at 16:12):

no, the old coercion did that by cheating

view this post on Zulip Mario Carneiro (May 27 2018 at 16:13):

you can still use nat.to_pnat' if you don't want to be bothered

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:13):

So how do I get (4 + n : pnat) to work?

view this post on Zulip Mario Carneiro (May 27 2018 at 16:13):

(4+n).to_pnat'

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:15):

But that's bad

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:15):

because the value is now not defeq to 4+n

view this post on Zulip Mario Carneiro (May 27 2018 at 16:15):

Really there's no need to use to_pnat unless you care that the nat component is defeq to the given arg

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:15):

`to_pnat' is not the function I had in mind

view this post on Zulip Mario Carneiro (May 27 2018 at 16:15):

the point is that it works when the input made sense

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:15):

The function I had in mind sends 4 + n to a pnat whose value is 4 + n

view this post on Zulip Mario Carneiro (May 27 2018 at 16:15):

it's like nat.sub

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:16):

We are missing a function

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:16):

That's what causes the problem

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:16):

Definitional equality is so important to you guys

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:16):

and I don't want to throw it away here

view this post on Zulip Mario Carneiro (May 27 2018 at 16:16):

that function exists too

view this post on Zulip Mario Carneiro (May 27 2018 at 16:16):

that's nat.to_pnat

view this post on Zulip Mario Carneiro (May 27 2018 at 16:16):

that's why there's two versions

view this post on Zulip Mario Carneiro (May 27 2018 at 16:17):

or just pnat.mk

view this post on Zulip Mario Carneiro (May 27 2018 at 16:17):

i.e. the constructor

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:17):

example (n : ℕ) : ℕ+ := nat.to_pnat (4 + n)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:17):

exact tactic failed, type mismatch, given expression has type
  true
but is expected to have type
  as_true (4 + n > 0)
state:
n : 
 as_true (4 + n > 0)
state:
n : 
 4 + n > 0

view this post on Zulip Mario Carneiro (May 27 2018 at 16:17):

but that one gives you a proof obligation

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:18):

But 4 + n > 0 is true by schookid

view this post on Zulip Mario Carneiro (May 27 2018 at 16:18):

and you'd better prove it

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:18):

It's true by schoolkid

view this post on Zulip Mario Carneiro (May 27 2018 at 16:18):

nat.to_pnat (4 + n) (by schoolkid)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:18):

I really want this schoolkid tactic

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:18):

Mathematicians want to pass over schoolkid stuff without any comment

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:19):

I see

view this post on Zulip Mario Carneiro (May 27 2018 at 16:19):

the scope of things you could write there is unbounded

view this post on Zulip Mario Carneiro (May 27 2018 at 16:19):

At some point you have to actually prove things

view this post on Zulip Mario Carneiro (May 27 2018 at 16:20):

If you don't care to prove that statement, you can use (4+n).to_pnat'

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:20):

rofl

view this post on Zulip Mario Carneiro (May 27 2018 at 16:20):

unless it's an important definition you are going to unfold later, I doubt you will even notice the difference

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:20):

import data.pnat
#check nat.to_pnat -- chaos ensues

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:20):

I think #check might have dealt with that one better

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:21):

Is that a bug?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:21):

#check @nat.to_pnat works fine

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:22):

you went for exact_dec_trivial??

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:22):

Not even simp?

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:22):

def to_pnat (n : ℕ) (h : n > 0 . tactic.exact_dec_trivial) : ℕ+ := ⟨n, h⟩

view this post on Zulip Mario Carneiro (May 27 2018 at 16:22):

Those are incomparable tactics

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:23):

I think you should use sledgehammer

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:23):

We want this coercion to work!

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:23):

to_pnat : 3/10. Must try harder to coerce.

view this post on Zulip Mario Carneiro (May 27 2018 at 16:23):

this is a basic function, it's not my job to select my favorite finishing tactic and introduce dependencies early in the development

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:24):

Dependencies?!

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:24):

We want it to work!

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:24):

So in fact you are suggesting that I should write "mathematicians mode"

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:25):

where we put the coercion back but we use by schoolkid

view this post on Zulip Mario Carneiro (May 27 2018 at 16:25):

The thing about auto params is that they can't be changed later

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:25):

right

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:25):

I am seriously suggesting a "mathematicians overlay"

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:25):

I was thinking about this earlier when chatting to Kenny and Chris

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:25):

So there's a coercion from nat to pnat

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:25):

(although it might not last long)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:26):

and so of course my first question is "what the hell are you going to do with zero"

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:26):

because of course you can use nat.rec to define it, and succ n goes to succ n together with the proof that succ n > 0

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:27):

and 0 goes to...this is just stupid

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:27):

So I think you should send 0 to 37

view this post on Zulip Kenny Lau (May 27 2018 at 16:27):

nat -> option pnat problem solved

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:27):

I think that that's a much better instance for the coercion because I think it better represents what is happening

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:28):

At the places it was supposed to be defined, it does what it is supposed to do

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:28):

and it sends everything else to 37

view this post on Zulip Mario Carneiro (May 27 2018 at 16:28):

That's a weird option for a coercion

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:28):

I don't see why it's any weirder than 1

view this post on Zulip Mario Carneiro (May 27 2018 at 16:28):

It's not even making a pnat?

view this post on Zulip Andrew Ashworth (May 27 2018 at 16:28):

how often do you move between nat and pnat? I feel like most people, once working with pnats, will continue to deal only in pnats

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:28):

Oh sorry

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:29):

I'll make it a pnat, sure

view this post on Zulip Andrew Ashworth (May 27 2018 at 16:29):

in that case explicitly providing the proof obligation n > 0 is not such a burden

view this post on Zulip Mario Carneiro (May 27 2018 at 16:29):

Of course pnat is inhabited, so we can use iget on that...

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:29):

but I just want to make the point that if you're coercing then you'd better realise that if you do this on 0 then you just did something stupid

view this post on Zulip Mario Carneiro (May 27 2018 at 16:29):

OF COURSE

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:29):

But I think that if the coercion did that

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:29):

then I think it would force people to write better code

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:30):

because they wouldn't do the lazy junk theorem thing which you do

view this post on Zulip Mario Carneiro (May 27 2018 at 16:30):

coercions don't have that luxury

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:30):

oh really

view this post on Zulip Kenny Lau (May 27 2018 at 16:30):

def coe (n):
  assert (n > 0)
  return [code]

view this post on Zulip Mario Carneiro (May 27 2018 at 16:30):

They are functions A -> B, where the user gets to pick A and B

view this post on Zulip Kenny Lau (May 27 2018 at 16:30):

Python style

view this post on Zulip Kenny Lau (May 27 2018 at 16:30):

we should have errors in Lean

view this post on Zulip Mario Carneiro (May 27 2018 at 16:30):

That's called monadic programming

view this post on Zulip Mario Carneiro (May 27 2018 at 16:31):

mathematicians don't want to deal with that

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:31):

so I'm sending nat to pnat, where everything positive goes to the correct thing (including defeq) and 0 goes to 37

view this post on Zulip Mario Carneiro (May 27 2018 at 16:31):

sure

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:31):

because then none of the junk theorems would work

view this post on Zulip Kenny Lau (May 27 2018 at 16:31):

@Kevin Buzzard I think you want something like nat.rec 37 id where you replace id with the appropriate thing so it works defeq

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:31):

and you would be forced to carry around the proof that n > 0 properly

view this post on Zulip Mario Carneiro (May 27 2018 at 16:32):

I don't think I prove any junk theorems about to_pnat'

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:32):

no but that's why you computer scientists tell us that functions should be total

view this post on Zulip Mario Carneiro (May 27 2018 at 16:32):

but I think you are making an issue where none exists here

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:32):

I am suggesting that real.sqrt should send all negative reals to 37

view this post on Zulip Mario Carneiro (May 27 2018 at 16:32):

There are options available, pick your favorite

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:32):

I think that 0 is the worst option

view this post on Zulip Kenny Lau (May 27 2018 at 16:33):

because then none of the junk theorems would work

except the one which says (0 : pnat) = 37 :P

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:33):

because it maximises the chance that the human prover doesn't spot their error

view this post on Zulip Mario Carneiro (May 27 2018 at 16:33):

Don't worry, they will notice

view this post on Zulip Mario Carneiro (May 27 2018 at 16:33):

you can't finish the proof if your model is wrong

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

That one time you take a square root and you forget to check the argument was non-negative

view this post on Zulip Mario Carneiro (May 27 2018 at 16:34):

then your theorem fails

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

you will discover this the very next time you try and use the square root

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

that's the point

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

it fails earlier

view this post on Zulip Mario Carneiro (May 27 2018 at 16:34):

and you come here and ask about it

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

which is a good thing

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

not me asking :-)

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:34):

the failure

view this post on Zulip Mario Carneiro (May 27 2018 at 16:34):

but composition is a really nice way to write expressions, and I don't want to lose it

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:35):

because the error says "x isn't 37" and I look at it and think "37? What the...Oh! I didn't check it wasn't negative!"

view this post on Zulip Kenny Lau (May 27 2018 at 16:35):

lol 37

view this post on Zulip Mario Carneiro (May 27 2018 at 16:35):

Obviously removing the coercion solves all these problems

view this post on Zulip Kenny Lau (May 27 2018 at 16:35):

as if x<0 is decidable

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:35):

It _has_ to be 37

view this post on Zulip Kenny Lau (May 27 2018 at 16:35):

they won't ever give 37 to you

view this post on Zulip Kenny Lau (May 27 2018 at 16:35):

x<0 is not decidable

view this post on Zulip Mario Carneiro (May 27 2018 at 16:35):

yes it is, it's false

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:35):

rofl you should have seen the original version of complex.lean

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:36):

I had to prove it was inhabited

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:36):

but I changed it before I made the PR

view this post on Zulip Kevin Buzzard (May 27 2018 at 16:36):

You're right, I'd never have got away with it

view this post on Zulip Mario Carneiro (May 27 2018 at 16:37):

When I removed the coercion, there was one place where it appeared in mathlib

view this post on Zulip Mario Carneiro (May 27 2018 at 16:38):

I had to define a positive sequence that converged to zero, and used (n:ℕ+)⁻¹

view this post on Zulip Mario Carneiro (May 27 2018 at 16:39):

I think that's a good example of use, since it doesn't matter what the value is at zero, it's just a value

view this post on Zulip Johan Commelin (May 27 2018 at 17:53):

@Kevin Buzzard I'm a bit confused. With division by zero, or subtraction of nat's you say "just get over it, there is a footnote explaining some edge cases". Why isn't that enough here? Why don't you want to define x / 0 as 37? (I actually prefer 57, since that is Grothendieck's prime...)

view this post on Zulip Johan Commelin (May 27 2018 at 17:54):

Or similarly (3 : nat) - (5 : nat). That should also be 57, I think...

view this post on Zulip Kenny Lau (May 27 2018 at 23:14):

https://github.com/leanprover/mathlib/blob/master/data/pnat.lean

view this post on Zulip Kenny Lau (May 27 2018 at 23:14):

@Kevin Buzzard congratulations, it has been removed

view this post on Zulip Kevin Buzzard (May 28 2018 at 04:19):

Maybe one day it will come back with super powers


Last updated: May 09 2021 at 10:11 UTC