Zulip Chat Archive

Stream: maths

Topic: LIVE CHAT: Structures for mathematicians


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

view this post on Zulip Kenny Lau (May 29 2018 at 17:54):

youtube live?

view this post on Zulip Johan Commelin (May 29 2018 at 18:01):

No, it seems "Zulip live"

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:00):

Hello, this is just me talking through pnat.lean

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:00):

It should be easy

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:00):

and maybe people will find it later.

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:01):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:01):

we could just make a structure

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:02):

hmm

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:02):

let me fire up lean

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:02):

that's better

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:03):

I am so rubbish at structures

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:03):

aah bingo

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:03):

it's not a structure

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:03):

it's an inductive type

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:03):

inductive pnat
| one : pnat
| succ : pnat  pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:03):

So there's pnat

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

and that would work

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

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

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

and do all that stuff again

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

and that's stuff we already did with nat

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

and that's kind of a waste

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:05):

Ok so it's in mathlib

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:05):

which means that computer scientists are not interested in this structure

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:05):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:06):

let's find it on github

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:06):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:06):

There it is.

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:06):

Last modified two days ago!

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:06):

Things never stand still around here

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:07):

and the first thing we notice

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:07):

is that on line 1

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:07):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:07):

they define it as a _subtype_

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:07):

which is a bit more annoying to use in practice

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

oh wait I skipped a line

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

import tactic.basic

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

And there it is.

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

There are sets {x | blah}

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

and there are subtypes {x // blah}

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:08):

this one is a subtype

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:09):

don't mind me I'm just editing mathlib

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:09):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:09):

but I know the answer

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:10):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:10):

1) a nat

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:10):

2) a proof that it's positive

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:10):

(that's > 0 for you French speakers)

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:10):

so here's an example

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:11):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:11):

that didn't go well

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:11):

I was in the middle of defining 59

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:11):

and all of a sudden I needed a proof.

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:11):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:12):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:12):

Ok that went better

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:12):

and now I can finally make my pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:13):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:13):

notation `ℕ+` := pnat

instance coe_pnat_nat : has_coe ℕ+  := subtype.val

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:13):

Those are the next couple of lines

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:14):

this sort of thing is a minefield

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:15):

ℕ+ will do

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:15):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:15):

ℕ^*

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:15):

because we are already finished with the structure

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:15):

Submit a PR Patrick

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

The thing that mathematicians don't realise

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

or at least that I didn't realise at all

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

(I suspect Patrick knew full well)

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

was that it's not just about making the structure

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:17):

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

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:17):

that not only did they design a function for it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:17):

but they made it into a coercion

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:17):

which means "it happens magically"

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

Aah I see what to do

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

I have mathlib pnat open

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

and a copy of it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

and I edit the copy

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

great

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

so let's see if we can understand this coercion

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

and then let's see it happen

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:18):

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

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

instances are something I never understood

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

coercions not really either

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

and then those dreaded pointy brackets

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

and then an incomprehensible subtype.val

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

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

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

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

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

so we can work out what this line does

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:20):

and then selecting "go to definition"

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:20):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:20):

and we see

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:20):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:21):

and pnat, the positive naturals, was a subtype

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:21):

in fact if we switch notation off and look at pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:21):

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

set_option pp.notation false
#print pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:22):

we see

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:22):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:22):

eew

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:22):

gt is >

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:22):

so indeed we see a function nat to Prop

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:22):

sending n to "n > 0"

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:24):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:24):

to its value

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:24):

which is 59

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:24):

and we made it a coercion using coercion instance magic

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:25):

so that means it should happen naturally

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:25):

Ok it works!

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:26):

it would be better if you could see me typing

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:26):

that would save me having to cut and paste

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:26):

how do I do that?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:26):

Did someone say youtube ?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:26):

Does twitch take this sort of stuff?

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

I have done all manner of weird things on twitch

view this post on Zulip Patrick Massot (May 29 2018 at 19:27):

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

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

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

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

so back to the point

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

a miracle occurred!

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

A contradiction in type theory!

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

x had type pnat

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

and type nat

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

as well

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

but actually what happened was that coercion kicked in

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

The output of the second check was ↑x : ℕ

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

and that arrow (which you get with \u)

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

means "I got coerced!"

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

so that has solved our first fundamental problem

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

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

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

and hence every pnat _is_ a nat

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

They don't have it so easy in DTT

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

so we are stuck with the cute little arrows

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

let's press on

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

The next line is clever

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:30):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:30):

