LIVE CHAT: Structures for mathematicians

Stream: maths

[Kevin Buzzard]

At 8pm UK time (2000 BST, so 1900 GMT) I am going to a live Lean explanation, in this thread, of a very simple mathlib file which defines a (non-inductive) structure. Mathematicians need to learn how to make structures, it's something we do very differently in mathematics. Here we need a far more formal kind of interface. I will hopefully do a few of these. It's like "talking people through mathlib files".

[Kenny Lau]

youtube live?

[Johan Commelin]

No, it seems "Zulip live"

[Kevin Buzzard]

Johan, I was inspired to do it after looking at the structure you constructed, which reminded me of the terrible first structure I constructed.

[Kevin Buzzard]

Hello, this is just me talking through pnat.lean

[Kevin Buzzard]

It should be easy

[Kevin Buzzard]

and maybe people will find it later.

[Kevin Buzzard]

Ok so mathematicians use a lot of structures, and one structure I was brought up on is "the UK mathematician's nat", namely {1,2,3,...}

[Kevin Buzzard]

Ok so how do we define the UK mathematician's nat?

[Kevin Buzzard]

Well pretty clearly we could define it like the computer scientist's nat := {0,1,2,3,...}

[Kevin Buzzard]

we could just make a structure

[Kevin Buzzard]

hmm

[Kevin Buzzard]

let me fire up lean

[Kevin Buzzard]

that's better

[Kevin Buzzard]

I am so rubbish at structures

[Kevin Buzzard]

aah bingo

[Kevin Buzzard]

it's not a structure

[Kevin Buzzard]

it's an inductive type

[Kevin Buzzard]

inductive pnat
| one : pnat
| succ : pnat → pnat

[Kevin Buzzard]

So there's pnat

[Kevin Buzzard]

and that would work

[Kevin Buzzard]

and we could define addition and multiplication and prove addition is commutative

[Kevin Buzzard]

and do all that stuff again

[Kevin Buzzard]

and that's stuff we already did with nat

[Kevin Buzzard]

and that's kind of a waste

[Kevin Buzzard]

it would be nice to inherit all those theorems about nat and get them to pnat immediately

[Kevin Buzzard]

so let's take a look at what they did in Lean or mathlib, wherever they defined pnat

[Kevin Buzzard]

Ok so it's in mathlib

[Kevin Buzzard]

which means that computer scientists are not interested in this structure

[Kevin Buzzard]

You can get to it with "import data.pnat"

[Kevin Buzzard]

let's find it on github

[Kevin Buzzard]

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

[Kevin Buzzard]

There it is.

[Kevin Buzzard]

Last modified two days ago!

[Kevin Buzzard]

Things never stand still around here

[Kevin Buzzard]

OK so I'm going to talk through this file, or at least what I understand of this file, which is pretty much all of it I hope

[Kevin Buzzard]

and the first thing we notice

[Kevin Buzzard]

is that on line 1

[Kevin Buzzard]

they don't define it using an inductive structure like nat

[Kevin Buzzard]

they define it as a _subtype_

[Kevin Buzzard]

which is a bit more annoying to use in practice

[Kevin Buzzard]

oh wait I skipped a line

[Kevin Buzzard]

import tactic.basic

[Kevin Buzzard]

let's come back to that line when I have figured out why it's there

[Kevin Buzzard]

def pnat := {n : ℕ // n > 0}

[Kevin Buzzard]

And there it is.

[Kevin Buzzard]

There are sets {x | blah}

[Kevin Buzzard]

and there are subtypes {x // blah}

[Kevin Buzzard]

this one is a subtype

[Kevin Buzzard]

don't mind me I'm just editing mathlib

[Kevin Buzzard]

Ok so I was trying to work out what a subtype was

[Kevin Buzzard]

but I know the answer

[Kevin Buzzard]

to make a pnat you have to give two pieces of data

[Kevin Buzzard]

1) a nat

[Kevin Buzzard]

2) a proof that it's positive

[Kevin Buzzard]

