## Stream: maths

### Topic: LIVE CHAT: Structures for mathematicians

#### Kevin Buzzard (May 29 2018 at 17:53):

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

#### Johan Commelin (May 29 2018 at 18:01):

No, it seems "Zulip live"

#### Kevin Buzzard (May 29 2018 at 18:20):

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 (May 29 2018 at 19:00):

Hello, this is just me talking through pnat.lean

#### Kevin Buzzard (May 29 2018 at 19:00):

It should be easy

#### Kevin Buzzard (May 29 2018 at 19:00):

and maybe people will find it later.

#### Kevin Buzzard (May 29 2018 at 19:01):

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 (May 29 2018 at 19:01):

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

#### Kevin Buzzard (May 29 2018 at 19:01):

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

#### Kevin Buzzard (May 29 2018 at 19:01):

we could just make a structure

hmm

#### Kevin Buzzard (May 29 2018 at 19:02):

let me fire up lean

that's better

#### Kevin Buzzard (May 29 2018 at 19:03):

I am so rubbish at structures

aah bingo

#### Kevin Buzzard (May 29 2018 at 19:03):

it's not a structure

#### Kevin Buzzard (May 29 2018 at 19:03):

it's an inductive type

#### Kevin Buzzard (May 29 2018 at 19:03):

inductive pnat
| one : pnat
| succ : pnat  pnat

So there's pnat

#### Kevin Buzzard (May 29 2018 at 19:04):

and that would work

#### Kevin Buzzard (May 29 2018 at 19:04):

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

#### Kevin Buzzard (May 29 2018 at 19:04):

and do all that stuff again

#### Kevin Buzzard (May 29 2018 at 19:04):

and that's stuff we already did with nat

#### Kevin Buzzard (May 29 2018 at 19:04):

and that's kind of a waste

#### Kevin Buzzard (May 29 2018 at 19:04):

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

#### Kevin Buzzard (May 29 2018 at 19:04):

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

#### Kevin Buzzard (May 29 2018 at 19:05):

Ok so it's in mathlib

#### Kevin Buzzard (May 29 2018 at 19:05):

which means that computer scientists are not interested in this structure

#### Kevin Buzzard (May 29 2018 at 19:05):

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

#### Kevin Buzzard (May 29 2018 at 19:06):

let's find it on github

#### Kevin Buzzard (May 29 2018 at 19:06):

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

There it is.

#### Kevin Buzzard (May 29 2018 at 19:06):

Things never stand still around here

#### Kevin Buzzard (May 29 2018 at 19:07):

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 (May 29 2018 at 19:07):

and the first thing we notice

#### Kevin Buzzard (May 29 2018 at 19:07):

is that on line 1

#### Kevin Buzzard (May 29 2018 at 19:07):

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

#### Kevin Buzzard (May 29 2018 at 19:07):

they define it as a _subtype_

#### Kevin Buzzard (May 29 2018 at 19:07):

which is a bit more annoying to use in practice

#### Kevin Buzzard (May 29 2018 at 19:08):

oh wait I skipped a line

#### Kevin Buzzard (May 29 2018 at 19:08):

import tactic.basic

#### Kevin Buzzard (May 29 2018 at 19:08):

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

#### Kevin Buzzard (May 29 2018 at 19:08):

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

And there it is.

#### Kevin Buzzard (May 29 2018 at 19:08):

There are sets {x | blah}

#### Kevin Buzzard (May 29 2018 at 19:08):

and there are subtypes {x // blah}

#### Kevin Buzzard (May 29 2018 at 19:08):

this one is a subtype

#### Kevin Buzzard (May 29 2018 at 19:09):

don't mind me I'm just editing mathlib

#### Kevin Buzzard (May 29 2018 at 19:09):

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

#### Kevin Buzzard (May 29 2018 at 19:10):

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

1) a nat

#### Kevin Buzzard (May 29 2018 at 19:10):

2) a proof that it's positive

#### Kevin Buzzard (May 29 2018 at 19:10):