That's using a really cool piece of Lean functionality

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:30):

...which breaks if I remove that import line

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:30):

so that's why the import is there

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:31):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:31):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:31):

there's something in the manual about this

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:31):

you can do pp.no_cute_arrows Patrick?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:32):

here we are

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:32):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:32):

set_option pp.coercions false

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:32):

does that mean Lean doesn't do them?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:32):

or just doesn't print the arrows?

view this post on Zulip Patrick Massot (May 29 2018 at 19:32):

doesn't print

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:32):

thought so :-)

view this post on Zulip Patrick Massot (May 29 2018 at 19:32):

hence the pp

view this post on Zulip Johan Commelin (May 29 2018 at 19:32):

pp means "pretty print"

view this post on Zulip Patrick Massot (May 29 2018 at 19:32):

meaning pretty print

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:33):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:33):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:33):

class.instance_max_depth

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:33):

"run a tactic to make the argument for you"

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:33):

Patrick: touch\'e

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:33):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:34):

Let's see this tactic in action

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:35):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:35):

It works!

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:35):

so I'm not going to do that

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:35):

but I know what is going on

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:35):

in fact there's a shorter way of doing it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:35):

theorem H : 59 > 0 := dec_trivial

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:36):

(not a tactic, so no by this time)

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:37):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:37):

theorem H1 : 0 > 0 := dec_trivial

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:37):

doesn't work

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:37):

so let's see to_pnat in action!

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

definition y : pnat := to_pnat 12

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

that's much better than what we had before

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

definition z : pnat := to_pnat 0

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

you get some weird error

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

OK so let's press on

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:38):

this one looks easy.

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:39):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:39):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:39):

we can check that easily

view this post on Zulip Mario Carneiro (May 29 2018 at 19:39):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 19:40):

but you can prove the negation using dec_trivial

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:40):

variable (n : )
#check succ_pos n

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:40):

succ_pos n : 0 < succ n

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:41):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:41):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:42):

but what do we need to do next?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:42):

This is the question that I as a mathematician find hard

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:42):

and I think that people like Mario just somehow know

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:42):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:42):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:43):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:43):

and Lean coerces the left hand side

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:43):

so if you think about it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:43):

when you unravel it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:43):

that theorem just says succ n = succ n

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:43):

so the proof is rfl

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:44):

but this one got lucky

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:44):

it got a name

view this post on Zulip Mario Carneiro (May 29 2018 at 19:44):

it's a simp lemma, those need names

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:44):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:44):

NOTE FOR BEGINNERS

view this post on Zulip Mario Carneiro (May 29 2018 at 19:44):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 19:45):

rfl proofs are very common

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:45):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:45):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:45):

because that would be a comp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:45):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

x = y and y = x mean the same thing

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

and even if simp does not use your lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

imagine when you're doing a rewrite

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

you are trying to prove something

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:46):

so you're usally trying to make stuff easier

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:47):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:47):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:47):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:47):

or else you should have proved y = x

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

Next line

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

that looks like really poor Lean to me

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

who wrote this file anyway

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

oh I heard of that guy

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

Now everyone knows that simp is used to prove _equalities_

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

so all your simp lemmas should be _equalities_

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

or _iff_s

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:48):

and anything which is a random thing like >

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:49):

obviously should not be a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:49):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:49):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:49):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:49):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:50):

but apparently there are other times when it's not

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:50):

Interesting point Patrick I guess you're right

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:50):

Maybe 0 is a special case

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

view this post on Zulip Mario Carneiro (May 29 2018 at 19:50):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:51):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:51):

Now look at these

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:52):

I did that a lot when I started

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:52):

but its full name is pnat.ne_zero

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:52):

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

view this post on Zulip Johan Commelin (May 29 2018 at 19:52):

So, why is theorem eq not a simp theorem?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:52):

so that's why we opened the pnat namespace

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:53):

we namespaced

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:53):

and we opened nat for good measure

view this post on Zulip Mario Carneiro (May 29 2018 at 19:53):

because the RHS has a variable not on the LHS

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:53):

So theorem eq says a fundamental thing about subtypes.

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

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:54):

What RHS variable?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:54):

And yes they are, because all proofs are the same

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:54):

so that's why pnat.eq is true

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:54):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:54):

or right click on ir

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:54):

it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:55):

or #check it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:55):

Oh I know why eq isn't a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:55):

it's not an equality

view this post on Zulip Mario Carneiro (May 29 2018 at 19:55):