(that's > 0 for you French speakers)

[Kevin Buzzard]

so here's an example

[Kevin Buzzard]

definition x : pnat := ⟨59,oh crap⟩

[Kevin Buzzard]

that didn't go well

[Kevin Buzzard]

I was in the middle of defining 59

[Kevin Buzzard]

and all of a sudden I needed a proof.

[Kevin Buzzard]

OK so let's try again but this time be prepared

[Kevin Buzzard]

theorem H : 59 > 0 := sorry
definition x : pnat := ⟨59,H⟩

[Kevin Buzzard]

Ok that went better

[Kevin Buzzard]

I cheated with my proof that 59 > 0 by saying the proof was sorry (which means "just assume it")

[Kevin Buzzard]

and now I can finally make my pnat

[Kevin Buzzard]

This is going to be pretty inconvenient having to prove that things are positive

[Kevin Buzzard]

but actually in a couple of lines we're going to see a really good way of doing it

[Kevin Buzzard]

notation `ℕ+` := pnat

instance coe_pnat_nat : has_coe ℕ+ ℕ := ⟨subtype.val⟩

[Kevin Buzzard]

Those are the next couple of lines

[Kevin Buzzard]

The first one is easy: it sets up notation, and we're going to use the completely non-standard notation ℕ+ for pnat

[Kevin Buzzard]

as opposed to a little plus or a little star or whatever the French use, maybe some sub zero or super zero

[Kevin Buzzard]

this sort of thing is a minefield

[Kevin Buzzard]

ℕ+ will do

[Kevin Buzzard]

and now this incomprehensible coe line is where we start making the interface for our structure

[Patrick Massot]

ℕ^*

[Kevin Buzzard]

because we are already finished with the structure

[Kevin Buzzard]

Submit a PR Patrick

[Kevin Buzzard]

The thing that mathematicians don't realise

[Kevin Buzzard]

or at least that I didn't realise at all

[Kevin Buzzard]

(I suspect Patrick knew full well)

[Kevin Buzzard]

was that it's not just about making the structure

[Kevin Buzzard]

the next thing you have to do is to say to yourself

[Kevin Buzzard]

"what is every single basic thing that my users might want to do with this structure?"

[Kevin Buzzard]

And the first basic thing is that given a positive natural, a mathematician might also want to think of it as a natural.

[Kevin Buzzard]

And in fact it's such a natural (no pun intended) to move from pnat to nat

[Kevin Buzzard]

that not only did they design a function for it

[Kevin Buzzard]

but they made it into a coercion

[Kevin Buzzard]

which means "it happens magically"

[Kevin Buzzard]

Aah I see what to do

[Kevin Buzzard]

I have mathlib pnat open

[Kevin Buzzard]

and a copy of it

[Kevin Buzzard]

and I edit the copy

[Kevin Buzzard]

great

[Kevin Buzzard]

so let's see if we can understand this coercion

[Kevin Buzzard]

and then let's see it happen

[Kevin Buzzard]

instance coe_pnat_nat : has_coe ℕ+ ℕ := ⟨subtype.val⟩

[Kevin Buzzard]

instances are something I never understood

[Kevin Buzzard]

coercions not really either

[Kevin Buzzard]

and then those dreaded pointy brackets

[Kevin Buzzard]

and then an incomprehensible subtype.val

[Kevin Buzzard]

That's what I thought of that line in about January.

[Kevin Buzzard]

But as Kenny once told me, Lean does not do magic

[Kevin Buzzard]

so we can work out what this line does

[Kevin Buzzard]

and I work it out by having this pnat file open in Lean and just right clicking on subtype.val

[Kevin Buzzard]

and then selecting "go to definition"

[Kevin Buzzard]

and then we find ourselves right in the heart of core lean

[Kevin Buzzard]

and we see

[Kevin Buzzard]

structure subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

[Kevin Buzzard]

and pnat, the positive naturals, was a subtype

[Kevin Buzzard]

in fact if we switch notation off and look at pnat

[Kevin Buzzard]

def pnat := {n : ℕ // n > 0}

set_option pp.notation false
#print pnat

[Kevin Buzzard]

we see

[Kevin Buzzard]

def pnat : Type := subtype (λ (n : nat), gt n 0)

[Kevin Buzzard]

eew

[Kevin Buzzard]

gt is >

[Kevin Buzzard]

so indeed we see a function nat to Prop

[Kevin Buzzard]

sending n to "n > 0"

[Kevin Buzzard]

and we get a subtype, consisting of the n such that we have a proof that n > 0

[Kevin Buzzard]

and we see from the definition of the subtype structure that the n is the val and the proof is the property

[Kevin Buzzard]

so subtype.val sends the pnat ⟨59,H⟩

[Kevin Buzzard]

to its value

[Kevin Buzzard]

which is 59

[Kevin Buzzard]

and we made it a coercion using coercion instance magic

[Kevin Buzzard]

so that means it should happen naturally

[Kevin Buzzard]

Ok it works!

[Kevin Buzzard]

theorem H : 59 > 0 := sorry
definition x : pnat := ⟨59,H⟩
#check (x : pnat) -- x : pnat
#check (x : ℕ)

[Kevin Buzzard]

it would be better if you could see me typing

[Kevin Buzzard]

that would save me having to cut and paste

[Kevin Buzzard]

how do I do that?

[Kevin Buzzard]

Did someone say youtube ?

[Kevin Buzzard]

Does twitch take this sort of stuff?

[Kevin Buzzard]

I have done all manner of weird things on twitch

[Patrick Massot]

Yes, I don't understand why you don't record that and put it on youtube

[Kevin Buzzard]

because I'm just squeezing this in before I put the kids to bed

[Kevin Buzzard]

so back to the point

[Kevin Buzzard]

a miracle occurred!

[Kevin Buzzard]

A contradiction in type theory!

[Kevin Buzzard]

x had type pnat

[Kevin Buzzard]

and type nat

[Kevin Buzzard]

as well

[Kevin Buzzard]

but actually what happened was that coercion kicked in

[Kevin Buzzard]

The output of the second check was ↑x : ℕ

[Kevin Buzzard]

and that arrow (which you get with \u)

[Kevin Buzzard]

means "I got coerced!"

[Kevin Buzzard]

so that has solved our first fundamental problem

[Kevin Buzzard]

which is that for a mathematician, pnat is a subset of nat

[Kevin Buzzard]

and hence every pnat _is_ a nat

[Kevin Buzzard]

They don't have it so easy in DTT

[Kevin Buzzard]

so we are stuck with the cute little arrows

[Kevin Buzzard]

let's press on

[Kevin Buzzard]

The next line is clever

[Kevin Buzzard]

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

[Kevin Buzzard]

That's using a really cool piece of Lean functionality

[Kevin Buzzard]

...which breaks if I remove that import line

[Kevin Buzzard]

so that's why the import is there

[Kevin Buzzard]

This is pretty much the rarest of ways to make a function input for Lean

[Patrick Massot]

you could still hide the cute little arrows from pp display though

[Kevin Buzzard]

there's something in the manual about this

[Kevin Buzzard]

you can do pp.no_cute_arrows Patrick?

[Kevin Buzzard]

here we are

[Kevin Buzzard]

https://leanprover.github.io/reference/expressions.html#implicit-arguments

[Patrick Massot]

set_option pp.coercions false

[Kevin Buzzard]

does that mean Lean doesn't do them?

[Kevin Buzzard]

or just doesn't print the arrows?

[Patrick Massot]

doesn't print

[Kevin Buzzard]

thought so :-)

[Patrick Massot]

hence the pp

[Johan Commelin]

pp means "pretty print"

[Patrick Massot]

meaning pretty print

[Kevin Buzzard]

presumably no setting of options can change Lean's behaviour?

[Kevin Buzzard]

in pnat we have the last of the ways that Lean can make an implicit argument

[Patrick Massot]

class.instance_max_depth

[Kevin Buzzard]

"run a tactic to make the argument for you"

[Kevin Buzzard]

Patrick: touch\'e

[Kevin Buzzard]

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

[Kevin Buzzard]

means "take an input n, and then see if you can prove n > 0 by using the tactic tactic.exact_dec_trivial"

[Kevin Buzzard]

Let's see this tactic in action

[Kevin Buzzard]

theorem H : 59 > 0 := by tactic.exact_dec_trivial

[Kevin Buzzard]

It works!

[Kevin Buzzard]

To find out what it does you can right click on it and it will be all tacticy stuff

[Kevin Buzzard]

so I'm not going to do that

[Kevin Buzzard]

but I know what is going on

[Kevin Buzzard]

in fact there's a shorter way of doing it

[Kevin Buzzard]

theorem H : 59 > 0 := dec_trivial

[Kevin Buzzard]

(not a tactic, so no by this time)

[Kevin Buzzard]

dec_trivial just means "> is decidable on nat so just please decide this for me by proving it's true"

[Kevin Buzzard]

apparently you can't use it to prove things are false though

[Kevin Buzzard]

theorem H1 : 0 > 0 := dec_trivial

[Kevin Buzzard]

doesn't work

[Kevin Buzzard]

so let's see to_pnat in action!

[Kevin Buzzard]

definition y : pnat := to_pnat 12

[Kevin Buzzard]

that's much better than what we had before

[Kevin Buzzard]

definition z : pnat := to_pnat 0

[Kevin Buzzard]

you get some weird error

[Kevin Buzzard]

OK so let's press on

[Kevin Buzzard]

def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩

[Kevin Buzzard]

this one looks easy.

[Kevin Buzzard]

Given n a nat, we are building a pnat called succ_pnat n

[Kevin Buzzard]

and you can guess from the name that it will be n + 1

[Kevin Buzzard]

so I reckon that succ_pos n is going to be the theorem that n + 1 > 0

[Kevin Buzzard]

we can check that easily

[Mario Carneiro]

Obviously you can't prove false things using dec_trivial, they're false

[Mario Carneiro]

but you can prove the negation using dec_trivial

[Kevin Buzzard]

variable (n : ℕ)
#check succ_pos n

[Kevin Buzzard]

succ_pos n : 0 < succ n

[Kevin Buzzard]

we could have right clicked and wandered back in to core lean or so, but this is another way

[Kevin Buzzard]

So that's two maps from nat to pnat and a map from pnat to nat

[Kevin Buzzard]

It's certainly the case that we could imagine using both those maps

[Kevin Buzzard]

but what do we need to do next?

[Kevin Buzzard]

This is the question that I as a mathematician find hard

[Kevin Buzzard]

and I think that people like Mario just somehow know

[Kevin Buzzard]

I'm just going to cheat and look at the code

[Kevin Buzzard]

@[simp] theorem succ_pnat_coe (n : ℕ) : (succ_pnat n : ℕ) = succ n := rfl

[Kevin Buzzard]

OK so this says that given a nat, if we compute its successor as a pnat then it equals its successor as a nat

[Kevin Buzzard]

Notice the secret coercion! That equality is between a pnat and a nat

[Kevin Buzzard]

and Lean coerces the left hand side

[Kevin Buzzard]

so if you think about it

[Kevin Buzzard]

when you unravel it

[Kevin Buzzard]

that theorem just says succ n = succ n

[Kevin Buzzard]

so the proof is rfl

[Kevin Buzzard]

Ok now @Mario Carneiro told me that theorems whose proofs were rfl sometimes don't get names

[Kevin Buzzard]

but this one got lucky

[Kevin Buzzard]

it got a name

[Mario Carneiro]

it's a simp lemma, those need names

[Kevin Buzzard]

and presumably that's because someone somewhere realised that this was a good simp lemma

[Kevin Buzzard]

NOTE FOR BEGINNERS

[Mario Carneiro]

also I'm not sure that's a good rule of thumb

[Mario Carneiro]

rfl proofs are very common

[Kevin Buzzard]

It's important that you get your simp lemma the right way round

[Kevin Buzzard]

you don't want to prove that succ n equals succ_pnat n

[Kevin Buzzard]

because that would be a comp lemma

[Kevin Buzzard]

in maths it doesn't matter which order you put the things that are equal

[Kevin Buzzard]

x = y and y = x mean the same thing

[Kevin Buzzard]

but in Lean you might want to consider putting the more complicated thing on the left

[Kevin Buzzard]

and then simp will simplify it to the right if it uses your lemma

[Kevin Buzzard]

and even if simp does not use your lemma

[Kevin Buzzard]

imagine when you're doing a rewrite

[Kevin Buzzard]

you are trying to prove something

[Kevin Buzzard]

so you're usally trying to make stuff easier

[Kevin Buzzard]

and you don't want to have to put left arrows everywhere because they look weird

[Kevin Buzzard]

so, mathematicians everywhere, remember that THIS WEIRD CS WORLD IS ASYMMETRIC

[Kevin Buzzard]

and if you've proved x = y, make sure x takes more characters to type

[Kevin Buzzard]

or else you should have proved y = x

[Kevin Buzzard]

Next line

[Kevin Buzzard]

@[simp] theorem pos (n : ℕ+) : (n : ℕ) > 0 := n.2

[Kevin Buzzard]

that looks like really poor Lean to me

[Kevin Buzzard]

who wrote this file anyway

[Kevin Buzzard]

oh I heard of that guy

[Kevin Buzzard]

Now everyone knows that simp is used to prove _equalities_

[Kevin Buzzard]

so all your simp lemmas should be _equalities_

[Kevin Buzzard]

or _iff_s

[Kevin Buzzard]

and anything which is a random thing like >

[Kevin Buzzard]

obviously should not be a simp lemma

[Kevin Buzzard]

because simp, it turns out, does not stand for "this lemma is pretty simple"

[Mario Carneiro]

This is useful for fulfulling side conditions in algebraic rules, which sometimes need that things are nonzero or positive

[Kevin Buzzard]

it stands for "this lemma is appropriate for the simplifier"

[Kevin Buzzard]

and 9 times out of 10 it's because it's an equality

[Patrick Massot]

I disagree our equality is symmetric. Would you write some cohomological vanishing theorem as $0 = H^i(X, F)$?

[Kevin Buzzard]

but apparently there are other times when it's not

[Kevin Buzzard]

Interesting point Patrick I guess you're right

[Kevin Buzzard]

Maybe 0 is a special case

[Kevin Buzzard]

The conclusion of this is that working out if something is a simp lemma is still something which I haven't got the hang of

[Mario Carneiro]

most "let x = value" type statements have the variable on the left in math

[Patrick Massot]

What about $$\int_{-\infty}^\infty e^{-x^2} dx = \srqt\pi$$?

[Kevin Buzzard]

Now look at these

[Kevin Buzzard]

namespace pnat

open nat
@[simp] theorem pos (n : ℕ+) : (n : ℕ) > 0 := n.2

theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq

@[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl

instance : has_add ℕ+ := ⟨λ m n, ⟨m + n, add_pos m.2 n.2⟩⟩

@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl

@[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := ne_of_gt n.2

[Kevin Buzzard]

The last thing we want to do is to define random theorems like ne_zero (the last one) and have its actual name be ne_zero in the root namespace

[Kevin Buzzard]

I did that a lot when I started

[Kevin Buzzard]

The statement that if n is a pnat then n isn't zero -- clearly ne_zero is a good name for it

[Kevin Buzzard]

but its full name is pnat.ne_zero

[Kevin Buzzard]

like all the other pnat things we're going to do now

[Johan Commelin]

So, why is theorem eq not a simp theorem?

[Kevin Buzzard]

so that's why we opened the pnat namespace

[Kevin Buzzard]

we namespaced

[Kevin Buzzard]

and we opened nat for good measure

[Mario Carneiro]

because the RHS has a variable not on the LHS

[Kevin Buzzard]

So theorem eq says a fundamental thing about subtypes.

[Kevin Buzzard]

Remember -- a subtype is a term and then a proof of something that depends only on the term

[Kevin Buzzard]

so if we have two subtype things with the same term and different proofs, are they the same?

[Patrick Massot]

What RHS variable?

[Kevin Buzzard]

And yes they are, because all proofs are the same

[Kevin Buzzard]

so that's why pnat.eq is true

[Kevin Buzzard]

and indeed the proof is subtype.eq and you can guess what that says

[Kevin Buzzard]

or right click on ir

[Kevin Buzzard]

it

[Kevin Buzzard]

or #check it

[Kevin Buzzard]

Oh I know why eq isn't a simp lemma

[Kevin Buzzard]

it's not an equality

[Mario Carneiro]

m = n is not a simplification

[Kevin Buzzard]

it's an implication

[Mario Carneiro]

and where is n coming from?

[Kevin Buzzard]

aah

[Mario Carneiro]

that's what I mean, n doesn't show up on the LHS

[Kevin Buzzard]

There's another simp rule of thumb

[Kevin Buzzard]

all the variables on the RHS should be in the LHS too

[Johan Commelin]

Whenever I have to subtype thingies in my goal, and I need to prove that they are equal, Lean should always apply subtype.eq. I can't think of any reason why you wouldn't want to do that.

[Patrick Massot]

why this rule?

[Kevin Buzzard]

I should mention that to the guy who wrote the simp docs

[Mario Carneiro]

It's an extensionality theorem

[Mario Carneiro]

you don't always want it applied, because it complicates the goal

[Patrick Massot]

should it be tagged as such?

[Mario Carneiro]

probably

[Kevin Buzzard]

More generally Johan, if you have two structures that are equal, you might want Lean to just decompose them and demand that you prove that all the bits you used to make them are equal

[Kevin Buzzard]

but I think it would be a bit confusing if you were just motoring along and all of a sudden you have 10 goals

[Johan Commelin]

you don't always want it applied, because it complicates the goal

Huh, the goal becomes easier, right? I just got rid of some irrelevant proofs...

[Kevin Buzzard]

because you wanted to prove complicated structures were equal

[Kevin Buzzard]

I think this sort of thing is an art

[Kevin Buzzard]

I'm not sure what the best answer is but clearly Mario will speak from experience

[Mario Carneiro]

you were trying to prove m = n, now you are proving \u m = \u n

[Mario Carneiro]

the goal got more complicated

[Mario Carneiro]

sometimes that's what you want, but it needs to be an explicit choice

[Kevin Buzzard]

Aah -- Johan -- if you actually had variables m and n which were pnats

[Kevin Buzzard]

then you might well not want it

[Kevin Buzzard]

but if m was explicitly <nat,proof>

[Kevin Buzzard]

and so was n

[Kevin Buzzard]

then you might want it

[Kevin Buzzard]

(but you might not)

[Johan Commelin]

Hmm, fair enough

[Mario Carneiro]

and that version is a simp lemma

[Kevin Buzzard]

ooh my son's gone

[Kevin Buzzard]

I just inherited a second screen

[Johan Commelin]

Ok, I have met subtypes where it was not a simp lemma, I think

[Kevin Buzzard]

Ok so mk_coe

[Johan Commelin]

Or is it a simp lemma for general subtypes?

[Kevin Buzzard]

that says "make the subtype and then coerce back to nat and you're back where you started"

[Johan Commelin]

Hmm, yes, let's move on with this chat

[Mario Carneiro]

subtype.mk_eq_mk

[Kevin Buzzard]

@[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl

[Mario Carneiro]

it's a general simp lemma

[Kevin Buzzard]

Actually there are several cool things about mk_coe

[Kevin Buzzard]

first, it's something which I wanted for my structure and Mario said it didn't have a name

[Kevin Buzzard]

hmm

[Kevin Buzzard]

maybe that's not entirely true

[Kevin Buzzard]

Mario -- why does this lemma use coercion instead of val?

[Kevin Buzzard]

They're definitionally equal, right?

[Kevin Buzzard]

Does it matter which one you choose when making your structure?

[Mario Carneiro]

it's a simp lemma

[Kevin Buzzard]

But what about (⟨n, h⟩ : ℕ+).val = n

[Mario Carneiro]

The val version is automatic, because simp knows about structures

[Kevin Buzzard]

or subtype.val (⟨n, h⟩ : ℕ+) = n

[Mario Carneiro]

but when the val is hidden in a coercion simp misses it

[Kevin Buzzard]

oh so simp doesn't need to be told that

[Kevin Buzzard]

the thing I wrote

[Kevin Buzzard]

but does need to be told the thing you put in the file

[Mario Carneiro]

right

[Kevin Buzzard]

You see -- there is so much subtlety in this stuff

[Kevin Buzzard]

I saw the definition of pnat in a maths lecture

[Mario Carneiro]

I mean you could have it as a simp lemma if you want

[Kevin Buzzard]

it was "take nat and remove 0"

[Kevin Buzzard]

and that was it

[Mario Carneiro]

but it probably won't trigger

[Kevin Buzzard]

There is all this extra stuff here

[Kevin Buzzard]

instance : has_add ℕ+ := ⟨λ m n, ⟨m + n, add_pos m.2 n.2⟩⟩

@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl

[Kevin Buzzard]

We want add on pnat

[Kevin Buzzard]

and here's something I only learnt recently

[Kevin Buzzard]

the only purpose of has_add and the 20 or so other has_notation things

[Kevin Buzzard]

is notation

[Kevin Buzzard]

The instance is so unimportant that it doesn't even deserve a name

[Kevin Buzzard]

although probably one could have called it pnat.add

[Mario Carneiro]

it gets an automatic name if you don't specify, in this case pnat.has_add

[Kevin Buzzard]

The definition of add on pnat clearly needs a theorem -- it needs the theorem that if a>0 and b>0 then a+b>0

[Kevin Buzzard]

Oh I didn't know that -- thanks

[Mario Carneiro]

pnat.add would be the name of the function itself

[Mario Carneiro]

if it had a name

[Kevin Buzzard]

Oh of course

[Kevin Buzzard]

The function is add

[Kevin Buzzard]

and the proof that it has an add is something else

[Kevin Buzzard]

actually it's not a proof

[Kevin Buzzard]

it's data

[Kevin Buzzard]

OK so we need to proev that if a>0 and b>0 then a+b>0

[Kevin Buzzard]

and we cheat and look at what Mario did

[Kevin Buzzard]

and why is the output from #check so ugly?

[Kevin Buzzard]

#check add_pos

[Kevin Buzzard]

add_pos : 0 < ?M_3 → 0 < ?M_4 → 0 < ?M_3 + ?M_4

[Kevin Buzzard]

thanks Lean

[Kevin Buzzard]

#check @add_pos

[Kevin Buzzard]

add_pos : ∀ {α : Type u_1} [_inst_1 : ordered_cancel_comm_monoid α] {a b : α}, 0 < a → 0 < b → 0 < a + b

[Kevin Buzzard]

not ideal either

[Kevin Buzzard]

I would have preferred

[Kevin Buzzard]

0 < a → 0 < b → 0 < a + b

[Kevin Buzzard]

but unsurprisingly

[Kevin Buzzard]

it's the lemma we need

[Kevin Buzzard]

Now these should be straightforward

[Kevin Buzzard]

@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl

@[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := ne_of_gt n.2

@[simp] theorem nat_coe_coe  {n : ℕ} : n > 0 → ((n : ℕ+) : ℕ) = n := succ_pred_eq_of_pos
@[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos

@[simp] theorem coe_nat_coe (n : ℕ+) : ((n : ℕ) : ℕ+) = n := eq (nat_coe_coe n.pos)

[Kevin Buzzard]

you see -- this is the advantage of making it a subtype

[Kevin Buzzard]

we have to carry around all these proofs

[Kevin Buzzard]

but add_coe says "adding the pnats is the same as adding the nats, by definition"

[Kevin Buzzard]

and indeed if you look at the coercion you can see that this is just a statement of the form X = X

[Kevin Buzzard]

ne_zero : we will need to prove n > 0 -> n ne 0

[Kevin Buzzard]

and it would not surprise me if that were called ne_of_gt

[Kevin Buzzard]

and note that

[Kevin Buzzard]

n.2 is the proof

[Kevin Buzzard]

that n > 0

[Kevin Buzzard]

it's n.property

[Kevin Buzzard]

for kids who are too cool to write such a long thing

[Kevin Buzzard]

nat_coe_coe

[Kevin Buzzard]

I have no idea why this is a simp lemma

[Kevin Buzzard]

I guess I do know

[Kevin Buzzard]

it's kind of "well there's only a minor precondition"

[Kevin Buzzard]

"and then we get some serious simplification"

[Kevin Buzzard]

I am kind of surprised this works

[Kevin Buzzard]

we coerce a nat to a pnat

[Kevin Buzzard]

that doesn't even make sense

[Kevin Buzzard]

oh crap

[Kevin Buzzard]

I am looking at an old version of pnat

[Kevin Buzzard]

rofl

[Kevin Buzzard]

I'm now looking at the up to date version

[Kevin Buzzard]

and that line is gone :-)

[Kevin Buzzard]

@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl

@[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := ne_of_gt n.2

@[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos

@[simp] theorem coe_to_pnat' (n : ℕ+) : (n : ℕ).to_pnat' = n := eq (to_pnat'_coe n.pos)

[Mario Carneiro]

Last modified two days ago!
Things never stand still around here

[Kevin Buzzard]

Things stand still with my mathlib install I can assure you :-)

[Kevin Buzzard]

Ok great

[Kevin Buzzard]

@[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos

[Kevin Buzzard]

that starts with a nat, uses to_pnat' to get to a pnat and then coerces back to a nat and the claim is we're back where we started

[Kevin Buzzard]

def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)

[Kevin Buzzard]

Ok so this looks good

[Kevin Buzzard]

if you unravel then we're claiming that succ (pred n) = n

[Kevin Buzzard]

and this is not rfl

[Kevin Buzzard]

indeed it's not even true

[Kevin Buzzard]

it's false for n=0

[Kevin Buzzard]

but we have the hypo n > 0

[Kevin Buzzard]

so we need a lemma that says n > 0 implies succ pred n = n

[Kevin Buzzard]

and that would be called something like succ_pred_eq_of_pos

[Kevin Buzzard]

which it indeed is

[Kevin Buzzard]

Ok nearly there

[Kevin Buzzard]

oh one more simp lemma

[Kevin Buzzard]

you see this is exactly what I don't get

[Kevin Buzzard]

who decides (a) what to prove (b) what to make a simp lemma

[Kevin Buzzard]

We have just proved 10 trivial things

[Kevin Buzzard]

@[simp] theorem coe_to_pnat' (n : ℕ+) : (n : ℕ).to_pnat' = n := eq (to_pnat'_coe n.pos)

[Mario Carneiro]

This is a very basic file, so it has almost nothing but simp lemmas

[Kevin Buzzard]

look!

[Kevin Buzzard]

We just proved n = n again

[Kevin Buzzard]

let's make it a simp lemma!

[Kevin Buzzard]

to_pnat' is a bit funny isn't it

[Kevin Buzzard]

def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)

[Kevin Buzzard]

sends n to n if n is positive

[Kevin Buzzard]

and 0 to 1

[Kevin Buzzard]

because nobody listens to me when I say it should be 37

[Mario Carneiro]

hey, the succ pred thing wouldn't work with 37

[Kevin Buzzard]

and perhaps in this particular case they're right

[Kevin Buzzard]

Ok so we basically think of every possible way we can move between nats and pnats and then figure out what is true and make every simplification a simp lemma

[Mario Carneiro]

exactly

[Kevin Buzzard]

Now here's a meaty bit of file

[Kevin Buzzard]

instance : comm_monoid ℕ+ :=
{ mul       := λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩,
  mul_assoc := λ a b c, subtype.eq (mul_assoc _ _ _),
  one       := succ_pnat 0,
  one_mul   := λ a, subtype.eq (one_mul _),
  mul_one   := λ a, subtype.eq (mul_one _),
  mul_comm  := λ a b, subtype.eq (mul_comm _ _) }

[Kevin Buzzard]

it's a commutative monoid!

[Kevin Buzzard]

You can see what Lean thinks the axioms for a commutative monoid are, right there

[Kevin Buzzard]

Now if I had been doing this I would have done instance : has_mul pnat := <...> first

[Kevin Buzzard]

outside the monoid

[Kevin Buzzard]

and I would have done has_one pnat

[Kevin Buzzard]

Mario -- does your pnat have a mul?

[Mario Carneiro]

yes, it's right there

[Mario Carneiro]

comm_monoid implies has_mul

[Kevin Buzzard]

If I type #print comm_monoid

[Kevin Buzzard]

I can't see this

[Kevin Buzzard]

Do I have to look at the source code to see that comm_monoid extends has_mul?

[Kevin Buzzard]

Or have I misunderstood?

[Mario Carneiro]

comm_monoid extends monoid which extends semigroup which extends has_mul

[Kevin Buzzard]

class comm_monoid (α : Type u) extends monoid α, comm_semigroup α

[Kevin Buzzard]

but you had to know that

[Kevin Buzzard]

I could have written comm_monoid in a different way

[Kevin Buzzard]

and it would have _looked_ like there was a mul

[Kevin Buzzard]

but you wouldn't have got the notation

[Kevin Buzzard]

so I have to look in the source code to check my mul is a mul?

[Mario Carneiro]

set_option pp.implicit true
#check (by apply_instance : has_mul ℕ+)
-- @semigroup.to_has_mul ℕ+ (@monoid.to_semigroup ℕ+ (@comm_monoid.to_monoid ℕ+ pnat.comm_monoid)) : has_mul ℕ+

[Kevin Buzzard]

The technical point here, for those wondering, is how I can get Lean to use the notation * for multiplication of pnats

[Mario Carneiro]

you already have the notation

[Mario Carneiro]

after that instance

[Kevin Buzzard]

after making it a commutative monoid

[Kevin Buzzard]

but you didn't know for sure that was going to happen

[Mario Carneiro]

proving it's a comm monoid a fortiori implies it's a monoid and a has_mul and all that

[Kevin Buzzard]

you could only work it out by doing it and then checking that the multiplication notation stuck

[Kevin Buzzard]

with your #check

[Kevin Buzzard]

if you had wanted to know before writing the code

[Kevin Buzzard]

you would have had to read Lean source code

[Mario Carneiro]

If you define something with a mul := field it's in all likelihood extending has_mul

[Kevin Buzzard]

you can't just work it out by querying the system

[Kevin Buzzard]

exactly

[Kevin Buzzard]

You had to rely on someone else being sensible

[Kevin Buzzard]

instance : comm_monoid ℕ+ :=
{ mul       := λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩,
  mul_assoc := λ a b c, subtype.eq (mul_assoc _ _ _),
  one       := succ_pnat 0,
  one_mul   := λ a, subtype.eq (one_mul _),
  mul_one   := λ a, subtype.eq (mul_one _),
  mul_comm  := λ a b, subtype.eq (mul_comm _ _) }

[Mario Carneiro]

you can either read the code, the inheritance hierarchy, or get lean to tell you

[Kevin Buzzard]

But you didn't get Lean to tell you

[Mario Carneiro]

no because I knew that comm_monoid extends has_mul (and it wouldn't make sense any other way)

[Kevin Buzzard]

structure tricky1 (G : Type) :=
(mul : G → G → G)
(tricky_bit : 0 = 1)

[Mario Carneiro]

It is important that has_mul be declared only once though

[Kevin Buzzard]

structure tricky2 (G : Type) extends has_mul G :=
(tricky_bit : 0 = 1)

[Mario Carneiro]

only tricky2 gets the notation, yes

[Kevin Buzzard]

but your method for checking this fails

[Kevin Buzzard]

because you can't make any instances

[Kevin Buzzard]

#check (by apply_instance : has_mul ℕ+)

[Kenny Lau]

sorry, you can

[Kevin Buzzard]

your method relied on pnat existing

[Kevin Buzzard]

show me Kenny :-)

[Kenny Lau]

just sorry everything

[Kevin Buzzard]

Fair enough

[Kevin Buzzard]

even mul?

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

I seem to have wandered a bit

[Kevin Buzzard]

OK so what do we need for mul -- clearly we need a proof that if a > 0 and b > 0 then a * b > 0, and we think of what a good name for this lemma would be, and we think "oh maybe mul_pos_of_pos_of_pos

[Kevin Buzzard]

and then we think "wait a minute that's too long"

[Kevin Buzzard]

why don't we just go with mul_pos

[Kevin Buzzard]

and indeed that's what it is

[Kevin Buzzard]

naming is an art

[Kevin Buzzard]

and it's another thing mathematicians are bad at

[Kevin Buzzard]

The only training we get

[Kevin Buzzard]

is "Now by lemma 3.1 and 3.2 we see that Theorem A is proved!"

[Kevin Buzzard]

from our teachers

[Mario Carneiro]

class tricky1 (G : Type) :=
(mul : G → G → G)
(tricky_bit : 0 = 1)

class tricky2 (G : Type) extends has_mul G :=
(tricky_bit : 0 = 1)

section
variables (G : Type) [tricky1 G]
#check (by apply_instance : has_mul G) --fail

instance tricky1.has_mul : has_mul G := ⟨tricky1.mul⟩

#check (by apply_instance : has_mul G) --fixed
end

section
variables (G : Type) [tricky2 G]
#check (by apply_instance : has_mul G) --success
end

[Kevin Buzzard]

There you go

[Kevin Buzzard]

couldn't be easier

[Kevin Buzzard]

Now

[Kevin Buzzard]

how are we going to prove all these stupid axioms?

[Kevin Buzzard]

instance : comm_monoid ℕ+ :=
{ mul       := λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩,
  mul_assoc := λ a b c, subtype.eq (mul_assoc _ _ _),
  one       := succ_pnat 0,
  one_mul   := λ a, subtype.eq (one_mul _),
  mul_one   := λ a, subtype.eq (mul_one _),
  mul_comm  := λ a b, subtype.eq (mul_comm _ _) }

[Kevin Buzzard]

mul_assoc -- that's already proved for nats

[Kevin Buzzard]

as is mul_comm

[Kevin Buzzard]

and the full proof of mul_comm is quite long if you have defined pnat as an inductive type with one and succ

[Kevin Buzzard]

so here we see the benefits

[Kevin Buzzard]

the proof of mul_comm is "to check a * b = b * a, all we have to do is to check the underlying nats are the same, which is true because that's mul_comm for nat"

[Kevin Buzzard]

was subtype.eq a simp lemma?

[Kevin Buzzard]

oh no

[Kevin Buzzard]

of course not

[Kevin Buzzard]

it has an implies

[Kevin Buzzard]

so we can't hope to prove that with simp I guess

[Kevin Buzzard]

all the proofs are the same

[Kevin Buzzard]

on the other hand it still feels like a machine could have written those four proofs

[Kevin Buzzard]

whereas I suspect Mario wrote them

[Kevin Buzzard]

Mario, why isn't there some weird tactic which deduces a bunch of lemmas for subtypes from the corresponding lemmas for the types?

[Patrick Massot]

We still have no conclusive proof that Mario is not a machine

[Kevin Buzzard]

true

[Patrick Massot]

This situation looks like what Simon solve for pi instances

[Kevin Buzzard]

People like Simon Hudon are good at writing that sort of thing

[Patrick Massot]

Where is Simon by the way?

[Kevin Buzzard]

he's cool -- don't underestimate him

[Patrick Massot]

Haven't we lost him?

[Kevin Buzzard]

All that's left is one

[Mario Carneiro]

because the proof is so short it's not worth automating

[Mario Carneiro]

there is a balance point there

[Kevin Buzzard]

and Mario used succ_pnat, there were 5 other ways he could have done it, I am pretty sure that 1 > 0 is a named theorem, he could have used that

[Kevin Buzzard]

I don't think it matters

[Mario Carneiro]

If I had to define a hundred more like that, sure

[Kevin Buzzard]

I think every method will produce basically the same term

[Kevin Buzzard]

All that's left is this:

[Kevin Buzzard]

@[simp] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl

@[simp] theorem mul_coe (m n : ℕ+) : ((m * n : ℕ+) : ℕ) = m * n := rfl

/-- The power of a pnat and a nat is a pnat. -/
def pow (m : ℕ+) (n : ℕ) : ℕ+ :=
⟨m ^ n, nat.pos_pow_of_pos _ m.pos⟩

instance : has_pow ℕ+ ℕ := ⟨pow⟩

@[simp] theorem pow_coe (m : ℕ+) (n : ℕ) : (↑(m ^ n) : ℕ) = m ^ n := rfl

end pnat

[Kevin Buzzard]

one_coe -- who knows why this is a simp lemma

[Kevin Buzzard]

Where does it end

[Kevin Buzzard]

two_coe? Why is that not a simp lemma?

[Mario Carneiro]

because that's not an atomic term

[Kevin Buzzard]

mul_coe -- proof is refl

[Kevin Buzzard]

Oh I see

[Kevin Buzzard]

one just _became_ an atomic term

[Mario Carneiro]

the simp lemma would be about \u bit0 n = bit0 \u n

[Kevin Buzzard]

when you decided that the fact that it was a monoid was worth proving

[Kevin Buzzard]

and finally power

[Kevin Buzzard]

There's a has_pow thing instance. That presumably is tied to the ^ notation

[Kevin Buzzard]

how new-fangled and fancy

[Kevin Buzzard]

it wasn't like this when I learnt it

[Kevin Buzzard]

#print notation ^

[Kevin Buzzard]

_ ^:80 _:79 := has_pow.pow #1 #0

[Kevin Buzzard]

Ok so the definition of pow is "work out pow in nats"

[Kevin Buzzard]

but you now need to prove that if m>0 and n>=0 then m^n>0

[Kevin Buzzard]

and if this was me 6 months ago

[Kevin Buzzard]

I would think "oh I quite fancy this one"

[Kevin Buzzard]

"induction on n should do it"

[Kevin Buzzard]

and I'd prove it

[Kevin Buzzard]

but that's not the way to think about Lean

[Kevin Buzzard]

the way to think about it is

[Kevin Buzzard]

"this looks pretty standard -- m > 0 implies m^n > 0"

[Kevin Buzzard]

maybe the person who was implementing pow on nat thought of this

[Kevin Buzzard]

and even if they didn't

[Kevin Buzzard]

maybe some obsessive mathlib guy thought of it

[Kevin Buzzard]

and maybe they gave it a name

[Kevin Buzzard]

and maybe it's someething like pos_pow_of_pos

[Kevin Buzzard]

This is the way to write Lean

[Kevin Buzzard]

don't write the code because you can

[Kevin Buzzard]

try and find the code someone else wrote already that does it

[Kevin Buzzard]

write nat.pos_pow and hit ctrl-space

[Kevin Buzzard]

and see if you get lucky

[Kevin Buzzard]

note that Mario used m.pos not m.2

[Kevin Buzzard]

That might just be for readability

[Kevin Buzzard]

The philosophy is that m.2 is something Lean will always offer you

[Kevin Buzzard]

but m.pos is basically better

[Kevin Buzzard]

because it's more readable

[Kevin Buzzard]

@[simp] theorem pos (n : ℕ+) : (n : ℕ) > 0 := n.2

[Mario Carneiro]

I'm sure it's just inconsistency

[Kevin Buzzard]

But you are making an interface for pnat

[Kevin Buzzard]

and that interface should involve a nice name for the assertion that a positive nat is positive

[Mario Carneiro]

of course it doesn't matter at all what gets used in the proof

[Kevin Buzzard]

which you should encourage the users to use

[Kevin Buzzard]

It literally makes no difference to anything?

[Kevin Buzzard]

Doesn't it increase compile time by a zillisecond?

[Kevin Buzzard]

you had to look up pos in some table

[Mario Carneiro]

It's not literally the same proof term, and who knows how compile time is affected, but whatever difference is extremely minimal

[Kevin Buzzard]

Let me think epsilon more about poe

[Kevin Buzzard]

pow

[Kevin Buzzard]

What is going through the writer's mind when they write this

[Kevin Buzzard]

/-- The power of a pnat and a nat is a pnat. -/
def pow (m : ℕ+) (n : ℕ) : ℕ+ :=
⟨m ^ n, nat.pos_pow_of_pos _ m.pos⟩

[Mario Carneiro]

note that projection notation in both cases only works if n has visible type pnat

[Kevin Buzzard]

They are thinking "yay we now have pow"

[Kevin Buzzard]

but then immediately after

[Kevin Buzzard]

they think "OK I now have some obligations"

[Kevin Buzzard]

There's the obvious one -- make an instance of has_pow, which is just an elaborate way of saying "let's enable ^ notation"

[Kevin Buzzard]

but then there's the less obvious (to me) fact:

[Kevin Buzzard]

which we've seen lots of times before

[Kevin Buzzard]

we want to check that powers in pnat agree with powers in nat

[Kevin Buzzard]

and even though the proof is refl

[Kevin Buzzard]

this looks like it should be a simp lemma

[Kevin Buzzard]

It says "if we coerce m ^ n to nat we get what we expect"

[Kevin Buzzard]

That is a way of thinking which is not normally taught to the mathematician

[Kevin Buzzard]

to define pow : pnat -> nat -> nat we just use induction

[Kevin Buzzard]

to prove it lands in pnat we prove a lemma

[Kevin Buzzard]

and that's the end

[Kevin Buzzard]

We stop here:

[Kevin Buzzard]

def pow (m : ℕ+) (n : ℕ) : ℕ+ :=
⟨m ^ n, nat.pos_pow_of_pos _ m.pos⟩

instance : has_pow ℕ+ ℕ := ⟨pow⟩

[Kevin Buzzard]

We don't do this bit

[Kevin Buzzard]

@[simp] theorem pow_coe (m : ℕ+) (n : ℕ) : (↑(m ^ n) : ℕ) = m ^ n := rfl

[Kevin Buzzard]

but in CS if you don't do this

[Kevin Buzzard]

then your users moan that they used a pnat 50 lines ago and it won't disappear

[Kevin Buzzard]

even though we only care about nats now

[Kevin Buzzard]

in fact did we prove all the coercions?

[Kevin Buzzard]

@[simp] theorem mul_coe (m n : ℕ+) : ((m * n : ℕ+) : ℕ) = m * n := rfl

[Kevin Buzzard]

@[simp] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl

[Kevin Buzzard]

@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl

[Kevin Buzzard]

They all got proved

[Kevin Buzzard]

Does that mean that if I have some complicated number made using lots of pnats and addition and multiplication etc

[Kevin Buzzard]

and then I made it a nat

[Kevin Buzzard]

then simp would remove all the pnats for me?

[Kevin Buzzard]

I think it might!

[Kevin Buzzard]

variables (a b c : nat)
variables (ha : a > 0) (hb : b > 0) (hc : c > 0)

[Kevin Buzzard]

def A : pnat := ⟨a,ha⟩
def B : pnat := ⟨b,hb⟩
def C : pnat := ⟨c,hc⟩

[Kevin Buzzard]

One thing I learnt a while ago was that instead of asking "can Lean do this"

[Kevin Buzzard]

it's not hard to just make Lean try to do it yourself

[Kevin Buzzard]

you just use variables to make stuff

[Kevin Buzzard]

rofl

[Kevin Buzzard]

I need to work harder

[Kevin Buzzard]

dammit

[Kevin Buzzard]

variables {a b c : nat}
variables {ha : a > 0} {hb : b > 0} {hc : c > 0}
def A : pnat := ⟨a,ha⟩
def B : pnat := ⟨b,hb⟩
def C : pnat := ⟨c,hc⟩


example : A * (A + B) * (C + (A + B)) = a * (a + b) * (c + (a + b)) := sorry

[Kevin Buzzard]

doesn't typecheck yet

[Mario Carneiro]

Note that A and B are the same

[Mario Carneiro]

You should use parameters instead

[Kevin Buzzard]

for a b c

[Kevin Buzzard]

what about the proofs?

[Mario Carneiro]

all six

[Kevin Buzzard]

Parameters can only be used in a section

[Kevin Buzzard]

section
parameters {a b c : nat}
parameters {ha : a > 0} {hb : b > 0} {hc : c > 0}
def A : pnat := ⟨a,ha⟩
def B : pnat := ⟨b,hb⟩
def C : pnat := ⟨c,hc⟩

example : (A * (A + B) * (C + (A + B)) : ℕ) = a * (a + b) * (c + (a + b)) := sorry

end section

[Kevin Buzzard]

and this typechecks

[Kevin Buzzard]

now let's remove the sorry (which I put there for typechecky reasons)

[Kevin Buzzard]

maybe that's something I could mention

[Kevin Buzzard]

I like my lean files to have no red squiggly underlines ever

[Kevin Buzzard]

but I am happy with plenty of sorrys

[Kevin Buzzard]

green squiggly underlines ftw

[Kevin Buzzard]

the reason for this

[Kevin Buzzard]

is that if you make an error

[Kevin Buzzard]

then sometimes your new red squiggly underline appears in a weird place

[Kevin Buzzard]

and you might not notice it if they're everywhere

[Kevin Buzzard]

so every time I split in tactic mode

[Kevin Buzzard]

I always put in two sorrys

[Kevin Buzzard]

etc etc

[Kevin Buzzard]

example : (A * (A + B) * (C + (A + B)) : ℕ) = a * (a + b) * (c + (a + b)) := rfl

[Kevin Buzzard]

that's not surprising

[Kevin Buzzard]

example : ↑(A * (A + B) * (C + (A + B))) = a * (a + b) * (c + (a + b)) := rfl

[Kevin Buzzard]

that's not surprising

[Kevin Buzzard]

why did he make all these rfl things simp lemmas?

[Kevin Buzzard]

example : ↑(A * (A + B) * (C + (A + B))) = a * (a + b) * (c + (a + b)) := by simp

[Kevin Buzzard]

fails :-)

[Kevin Buzzard]

doh

[Kevin Buzzard]

aah well so it was probably for another reason

[Kevin Buzzard]

but at least we made it to the end, even if I'm still not 100% sure what makes a good simp lemma. Maybe I'm beginning to get the hang of it.

[Mario Carneiro]

You have to unfold your new definitions

[Kevin Buzzard]

But it's interesting to see the way of thinking -- put new structure on pnat, now immediately ask yourself if we need some lemmas

[Mario Carneiro]

try by simp [A, B, C]

[Kevin Buzzard]

section
parameters {a b c : nat}
parameters {ha : a > 0} {hb : b > 0} {hc : c > 0}
@[reducible] def A : pnat := ⟨a,ha⟩
@[reducible] def B : pnat := ⟨b,hb⟩
@[reducible] def C : pnat := ⟨c,hc⟩

example : (A * (A + B) * (C + (A + B)) : ℕ) = a * (a + b) * (c + (a + b)) := by simp

end section

[Kevin Buzzard]

That works because I told Lean to unfold A B and C eagerly

[Kevin Buzzard]

simp [A,B,C]?

[Kevin Buzzard]

Is A a good simp lemma??

[Kevin Buzzard]

Normally when you start putting simp [random thing] it complains that the random thing isn't a good simp lemma

[Kevin Buzzard]

section
parameters {a b c : nat}
parameters {ha : a > 0} {hb : b > 0} {hc : c > 0}
def A : pnat := ⟨a,ha⟩
def B : pnat := ⟨b,hb⟩
def C : pnat := ⟨c,hc⟩

example : (A * (A + B) * (C + (A + B)) : ℕ) = a * (a + b) * (c + (a + b)) := by simp [A,B,C]


end section

[Kevin Buzzard]

well blow me down it works

[Mario Carneiro]

simp [my_def] where my_def is a def means simp [my_def.<equation lemmas>]

[Kevin Buzzard]

ooh

[Kevin Buzzard]

How do I see A's equation lemmas?

[Kevin Buzzard]

#print prefix A

[Kevin Buzzard]

A : Π {a : ℕ} {ha : a > 0}, ℕ+
A.equations._eqn_1 : ∀ {a : ℕ} {ha : a > 0}, A = ⟨a, ha⟩

[Kevin Buzzard]

That doesn't look like a good simp lemma to me

[Mario Carneiro]

not by default, no

[Kevin Buzzard]

there are variables on the RHS which don't appear on the LHS

[Mario Carneiro]

Actually they appear on the left too

[Kevin Buzzard]

and a wise person once told me not to put these into simp

[Mario Carneiro]

they are hidden because of the parameter thing

[Mario Carneiro]

or possibly because you have {a} {ha}

[Kevin Buzzard]

heh

[Kevin Buzzard]

I think the latter

[Kevin Buzzard]

Ok so we got there

[Kevin Buzzard]

and that's pnat.

[Mario Carneiro]

if they didn't appear on the left, you could use this theorem to prove 1 = 2

[Kevin Buzzard]

Oh that would be a cool application of pnat

[Kevin Buzzard]

I need to go to tend to the family

[Kevin Buzzard]

but there's a random thing

[Kevin Buzzard]

which people will be able to link to and look at later on

[Kevin Buzzard]

and in particular in a couple of weeks when I am supposed to be teaching a bunch of mathematicians Lean and they don't know how to make structures

[Kevin Buzzard]

and it was much easier to write than a proper document

[Kevin Buzzard]

Thanks for the help Mario and Patrick and Johan and others