Zulip Chat Archive

Stream: maths

Topic: nat and pnat

Kevin Buzzard (May 27 2018 at 15:42):

Should I not be using these functions:

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

Kevin Buzzard (May 27 2018 at 15:42):

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

Kevin Buzzard (May 27 2018 at 15:42):

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

Kevin Buzzard (May 27 2018 at 15:43):

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

Kevin Buzzard (May 27 2018 at 15:43):

But I really want it to be easy to work with

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?

Mario Carneiro (May 27 2018 at 15:45):

The functions have names

Mario Carneiro (May 27 2018 at 15:45):

Have you looked at pnat.lean?

Kevin Buzzard (May 27 2018 at 15:58):

I have

Kevin Buzzard (May 27 2018 at 15:58):

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

Kevin Buzzard (May 27 2018 at 15:58):

because the old ones will have been made better

Mario Carneiro (May 27 2018 at 15:59):

By the way I'm revising pnat right now

Mario Carneiro (May 27 2018 at 15:59):

to remove that funny coercion

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?

Kevin Buzzard (May 27 2018 at 16:01):

wait those aren't the functions

Kevin Buzzard (May 27 2018 at 16:02):

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

Kevin Buzzard (May 27 2018 at 16:02):

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

Mario Carneiro (May 27 2018 at 16:02):

yes

Mario Carneiro (May 27 2018 at 16:02):

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

Mario Carneiro (May 27 2018 at 16:02):

but the other coercion will stay

Kevin Buzzard (May 27 2018 at 16:03):

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

Mario Carneiro (May 27 2018 at 16:03):

what are those coercions?

Kevin Buzzard (May 27 2018 at 16:03):

Oh -- you're removing the instance?

Kevin Buzzard (May 27 2018 at 16:03):

the coercion from nat to pnat?

Mario Carneiro (May 27 2018 at 16:03):

yes

Kevin Buzzard (May 27 2018 at 16:03):

Oh great

Kevin Buzzard (May 27 2018 at 16:04):

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

Kevin Buzzard (May 27 2018 at 16:04):

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

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?

Kevin Buzzard (May 27 2018 at 16:06):

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

Kevin Buzzard (May 27 2018 at 16:06):

or some other cool new system

Kevin Buzzard (May 27 2018 at 16:07):

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

Kevin Buzzard (May 27 2018 at 16:07):

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

Kevin Buzzard (May 27 2018 at 16:07):

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

Kevin Buzzard (May 27 2018 at 16:08):

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

Mario Carneiro (May 27 2018 at 16:08):

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

Kevin Buzzard (May 27 2018 at 16:08):

thought not

Mario Carneiro (May 27 2018 at 16:08):

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

Kevin Buzzard (May 27 2018 at 16:08):

less ambitious

Mario Carneiro (May 27 2018 at 16:09):

there is a coercion that asks dec_trivial for the positivity proof

Kevin Buzzard (May 27 2018 at 16:09):

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

Mario Carneiro (May 27 2018 at 16:09):

that's nat.to_pnat

Kevin Buzzard (May 27 2018 at 16:09):

Oh yeah I saw that

Kevin Buzzard (May 27 2018 at 16:09):

you fill in the hole with a tactic

Kevin Buzzard (May 27 2018 at 16:09):

I see

Mario Carneiro (May 27 2018 at 16:09):

it could ask some other tactic, like simp

Kevin Buzzard (May 27 2018 at 16:09):

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

Kevin Buzzard (May 27 2018 at 16:09):

and you have loads of options

Mario Carneiro (May 27 2018 at 16:09):

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

Kevin Buzzard (May 27 2018 at 16:09):

you could ask the type class dude

Kevin Buzzard (May 27 2018 at 16:10):

or a tactic

Kevin Buzzard (May 27 2018 at 16:10):

or you could pester the user

Kevin Buzzard (May 27 2018 at 16:10):

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

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

Kevin Buzzard (May 27 2018 at 16:10):

Yes

Kevin Buzzard (May 27 2018 at 16:10):

so in some sense my example was not good

Mario Carneiro (May 27 2018 at 16:11):

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

Kevin Buzzard (May 27 2018 at 16:11):

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

Kevin Buzzard (May 27 2018 at 16:11):

if n is a nat

Kevin Buzzard (May 27 2018 at 16:11):

A mathematician would be able to do that

Mario Carneiro (May 27 2018 at 16:11):

that's succ_pnat

Kevin Buzzard (May 27 2018 at 16:11):

damn you

Kevin Buzzard (May 27 2018 at 16:11):

What about (n + 4 + n : pnat)

Mario Carneiro (May 27 2018 at 16:12):

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

Kevin Buzzard (May 27 2018 at 16:12):

A mathematician could do that

Kevin Buzzard (May 27 2018 at 16:12):