m = n is not a simplification

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:55):

it's an implication

view this post on Zulip Mario Carneiro (May 29 2018 at 19:55):

and where is n coming from?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:55):

aah

view this post on Zulip Mario Carneiro (May 29 2018 at 19:55):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:55):

There's another simp rule of thumb

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:56):

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

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:56):

why this rule?

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:56):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 19:56):

It's an extensionality theorem

view this post on Zulip Mario Carneiro (May 29 2018 at 19:57):

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

view this post on Zulip Patrick Massot (May 29 2018 at 19:57):

should it be tagged as such?

view this post on Zulip Mario Carneiro (May 29 2018 at 19:57):

probably

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

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:57):

because you wanted to prove complicated structures were equal

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:58):

I think this sort of thing is an art

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:58):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 19:58):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 19:58):

the goal got more complicated

view this post on Zulip Mario Carneiro (May 29 2018 at 19:58):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:58):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:58):

then you might well not want it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:59):

but if m was explicitly <nat,proof>

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:59):

and so was n

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:59):

then you might want it

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:59):

(but you might not)

view this post on Zulip Johan Commelin (May 29 2018 at 19:59):

Hmm, fair enough

view this post on Zulip Mario Carneiro (May 29 2018 at 19:59):

and that version is a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:59):

ooh my son's gone

view this post on Zulip Kevin Buzzard (May 29 2018 at 19:59):

I just inherited a second screen

view this post on Zulip Johan Commelin (May 29 2018 at 19:59):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:00):

Ok so mk_coe

view this post on Zulip Johan Commelin (May 29 2018 at 20:00):

Or is it a simp lemma for general subtypes?

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

view this post on Zulip Johan Commelin (May 29 2018 at 20:00):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:00):

subtype.mk_eq_mk

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:00):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:00):

it's a general simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:00):

Actually there are several cool things about mk_coe

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:01):

hmm

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:01):

maybe that's not entirely true

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:01):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:01):

They're definitionally equal, right?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:02):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:02):

it's a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:02):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:02):

The val version is automatic, because simp knows about structures

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:02):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:02):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:02):

oh so simp doesn't need to be told that

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:02):

the thing I wrote

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:02):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:03):

right

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:03):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:03):

I saw the definition of pnat in a maths lecture

view this post on Zulip Mario Carneiro (May 29 2018 at 20:03):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:03):

it was "take nat and remove 0"

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:03):

and that was it

view this post on Zulip Mario Carneiro (May 29 2018 at 20:03):

but it probably won't trigger

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:03):

There is all this extra stuff here

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:04):

We want add on pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:04):

and here's something I only learnt recently

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:04):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:04):

is notation

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:05):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:05):

although probably one could have called it pnat.add

view this post on Zulip Mario Carneiro (May 29 2018 at 20:05):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:05):

Oh I didn't know that -- thanks

view this post on Zulip Mario Carneiro (May 29 2018 at 20:05):

pnat.add would be the name of the function itself

view this post on Zulip Mario Carneiro (May 29 2018 at 20:05):

if it had a name

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:05):

Oh of course

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:06):

The function is add

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:06):

and the proof that it has an add is something else

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:06):

actually it's not a proof

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:06):

it's data

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:06):

and we cheat and look at what Mario did

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:07):

and why is the output from #check so ugly?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:07):

#check add_pos

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:07):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:07):

thanks Lean

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:07):

#check @add_pos

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:08):

not ideal either

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:08):

I would have preferred

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:08):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:08):

but unsurprisingly

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:08):

it's the lemma we need

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:09):

Now these should be straightforward

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:09):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:09):

we have to carry around all these proofs

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:09):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:10):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:10):

and it would not surprise me if that were called ne_of_gt

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:10):

and note that

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:10):

n.2 is the proof

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:10):

that n > 0

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:11):

it's n.property

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:11):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:11):

nat_coe_coe

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:11):

I have no idea why this is a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:11):

I guess I do know

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:11):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

"and then we get some serious simplification"

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

I am kind of surprised this works

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

we coerce a nat to a pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

that doesn't even make sense

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

oh crap

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

I am looking at an old version of pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:12):

rofl

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:13):

I'm now looking at the up to date version

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:13):

and that line is gone :-)

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:13):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:14):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:14):

Ok great

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:15):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:15):

Ok so this looks good

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:15):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:15):

and this is not rfl

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

indeed it's not even true

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

it's false for n=0

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

but we have the hypo n > 0

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

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

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