(that's > 0 for you French speakers)

#### Kevin Buzzard (May 29 2018 at 19:10):

so here's an example

#### Kevin Buzzard (May 29 2018 at 19:11):

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

#### Kevin Buzzard (May 29 2018 at 19:11):

that didn't go well

#### Kevin Buzzard (May 29 2018 at 19:11):

I was in the middle of defining 59

#### Kevin Buzzard (May 29 2018 at 19:11):

and all of a sudden I needed a proof.

#### Kevin Buzzard (May 29 2018 at 19:11):

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

#### Kevin Buzzard (May 29 2018 at 19:12):

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

#### Kevin Buzzard (May 29 2018 at 19:12):

Ok that went better

#### Kevin Buzzard (May 29 2018 at 19:12):

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

#### Kevin Buzzard (May 29 2018 at 19:12):

and now I can finally make my pnat

#### Kevin Buzzard (May 29 2018 at 19:13):

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

#### Kevin Buzzard (May 29 2018 at 19:13):

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

#### Kevin Buzzard (May 29 2018 at 19:13):

notation ℕ+ := pnat

instance coe_pnat_nat : has_coe ℕ+  := subtype.val

#### Kevin Buzzard (May 29 2018 at 19:13):

Those are the next couple of lines

#### Kevin Buzzard (May 29 2018 at 19:14):

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

#### Kevin Buzzard (May 29 2018 at 19:14):

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

#### Kevin Buzzard (May 29 2018 at 19:14):

this sort of thing is a minefield

ℕ+ will do

#### Kevin Buzzard (May 29 2018 at 19:15):

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

ℕ^*

#### Kevin Buzzard (May 29 2018 at 19:15):

because we are already finished with the structure

#### Kevin Buzzard (May 29 2018 at 19:15):

Submit a PR Patrick

#### Kevin Buzzard (May 29 2018 at 19:16):

The thing that mathematicians don't realise

#### Kevin Buzzard (May 29 2018 at 19:16):

or at least that I didn't realise at all

#### Kevin Buzzard (May 29 2018 at 19:16):

(I suspect Patrick knew full well)

#### Kevin Buzzard (May 29 2018 at 19:16):

was that it's not just about making the structure

#### Kevin Buzzard (May 29 2018 at 19:16):

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

#### Kevin Buzzard (May 29 2018 at 19:17):

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

#### Kevin Buzzard (May 29 2018 at 19:17):

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 (May 29 2018 at 19:17):

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

#### Kevin Buzzard (May 29 2018 at 19:17):

that not only did they design a function for it

#### Kevin Buzzard (May 29 2018 at 19:17):

but they made it into a coercion

#### Kevin Buzzard (May 29 2018 at 19:17):

which means "it happens magically"

#### Kevin Buzzard (May 29 2018 at 19:18):

Aah I see what to do

#### Kevin Buzzard (May 29 2018 at 19:18):

I have mathlib pnat open

and a copy of it

#### Kevin Buzzard (May 29 2018 at 19:18):

and I edit the copy

great

#### Kevin Buzzard (May 29 2018 at 19:18):

so let's see if we can understand this coercion

#### Kevin Buzzard (May 29 2018 at 19:18):

and then let's see it happen

#### Kevin Buzzard (May 29 2018 at 19:18):

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

#### Kevin Buzzard (May 29 2018 at 19:19):

instances are something I never understood

#### Kevin Buzzard (May 29 2018 at 19:19):

coercions not really either

#### Kevin Buzzard (May 29 2018 at 19:19):

and then those dreaded pointy brackets

#### Kevin Buzzard (May 29 2018 at 19:19):

and then an incomprehensible subtype.val

#### Kevin Buzzard (May 29 2018 at 19:19):

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

#### Kevin Buzzard (May 29 2018 at 19:19):

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

#### Kevin Buzzard (May 29 2018 at 19:19):

so we can work out what this line does

#### Kevin Buzzard (May 29 2018 at 19:20):

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

#### Kevin Buzzard (May 29 2018 at 19:20):

and then selecting "go to definition"

#### Kevin Buzzard (May 29 2018 at 19:20):

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

and we see

#### Kevin Buzzard (May 29 2018 at 19:20):

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

#### Kevin Buzzard (May 29 2018 at 19:21):

and pnat, the positive naturals, was a subtype

#### Kevin Buzzard (May 29 2018 at 19:21):

in fact if we switch notation off and look at pnat

#### Kevin Buzzard (May 29 2018 at 19:21):

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

set_option pp.notation false
#print pnat

we see

#### Kevin Buzzard (May 29 2018 at 19:22):

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

eew

gt is >

#### Kevin Buzzard (May 29 2018 at 19:22):

so indeed we see a function nat to Prop

#### Kevin Buzzard (May 29 2018 at 19:22):

sending n to "n > 0"

#### Kevin Buzzard (May 29 2018 at 19:23):

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

#### Kevin Buzzard (May 29 2018 at 19:23):

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

#### Kevin Buzzard (May 29 2018 at 19:24):

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

to its value

which is 59

#### Kevin Buzzard (May 29 2018 at 19:24):

and we made it a coercion using coercion instance magic

#### Kevin Buzzard (May 29 2018 at 19:25):

so that means it should happen naturally

Ok it works!

#### Kevin Buzzard (May 29 2018 at 19:26):

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

#### Kevin Buzzard (May 29 2018 at 19:26):

it would be better if you could see me typing

#### Kevin Buzzard (May 29 2018 at 19:26):

that would save me having to cut and paste

#### Kevin Buzzard (May 29 2018 at 19:26):

how do I do that?

#### Kevin Buzzard (May 29 2018 at 19:26):

Does twitch take this sort of stuff?

#### Kevin Buzzard (May 29 2018 at 19:27):

I have done all manner of weird things on twitch

#### Patrick Massot (May 29 2018 at 19:27):

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

#### Kevin Buzzard (May 29 2018 at 19:27):

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

#### Kevin Buzzard (May 29 2018 at 19:27):

so back to the point

#### Kevin Buzzard (May 29 2018 at 19:27):

a miracle occurred!

and type nat

as well

#### Kevin Buzzard (May 29 2018 at 19:27):

but actually what happened was that coercion kicked in

#### Kevin Buzzard (May 29 2018 at 19:28):

The output of the second check was ↑x : ℕ

#### Kevin Buzzard (May 29 2018 at 19:28):

and that arrow (which you get with \u)

#### Kevin Buzzard (May 29 2018 at 19:28):

means "I got coerced!"

#### Kevin Buzzard (May 29 2018 at 19:28):

so that has solved our first fundamental problem

#### Kevin Buzzard (May 29 2018 at 19:28):

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

#### Kevin Buzzard (May 29 2018 at 19:28):

and hence every pnat _is_ a nat

#### Kevin Buzzard (May 29 2018 at 19:28):

They don't have it so easy in DTT

#### Kevin Buzzard (May 29 2018 at 19:29):

so we are stuck with the cute little arrows

let's press on

#### Kevin Buzzard (May 29 2018 at 19:29):

The next line is clever

#### Kevin Buzzard (May 29 2018 at 19:30):

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

#### Kevin Buzzard (May 29 2018 at 19:30):

That's using a really cool piece of Lean functionality

#### Kevin Buzzard (May 29 2018 at 19:30):

...which breaks if I remove that import line

#### Kevin Buzzard (May 29 2018 at 19:30):

so that's why the import is there

#### Kevin Buzzard (May 29 2018 at 19:31):

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

#### Patrick Massot (May 29 2018 at 19:31):

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

#### Kevin Buzzard (May 29 2018 at 19:31):

you can do pp.no_cute_arrows Patrick?

here we are

#### Kevin Buzzard (May 29 2018 at 19:32):

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

#### Patrick Massot (May 29 2018 at 19:32):

set_option pp.coercions false

#### Kevin Buzzard (May 29 2018 at 19:32):

does that mean Lean doesn't do them?

#### Kevin Buzzard (May 29 2018 at 19:32):

or just doesn't print the arrows?

doesn't print

thought so :-)

hence the pp

#### Johan Commelin (May 29 2018 at 19:32):

pp means "pretty print"

#### Patrick Massot (May 29 2018 at 19:32):

meaning pretty print

#### Kevin Buzzard (May 29 2018 at 19:33):

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

#### Kevin Buzzard (May 29 2018 at 19:33):

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

#### Patrick Massot (May 29 2018 at 19:33):

class.instance_max_depth

#### Kevin Buzzard (May 29 2018 at 19:33):

"run a tactic to make the argument for you"

#### Kevin Buzzard (May 29 2018 at 19:33):

Patrick: touch\'e