what about (4 + n : pnat)

Mario Carneiro (May 27 2018 at 16:12):

that would cover your example

Kevin Buzzard (May 27 2018 at 16:12):

I see

Kevin Buzzard (May 27 2018 at 16:12):

But can we get the coercion to do it?

Kevin Buzzard (May 27 2018 at 16:12):

Why is the coercion system part of type class resolution?

Kevin Buzzard (May 27 2018 at 16:12):

could it be its own system?

Mario Carneiro (May 27 2018 at 16:12):

no, the old coercion did that by cheating

Mario Carneiro (May 27 2018 at 16:13):

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

Kevin Buzzard (May 27 2018 at 16:13):

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

Mario Carneiro (May 27 2018 at 16:13):

(4+n).to_pnat'

Kevin Buzzard (May 27 2018 at 16:15):

But that's bad

Kevin Buzzard (May 27 2018 at 16:15):

because the value is now not defeq to 4+n

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

Kevin Buzzard (May 27 2018 at 16:15):

`to_pnat' is not the function I had in mind

Mario Carneiro (May 27 2018 at 16:15):

the point is that it works when the input made sense

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

Mario Carneiro (May 27 2018 at 16:15):

it's like nat.sub

Kevin Buzzard (May 27 2018 at 16:16):

We are missing a function

Kevin Buzzard (May 27 2018 at 16:16):

That's what causes the problem

Kevin Buzzard (May 27 2018 at 16:16):

Definitional equality is so important to you guys

Kevin Buzzard (May 27 2018 at 16:16):

and I don't want to throw it away here

Mario Carneiro (May 27 2018 at 16:16):

that function exists too

Mario Carneiro (May 27 2018 at 16:16):

that's nat.to_pnat

Mario Carneiro (May 27 2018 at 16:16):

that's why there's two versions

Mario Carneiro (May 27 2018 at 16:17):

or just pnat.mk

Mario Carneiro (May 27 2018 at 16:17):

i.e. the constructor

Kevin Buzzard (May 27 2018 at 16:17):

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

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

Mario Carneiro (May 27 2018 at 16:17):

but that one gives you a proof obligation

Kevin Buzzard (May 27 2018 at 16:18):

But 4 + n > 0 is true by schookid

Mario Carneiro (May 27 2018 at 16:18):

and you'd better prove it

Kevin Buzzard (May 27 2018 at 16:18):

It's true by schoolkid

Mario Carneiro (May 27 2018 at 16:18):

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

Kevin Buzzard (May 27 2018 at 16:18):

I really want this schoolkid tactic

Kevin Buzzard (May 27 2018 at 16:18):

Mathematicians want to pass over schoolkid stuff without any comment

Kevin Buzzard (May 27 2018 at 16:19):

I see

Mario Carneiro (May 27 2018 at 16:19):

the scope of things you could write there is unbounded

Mario Carneiro (May 27 2018 at 16:19):

At some point you have to actually prove things

Mario Carneiro (May 27 2018 at 16:20):

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

Kevin Buzzard (May 27 2018 at 16:20):

rofl

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

Kevin Buzzard (May 27 2018 at 16:20):

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

Kevin Buzzard (May 27 2018 at 16:20):

I think #check might have dealt with that one better

Kevin Buzzard (May 27 2018 at 16:21):

Is that a bug?

Kevin Buzzard (May 27 2018 at 16:21):

#check @nat.to_pnat works fine

Kevin Buzzard (May 27 2018 at 16:22):

you went for exact_dec_trivial??

Kevin Buzzard (May 27 2018 at 16:22):

Not even simp?

Kevin Buzzard (May 27 2018 at 16:22):

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

Mario Carneiro (May 27 2018 at 16:22):

Those are incomparable tactics

Kevin Buzzard (May 27 2018 at 16:23):

I think you should use sledgehammer

Kevin Buzzard (May 27 2018 at 16:23):

We want this coercion to work!

Kevin Buzzard (May 27 2018 at 16:23):

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

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

Kevin Buzzard (May 27 2018 at 16:24):

Dependencies?!

Kevin Buzzard (May 27 2018 at 16:24):

We want it to work!

Kevin Buzzard (May 27 2018 at 16:24):

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

Kevin Buzzard (May 27 2018 at 16:25):

where we put the coercion back but we use by schoolkid

Mario Carneiro (May 27 2018 at 16:25):

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

Kevin Buzzard (May 27 2018 at 16:25):

right

Kevin Buzzard (May 27 2018 at 16:25):

I am seriously suggesting a "mathematicians overlay"

Kevin Buzzard (May 27 2018 at 16:25):

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

Kevin Buzzard (May 27 2018 at 16:25):

So there's a coercion from nat to pnat

Kevin Buzzard (May 27 2018 at 16:25):

(although it might not last long)

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"

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

Kevin Buzzard (May 27 2018 at 16:27):

and 0 goes to...this is just stupid

Kevin Buzzard (May 27 2018 at 16:27):

So I think you should send 0 to 37

Kenny Lau (May 27 2018 at 16:27):

nat -> option pnat problem solved

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

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

Kevin Buzzard (May 27 2018 at 16:28):

and it sends everything else to 37

Mario Carneiro (May 27 2018 at 16:28):

That's a weird option for a coercion

Kevin Buzzard (May 27 2018 at 16:28):

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

Mario Carneiro (May 27 2018 at 16:28):

It's not even making a pnat?

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

Kevin Buzzard (May 27 2018 at 16:28):

Oh sorry

Kevin Buzzard (May 27 2018 at 16:29):

I'll make it a pnat, sure

Andrew Ashworth (May 27 2018 at 16:29):

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

Mario Carneiro (May 27 2018 at 16:29):

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

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

Mario Carneiro (May 27 2018 at 16:29):

OF COURSE

Kevin Buzzard (May 27 2018 at 16:29):

But I think that if the coercion did that

Kevin Buzzard (May 27 2018 at 16:29):

then I think it would force people to write better code

Kevin Buzzard (May 27 2018 at 16:30):

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

Mario Carneiro (May 27 2018 at 16:30):

coercions don't have that luxury

Kevin Buzzard (May 27 2018 at 16:30):

oh really

Kenny Lau (May 27 2018 at 16:30):

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

Mario Carneiro (May 27 2018 at 16:30):

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

Kenny Lau (May 27 2018 at 16:30):

Python style

Kenny Lau (May 27 2018 at 16:30):

we should have errors in Lean

Mario Carneiro (May 27 2018 at 16:30):

That's called monadic programming

Mario Carneiro (May 27 2018 at 16:31):

mathematicians don't want to deal with that

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

Mario Carneiro (May 27 2018 at 16:31):

sure

Kevin Buzzard (May 27 2018 at 16:31):

because then none of the junk theorems would work

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

Kevin Buzzard (May 27 2018 at 16:31):

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

Mario Carneiro (May 27 2018 at 16:32):

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

Kevin Buzzard (May 27 2018 at 16:32):

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

Mario Carneiro (May 27 2018 at 16:32):

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

Kevin Buzzard (May 27 2018 at 16:32):

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

Mario Carneiro (May 27 2018 at 16:32):

There are options available, pick your favorite

Kevin Buzzard (May 27 2018 at 16:32):

I think that 0 is the worst option

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

Kevin Buzzard (May 27 2018 at 16:33):

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

Mario Carneiro (May 27 2018 at 16:33):

Don't worry, they will notice

Mario Carneiro (May 27 2018 at 16:33):

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

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

Mario Carneiro (May 27 2018 at 16:34):

then your theorem fails

Kevin Buzzard (May 27 2018 at 16:34):

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

Kevin Buzzard (May 27 2018 at 16:34):

that's the point

Kevin Buzzard (May 27 2018 at 16:34):

it fails earlier

Mario Carneiro (May 27 2018 at 16:34):

and you come here and ask about it

Kevin Buzzard (May 27 2018 at 16:34):

which is a good thing

Kevin Buzzard (May 27 2018 at 16:34):

not me asking :-)

Kevin Buzzard (May 27 2018 at 16:34):

the failure

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

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!"

Kenny Lau (May 27 2018 at 16:35):

lol 37

Mario Carneiro (May 27 2018 at 16:35):

Obviously removing the coercion solves all these problems

Kenny Lau (May 27 2018 at 16:35):

as if x<0 is decidable

Kevin Buzzard (May 27 2018 at 16:35):

It _has_ to be 37

Kenny Lau (May 27 2018 at 16:35):

they won't ever give 37 to you

Kenny Lau (May 27 2018 at 16:35):

x<0 is not decidable

Mario Carneiro (May 27 2018 at 16:35):

yes it is, it's false

Kevin Buzzard (May 27 2018 at 16:35):

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

Kevin Buzzard (May 27 2018 at 16:36):

I had to prove it was inhabited

Kevin Buzzard (May 27 2018 at 16:36):

but I changed it before I made the PR

Kevin Buzzard (May 27 2018 at 16:36):

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

Mario Carneiro (May 27 2018 at 16:37):

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

Mario Carneiro (May 27 2018 at 16:38):

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

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

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...)

Johan Commelin (May 27 2018 at 17:54):

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

Kenny Lau (May 27 2018 at 23:14):

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

Kenny Lau (May 27 2018 at 23:14):

@Kevin Buzzard congratulations, it has been removed

Kevin Buzzard (May 28 2018 at 04:19):

Maybe one day it will come back with super powers

Last updated: Dec 20 2023 at 11:08 UTC