and that would be called something like succ_pred_eq_of_pos

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

which it indeed is

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

Ok nearly there

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

oh one more simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

you see this is exactly what I don't get

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

We have just proved 10 trivial things

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:17):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

look!

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

We just proved n = n again

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:17):

let's make it a simp lemma!

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:18):

to_pnat' is a bit funny isn't it

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:18):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:18):

sends n to n if n is positive

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:18):

and 0 to 1

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:19):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:19):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:19):

and perhaps in this particular case they're right

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

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

exactly

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

Now here's a meaty bit of file

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

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

it's a commutative monoid!

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:21):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:21):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:21):

outside the monoid

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:21):

and I would have done has_one pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:21):

Mario -- does your pnat have a mul?

view this post on Zulip Mario Carneiro (May 29 2018 at 20:21):

yes, it's right there

view this post on Zulip Mario Carneiro (May 29 2018 at 20:22):

comm_monoid implies has_mul

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:23):

If I type #print comm_monoid

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:23):

I can't see this

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:23):

Or have I misunderstood?

view this post on Zulip Mario Carneiro (May 29 2018 at 20:23):

comm_monoid extends monoid which extends semigroup which extends has_mul

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:24):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:24):

but you had to know that

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:24):

I could have written comm_monoid in a different way

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:24):

and it would have _looked_ like there was a mul

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:24):

but you wouldn't have got the notation

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:25):

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

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

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:25):

you already have the notation

view this post on Zulip Mario Carneiro (May 29 2018 at 20:25):

after that instance

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:26):

after making it a commutative monoid

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:26):

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

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:26):

with your #check

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:26):

if you had wanted to know before writing the code

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:26):

you would have had to read Lean source code

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

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

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

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

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

exactly

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

You had to rely on someone else being sensible

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

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:28):

But you didn't get Lean to tell you

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

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

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

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

It is important that has_mul be declared only once though

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

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

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

only tricky2 gets the notation, yes

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

but your method for checking this fails

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

because you can't make any instances

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

#check (by apply_instance : has_mul ℕ+)

view this post on Zulip Kenny Lau (May 29 2018 at 20:30):

sorry, you can

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

your method relied on pnat existing

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

show me Kenny :-)

view this post on Zulip Kenny Lau (May 29 2018 at 20:30):

just sorry everything

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

Fair enough

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:30):

even mul?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:31):

(deleted)

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:31):

I seem to have wandered a bit

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:32):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:32):

why don't we just go with mul_pos

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:32):

and indeed that's what it is

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:32):

naming is an art

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:32):

and it's another thing mathematicians are bad at

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:32):

The only training we get

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:33):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:33):

from our teachers

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:33):

There you go

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:33):

couldn't be easier

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:34):

Now

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:34):

how are we going to prove all these stupid axioms?

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:34):

mul_assoc -- that's already proved for nats

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:34):

as is mul_comm

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:35):

so here we see the benefits

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:35):

was subtype.eq a simp lemma?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

oh no

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

of course not

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

it has an implies

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

all the proofs are the same

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:36):

whereas I suspect Mario wrote them

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

view this post on Zulip Patrick Massot (May 29 2018 at 20:37):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:37):

true

view this post on Zulip Patrick Massot (May 29 2018 at 20:37):

This situation looks like what Simon solve for pi instances

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:37):

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

view this post on Zulip Patrick Massot (May 29 2018 at 20:38):

Where is Simon by the way?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:38):

he's cool -- don't underestimate him

view this post on Zulip Patrick Massot (May 29 2018 at 20:38):

Haven't we lost him?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:38):

All that's left is one

view this post on Zulip Mario Carneiro (May 29 2018 at 20:38):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:38):

there is a balance point there

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:38):

I don't think it matters

view this post on Zulip Mario Carneiro (May 29 2018 at 20:38):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:39):

I think every method will produce basically the same term

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:39):

All that's left is this:

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:40):

one_coe -- who knows why this is a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:40):

Where does it end

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:40):

two_coe? Why is that not a simp lemma?

view this post on Zulip Mario Carneiro (May 29 2018 at 20:40):

because that's not an atomic term

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:40):

mul_coe -- proof is refl

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:40):

Oh I see

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:41):

one just _became_ an atomic term

view this post on Zulip Mario Carneiro (May 29 2018 at 20:41):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:41):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:41):

and finally power

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:42):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:42):

how new-fangled and fancy

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:42):

it wasn't like this when I learnt it

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:42):