#### Kevin Buzzard (May 29 2018 at 19:33):

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

#### Kevin Buzzard (May 29 2018 at 19:34):

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

#### Kevin Buzzard (May 29 2018 at 19:34):

Let's see this tactic in action

#### Kevin Buzzard (May 29 2018 at 19:35):

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

It works!

#### Kevin Buzzard (May 29 2018 at 19:35):

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

#### Kevin Buzzard (May 29 2018 at 19:35):

so I'm not going to do that

#### Kevin Buzzard (May 29 2018 at 19:35):

but I know what is going on

#### Kevin Buzzard (May 29 2018 at 19:35):

in fact there's a shorter way of doing it

#### Kevin Buzzard (May 29 2018 at 19:35):

theorem H : 59 > 0 := dec_trivial

#### Kevin Buzzard (May 29 2018 at 19:36):

(not a tactic, so no by this time)

#### Kevin Buzzard (May 29 2018 at 19:36):

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

#### Kevin Buzzard (May 29 2018 at 19:37):

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

#### Kevin Buzzard (May 29 2018 at 19:37):

theorem H1 : 0 > 0 := dec_trivial

doesn't work

#### Kevin Buzzard (May 29 2018 at 19:37):

so let's see to_pnat in action!

#### Kevin Buzzard (May 29 2018 at 19:38):

definition y : pnat := to_pnat 12

#### Kevin Buzzard (May 29 2018 at 19:38):

that's much better than what we had before

#### Kevin Buzzard (May 29 2018 at 19:38):

definition z : pnat := to_pnat 0

#### Kevin Buzzard (May 29 2018 at 19:38):

you get some weird error

#### Kevin Buzzard (May 29 2018 at 19:38):

OK so let's press on

#### Kevin Buzzard (May 29 2018 at 19:38):

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

#### Kevin Buzzard (May 29 2018 at 19:38):

this one looks easy.

#### Kevin Buzzard (May 29 2018 at 19:39):

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

#### Kevin Buzzard (May 29 2018 at 19:39):

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

#### Kevin Buzzard (May 29 2018 at 19:39):

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

#### Kevin Buzzard (May 29 2018 at 19:39):

we can check that easily

#### Mario Carneiro (May 29 2018 at 19:39):

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

#### Mario Carneiro (May 29 2018 at 19:40):

but you can prove the negation using dec_trivial

#### Kevin Buzzard (May 29 2018 at 19:40):

variable (n : )
#check succ_pos n

#### Kevin Buzzard (May 29 2018 at 19:40):

succ_pos n : 0 < succ n

#### Kevin Buzzard (May 29 2018 at 19:40):

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

#### Kevin Buzzard (May 29 2018 at 19:41):

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

#### Kevin Buzzard (May 29 2018 at 19:41):

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

#### Kevin Buzzard (May 29 2018 at 19:42):

but what do we need to do next?

#### Kevin Buzzard (May 29 2018 at 19:42):

This is the question that I as a mathematician find hard

#### Kevin Buzzard (May 29 2018 at 19:42):

and I think that people like Mario just somehow know

#### Kevin Buzzard (May 29 2018 at 19:42):

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

#### Kevin Buzzard (May 29 2018 at 19:42):

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

#### Kevin Buzzard (May 29 2018 at 19:43):

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 (May 29 2018 at 19:43):

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

#### Kevin Buzzard (May 29 2018 at 19:43):

and Lean coerces the left hand side

#### Kevin Buzzard (May 29 2018 at 19:43):

so if you think about it

#### Kevin Buzzard (May 29 2018 at 19:43):

when you unravel it

#### Kevin Buzzard (May 29 2018 at 19:43):

that theorem just says succ n = succ n

#### Kevin Buzzard (May 29 2018 at 19:43):

so the proof is rfl

#### Kevin Buzzard (May 29 2018 at 19:44):

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

#### Kevin Buzzard (May 29 2018 at 19:44):

but this one got lucky

it got a name

#### Mario Carneiro (May 29 2018 at 19:44):

it's a simp lemma, those need names

#### Kevin Buzzard (May 29 2018 at 19:44):

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

#### Kevin Buzzard (May 29 2018 at 19:44):

NOTE FOR BEGINNERS

#### Mario Carneiro (May 29 2018 at 19:44):

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

#### Mario Carneiro (May 29 2018 at 19:45):

rfl proofs are very common

#### Kevin Buzzard (May 29 2018 at 19:45):

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

#### Kevin Buzzard (May 29 2018 at 19:45):

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

#### Kevin Buzzard (May 29 2018 at 19:45):

because that would be a comp lemma

#### Kevin Buzzard (May 29 2018 at 19:45):

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

#### Kevin Buzzard (May 29 2018 at 19:46):

x = y and y = x mean the same thing

#### Kevin Buzzard (May 29 2018 at 19:46):

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

#### Kevin Buzzard (May 29 2018 at 19:46):

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

#### Kevin Buzzard (May 29 2018 at 19:46):

and even if simp does not use your lemma

#### Kevin Buzzard (May 29 2018 at 19:46):

imagine when you're doing a rewrite

#### Kevin Buzzard (May 29 2018 at 19:46):

you are trying to prove something

#### Kevin Buzzard (May 29 2018 at 19:46):

so you're usally trying to make stuff easier

#### Kevin Buzzard (May 29 2018 at 19:47):

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

#### Kevin Buzzard (May 29 2018 at 19:47):

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

#### Kevin Buzzard (May 29 2018 at 19:47):

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

#### Kevin Buzzard (May 29 2018 at 19:47):

or else you should have proved y = x

Next line

#### Kevin Buzzard (May 29 2018 at 19:48):

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

#### Kevin Buzzard (May 29 2018 at 19:48):

that looks like really poor Lean to me

#### Kevin Buzzard (May 29 2018 at 19:48):

who wrote this file anyway

#### Kevin Buzzard (May 29 2018 at 19:48):

oh I heard of that guy

#### Kevin Buzzard (May 29 2018 at 19:48):

Now everyone knows that simp is used to prove _equalities_

#### Kevin Buzzard (May 29 2018 at 19:48):

so all your simp lemmas should be _equalities_

or _iff_s

#### Kevin Buzzard (May 29 2018 at 19:48):

and anything which is a random thing like >

#### Kevin Buzzard (May 29 2018 at 19:49):