#print notation ^

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:42):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:43):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:43):

and if this was me 6 months ago

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:43):

I would think "oh I quite fancy this one"

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:43):

"induction on n should do it"

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:43):

and I'd prove it

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

but that's not the way to think about Lean

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

the way to think about it is

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

and even if they didn't

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

maybe some obsessive mathlib guy thought of it

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:44):

and maybe they gave it a name

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:45):

and maybe it's someething like pos_pow_of_pos

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:45):

This is the way to write Lean

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:45):

don't write the code because you can

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:45):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:45):

write nat.pos_pow and hit ctrl-space

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:45):

and see if you get lucky

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:46):

note that Mario used m.pos not m.2

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:46):

That might just be for readability

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:46):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:47):

but m.pos is basically better

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:47):

because it's more readable

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:47):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:47):

I'm sure it's just inconsistency

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:47):

But you are making an interface for pnat

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:47):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:48):

which you should encourage the users to use

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:48):

It literally makes no difference to anything?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:48):

Doesn't it increase compile time by a zillisecond?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:48):

you had to look up pos in some table

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:49):

Let me think epsilon more about poe

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:49):

pow

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:49):

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

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

view this post on Zulip Mario Carneiro (May 29 2018 at 20:49):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:50):

They are thinking "yay we now have pow"

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:50):

but then immediately after

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:50):

they think "OK I now have some obligations"

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:51):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:51):

which we've seen lots of times before

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:51):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:51):

and even though the proof is refl

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:51):

this looks like it should be a simp lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:52):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:52):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

to prove it lands in pnat we prove a lemma

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

and that's the end

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

We stop here:

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

We don't do this bit

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:53):

but in CS if you don't do this

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:54):

even though we only care about nats now

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:54):

in fact did we prove all the coercions?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:54):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:54):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:54):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:55):

They all got proved

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:55):

and then I made it a nat

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:55):

then simp would remove all the pnats for me?

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:55):

I think it might!

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:56):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:57):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:57):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:57):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:57):

you just use variables to make stuff

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:58):

rofl

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:59):

I need to work harder

view this post on Zulip Kevin Buzzard (May 29 2018 at 20:59):

dammit

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:00):

doesn't typecheck yet

view this post on Zulip Mario Carneiro (May 29 2018 at 21:00):

Note that A and B are the same

view this post on Zulip Mario Carneiro (May 29 2018 at 21:00):

You should use parameters instead

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:00):

for a b c

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:00):

what about the proofs?

view this post on Zulip Mario Carneiro (May 29 2018 at 21:00):

all six

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:01):

Parameters can only be used in a section

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:02):

and this typechecks

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:02):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:02):

maybe that's something I could mention

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:02):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

but I am happy with plenty of sorrys

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

green squiggly underlines ftw

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

the reason for this

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

is that if you make an error

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

and you might not notice it if they're everywhere

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

so every time I split in tactic mode

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:03):

I always put in two sorrys

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:04):

etc etc

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:04):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:04):

that's not surprising

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:04):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:04):

that's not surprising

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:04):

why did he make all these rfl things simp lemmas?

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:05):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:05):

fails :-)

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:05):

doh

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:05):

aah well so it was probably for another reason

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

view this post on Zulip Mario Carneiro (May 29 2018 at 21:06):

You have to unfold your new definitions

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

view this post on Zulip Mario Carneiro (May 29 2018 at 21:06):

try by simp [A, B, C]

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:07):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:07):

simp [A,B,C]?

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:07):

Is A a good simp lemma??

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:08):

well blow me down it works

view this post on Zulip Mario Carneiro (May 29 2018 at 21:08):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:09):

ooh

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:09):

How do I see A's equation lemmas?

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:09):

#print prefix A

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:09):

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:10):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 21:10):

not by default, no

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:10):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 21:10):

Actually they appear on the left too

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:10):

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

view this post on Zulip Mario Carneiro (May 29 2018 at 21:10):

they are hidden because of the parameter thing

view this post on Zulip Mario Carneiro (May 29 2018 at 21:11):

or possibly because you have {a} {ha}

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:11):

heh

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:11):

I think the latter

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:11):

Ok so we got there

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:12):

and that's pnat.

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:12):

Oh that would be a cool application of pnat

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:12):

I need to go to tend to the family

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:12):

but there's a random thing

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:12):

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

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

view this post on Zulip Kevin Buzzard (May 29 2018 at 21:13):

and it was much easier to write than a proper document

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