obviously should not be a simp lemma

#### Kevin Buzzard (May 29 2018 at 19:49):

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

#### Mario Carneiro (May 29 2018 at 19:49):

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

#### Kevin Buzzard (May 29 2018 at 19:49):

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

#### Kevin Buzzard (May 29 2018 at 19:49):

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

#### Patrick Massot (May 29 2018 at 19:49):

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

#### Kevin Buzzard (May 29 2018 at 19:50):

but apparently there are other times when it's not

#### Kevin Buzzard (May 29 2018 at 19:50):

Interesting point Patrick I guess you're right

#### Kevin Buzzard (May 29 2018 at 19:50):

Maybe 0 is a special case

#### Kevin Buzzard (May 29 2018 at 19:50):

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 (May 29 2018 at 19:50):

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

#### Patrick Massot (May 29 2018 at 19:51):

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

#### Kevin Buzzard (May 29 2018 at 19:51):

Now look at these

#### Kevin Buzzard (May 29 2018 at 19:51):

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 (May 29 2018 at 19:52):

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 (May 29 2018 at 19:52):

I did that a lot when I started

#### Kevin Buzzard (May 29 2018 at 19:52):

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

#### Kevin Buzzard (May 29 2018 at 19:52):

but its full name is pnat.ne_zero

#### Kevin Buzzard (May 29 2018 at 19:52):

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

#### Johan Commelin (May 29 2018 at 19:52):

So, why is theorem eq not a simp theorem?

#### Kevin Buzzard (May 29 2018 at 19:52):

so that's why we opened the pnat namespace

we namespaced

#### Kevin Buzzard (May 29 2018 at 19:53):

and we opened nat for good measure

#### Mario Carneiro (May 29 2018 at 19:53):

because the RHS has a variable not on the LHS

#### Kevin Buzzard (May 29 2018 at 19:53):

So theorem eq says a fundamental thing about subtypes.

#### Kevin Buzzard (May 29 2018 at 19:54):

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

#### Kevin Buzzard (May 29 2018 at 19:54):

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

#### Patrick Massot (May 29 2018 at 19:54):

What RHS variable?

#### Kevin Buzzard (May 29 2018 at 19:54):

And yes they are, because all proofs are the same

#### Kevin Buzzard (May 29 2018 at 19:54):

so that's why pnat.eq is true

#### Kevin Buzzard (May 29 2018 at 19:54):

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

#### Kevin Buzzard (May 29 2018 at 19:54):

or right click on ir

it

or #check it

#### Kevin Buzzard (May 29 2018 at 19:55):

Oh I know why eq isn't a simp lemma

#### Kevin Buzzard (May 29 2018 at 19:55):

it's not an equality

#### Mario Carneiro (May 29 2018 at 19:55):

m = n is not a simplification

#### Kevin Buzzard (May 29 2018 at 19:55):

it's an implication

#### Mario Carneiro (May 29 2018 at 19:55):

and where is n coming from?

aah

#### Mario Carneiro (May 29 2018 at 19:55):

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

#### Kevin Buzzard (May 29 2018 at 19:55):

There's another simp rule of thumb

#### Kevin Buzzard (May 29 2018 at 19:56):

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

#### Johan Commelin (May 29 2018 at 19:56):

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.

why this rule?

#### Kevin Buzzard (May 29 2018 at 19:56):

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

#### Mario Carneiro (May 29 2018 at 19:56):

It's an extensionality theorem

#### Mario Carneiro (May 29 2018 at 19:57):

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

#### Patrick Massot (May 29 2018 at 19:57):

should it be tagged as such?

probably

#### Kevin Buzzard (May 29 2018 at 19:57):

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 (May 29 2018 at 19:57):

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 (May 29 2018 at 19:57):

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 (May 29 2018 at 19:57):

because you wanted to prove complicated structures were equal

#### Kevin Buzzard (May 29 2018 at 19:58):

I think this sort of thing is an art

#### Kevin Buzzard (May 29 2018 at 19:58):

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

#### Mario Carneiro (May 29 2018 at 19:58):

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

#### Mario Carneiro (May 29 2018 at 19:58):

the goal got more complicated

#### Mario Carneiro (May 29 2018 at 19:58):

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

#### Kevin Buzzard (May 29 2018 at 19:58):

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

#### Kevin Buzzard (May 29 2018 at 19:58):

then you might well not want it

#### Kevin Buzzard (May 29 2018 at 19:59):

but if m was explicitly <nat,proof>

and so was n

#### Kevin Buzzard (May 29 2018 at 19:59):

then you might want it

#### Kevin Buzzard (May 29 2018 at 19:59):

(but you might not)

Hmm, fair enough

#### Mario Carneiro (May 29 2018 at 19:59):

and that version is a simp lemma

#### Kevin Buzzard (May 29 2018 at 19:59):

ooh my son's gone

#### Kevin Buzzard (May 29 2018 at 19:59):

I just inherited a second screen

#### Johan Commelin (May 29 2018 at 19:59):

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

Ok so mk_coe

#### Johan Commelin (May 29 2018 at 20:00):

Or is it a simp lemma for general subtypes?

#### Kevin Buzzard (May 29 2018 at 20:00):

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

#### Johan Commelin (May 29 2018 at 20:00):

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

subtype.mk_eq_mk

#### Kevin Buzzard (May 29 2018 at 20:00):

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

#### Mario Carneiro (May 29 2018 at 20:00):

it's a general simp lemma

#### Kevin Buzzard (May 29 2018 at 20:00):

Actually there are several cool things about mk_coe

#### Kevin Buzzard (May 29 2018 at 20:01):

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

hmm

#### Kevin Buzzard (May 29 2018 at 20:01):

maybe that's not entirely true

#### Kevin Buzzard (May 29 2018 at 20:01):

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

#### Kevin Buzzard (May 29 2018 at 20:01):

They're definitionally equal, right?

#### Kevin Buzzard (May 29 2018 at 20:02):

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

#### Mario Carneiro (May 29 2018 at 20:02):

it's a simp lemma

#### Kevin Buzzard (May 29 2018 at 20:02):

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

#### Mario Carneiro (May 29 2018 at 20:02):

The val version is automatic, because simp knows about structures

#### Kevin Buzzard (May 29 2018 at 20:02):

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

#### Mario Carneiro (May 29 2018 at 20:02):

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

#### Kevin Buzzard (May 29 2018 at 20:02):

oh so simp doesn't need to be told that

#### Kevin Buzzard (May 29 2018 at 20:02):

the thing I wrote

#### Kevin Buzzard (May 29 2018 at 20:02):

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

right

#### Kevin Buzzard (May 29 2018 at 20:03):

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

#### Kevin Buzzard (May 29 2018 at 20:03):

I saw the definition of pnat in a maths lecture

#### Mario Carneiro (May 29 2018 at 20:03):

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

#### Kevin Buzzard (May 29 2018 at 20:03):

it was "take nat and remove 0"

and that was it

#### Mario Carneiro (May 29 2018 at 20:03):

but it probably won't trigger

#### Kevin Buzzard (May 29 2018 at 20:03):

There is all this extra stuff here

#### Kevin Buzzard (May 29 2018 at 20:03):

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 (May 29 2018 at 20:04):

and here's something I only learnt recently

#### Kevin Buzzard (May 29 2018 at 20:04):

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

is notation

#### Kevin Buzzard (May 29 2018 at 20:05):

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

#### Kevin Buzzard (May 29 2018 at 20:05):

although probably one could have called it pnat.add

#### Mario Carneiro (May 29 2018 at 20:05):

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

#### Kevin Buzzard (May 29 2018 at 20:05):

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 (May 29 2018 at 20:05):

Oh I didn't know that -- thanks

#### Mario Carneiro (May 29 2018 at 20:05):

pnat.add would be the name of the function itself

Oh of course

#### Kevin Buzzard (May 29 2018 at 20:06):

and the proof that it has an add is something else

#### Kevin Buzzard (May 29 2018 at 20:06):

actually it's not a proof

it's data

#### Kevin Buzzard (May 29 2018 at 20:06):

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

#### Kevin Buzzard (May 29 2018 at 20:06):

and we cheat and look at what Mario did

#### Kevin Buzzard (May 29 2018 at 20:07):

and why is the output from #check so ugly?

#### Kevin Buzzard (May 29 2018 at 20:07):

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

thanks Lean

#### Kevin Buzzard (May 29 2018 at 20:07):

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

not ideal either

#### Kevin Buzzard (May 29 2018 at 20:08):

I would have preferred

#### Kevin Buzzard (May 29 2018 at 20:08):

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

#### Kevin Buzzard (May 29 2018 at 20:08):

but unsurprisingly

#### Kevin Buzzard (May 29 2018 at 20:08):

it's the lemma we need

#### Kevin Buzzard (May 29 2018 at 20:09):

Now these should be straightforward

#### Kevin Buzzard (May 29 2018 at 20:09):

@[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 (May 29 2018 at 20:09):

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

#### Kevin Buzzard (May 29 2018 at 20:09):

we have to carry around all these proofs

#### Kevin Buzzard (May 29 2018 at 20:10):

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

#### Kevin Buzzard (May 29 2018 at 20:10):

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

#### Kevin Buzzard (May 29 2018 at 20:10):

and it would not surprise me if that were called ne_of_gt

and note that

n.2 is the proof

that n > 0

it's n.property

#### Kevin Buzzard (May 29 2018 at 20:11):

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

nat_coe_coe

#### Kevin Buzzard (May 29 2018 at 20:11):

I have no idea why this is a simp lemma

#### Kevin Buzzard (May 29 2018 at 20:11):

I guess I do know

#### Kevin Buzzard (May 29 2018 at 20:11):

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

#### Kevin Buzzard (May 29 2018 at 20:12):

"and then we get some serious simplification"

#### Kevin Buzzard (May 29 2018 at 20:12):

I am kind of surprised this works

#### Kevin Buzzard (May 29 2018 at 20:12):

we coerce a nat to a pnat

#### Kevin Buzzard (May 29 2018 at 20:12):

that doesn't even make sense

oh crap

#### Kevin Buzzard (May 29 2018 at 20:12):

I am looking at an old version of pnat

rofl

#### Kevin Buzzard (May 29 2018 at 20:13):

I'm now looking at the up to date version

#### Kevin Buzzard (May 29 2018 at 20:13):

and that line is gone :-)

#### Kevin Buzzard (May 29 2018 at 20:13):

@[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 (May 29 2018 at 20:13):

Things never stand still around here

#### Kevin Buzzard (May 29 2018 at 20:14):

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

Ok great

#### Kevin Buzzard (May 29 2018 at 20:14):

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

#### Kevin Buzzard (May 29 2018 at 20:15):

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 (May 29 2018 at 20:15):

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

#### Kevin Buzzard (May 29 2018 at 20:15):

Ok so this looks good

#### Kevin Buzzard (May 29 2018 at 20:15):

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

#### Kevin Buzzard (May 29 2018 at 20:15):

and this is not rfl

#### Kevin Buzzard (May 29 2018 at 20:16):

indeed it's not even true

#### Kevin Buzzard (May 29 2018 at 20:16):

it's false for n=0

#### Kevin Buzzard (May 29 2018 at 20:16):

but we have the hypo n > 0

#### Kevin Buzzard (May 29 2018 at 20:16):

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

#### Kevin Buzzard (May 29 2018 at 20:16):

and that would be called something like succ_pred_eq_of_pos

#### Kevin Buzzard (May 29 2018 at 20:16):

which it indeed is

Ok nearly there

#### Kevin Buzzard (May 29 2018 at 20:17):

oh one more simp lemma

#### Kevin Buzzard (May 29 2018 at 20:17):

you see this is exactly what I don't get

#### Kevin Buzzard (May 29 2018 at 20:17):

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

#### Kevin Buzzard (May 29 2018 at 20:17):

We have just proved 10 trivial things

#### Kevin Buzzard (May 29 2018 at 20:17):

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

#### Mario Carneiro (May 29 2018 at 20:17):

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

look!

#### Kevin Buzzard (May 29 2018 at 20:17):

We just proved n = n again

#### Kevin Buzzard (May 29 2018 at 20:17):

let's make it a simp lemma!

#### Kevin Buzzard (May 29 2018 at 20:18):

to_pnat' is a bit funny isn't it

#### Kevin Buzzard (May 29 2018 at 20:18):

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

#### Kevin Buzzard (May 29 2018 at 20:18):

sends n to n if n is positive

and 0 to 1

#### Kevin Buzzard (May 29 2018 at 20:19):

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

#### Mario Carneiro (May 29 2018 at 20:19):

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

#### Kevin Buzzard (May 29 2018 at 20:19):

and perhaps in this particular case they're right

#### Kevin Buzzard (May 29 2018 at 20:20):

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

exactly

#### Kevin Buzzard (May 29 2018 at 20:20):

Now here's a meaty bit of file

#### Kevin Buzzard (May 29 2018 at 20:20):

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 (May 29 2018 at 20:20):

it's a commutative monoid!

#### Kevin Buzzard (May 29 2018 at 20:21):

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

#### Kevin Buzzard (May 29 2018 at 20:21):

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

#### Kevin Buzzard (May 29 2018 at 20:21):

outside the monoid

#### Kevin Buzzard (May 29 2018 at 20:21):

and I would have done has_one pnat

#### Kevin Buzzard (May 29 2018 at 20:21):

Mario -- does your pnat have a mul?

#### Mario Carneiro (May 29 2018 at 20:21):

yes, it's right there

#### Mario Carneiro (May 29 2018 at 20:22):

comm_monoid implies has_mul

#### Kevin Buzzard (May 29 2018 at 20:23):

If I type #print comm_monoid

I can't see this

#### Kevin Buzzard (May 29 2018 at 20:23):

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

#### Kevin Buzzard (May 29 2018 at 20:23):

Or have I misunderstood?

#### Mario Carneiro (May 29 2018 at 20:23):

comm_monoid extends monoid which extends semigroup which extends has_mul

#### Kevin Buzzard (May 29 2018 at 20:24):

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

#### Kevin Buzzard (May 29 2018 at 20:24):

but you had to know that

#### Kevin Buzzard (May 29 2018 at 20:24):

I could have written comm_monoid in a different way

#### Kevin Buzzard (May 29 2018 at 20:24):

and it would have _looked_ like there was a mul

#### Kevin Buzzard (May 29 2018 at 20:24):

but you wouldn't have got the notation

#### Kevin Buzzard (May 29 2018 at 20:25):

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

#### Mario Carneiro (May 29 2018 at 20:25):

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 (May 29 2018 at 20:25):

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

#### Mario Carneiro (May 29 2018 at 20:25):

after that instance

#### Kevin Buzzard (May 29 2018 at 20:26):

after making it a commutative monoid

#### Kevin Buzzard (May 29 2018 at 20:26):

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

#### Mario Carneiro (May 29 2018 at 20:26):

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

#### Kevin Buzzard (May 29 2018 at 20:26):

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

#### Kevin Buzzard (May 29 2018 at 20:26):

if you had wanted to know before writing the code

#### Mario Carneiro (May 29 2018 at 20:27):

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

#### Kevin Buzzard (May 29 2018 at 20:27):

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

exactly

#### Kevin Buzzard (May 29 2018 at 20:27):

You had to rely on someone else being sensible

#### Kevin Buzzard (May 29 2018 at 20:27):

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 (May 29 2018 at 20:27):

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

#### Kevin Buzzard (May 29 2018 at 20:28):

But you didn't get Lean to tell you

#### Mario Carneiro (May 29 2018 at 20:28):

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

#### Kevin Buzzard (May 29 2018 at 20:29):

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

#### Mario Carneiro (May 29 2018 at 20:29):

It is important that has_mul be declared only once though

#### Kevin Buzzard (May 29 2018 at 20:29):

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

#### Mario Carneiro (May 29 2018 at 20:29):

only tricky2 gets the notation, yes

#### Kevin Buzzard (May 29 2018 at 20:30):

but your method for checking this fails

#### Kevin Buzzard (May 29 2018 at 20:30):

because you can't make any instances

#### Kevin Buzzard (May 29 2018 at 20:30):

#check (by apply_instance : has_mul ℕ+)

sorry, you can

#### Kevin Buzzard (May 29 2018 at 20:30):

your method relied on pnat existing

#### Kevin Buzzard (May 29 2018 at 20:30):

show me Kenny :-)

#### Kenny Lau (May 29 2018 at 20:30):

just sorry everything

Fair enough

even mul?

(deleted)

#### Kevin Buzzard (May 29 2018 at 20:31):

I seem to have wandered a bit

#### Kevin Buzzard (May 29 2018 at 20:32):

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 (May 29 2018 at 20:32):

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

#### Kevin Buzzard (May 29 2018 at 20:32):

why don't we just go with mul_pos

#### Kevin Buzzard (May 29 2018 at 20:32):

and indeed that's what it is

naming is an art

#### Kevin Buzzard (May 29 2018 at 20:32):

and it's another thing mathematicians are bad at

#### Kevin Buzzard (May 29 2018 at 20:32):

The only training we get

#### Kevin Buzzard (May 29 2018 at 20:33):

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

#### Kevin Buzzard (May 29 2018 at 20:33):

from our teachers

#### Mario Carneiro (May 29 2018 at 20:33):

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

There you go

#### Kevin Buzzard (May 29 2018 at 20:33):

couldn't be easier

Now

#### Kevin Buzzard (May 29 2018 at 20:34):

how are we going to prove all these stupid axioms?

#### Kevin Buzzard (May 29 2018 at 20:34):

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 (May 29 2018 at 20:34):

mul_assoc -- that's already proved for nats

as is mul_comm

#### Kevin Buzzard (May 29 2018 at 20:35):

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 (May 29 2018 at 20:35):

so here we see the benefits

#### Kevin Buzzard (May 29 2018 at 20:35):

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 (May 29 2018 at 20:35):

was subtype.eq a simp lemma?

oh no

of course not

#### Kevin Buzzard (May 29 2018 at 20:36):

it has an implies

#### Kevin Buzzard (May 29 2018 at 20:36):

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

#### Kevin Buzzard (May 29 2018 at 20:36):

all the proofs are the same

#### Kevin Buzzard (May 29 2018 at 20:36):

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

#### Kevin Buzzard (May 29 2018 at 20:36):

whereas I suspect Mario wrote them

#### Kevin Buzzard (May 29 2018 at 20:37):

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 (May 29 2018 at 20:37):

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

true

#### Patrick Massot (May 29 2018 at 20:37):

This situation looks like what Simon solve for pi instances

#### Kevin Buzzard (May 29 2018 at 20:37):

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

#### Patrick Massot (May 29 2018 at 20:38):

Where is Simon by the way?

#### Kevin Buzzard (May 29 2018 at 20:38):

he's cool -- don't underestimate him

#### Patrick Massot (May 29 2018 at 20:38):

Haven't we lost him?

#### Kevin Buzzard (May 29 2018 at 20:38):

All that's left is one

#### Mario Carneiro (May 29 2018 at 20:38):

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

#### Mario Carneiro (May 29 2018 at 20:38):

there is a balance point there

#### Kevin Buzzard (May 29 2018 at 20:38):

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 (May 29 2018 at 20:38):

I don't think it matters

#### Mario Carneiro (May 29 2018 at 20:38):

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

#### Kevin Buzzard (May 29 2018 at 20:39):

I think every method will produce basically the same term

#### Kevin Buzzard (May 29 2018 at 20:39):

All that's left is this:

#### Kevin Buzzard (May 29 2018 at 20:39):

@[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 (May 29 2018 at 20:40):

one_coe -- who knows why this is a simp lemma

#### Kevin Buzzard (May 29 2018 at 20:40):

Where does it end

#### Kevin Buzzard (May 29 2018 at 20:40):

two_coe? Why is that not a simp lemma?

#### Mario Carneiro (May 29 2018 at 20:40):

because that's not an atomic term

#### Kevin Buzzard (May 29 2018 at 20:40):

mul_coe -- proof is refl

Oh I see

#### Kevin Buzzard (May 29 2018 at 20:41):

one just _became_ an atomic term

#### Mario Carneiro (May 29 2018 at 20:41):

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

#### Kevin Buzzard (May 29 2018 at 20:41):

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

#### Kevin Buzzard (May 29 2018 at 20:41):

and finally power

#### Kevin Buzzard (May 29 2018 at 20:42):

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

#### Kevin Buzzard (May 29 2018 at 20:42):

how new-fangled and fancy

#### Kevin Buzzard (May 29 2018 at 20:42):

it wasn't like this when I learnt it

#### Kevin Buzzard (May 29 2018 at 20:42):

#print notation ^

#### Kevin Buzzard (May 29 2018 at 20:42):

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

#### Kevin Buzzard (May 29 2018 at 20:43):

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

#### Kevin Buzzard (May 29 2018 at 20:43):

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

#### Kevin Buzzard (May 29 2018 at 20:43):

and if this was me 6 months ago

#### Kevin Buzzard (May 29 2018 at 20:43):

I would think "oh I quite fancy this one"

#### Kevin Buzzard (May 29 2018 at 20:43):

"induction on n should do it"

and I'd prove it

#### Kevin Buzzard (May 29 2018 at 20:44):

but that's not the way to think about Lean

#### Kevin Buzzard (May 29 2018 at 20:44):

the way to think about it is

#### Kevin Buzzard (May 29 2018 at 20:44):

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

#### Kevin Buzzard (May 29 2018 at 20:44):

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

#### Kevin Buzzard (May 29 2018 at 20:44):

and even if they didn't

#### Kevin Buzzard (May 29 2018 at 20:44):

maybe some obsessive mathlib guy thought of it

#### Kevin Buzzard (May 29 2018 at 20:44):

and maybe they gave it a name

#### Kevin Buzzard (May 29 2018 at 20:45):

and maybe it's someething like pos_pow_of_pos

#### Kevin Buzzard (May 29 2018 at 20:45):

This is the way to write Lean

#### Kevin Buzzard (May 29 2018 at 20:45):

don't write the code because you can

#### Kevin Buzzard (May 29 2018 at 20:45):

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

#### Kevin Buzzard (May 29 2018 at 20:45):

write nat.pos_pow and hit ctrl-space

#### Kevin Buzzard (May 29 2018 at 20:45):

and see if you get lucky

#### Kevin Buzzard (May 29 2018 at 20:46):

note that Mario used m.pos not m.2

#### Kevin Buzzard (May 29 2018 at 20:46):

That might just be for readability

#### Kevin Buzzard (May 29 2018 at 20:46):

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

#### Kevin Buzzard (May 29 2018 at 20:47):

but m.pos is basically better

#### Kevin Buzzard (May 29 2018 at 20:47):

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

#### Mario Carneiro (May 29 2018 at 20:47):

I'm sure it's just inconsistency

#### Kevin Buzzard (May 29 2018 at 20:47):

But you are making an interface for pnat

#### Kevin Buzzard (May 29 2018 at 20:47):

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

#### Mario Carneiro (May 29 2018 at 20:47):

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

#### Kevin Buzzard (May 29 2018 at 20:48):

which you should encourage the users to use

#### Kevin Buzzard (May 29 2018 at 20:48):

It literally makes no difference to anything?

#### Kevin Buzzard (May 29 2018 at 20:48):

Doesn't it increase compile time by a zillisecond?

#### Kevin Buzzard (May 29 2018 at 20:48):

you had to look up pos in some table

#### Mario Carneiro (May 29 2018 at 20:49):

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

#### Kevin Buzzard (May 29 2018 at 20:49):

Let me think epsilon more about poe

pow

#### Kevin Buzzard (May 29 2018 at 20:49):

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

#### Kevin Buzzard (May 29 2018 at 20:49):

/-- 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 (May 29 2018 at 20:49):

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

#### Kevin Buzzard (May 29 2018 at 20:50):

They are thinking "yay we now have pow"

#### Kevin Buzzard (May 29 2018 at 20:50):

but then immediately after

#### Kevin Buzzard (May 29 2018 at 20:50):

they think "OK I now have some obligations"

#### Kevin Buzzard (May 29 2018 at 20:50):

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 (May 29 2018 at 20:51):

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

#### Kevin Buzzard (May 29 2018 at 20:51):

which we've seen lots of times before

#### Kevin Buzzard (May 29 2018 at 20:51):

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

#### Kevin Buzzard (May 29 2018 at 20:51):

and even though the proof is refl

#### Kevin Buzzard (May 29 2018 at 20:51):

this looks like it should be a simp lemma

#### Kevin Buzzard (May 29 2018 at 20:52):

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

#### Kevin Buzzard (May 29 2018 at 20:52):

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

#### Kevin Buzzard (May 29 2018 at 20:53):

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

#### Kevin Buzzard (May 29 2018 at 20:53):

to prove it lands in pnat we prove a lemma

#### Kevin Buzzard (May 29 2018 at 20:53):

and that's the end

We stop here:

#### Kevin Buzzard (May 29 2018 at 20:53):

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

instance : has_pow ℕ+  := pow

#### Kevin Buzzard (May 29 2018 at 20:53):

We don't do this bit

#### Kevin Buzzard (May 29 2018 at 20:53):

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

#### Kevin Buzzard (May 29 2018 at 20:53):

but in CS if you don't do this

#### Kevin Buzzard (May 29 2018 at 20:54):

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

#### Kevin Buzzard (May 29 2018 at 20:54):

even though we only care about nats now

#### Kevin Buzzard (May 29 2018 at 20:54):

in fact did we prove all the coercions?

#### Kevin Buzzard (May 29 2018 at 20:54):

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

#### Kevin Buzzard (May 29 2018 at 20:54):

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

#### Kevin Buzzard (May 29 2018 at 20:54):

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

#### Kevin Buzzard (May 29 2018 at 20:55):

They all got proved

#### Kevin Buzzard (May 29 2018 at 20:55):

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

#### Kevin Buzzard (May 29 2018 at 20:55):

and then I made it a nat

#### Kevin Buzzard (May 29 2018 at 20:55):

then simp would remove all the pnats for me?

#### Kevin Buzzard (May 29 2018 at 20:55):

I think it might!

#### Kevin Buzzard (May 29 2018 at 20:56):

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

#### Kevin Buzzard (May 29 2018 at 20:57):

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

#### Kevin Buzzard (May 29 2018 at 20:57):

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

#### Kevin Buzzard (May 29 2018 at 20:57):

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

#### Kevin Buzzard (May 29 2018 at 20:57):

you just use variables to make stuff

rofl

#### Kevin Buzzard (May 29 2018 at 20:59):

I need to work harder

dammit

#### Kevin Buzzard (May 29 2018 at 20:59):

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 (May 29 2018 at 21:00):

doesn't typecheck yet

#### Mario Carneiro (May 29 2018 at 21:00):

Note that A and B are the same

for a b c

all six

#### Kevin Buzzard (May 29 2018 at 21:01):

Parameters can only be used in a section

#### Kevin Buzzard (May 29 2018 at 21:01):

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 (May 29 2018 at 21:02):

and this typechecks

#### Kevin Buzzard (May 29 2018 at 21:02):

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

#### Kevin Buzzard (May 29 2018 at 21:02):

maybe that's something I could mention

#### Kevin Buzzard (May 29 2018 at 21:02):

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

#### Kevin Buzzard (May 29 2018 at 21:03):

but I am happy with plenty of sorrys

#### Kevin Buzzard (May 29 2018 at 21:03):

green squiggly underlines ftw

#### Kevin Buzzard (May 29 2018 at 21:03):

the reason for this

#### Kevin Buzzard (May 29 2018 at 21:03):

is that if you make an error

#### Kevin Buzzard (May 29 2018 at 21:03):

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

#### Kevin Buzzard (May 29 2018 at 21:03):

and you might not notice it if they're everywhere

#### Kevin Buzzard (May 29 2018 at 21:03):

so every time I split in tactic mode

#### Kevin Buzzard (May 29 2018 at 21:03):

I always put in two sorrys

etc etc

#### Kevin Buzzard (May 29 2018 at 21:04):

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

#### Kevin Buzzard (May 29 2018 at 21:04):

that's not surprising

#### Kevin Buzzard (May 29 2018 at 21:04):

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

#### Kevin Buzzard (May 29 2018 at 21:04):

that's not surprising

#### Kevin Buzzard (May 29 2018 at 21:04):

why did he make all these rfl things simp lemmas?

#### Kevin Buzzard (May 29 2018 at 21:05):

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

fails :-)

doh

#### Kevin Buzzard (May 29 2018 at 21:05):

aah well so it was probably for another reason

#### Kevin Buzzard (May 29 2018 at 21:06):

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 (May 29 2018 at 21:06):

You have to unfold your new definitions

#### Kevin Buzzard (May 29 2018 at 21:06):

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 (May 29 2018 at 21:06):

try by simp [A, B, C]

#### Kevin Buzzard (May 29 2018 at 21:07):

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 (May 29 2018 at 21:07):

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

simp [A,B,C]?

#### Kevin Buzzard (May 29 2018 at 21:07):

Is A a good simp lemma??

#### Kevin Buzzard (May 29 2018 at 21:08):

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

#### Kevin Buzzard (May 29 2018 at 21:08):

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 (May 29 2018 at 21:08):

well blow me down it works

#### Mario Carneiro (May 29 2018 at 21:08):

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

ooh

#### Kevin Buzzard (May 29 2018 at 21:09):

How do I see A's equation lemmas?

#print prefix A

#### Kevin Buzzard (May 29 2018 at 21:09):

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

#### Kevin Buzzard (May 29 2018 at 21:10):

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

#### Mario Carneiro (May 29 2018 at 21:10):

not by default, no

#### Kevin Buzzard (May 29 2018 at 21:10):

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

#### Mario Carneiro (May 29 2018 at 21:10):

Actually they appear on the left too

#### Kevin Buzzard (May 29 2018 at 21:10):

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

#### Mario Carneiro (May 29 2018 at 21:10):

they are hidden because of the parameter thing

#### Mario Carneiro (May 29 2018 at 21:11):

or possibly because you have {a} {ha}

heh

#### Kevin Buzzard (May 29 2018 at 21:11):

I think the latter

#### Kevin Buzzard (May 29 2018 at 21:11):

Ok so we got there

and that's pnat.

#### Mario Carneiro (May 29 2018 at 21:12):

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

#### Kevin Buzzard (May 29 2018 at 21:12):

Oh that would be a cool application of pnat

#### Kevin Buzzard (May 29 2018 at 21:12):

I need to go to tend to the family

#### Kevin Buzzard (May 29 2018 at 21:12):

but there's a random thing

#### Kevin Buzzard (May 29 2018 at 21:12):

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

#### Kevin Buzzard (May 29 2018 at 21:13):

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 (May 29 2018 at 21:13):

and it was much easier to write than a proper document

#### Kevin Buzzard (May 29 2018 at 21:13):

Thanks for the help Mario and Patrick and Johan and others

Last updated: May 10 2021 at 08:14 UTC