## Stream: maths

### Topic: ZFC equality

#### Kevin Buzzard (May 28 2018 at 09:31):

There were a couple of times in the schemes project when I really had to think "beyond ZFC" -- I had to write down a map, and there were two ways of doing it, and in ZFC they were the literally the same way but in Lean they were different. In this example I just chose a random Lean route to model my ZFC thoughts and it got me in to real trouble later.

#### Kevin Buzzard (May 28 2018 at 09:32):

Here's a naive definition of the image of a morphism in ZFC, translated seamlessly into Lean:

#### Kevin Buzzard (May 28 2018 at 09:32):

import data.set

-- ZFC-safe! The below code uses only Prop and Type

variables {X Y : Type} (f : X → Y) (U : set X)

definition image := {y : Y | ∃ x ∈ U, f x = y}


#### Kevin Buzzard (May 28 2018 at 09:33):

And now here's something which doesn't work

#### Kevin Buzzard (May 28 2018 at 09:33):

theorem they_are_not_defeq : image (@id X) U = U := rfl -- fails

#### Kevin Buzzard (May 28 2018 at 09:33):

Does that mean that my definition of image is wrong?

#### Kevin Buzzard (May 28 2018 at 09:33):

Or is there literally no way to make that happen in dependent type theory

#### Kenny Lau (May 28 2018 at 09:34):

they are definitely not defeq

#### Kenny Lau (May 28 2018 at 09:34):

you see, a set is nothing more than a function to Prop

#### Kevin Buzzard (May 28 2018 at 09:34):

Is that because I am bad at writing the image function?

#### Kevin Buzzard (May 28 2018 at 09:34):

Can you write a better one for me

no, it isn't

#### Kevin Buzzard (May 28 2018 at 09:34):

where they are defeq

you can't

#### Kenny Lau (May 28 2018 at 09:34):

you have to have an existential quantifier

#### Kevin Buzzard (May 28 2018 at 09:34):

can you prove that you can't?

in Lean

3.4.1

not in lean

#### Mario Carneiro (May 28 2018 at 09:35):

it's a metatheorem

Great.

#### Kenny Lau (May 28 2018 at 09:35):

@Mario Carneiro can it actually be proved?

probably

#### Kevin Buzzard (May 28 2018 at 09:35):

Well you know what

#### Kevin Buzzard (May 28 2018 at 09:35):

I think defeq is rubbish

#### Kevin Buzzard (May 28 2018 at 09:35):

because those two sets are equal

#### Kenny Lau (May 28 2018 at 09:36):

f(x) = x^2 and f(x) = x^2+1-1 are equal

#### Kevin Buzzard (May 28 2018 at 09:36):

and mathematicians have been thinking of those sets as equal since they started formalizing mathematics

#### Kenny Lau (May 28 2018 at 09:36):

but not definitionally equal

#### Kevin Buzzard (May 28 2018 at 09:36):

so what has gone wrong?

nothing is wrong

#### Mario Carneiro (May 28 2018 at 09:36):

defeq is not ZFC equality

#### Kevin Buzzard (May 28 2018 at 09:36):

Kenny -- the ZFC analogues of the two concepts U and image id U are identical

#### Kevin Buzzard (May 28 2018 at 09:37):

I mean equal in the purest form

are they?

#### Kevin Buzzard (May 28 2018 at 09:37):

they are indistinguishable with the tools of ZFC

#### Mario Carneiro (May 28 2018 at 09:37):

no, there is more to prove under one definition than the other in ZFC

#### Kenny Lau (May 28 2018 at 09:37):

the latter is { y in U | exists x, x = y }

#### Kevin Buzzard (May 28 2018 at 09:37):

In ZFC they are the same object

#### Mario Carneiro (May 28 2018 at 09:37):

in lean they are the same object

#### Kenny Lau (May 28 2018 at 09:37):

sure, but they aren't equal by definition

#### Kenny Lau (May 28 2018 at 09:37):

they are equivalent

#### Kenny Lau (May 28 2018 at 09:37):

exists x, x = y is equivalent to true

#### Kevin Buzzard (May 28 2018 at 09:38):

How is one supposed to prove that stupid lemma anyway?

#### Mario Carneiro (May 28 2018 at 09:38):

ext (by simp)

I would guess

#### Mario Carneiro (May 28 2018 at 09:38):

actually it's probably already a theorem

#### Kevin Buzzard (May 28 2018 at 09:39):

-- What actually happens in my head when proving the lemma id(U) = U for sets in Lean.

import data.set

-- ZFC-safe! The below code uses only Prop and Type
-- (I didn't check the imports though)
variables {X Y : Type} (f : X → Y) (U : set X)

definition image := {y : Y | ∃ x ∈ U, f x = y}

theorem are_they_equal : image (@id X) U = U := begin
/-
why am I wasting my time proving this stupid theorem. These
objects are ZFC-equal and thus equal. I will not even try.
-/
-- rfl, -- fails
-- simp, -- fails -- *rolls eyes*
-- finish, -- I don't even understand what this one does but it sometimes works
-- cc (see comment above)
-- dsimp -- thought unlikely but maybe worth trying
-- can't think of any more tactics
unfold image,
apply set.eq_of_subset_of_subset,
{ intros x Hx,
simpa using Hx},
{ intros x Hx,
simpa using Hx,
}
-- thank goodness it's over
end


#### Kevin Buzzard (May 28 2018 at 09:39):

That's what actually happened

#### Mario Carneiro (May 28 2018 at 09:39):

set.image_id

#### Mario Carneiro (May 28 2018 at 09:39):

why are you proving trivial set theorems?

#### Kevin Buzzard (May 28 2018 at 09:39):

It's hard for me to prove that ZFC-equal things are equal

#### Kevin Buzzard (May 28 2018 at 09:40):

because the tools I have honed in my brain to solve these problems

are ZFC tools

#### Mario Carneiro (May 28 2018 at 09:40):

that theorem is just as hard in zfc land

#### Kevin Buzzard (May 28 2018 at 09:40):

and here for some reason ZFC tools are not adequate

#### Mario Carneiro (May 28 2018 at 09:40):

the proof is literally no different

#### Kevin Buzzard (May 28 2018 at 09:41):

why does simp fail?

#### Kevin Buzzard (May 28 2018 at 09:41):

This proof is simple

#### Kenny Lau (May 28 2018 at 09:41):

@Mario Carneiro I tell you, when a mathematician says they work in ZFC, they actually don't. They won't even be able to name all of the ZFC axioms.

#### Kevin Buzzard (May 28 2018 at 09:41):

That's true for a general mathematician

#### Mario Carneiro (May 28 2018 at 09:41):

I can tell you I have worked in ZFC

#### Kevin Buzzard (May 28 2018 at 09:41):

but I know the axioms of ZFC and I've been working happily in it for years

like for real

#### Kevin Buzzard (May 28 2018 at 09:42):

You mean "not using pen and paper"

#### Kenny Lau (May 28 2018 at 09:42):

example {α : Type*} (s : set α) : id '' s = s :=
set.ext (by simp [-set.image_id])


#### Mario Carneiro (May 28 2018 at 09:42):

I've done ZFC with pen and paper too, but that gets old fast

#### Kevin Buzzard (May 28 2018 at 09:42):

I guess LaTeX is the true home of ZFC.

For most people.

#### Andrew Ashworth (May 28 2018 at 09:43):

... isn't metamath basically zfc on pen and paper

#### Kevin Buzzard (May 28 2018 at 09:43):

OK so I think dependent type theory is stupid and I've decided to go back to ZFC and formulate perfectoid spaces there instead where I don't have to waste my time worrying about whether or not id U is equal to U.

#### Kevin Buzzard (May 28 2018 at 09:43):

So where do I start?

#### Kevin Buzzard (May 28 2018 at 09:44):

if I want to do it on a computer

#### Kenny Lau (May 28 2018 at 09:44):

I thought Isabelle works in ZFC

#### Kevin Buzzard (May 28 2018 at 09:44):

I don't even know what Isabelle is

#### Mario Carneiro (May 28 2018 at 09:44):

It uses HOL for all the good stuff

#### Kevin Buzzard (May 28 2018 at 09:44):

so Isabelle-ZFC is a thing?

#### Mario Carneiro (May 28 2018 at 09:44):

Isabelle/ZFC is more of a proof of concept

#### Kevin Buzzard (May 28 2018 at 09:44):

that doesn't sound good

#### Kevin Buzzard (May 28 2018 at 09:44):

does it have number fields?

#### Kenny Lau (May 28 2018 at 09:45):

and secondly, nobody works in ZFC. they work in ZFC + definitorial expansion

#### Mario Carneiro (May 28 2018 at 09:45):

If you want to really use ZFC on the computer, you should use Mizar or Metamath

#### Kevin Buzzard (May 28 2018 at 09:45):

Why not Isabelle-ZFC?

#### Mario Carneiro (May 28 2018 at 09:45):

because it is not mature enough

#### Mario Carneiro (May 28 2018 at 09:45):

maybe mature is the wrong word, it's been around for a while but it doesn't have enough theorems

#### Kevin Buzzard (May 28 2018 at 09:45):

Which of the three possibilities for computer-ZFC is most mathematician-friendly?

#### Kevin Buzzard (May 28 2018 at 09:46):

Or is it a case of "learn one of them, you just learned all of them"

I have no idea

#### Kevin Buzzard (May 28 2018 at 09:46):

I just play ZFC internally on my own emulator

#### Mario Carneiro (May 28 2018 at 09:46):

Mizar was written by mathematicians for mathematicians

#### Mario Carneiro (May 28 2018 at 09:46):

this is not necessarily a good thing

In ZFC

in TG set theory

#### Kevin Buzzard (May 28 2018 at 09:47):

If ZFC and DTT had a race to perfectoid spaces, and you could choose your foundational system, and we started tomorrow, who would win?

#### Mario Carneiro (May 28 2018 at 09:47):

ZFC is an axiom system not a program

#### Kevin Buzzard (May 28 2018 at 09:47):

I am not CS-wise enough to understand the difference

#### Kevin Buzzard (May 28 2018 at 09:47):

I want a program whose only commands are things allowed in ZFC

#### Kevin Buzzard (May 28 2018 at 09:48):

and all things allowed in ZFC are commands

#### Mario Carneiro (May 28 2018 at 09:48):

You aren't choosing ZFC or DTT, you're choosing Mizar or Lean or Coq or Isabelle

#### Kevin Buzzard (May 28 2018 at 09:48):

Does this make sense -- "I choose Mizar, and therefore I choose ZFC"

sure

#### Kevin Buzzard (May 28 2018 at 09:48):

I don't know what Mizar is

#### Kevin Buzzard (May 28 2018 at 09:48):

but I do know what ZFC is

#### Kevin Buzzard (May 28 2018 at 09:48):

And "I choose Lean, and therefore I choose dependent type theory"

#### Mario Carneiro (May 28 2018 at 09:49):

right, lean doesn't give you a choice here

#### Mario Carneiro (May 28 2018 at 09:49):

same with most other systems

#### Kevin Buzzard (May 28 2018 at 09:49):

So who would win the perfectoid space showdown between Lean and "insert computer program which models ZFC in some way"

#### Kevin Buzzard (May 28 2018 at 09:50):

If I got cloned into two people and just had a race with myself

#### Mario Carneiro (May 28 2018 at 09:50):

Isabelle and Metamath are a bit special since they are foundational frameworks, so you can technically pick your favorite axiom system, but in practice all the theorems go to one particular axiom system

#### Mario Carneiro (May 28 2018 at 09:50):

If you got cloned? Lean of course

#### Kevin Buzzard (May 28 2018 at 09:50):

Are there more mathematical theorems in Mathlib than in any library for any ZFC system?

#### Mario Carneiro (May 28 2018 at 09:51):

because you know lean better than any other system

#### Kevin Buzzard (May 28 2018 at 09:51):

But Mario, I speak fluent ZFC

#### Mario Carneiro (May 28 2018 at 09:51):

and you will find that it doesn't matter

#### Kevin Buzzard (May 28 2018 at 09:51):

It's my native language

#### Mario Carneiro (May 28 2018 at 09:51):

because you will be struggling with formal details the whole way

#### Mario Carneiro (May 28 2018 at 09:51):

that's always the way it goes

#### Kevin Buzzard (May 28 2018 at 09:51):

I think this is precisely the point I don't understand

#### Kevin Buzzard (May 28 2018 at 09:52):

let me rephrase that -- the distinction between "Lean" and "Dependent type theory" is quite blurred in my mind

#### Kevin Buzzard (May 28 2018 at 09:53):

I thought I could just define dependent type theory to be Lean

#### Kenny Lau (May 28 2018 at 09:53):

it's one thing to know the theory behind Python

#### Kenny Lau (May 28 2018 at 09:53):

it's a completely other thing to use Python

I guess

#### Kevin Buzzard (May 28 2018 at 09:53):

I completely understand that

I see

#### Kevin Buzzard (May 28 2018 at 09:54):

But this is a really easy problem

#### Kevin Buzzard (May 28 2018 at 09:54):

I just get the CS people to write python for me

#### Kevin Buzzard (May 28 2018 at 09:54):

so they are the same thing

#### Kevin Buzzard (May 28 2018 at 09:54):

Now who wrote ZFC for me?

#### Mario Carneiro (May 28 2018 at 09:54):

but you don't want ZFC, not really

I love ZFC Mario

#### Mario Carneiro (May 28 2018 at 09:55):

you want by schoolkid and tactics and magic

#### Kevin Buzzard (May 28 2018 at 09:55):

Yeah and we _need_ schoolkid

#### Mario Carneiro (May 28 2018 at 09:55):

ZFC is an axiom system, it made no magical promises

#### Kevin Buzzard (May 28 2018 at 09:55):

no but you CS guys will just sort all that out

#### Kevin Buzzard (May 28 2018 at 09:55):

that's just some stupid engineering issue

#### Kevin Buzzard (May 28 2018 at 09:55):

I want to do ZFC, like I do Python in Python

#### Mario Carneiro (May 28 2018 at 09:55):

but it's a really important engineering issue for you

#### Kenny Lau (May 28 2018 at 09:55):

@Kevin Buzzard how would you prove in ZFC that id '' U = U?

#### Mario Carneiro (May 28 2018 at 09:56):

I dare say it's far more important than the underlying axiom system

#### Kevin Buzzard (May 28 2018 at 09:56):

id(u) is the same as u

no they aren't

sure it is

#### Kenny Lau (May 28 2018 at 09:56):

how would you prove it?

#### Mario Carneiro (May 28 2018 at 09:56):

that's not a proof

#### Kevin Buzzard (May 28 2018 at 09:56):

id is a big set of ordered pairs

#### Kevin Buzzard (May 28 2018 at 09:56):

and they're all just (u,u)

a proper class

no it's a set

don't be silly

wha...

ok

#### Kevin Buzzard (May 28 2018 at 09:57):

it's a function from U to U

#### Kenny Lau (May 28 2018 at 09:57):

but here it isn't

ZFC warning

#### Kenny Lau (May 28 2018 at 09:57):

it's a function from alpha to alpha, U is just a subset

#### Kevin Buzzard (May 28 2018 at 09:57):

but here is stupid. I'm telling you the right way.

#### Mario Carneiro (May 28 2018 at 09:57):

that's doing to make your job messy

#### Kevin Buzzard (May 28 2018 at 09:57):

so id(u) is equal to u OK

#### Kevin Buzzard (May 28 2018 at 09:57):

so {id(u) : u in U}

EQUALS

{u : u in U}

which

#### Kenny Lau (May 28 2018 at 09:57):

so id(u) is equal to u OK

you still haven't proved it. what after id being a big set of pairs

EQUALS

U

#### Kevin Buzzard (May 28 2018 at 09:58):

I don't understand which bit I missed

#### Kenny Lau (May 28 2018 at 09:58):

you're abusing notations.

oh

#### Mario Carneiro (May 28 2018 at 09:58):

yes, you unfold the definitions, that {id(u) : u in U} thing becomes {y : \ex u, id(u) = y}

#### Kenny Lau (May 28 2018 at 09:58):

{u : u in U} isn't equal to {u in U | true}

#### Kevin Buzzard (May 28 2018 at 09:58):

I thought I was using "=" as in the underlying logic or syntax or whatever it's called of ZFC or logic or

#### Kenny Lau (May 28 2018 at 09:58):

you mixed comprehension notation and subset notation

#### Kevin Buzzard (May 28 2018 at 09:58):

I am not clear about what = is in ZFC

#### Kevin Buzzard (May 28 2018 at 09:58):

I forgot the details

#### Mario Carneiro (May 28 2018 at 09:58):

and then you have a lemma proving that id(u) = u since (u,u) in id

#### Kevin Buzzard (May 28 2018 at 09:58):

but it just means they're the same object

#### Kenny Lau (May 28 2018 at 09:58):

by "isn't equal to" I mean "you haven't proved that they are equal"

#### Mario Carneiro (May 28 2018 at 09:59):

and id is a function because ...

#### Kenny Lau (May 28 2018 at 09:59):

but it just means they're the same object

but it needs to be proved

#### Kenny Lau (May 28 2018 at 09:59):

you can't just say "they must be equal"

#### Kenny Lau (May 28 2018 at 09:59):

you see, the problem is not in the axioms

#### Kenny Lau (May 28 2018 at 09:59):

but in the formality

#### Mario Carneiro (May 28 2018 at 09:59):

and then you get \ex u in U, u = y <-> u in U

#### Mario Carneiro (May 28 2018 at 09:59):

and hey presto it's the lean proof

#### Kevin Buzzard (May 28 2018 at 09:59):

But in the world where proofs are free and can be appealed to at will using good tactics, "simp" would prove this

#### Kenny Lau (May 28 2018 at 10:00):

right, so ZFC isn't the problem at all

#### Mario Carneiro (May 28 2018 at 10:00):

SIMP CAN PROVE THIS

yes

#### Kevin Buzzard (May 28 2018 at 10:00):

because my definition of "simp" is the ZFC tactic "this is simple if you use ZFC"

#### Mario Carneiro (May 28 2018 at 10:00):

That's not a tactic, that's magic

#### Kevin Buzzard (May 28 2018 at 10:00):

I think that's why my understanding of tactics is so poor

#### Kenny Lau (May 28 2018 at 10:00):

example {α : Type*} (s : set α) : id '' s = s :=

#### Kevin Buzzard (May 28 2018 at 10:10):

Tactic State

X : Type,
U : set X
⊢ image id U = U
id_U_equals_U.lean:11:51: error

simplify tactic failed to simplify
state:
X : Type,
U : set X
⊢ image id U = U


#### Kevin Buzzard (May 28 2018 at 10:10):

"by simp" doesn't solve it so "by simp" is broken

#### Kevin Buzzard (May 28 2018 at 10:10):

because it's simple

#### Kevin Buzzard (May 28 2018 at 10:10):

that's all I'm saying

#### Mario Carneiro (May 28 2018 at 10:11):

it has no simp lemmas like the real one

#### Kevin Buzzard (May 28 2018 at 10:11):

you guys are just weirdos

Kevin

#### Mario Carneiro (May 28 2018 at 10:11):

It's like you shot me in the leg and asked why I can't run as fast

#### Kenny Lau (May 28 2018 at 10:11):

have we established that in ZFC you still need to prove it

#### Kevin Buzzard (May 28 2018 at 10:11):

Maybe it's time I tried Mizar.

#### Kevin Buzzard (May 28 2018 at 10:11):

I'll come back with egg on my face later

#### Kenny Lau (May 28 2018 at 10:12):

I don't really see the issue

#### Kenny Lau (May 28 2018 at 10:12):

I think you're misunderstanding

#### Kenny Lau (May 28 2018 at 10:12):

you said it's stupid because they aren't defeq

#### Kevin Buzzard (May 28 2018 at 10:12):

if it's not by simp for some reason

#### Mario Carneiro (May 28 2018 at 10:12):

simp requires a whole library of carefully crafted lemmas to work well

#### Kevin Buzzard (May 28 2018 at 10:12):

then it should be by schoolkid

#### Mario Carneiro (May 28 2018 at 10:12):

because it's not magic

#### Kevin Buzzard (May 28 2018 at 10:12):

How can you claim it works well

#### Kevin Buzzard (May 28 2018 at 10:12):

if it cannot even prove id(U)=U

#### Kevin Buzzard (May 28 2018 at 10:12):

when they're the same object

#### Kevin Buzzard (May 28 2018 at 10:13):

That's what I'm hearing :-)

#### Mario Carneiro (May 28 2018 at 10:13):

you are being unusually stubborn today

#### Kenny Lau (May 28 2018 at 10:13):

1. you said Lean is stupid because id '' U = U isn't rfl. But they also aren't rfl in ZFC, you also need to prove it (remember how you mixed comprehension notation and subset notation)

#### Kevin Buzzard (May 28 2018 at 10:13):

and I know it's not what you're saying

#### Kevin Buzzard (May 28 2018 at 10:13):

but I'm a bit deaf

#### Kenny Lau (May 28 2018 at 10:13):

2. you said Lean is stupid because id '' U = u isn't by simp. But it is.

#### Kevin Buzzard (May 28 2018 at 10:13):

I was just doing my ZFC-baiting thing

#### Kenny Lau (May 28 2018 at 10:13):

3. you said Lean is stupid because id '' U = U isn't ext \$ by simp. But it is.

#### Kenny Lau (May 28 2018 at 10:13):

so I don't know what your issue is

#### Kevin Buzzard (May 28 2018 at 10:14):

by simp doesn't work for me

#### Kevin Buzzard (May 28 2018 at 10:14):

does it work for you?

#### Kenny Lau (May 28 2018 at 10:14):

because you're using the wrong image

#### Kevin Buzzard (May 28 2018 at 10:14):

I'm using the image I wrote

#### Kenny Lau (May 28 2018 at 10:14):

use the official image and everything will be fine

#### Kenny Lau (May 28 2018 at 10:14):

of course your new image doesn't have simp lemmas

#### Kevin Buzzard (May 28 2018 at 10:14):

Wait so didn't lots of people tell me that this was impossible or something?

#### Kenny Lau (May 28 2018 at 10:15):

4. you said Lean is stupid because simp doesn't simplify it with your new image definition. But we already established that it is not a rfl theorem, so you have to use the official image if you want to use a simp lemma

#### Kevin Buzzard (May 28 2018 at 10:15):

that's stupid. What if I can't find the official image so I just make my own image which would then be identical so all the old theorems would work anyway

hmm

no

OK so

#### Kevin Buzzard (May 28 2018 at 10:16):

I can see there might be issues here

#### Kenny Lau (May 28 2018 at 10:16):

@Kevin Buzzard read my point 4 again

at least

#### Kevin Buzzard (May 28 2018 at 10:16):

from an engineering point of view

#### Mario Carneiro (May 28 2018 at 10:16):

the theorems only "work" if you apply them

#### Kenny Lau (May 28 2018 at 10:16):

@Mario Carneiro it doesn't work

No

I'm listening

#### Mario Carneiro (May 28 2018 at 10:17):

yeah, I messed up the copy there

#### Kevin Buzzard (May 28 2018 at 10:17):

I understand that I have to apply my theorems

#### Kenny Lau (May 28 2018 at 10:17):

@Kevin Buzzard so I don't really see where the issue is.

but in return

here's the thing

#### Kenny Lau (May 28 2018 at 10:17):

you're complaining that simp doesn't know about your new image

#### Johan Commelin (May 28 2018 at 10:17):

Kevin, don't think of simp as "simple", but as "simplify"

#### Kevin Buzzard (May 28 2018 at 10:17):

when I prove a theorem that says that A and B are equal

in DTT speak

#### Kevin Buzzard (May 28 2018 at 10:18):

theorem they_are_equal : X = Y := by schoolkid

#### Johan Commelin (May 28 2018 at 10:18):

So, it's not simp's purpose to prove it. But schoolkid or math_trivial should be able to prove it

#### Kevin Buzzard (May 28 2018 at 10:18):

Whenever that happens in dependent type theory

#### Kenny Lau (May 28 2018 at 10:18):

@Kevin Buzzard Kevin.

#### Kevin Buzzard (May 28 2018 at 10:18):

I want dependent type theory to now collapse a little

#### Kenny Lau (May 28 2018 at 10:18):

I think this will convince you.

#### Kenny Lau (May 28 2018 at 10:19):

definition image := {y : Y | ∃ x ∈ U, f x = y}
example : image (@id X) U = U :=
by simp [image]


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

I think you are focusing on the wrong issue Kevin

#### Kenny Lau (May 28 2018 at 10:20):

you broke the silence >_>

#### Johan Commelin (May 28 2018 at 10:20):

So we want schoolkid_1 which just does simp [..every definition preceding it in the file..]

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

There is nothing at all wrong with the proof of id '' U = U, but it caused problems later when you used it as a functor in your presheaf

#### Mario Carneiro (May 28 2018 at 10:22):

For that you need theorems about the action of eq.rec or cast

#### Kevin Buzzard (May 28 2018 at 10:22):

Is this supposed to be rfl?

#### Mario Carneiro (May 28 2018 at 10:22):

and they aren't free, you have to state them

#### Kevin Buzzard (May 28 2018 at 10:22):

theorem X : id '' U = U := sorry

#### Kenny Lau (May 28 2018 at 10:22):

Is this supposed to be rfl?

I thought we already established that it is not rfl

#### Kenny Lau (May 28 2018 at 10:22):

not in ZFC either

#### Kevin Buzzard (May 28 2018 at 10:22):

So that is not rfl

#### Kevin Buzzard (May 28 2018 at 10:22):

but what was rfl?

#### Kenny Lau (May 28 2018 at 10:22):

rfl is using "forall x, x = x"

#### Mario Carneiro (May 28 2018 at 10:22):

schoolkid_1 is simp!

#### Kenny Lau (May 28 2018 at 10:23):

so in ZFC, you need to do reductions to simplify them to the same expression, and then use that axiom

#### Kenny Lau (May 28 2018 at 10:23):

but they can't be reduced to the same thing

#### Mario Carneiro (May 28 2018 at 10:23):

ZFC has no reductions at all

#### Kenny Lau (May 28 2018 at 10:23):

schoolkid_1 is simp!

nope, doesn't work

#### Mario Carneiro (May 28 2018 at 10:23):

In fact rfl is much weaker in ZFC

#### Kenny Lau (May 28 2018 at 10:24):

@Kevin Buzzard you aren't working in ZFC. you are working in ZFC + definition expansion + delta reduction

#### Kevin Buzzard (May 28 2018 at 10:24):

Mario quote

import data.set

-- ZFC-safe! The below code uses only Prop and Type

variables {X Y : Type} (f : X → Y) (U : set X)

theorem they_are_not_defeq : image (@id X) U = U := rfl -- works


Doesn't work for me

#### Mario Carneiro (May 28 2018 at 10:24):

+ equality reflection

#### Kevin Buzzard (May 28 2018 at 10:24):

unknown identifier 'image'

#### Kenny Lau (May 28 2018 at 10:24):

@Kevin Buzzard I really do not see any problem at all. id '' U does not expand to U. you have to destruct the definitions and use extensionality

#### Mario Carneiro (May 28 2018 at 10:24):

I didn't say that

#### Kenny Lau (May 28 2018 at 10:25):

that's what I mean

#### Kevin Buzzard (May 28 2018 at 10:25):

I am just trying to get to the bottom of things

#### Kevin Buzzard (May 28 2018 at 10:25):

but I have never seen refl work for anything

#### Kenny Lau (May 28 2018 at 10:25):

if you need to use the axiom of extensionality to prove that they are equal, then they aren't definitionally equal

#### Kevin Buzzard (May 28 2018 at 10:25):

and I've never seen by simp work either

#### Kenny Lau (May 28 2018 at 10:25):

and i'm working in ZFC to say that

#### Kevin Buzzard (May 28 2018 at 10:25):

but I'm just trying to put everything together

#### Kevin Buzzard (May 28 2018 at 10:25):

it's hard trying to distinguish between equal things

#### Mario Carneiro (May 28 2018 at 10:26):

It's not so hard: id '' U has more words than U, so they aren't the same

#### Mario Carneiro (May 28 2018 at 10:28):

Here's an example of rfl working:

definition image := {y : Y | ∃ x ∈ U, y = f x}

example : image (@id X) U = {y | ∃ x ∈ U, y = x} := rfl


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

that's how definitional expansion is supposed to work

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

this is what ZFC gives you (except you would have to work on id(x) = x in the middle there, that's not definitional in ZFC)

#### Kenny Lau (May 28 2018 at 10:29):

@Kevin Buzzard here's how I can formalize what I say: if you didn't have propext as an axiom, then you won't be able to prove that the two sets are equal, in Lean

#### Kenny Lau (May 28 2018 at 10:30):

the ZFC version replaces propext with the axiom of extensionality

#### Kevin Buzzard (May 28 2018 at 10:31):

import data.set

-- ZFC-safe! The below code uses only Prop and Type

variables {X Y : Type} (f : X → Y) (U : set X)

definition image' := {y : Y | ∃ x ∈ U, f x = y}

theorem they_are_the_same : image' (@id X) U = U := by refl -- fails
theorem they_are_the_same' : id '' U = U := by refl -- fails
theorem they_are_all_the_same_thing_ : id '' U = image' (@id X) U := by refl -- fails
theorem but_they_are_all_the_same : set.image (@id X) U = U := by refl -- fails
theorem why_are_they_all_different : id '' U = set.image (@id X) U := by refl -- thank god


:-(

#### Kevin Buzzard (May 28 2018 at 10:31):

They are the same -- you just have the wrong equivalence relation

#### Kenny Lau (May 28 2018 at 10:31):

I've been repeating the same thing 100 times.

#### Mario Carneiro (May 28 2018 at 10:32):

set.image is defined as {y : Y | ∃ x, x ∈ U ∧ f x = y}

#### Kevin Buzzard (May 28 2018 at 10:32):

I've been repeating the same thing 100 times.

I know but you didn't fix it yet

#### Kevin Buzzard (May 28 2018 at 10:32):

all the proofs are "by schoolkid"

#### Kevin Buzzard (May 28 2018 at 10:32):

Kenny do you want to do that for your 1st year project?

#### Kenny Lau (May 28 2018 at 10:32):

definition image := {y : Y | ∃ x ∈ U, f x = y}
example : image (@id X) U = U :=
by simp [image]


#### Kenny Lau (May 28 2018 at 10:32):

you must be blind

#### Kevin Buzzard (May 28 2018 at 10:33):

but it never just says "by simp"

#### Kevin Buzzard (May 28 2018 at 10:33):

which ones get done by simp

#### Mario Carneiro (May 28 2018 at 10:33):

no because that would be horrible in most proofs

#### Kenny Lau (May 28 2018 at 10:33):

Kevin, you don't want by simp to automatically unfold every definition for you.

#### Kevin Buzzard (May 28 2018 at 10:34):

import data.set

-- ZFC-safe! The below code uses only Prop and Type

variables {X Y : Type} (f : X → Y) (U : set X)

definition image' := {y : Y | ∃ x ∈ U, f x = y}

theorem they_are_the_same : image' (@id X) U = U := by simp -- fails
theorem they_are_the_same' : id '' U = U := by simp -- fails
theorem they_are_all_the_same_thing_ : id '' U = image' (@id X) U := by simp -- fails
theorem but_they_are_all_the_same : set.image (@id X) U = U := by simp -- fails
theorem why_are_they_all_different : id '' U = set.image (@id X) U := by simp -- I wasn't 100% confident but we got through


#### Kevin Buzzard (May 28 2018 at 10:34):

Why do I have to work, or even think, about proving that two objects are the same, when they are the same object?

here we go again

#### Kevin Buzzard (May 28 2018 at 10:34):

Why doesn't it do it for me?

#### Kevin Buzzard (May 28 2018 at 10:34):

That's what I want

#### Kevin Buzzard (May 28 2018 at 10:34):

Make it do it for me

simp is rubbish

#### Kevin Buzzard (May 28 2018 at 10:34):

make a proper one

#### Kenny Lau (May 28 2018 at 10:34):

do we have to go through the ZFC proof that they are the same again?

make schoolkid

#### Mario Carneiro (May 28 2018 at 10:35):

Stop trolling Kevin

#### Kevin Buzzard (May 28 2018 at 10:35):

I don't understand why this can't be done

#### Kevin Buzzard (May 28 2018 at 10:35):

Why can my brain do it?

#### Kevin Buzzard (May 28 2018 at 10:35):

Aren't I just a computer?

#### Kenny Lau (May 28 2018 at 10:35):

because your brain knows when to expand a definition and when not to

#### Kevin Buzzard (May 28 2018 at 10:36):

I think Lean can also decide when to expand a definition and when not to

how?

#### Kevin Buzzard (May 28 2018 at 10:36):

I don't get what I'm so good at that Lean can't do

#### Kenny Lau (May 28 2018 at 10:36):

with 10 definitions that is 1024 choices

#### Kenny Lau (May 28 2018 at 10:36):

humans are good at small things

#### Kenny Lau (May 28 2018 at 10:36):

humans don't have the guarantee that their algorithm works in every case

#### Kevin Buzzard (May 28 2018 at 10:36):

I guess here's a good analogue.

#### Kevin Buzzard (May 28 2018 at 10:37):

"OK so I'm quite good at go. Why don't you CS guys quickly knock up something that's as good as me at go and then I can retire"

#### Kenny Lau (May 28 2018 at 10:37):

a human may be able to square a small number faster than a computer (not really)

#### Kenny Lau (May 28 2018 at 10:37):

but as the number gets large, the computer wins by a lot

#### Kevin Buzzard (May 28 2018 at 10:37):

I square small numbers by lookup

#### Kevin Buzzard (May 28 2018 at 10:37):

they're hard wired

right

#### Kevin Buzzard (May 28 2018 at 10:37):

unlike whatever I said 5 minutes ago

#### Kenny Lau (May 28 2018 at 10:37):

humans are good at small things

#### Kenny Lau (May 28 2018 at 10:37):

id '' U = U is short

and true!

here we go again

#### Kevin Buzzard (May 28 2018 at 10:38):

The world just became a smaller place!

#### Kevin Buzzard (May 28 2018 at 10:38):

Two things became equal!

#### Kevin Buzzard (May 28 2018 at 10:38):

Why doesn't it work like that?

#### Kevin Buzzard (May 28 2018 at 10:38):

Where's the tactic that takes care of this for me?

#### Kenny Lau (May 28 2018 at 10:38):

you want a tactic to try to expand definitions

#### Kevin Buzzard (May 28 2018 at 10:39):

I have no clear idea what tactics do

#### Kenny Lau (May 28 2018 at 10:39):

that will work for small cases

#### Kenny Lau (May 28 2018 at 10:39):

that will not work for big cases

#### Mario Carneiro (May 28 2018 at 10:39):

In general that's undecidable

#### Kenny Lau (May 28 2018 at 10:39):

humans are only good at small things

#### Kevin Buzzard (May 28 2018 at 10:39):

Maybe learning tactics would help me understand my frustrations better.

#### Andrew Ashworth (May 28 2018 at 10:39):

Maybe learning tactics would help me understand my frustrations better.

yes

#### Kevin Buzzard (May 28 2018 at 10:39):

It's a huge hole in my Lean knowledge

#### Kenny Lau (May 28 2018 at 10:39):

definition image' := {y : Y | ∃ x ∈ U, f x = y}

attribute [simp] set.image_id

theorem they_are_the_same : image' (@id X) U = U := by simp [image'] -- works
theorem they_are_the_same' : id '' U = U := by simp -- works
theorem they_are_all_the_same_thing_ : id '' U = image' (@id X) U := by simp [image'] -- works
theorem but_they_are_all_the_same : set.image (@id X) U = U := by simp -- works
theorem why_are_they_all_different : id '' U = set.image (@id X) U := by simp


#### Kevin Buzzard (May 28 2018 at 10:39):

All I know is that tactic is a monoid or monad or something

#### Kevin Buzzard (May 28 2018 at 10:40):

theorem they_are_the_same' : id '' U = U := by simp -- fails

?

#### Kevin Buzzard (May 28 2018 at 10:40):

it works for you?

#### Kenny Lau (May 28 2018 at 10:40):

@Mario Carneiro can I get simp to automatically unfold certain definitions? reducible doesn't work

oh you CHEATED

#### Mario Carneiro (May 28 2018 at 10:40):

@[simp] can go on definitions

#### Kevin Buzzard (May 28 2018 at 10:40):

You gave simp a hint

YES

#### Kevin Buzzard (May 28 2018 at 10:41):

So that hint should have been there alreadyt

#### Kenny Lau (May 28 2018 at 10:41):

thanks @Mario Carneiro

#### Kevin Buzzard (May 28 2018 at 10:41):

why isn't it a simp lemma?

#### Kenny Lau (May 28 2018 at 10:41):

now I can convince him:

#### Kenny Lau (May 28 2018 at 10:41):

@[simp] def image' := {y : Y | ∃ x ∈ U, f x = y}

attribute [simp] set.image

theorem they_are_the_same : image' (@id X) U = U := by simp -- works
theorem they_are_the_same' : id '' U = U := by simp -- works
theorem they_are_all_the_same_thing_ : id '' U = image' (@id X) U := by simp -- works
theorem but_they_are_all_the_same : set.image (@id X) U = U := by simp -- works
theorem why_are_they_all_different : id '' U = set.image (@id X) U := by simp


#### Mario Carneiro (May 28 2018 at 10:41):

like I said, you shoot me in the leg and ask me to run a marathon

#### Mario Carneiro (May 28 2018 at 10:41):

it should be a simp lemma, I fixed

#### Johan Commelin (May 28 2018 at 10:41):

why isn't it a simp lemma?

you mean a simp definition?

#### Kenny Lau (May 28 2018 at 10:41):

@Johan Commelin no, set.image_id

not a definition

Aaah, ok, true

#### Kenny Lau (May 28 2018 at 10:42):

now is @Kevin Buzzard happy?

#### Kenny Lau (May 28 2018 at 10:42):

after the fix I will be able to remove that line

Oh!

#### Kenny Lau (May 28 2018 at 10:42):

@[simp] def image' := {y : Y | ∃ x ∈ U, f x = y}

attribute [simp] set.image_id

theorem they_are_the_same : image' (@id X) U = U := by simp -- works
theorem they_are_the_same' : id '' U = U := by simp -- works
theorem they_are_all_the_same_thing_ : id '' U = image' (@id X) U := by simp -- works
theorem but_they_are_all_the_same : set.image (@id X) U = U := by simp -- works
theorem why_are_they_all_different : id '' U = set.image (@id X) U := by simp


#### Kevin Buzzard (May 28 2018 at 10:43):

You see I have absolutely no idea about whether this is suitable as a simp lemma.

#### Kevin Buzzard (May 28 2018 at 10:43):

All i know is that it passes two basic tests

#### Kevin Buzzard (May 28 2018 at 10:43):

(1) it's an equality

#### Kevin Buzzard (May 28 2018 at 10:43):

(2) the left hand side has more characters than the right hand side

#### Mario Carneiro (May 28 2018 at 10:43):

image_id is a good simp lemma

#### Kevin Buzzard (May 28 2018 at 10:43):

My entry requirements for simp are pretty low

#### Kenny Lau (May 28 2018 at 10:43):

so is @Kevin Buzzard satisfied now?

#### Mario Carneiro (May 28 2018 at 10:43):

most theorems of the form "my_func special_arg = value" are good simp lemmas

#### Kevin Buzzard (May 28 2018 at 10:43):

image_id is a good simp lemma

I feel I could not say that with confidence

#### Kevin Buzzard (May 28 2018 at 10:44):

and that's what I mean when I say that I still don't understand simp properly

#### Mario Carneiro (May 28 2018 at 10:44):

It takes more knowledge to set up good simp lemmas than to use simp of course

Exactly.

#### Kevin Buzzard (May 28 2018 at 10:44):

I want to become a power user

#### Mario Carneiro (May 28 2018 at 10:45):

because it's a global problem with some locality

#### Kevin Buzzard (May 28 2018 at 10:45):

but I don't know anywhere where random nuggets such as

#### Kevin Buzzard (May 28 2018 at 10:45):

most theorems of the form "my_func special_arg = value" are good simp lemmas

#### Kevin Buzzard (May 28 2018 at 10:45):

appear, other than here

#### Mario Carneiro (May 28 2018 at 10:45):

You could just look at the many many examples in mathlib

#### Andrew Ashworth (May 28 2018 at 10:46):

only masochistic CS graduate students get interested in software verification

#### Kevin Buzzard (May 28 2018 at 10:46):

that's what CS people do

#### Andrew Ashworth (May 28 2018 at 10:46):

your tips are folklore in CS departments

#### Kevin Buzzard (May 28 2018 at 10:46):

I want to talk to more CS people

#### Andrew Ashworth (May 28 2018 at 10:46):

and that textbook I mentioned yesterday

#### Kevin Buzzard (May 28 2018 at 10:46):

I need simp tips so I can be a power user

#### Mario Carneiro (May 28 2018 at 10:46):

term rewriting and all that?

yeah

#### Kevin Buzzard (May 28 2018 at 10:46):

I remember a couple of months ago it all dawning on Chris

#### Mario Carneiro (May 28 2018 at 10:46):

I'm willing to bet it's full of tips on setting up simp

#### Kevin Buzzard (May 28 2018 at 10:47):

all of a sudden every other day he was saying to me "wooah simp does much more than you'd expect"

#### Kevin Buzzard (May 28 2018 at 10:47):

and then I knew he'd cracked it

#### Mario Carneiro (May 28 2018 at 10:47):

and now you are stuck on the other end, where you think simp is magic that solves all problems

#### Kevin Buzzard (May 28 2018 at 10:48):

I'm still at the novice stage, behind Patrick who can remember the {something = true} stuff that you sometimes have to write at the end of simp for some reason and which you don't have to write in schoolkid

#### Kevin Buzzard (May 28 2018 at 10:48):

I look through all the permutations and incantations that people have been using with simp recently

#### Kevin Buzzard (May 28 2018 at 10:49):

and I just write a tactic that tries all of them on my goal

#### Kevin Buzzard (May 28 2018 at 10:49):

and calls it schoolkid

#### Mario Carneiro (May 28 2018 at 10:49):

I think you could use some CS education, if only so that your suggestions come with algorithms

#### Kevin Buzzard (May 28 2018 at 10:49):

that way I will never have to remember what comes after the [] in simp

#### Kevin Buzzard (May 28 2018 at 10:50):

So I was under the misapprehension that the "your brain is just a big computer" people think that writing tactics to do what we do should be fine

#### Kenny Lau (May 28 2018 at 10:50):

your brain is a big computer that doesn't have to do everything correctly, just the small things

#### Mario Carneiro (May 28 2018 at 10:51):

That same argument says that general AI is just around the corner

I see

#### Kevin Buzzard (May 28 2018 at 10:51):

So is it possible to isolate "the techniques that I use to solve goals in ZFC"?

#### Kevin Buzzard (May 28 2018 at 10:51):

Is that the question?

#### Kevin Buzzard (May 28 2018 at 10:51):

Can I code this in a Lean tactic?

#### Kenny Lau (May 28 2018 at 10:52):

those techniques only work for small cases

#### Kevin Buzzard (May 28 2018 at 10:52):

Are you saying that this is hard

#### Kenny Lau (May 28 2018 at 10:52):

they can't be verified

#### Andrew Ashworth (May 28 2018 at 10:52):

can you write those techniques down as a sequence of steps in the language of Lean?

#### Kevin Buzzard (May 28 2018 at 10:52):

I find it so difficult to see how it can be hard when it's just checking that things are all the same

#### Kevin Buzzard (May 28 2018 at 10:52):

@Andrew Ashworth This is exactly the point.

#### Kenny Lau (May 28 2018 at 10:52):

@Kevin Buzzard the techniques include "run upon seeing a theorem with 10000 characters", which can't be one of the things a verified algorithm can do

#### Mario Carneiro (May 28 2018 at 10:52):

https://en.wikipedia.org/wiki/Word_problem_for_groups

#### Kevin Buzzard (May 28 2018 at 10:52):

When I discovered Lean I realised that it was the computer language I had been waiting for all my life

#### Kevin Buzzard (May 28 2018 at 10:52):

and so just thought I'd code my brain up in it

#### Kevin Buzzard (May 28 2018 at 10:53):

and I was just assuming it was going to be easy

#### Kenny Lau (May 28 2018 at 10:53):

the world is imperfect

#### Kenny Lau (May 28 2018 at 10:53):

computability matters

#### Mario Carneiro (May 28 2018 at 10:53):

just checking that things are all the same is undecidable in some simple situations

#### Kevin Buzzard (May 28 2018 at 10:53):

that's an engineering problem

#### Kevin Buzzard (May 28 2018 at 10:53):

you CS guys write great algos

#### Kevin Buzzard (May 28 2018 at 10:53):

I'm sure you can decide all the stuff I want decided

#### Mario Carneiro (May 28 2018 at 10:53):

no that's a fundamental limit on progress

no, you can't

#### Kevin Buzzard (May 28 2018 at 10:54):

because I have a really good feeling for the provability boundaries of ZFC

#### Kevin Buzzard (May 28 2018 at 10:54):

I know which questions look "weird to me" like CH

you don't

#### Kevin Buzzard (May 28 2018 at 10:54):

and which questions look sensible to me like the Langlands Programme

#### Kenny Lau (May 28 2018 at 10:54):

there are infinitely many independent theorem in any computable extension of ZFC

#### Kenny Lau (May 28 2018 at 10:54):

and there's no way any algorithm can decide whether a theorem is independent

#### Kenny Lau (May 28 2018 at 10:54):

your brain only knows special cases like CH and AD and AC

#### Mario Carneiro (May 28 2018 at 10:55):

and it only knows those because it has lots of simp lemmas

#### Andrew Ashworth (May 28 2018 at 10:55):

hmm, I don't know if you will have long-term success with formal proofs if you don't engage with CS theory and tactic writing. because the tedious bits need to be attacked via automation, and lots of custom automation at that. Remember Bertrand Russell tried to do everything by hand and spent 5 years proving 2+2=4

#### Andrew Ashworth (May 28 2018 at 10:55):

and this is my own failing too, it's hard, I haven't learned Lean tactics yet

#### Mario Carneiro (May 28 2018 at 10:56):

I could argue that automation is not necessary for getting things done formally

#### Mario Carneiro (May 28 2018 at 10:56):

I have plenty of theorems in metamath as evidence

#### Mario Carneiro (May 28 2018 at 10:57):

but proof engineering is a really important skill

#### Andrew Ashworth (May 28 2018 at 10:58):

but there's also evidence from adam chlipala and john harrison that automation is kind of a big deal

#### Andrew Ashworth (May 28 2018 at 10:59):

well, and I don't know about math, but software definitely needs automation to discharge repetitive, yet tediously involved goals

#### Mario Carneiro (May 28 2018 at 10:59):

there are multiple styles of proof, and they are all effective in the right hands

#### Andrew Ashworth (May 28 2018 at 10:59):

and i get the feeling from Kevin's worry about schemes that advanced mathematical constructs could also use a large helping of custom automation

#### Mario Carneiro (May 28 2018 at 10:59):

I find that good lemmas take most of the brunt of that

#### Mario Carneiro (May 28 2018 at 11:00):

but I grant that working with lean encourages good automation practices

#### Andrew Ashworth (May 28 2018 at 11:01):

there was that whole week long discussion about transporting across equivs and I was thinking "so use transfer or write a tactic" bingo problem solved

#### Kenny Lau (May 28 2018 at 11:01):

what was the solution?

to what?

#### Kevin Buzzard (May 28 2018 at 11:11):

in ZFC id '' U isn't even defined

Oh what a bore, you're right

#### Mario Carneiro (May 28 2018 at 11:12):

metamath uses ZFC + classes to get around this

#### Mario Carneiro (May 28 2018 at 11:13):

it's a conservative extension, it just lets you express class equalities like this

#### Mario Carneiro (May 28 2018 at 11:13):

http://us.metamath.org/mpeuni/imai.html

#### Kevin Buzzard (May 28 2018 at 11:16):

that's stupid. What if I can't find the official image so I just make my own image which would then be identical so all the old theorems would work anyway

This is bad, isn't it? Doesn't it mean that every time I have a terrific new idea for a function, I have to stop what I'm doing and plough through the library to see if someone already wrote it?

#### Kenny Lau (May 28 2018 at 11:16):

it's called using interface to make your life better

#### Kevin Buzzard (May 28 2018 at 11:24):

schoolkid_1 is simp!

Then why do I even bother using simp? Should I just be using simp! all the time? Is there any case where simp works and simp! doesn't?

#### Kevin Buzzard (May 28 2018 at 11:26):

@Kevin Buzzard I really do not see any problem at all. id '' U does not expand to U. you have to destruct the definitions and use extensionality

Yes -- you mean the definition of equal, right?

#### Kenny Lau (May 28 2018 at 11:26):

no, I mean the axiom of extensionality.

#### Kevin Buzzard (May 28 2018 at 11:27):

@Kevin Buzzard here's how I can formalize what I say: if you didn't have propext as an axiom, then you won't be able to prove that the two sets are equal, in Lean

But propext is in Lean! Is it a good simp lemma?

no

#### Kevin Buzzard (May 28 2018 at 11:27):

it looks good to me

simple predicate

#### Kevin Buzzard (May 28 2018 at 11:27):

implies an equality

#### Mario Carneiro (May 28 2018 at 11:28):

it says p = q in the conclusion

#### Kevin Buzzard (May 28 2018 at 11:28):

it got over my simp bar

#### Mario Carneiro (May 28 2018 at 11:28):

that means anything equals anything

it's too general

#### Kevin Buzzard (May 28 2018 at 11:28):

Just apply it sensibly

and stop moaning

#### Kevin Buzzard (May 28 2018 at 11:28):

don't just apply it randomly

:-/

#### Kevin Buzzard (May 28 2018 at 11:28):

This is really interesting

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

this is the hard bit

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

Here's another constraint: all the variables on the RHS should appear on the LHS

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

You can't make all the things I know are obvious yield to one tactic because you haven't worked hard enough

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

otherwise simp has to be creative when rewriting

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

So again this is somehow about can we build a tactic that beats a human at maths

#### Kevin Buzzard (May 28 2018 at 11:30):

Will this happen before I die? Say I live another 30 years

#### Mario Carneiro (May 28 2018 at 11:30):

I think you should try writing that tactic and get back to me

#### Kevin Buzzard (May 28 2018 at 11:30):

you went to math classe

s

#### Kevin Buzzard (May 28 2018 at 11:30):

you know how we think

#### Mario Carneiro (May 28 2018 at 11:30):

I want you to fail at it first so you understand what you are asking

#### Kevin Buzzard (May 28 2018 at 11:30):

can you write a better interface?

#### Johan Commelin (May 28 2018 at 11:30):

Kevin, I completely agree that we need a smarter tactic. But I think that doesn't have to be simp. Simp is a very straightforward tool, that shouldn't try to be smart.

#### Kevin Buzzard (May 28 2018 at 11:30):

Yes, I need to go and play with Mizar and then some things which are conflated in my mind will become more separate

#### Kevin Buzzard (May 28 2018 at 11:31):

no, we should use schoolkid or whatever you wanted to call it

#### Kevin Buzzard (May 28 2018 at 11:31):

I think you had a more grown-up name

#### Kenny Lau (May 28 2018 at 11:31):

Yes, I need to go and play with Mizar and then some things which are conflated in my mind will become more separate

I don't see the point going to a weaker foundational system

#### Johan Commelin (May 28 2018 at 11:31):

I think you had a more grown-up name

math_trivial?

#### Mario Carneiro (May 28 2018 at 11:32):

Mizar is actually stronger axiomatically than lean

why?

#### Mario Carneiro (May 28 2018 at 11:32):

it has a proper class of inaccessibles

#### Johan Commelin (May 28 2018 at 11:32):

But I wouldn't mind have kindergarten or schoolkid

#### Kenny Lau (May 28 2018 at 11:32):

@Kevin Buzzard again, your issue is not in the foundational system

#### Kenny Lau (May 28 2018 at 11:32):

but it seems that you are deaf

#### Andrew Ashworth (May 28 2018 at 11:33):

it can't hurt to play around with Mizar and Isabelle

#### Kevin Buzzard (May 28 2018 at 11:34):

why are you proving trivial set theorems?

in this case it was because I was trying to understand something. But on other occasions the answer is "because I don't really know a good way of finding it in the library and it's almost certainly in a file which I haven't imported yet"

#### Andrew Ashworth (May 28 2018 at 11:34):

most of us here are refugees from Coq / Agda / Isabelle anyway

#### Mario Carneiro (May 28 2018 at 11:34):

they are organized fairly logically

#### Mario Carneiro (May 28 2018 at 11:35):

set.image_id is in the image section of data.set.basic

#### Kevin Buzzard (May 28 2018 at 11:35):

I don't see the point going to a weaker foundational system

I need to see it, in order to refine my definition of "equality in ZFC".

#### Kevin Buzzard (May 28 2018 at 11:37):

set.image_id is in the image section of data.set.basic

I just can't remember all this data.set.basic stuff. I just want to write set.image and hit tab a few times. This is a genuine frustration I have in my lean life

#### Kevin Buzzard (May 28 2018 at 11:37):

I am not capable of learning all the names of all the library files

#### Kevin Buzzard (May 28 2018 at 11:37):

it's init this and data that

#### Kevin Buzzard (May 28 2018 at 11:37):

when I want set.image_id

#### Kevin Buzzard (May 28 2018 at 11:38):

I type #check set.image_id

#### Kevin Buzzard (May 28 2018 at 11:38):

and it's not there

#### Kevin Buzzard (May 28 2018 at 11:38):

and then I have to stop what I'm doing and start faffing around with the search tool

#### Kevin Buzzard (May 28 2018 at 11:38):

I have no clue where anything is

#### Kevin Buzzard (May 28 2018 at 11:38):

they're just all theorems

#### Kevin Buzzard (May 28 2018 at 11:38):

Can we have a better search?

#### Mario Carneiro (May 28 2018 at 11:38):

I just type import set and the autocomplete is pretty smart about it

oh!

#### Kevin Buzzard (May 28 2018 at 11:39):

Because I know it's set.something I can just import set?

#### Kevin Buzzard (May 28 2018 at 11:39):

Does that work with everything?

#### Mario Carneiro (May 28 2018 at 11:39):

it's not even set.something

#### Kevin Buzzard (May 28 2018 at 11:39):

can I import scheme?

#### Mario Carneiro (May 28 2018 at 11:39):

it's data.set.basic

#### Mario Carneiro (May 28 2018 at 11:39):

but vscode will still give it to you

I see

#### Kevin Buzzard (May 28 2018 at 11:40):

I should "key on set"

#### Kevin Buzzard (May 28 2018 at 11:45):

there are infinitely many independent theorem in any computable extension of ZFC

I know but Kenny my point is that those independent theorems are just junk theorems like stupid theorems about how pi can't be a complex manifold.

are they

#### Kevin Buzzard (May 28 2018 at 11:46):

All the undecidable statements about stupid things like sets. [added later] -- that's not what ZFC is even _for_!

#### Kevin Buzzard (May 28 2018 at 11:46):

I am only interested in the Langlands Programme

#### Kevin Buzzard (May 28 2018 at 11:48):

there was that whole week long discussion about transporting across equivs and I was thinking "so use transfer or write a tactic" bingo problem solved

That's on my todo list. I'm going to write a short paper about my whole scheme experience for the ZFC people and I am going to have to get up to date as to exactly what we think is possible there

#### Kevin Buzzard (May 28 2018 at 11:48):

it's called using interface to make your life better

I need better interface search.

#### Kevin Buzzard (May 28 2018 at 11:49):

Why can't I write set.image_id and something pops up saying "do you want to import data.set.basic"?

#### Kevin Buzzard (May 28 2018 at 11:49):

Can that be a thing one day?

#### Sean Leather (May 28 2018 at 11:50):

Because nobody's written the code to do it. That's usually your answer.

#### Andrew Ashworth (May 28 2018 at 11:50):

It could be. Maybe Lean gets tremendously popular, gets a research grant, and somebody gets hired to work on it to make it easier to use for mathematicians

#### Kevin Buzzard (May 28 2018 at 11:50):

Here's another constraint: all the variables on the RHS should appear on the LHS

Is it possible to make a flowchart -- "am I a good simp lemma?"

#### Kevin Buzzard (May 28 2018 at 11:53):

It could be. Maybe Lean gets tremendously popular, gets a research grant, and somebody gets hired to work on it to make it easier to use for mathematicians

How much does that cost in your CS world?

#### Kevin Buzzard (May 28 2018 at 11:53):

I could do all the costings for that other than salary

#### Kevin Buzzard (May 28 2018 at 11:53):

I have no idea how much you guys get paid

#### Kevin Buzzard (May 28 2018 at 11:53):

the administration would be able to fill in the other boxes

#### Kevin Buzzard (May 28 2018 at 11:54):

I'm meeting with EPSRC in two weeks

#### Kevin Buzzard (May 28 2018 at 11:54):

I have several hours of meetings with them and I have already pre-warned them that I will be after money to spend on computer scientists

#### Kevin Buzzard (May 28 2018 at 11:55):

But it would be good to get an idea of how much to pay someone to do that job

#### Andrew Ashworth (May 28 2018 at 12:06):

I'm not too familiar with London CS pay, my general instinct is that it ranges from 30 ~ 70 thousand pounds / year

#### Andrew Ashworth (May 28 2018 at 12:10):

you could wait until Lean 4. We've been promised by Moses Schönfinkel that he wants to take a look at theorem search in Lean after the parser and tactics framework settles down

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

I just wrote a theorem that was in the library

yay me

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

#check topological_space.open_immersion_id

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

#check topological_space.id_open_immersion

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

what should it be called?

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

The statement that the identity map is an open immersion

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

I did the other one

#### Kevin Buzzard (May 28 2018 at 12:22):

is there a hard and fast convention for naming that extends beyond my mul_one levels?

#### Kevin Buzzard (May 28 2018 at 12:22):

I get the feeling that there's more of an art to it

#### Patrick Massot (May 28 2018 at 12:24):

Yeah, Kevin is back to work! I'm amazed how fast he travels those math formalization DTT stages every month or so.

I'm much slower

#### Kevin Buzzard (May 28 2018 at 12:36):

I am trying to write a hard level for these CS guys

#### Kevin Buzzard (May 28 2018 at 12:36):

But I am stuck on something

#### Kevin Buzzard (May 28 2018 at 12:36):

If I have x : (presheaf_of_types_pullback_under_open_immersion ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types) id _).F HU 

in my context

#### Kevin Buzzard (May 28 2018 at 12:36):

oh I can answer my own question

oh no I can't

#### Kevin Buzzard (May 28 2018 at 12:38):

Ok so there's my x

#### Kevin Buzzard (May 28 2018 at 12:39):

and presheaf_of_types_pullback_under_open_immersion just has some definition

#### Kevin Buzzard (May 28 2018 at 12:39):

which explictly says what its F bit is

#### Kevin Buzzard (May 28 2018 at 12:39):

and so probably this expands out to something with no .F in, by rfl

#### Kevin Buzzard (May 28 2018 at 12:39):

but how do I find out what it expands to without having to work it out myself?

#### Kevin Buzzard (May 28 2018 at 12:40):

I can't unfold presheaf_of_types_pullback_under_open_immersion

#### Kevin Buzzard (May 28 2018 at 12:40):

Do people need more context?

#### Kevin Buzzard (May 28 2018 at 12:40):

I can provide a MWE but I just wondered if I'd already said enough for someone to tell me a trick

#### Patrick Massot (May 28 2018 at 12:41):

Did you try dsimp at x?

I did

#### Kevin Buzzard (May 28 2018 at 12:41):

it wasn't very effective

#### Kevin Buzzard (May 28 2018 at 12:41):

it turned presheaf_of_rings_pullback_under_open_immersion

#### Kevin Buzzard (May 28 2018 at 12:41):

into presheaf_of_types_pullback_under_open_immersion

and then stopped

#### Kevin Buzzard (May 28 2018 at 12:43):

Actually I should do it manually and see if it is refl

#### Patrick Massot (May 28 2018 at 12:43):

Is it something I can git clone?

#### Kevin Buzzard (May 28 2018 at 12:47):

I have just done a bunch of editing to scheme.lean but not committed or pushed or anything

#### Kevin Buzzard (May 28 2018 at 12:47):

I'd rather just move all those edits to a different file

#### Kevin Buzzard (May 28 2018 at 12:47):

can git help me here?

#### Kevin Buzzard (May 28 2018 at 12:47):

i.e. I want to push the file I have open

#### Kevin Buzzard (May 28 2018 at 12:47):

but unfortunately it's an important file which I just broke

goofing around

#### Patrick Massot (May 28 2018 at 12:48):

you could create a broken branch

#### Kevin Buzzard (May 28 2018 at 12:48):

Can I do that in VS Code?

#### Kevin Buzzard (May 28 2018 at 12:49):

I only have master

#### Patrick Massot (May 28 2018 at 12:49):

git stash, git checkout -b experimental, git stash pop, git commit -a, git push --set-upstream experimental

I've got it

#### Patrick Massot (May 28 2018 at 12:49):

you can problably do it in VScode but it would be longer

#### Kevin Buzzard (May 28 2018 at 12:50):

Oh crap I didn't stash

#### Kevin Buzzard (May 28 2018 at 12:50):

is that an issue?

maybe not

#### Patrick Massot (May 28 2018 at 12:50):

it wrote that to be on the safe side

#### Kevin Buzzard (May 28 2018 at 12:51):

      let y := (presheaf_of_types_pullback_under_open_immersion ((zariski.structure_presheaf_of_rings R).to_presheaf_of_types) id


oops

#### Kevin Buzzard (May 28 2018 at 12:51):

https://github.com/kbuzzard/lean-stacks-project/blob/broken/src/scheme.lean#L495

#### Kevin Buzzard (May 28 2018 at 12:51):

was what I meant to say

#### Kevin Buzzard (May 28 2018 at 12:52):

line 495, I want to unfold that presheaf_of_types_pullback_under_open_immersion

no

#### Kevin Buzzard (May 28 2018 at 12:52):

I want Lean to unfold it

#### Kevin Buzzard (May 28 2018 at 12:52):

I'm going to try it myself to see what I'm missing

#### Patrick Massot (May 28 2018 at 13:10):

This is really irritating

OK I minimised

#### Kevin Buzzard (May 28 2018 at 13:38):

https://gist.github.com/kbuzzard/e051858b8e3348e884610ace8cd87c20

#### Kevin Buzzard (May 28 2018 at 13:39):

That is me setting up the theory of pre-semi-sheaves

#### Kevin Buzzard (May 28 2018 at 13:39):

which are a bit like distribs

#### Kevin Buzzard (May 28 2018 at 13:39):

and although the objects are a bit silly

#### Kevin Buzzard (May 28 2018 at 13:39):

I have tried to set up the theory in a sensible way

#### Kevin Buzzard (May 28 2018 at 13:40):

and to create Line 53 of that script I had to do some work

#### Kevin Buzzard (May 28 2018 at 13:40):

which I am convinced a computer could have done for me

#### Kevin Buzzard (May 28 2018 at 13:40):

I cut and pasted the definition of pre_semi_sheaf_of_rings_pullback

#### Kevin Buzzard (May 28 2018 at 13:40):

because I wanted to know what would happen if I unfolded it

#### Kevin Buzzard (May 28 2018 at 13:41):

but the problem is that the unfolding is refl

#### Kevin Buzzard (May 28 2018 at 13:41):

so the lemma has no name and I can't rewrite it to see what the answer is

#### Kevin Buzzard (May 28 2018 at 13:41):

I have to work it out myself

#### Kevin Buzzard (May 28 2018 at 13:41):

This is an independent question

#### Johan Commelin (May 28 2018 at 13:45):

(Aside: Kevin, you can tell Github that your gist is a lean file. Then you/we have syntax highlighting.)

Oh cool

#### Kevin Buzzard (May 28 2018 at 13:46):

but OK I have finally minimised my question

#### Kevin Buzzard (May 28 2018 at 13:47):

my question is this gist which I'll attempt to highlight properly

#### Kevin Buzzard (May 28 2018 at 13:47):

https://gist.github.com/kbuzzard/123384f9132d6db8650c3484e42bda81

#### Kevin Buzzard (May 28 2018 at 13:48):

That's my challenge to the CS people, I think

#### Kevin Buzzard (May 28 2018 at 13:48):

I'm not sure I can prove that goal

#### Kevin Buzzard (May 28 2018 at 13:48):

I'm not even sure that goal is true

#### Kevin Buzzard (May 28 2018 at 13:48):

but I think it is

#### Kevin Buzzard (May 28 2018 at 13:48):

for some reason it's a pain to prove though

#### Kevin Buzzard (May 28 2018 at 13:49):

I'm hoping the file is fairly self-explanatory

#### Johan Commelin (May 28 2018 at 13:49):

It is "math-true", right?

exactly Johan

#### Kevin Buzzard (May 28 2018 at 13:50):

Before I had something which was math-true

#### Kevin Buzzard (May 28 2018 at 13:50):

and Kenny and Mario kept telling me it could be done by simp

#### Kevin Buzzard (May 28 2018 at 13:50):

I would like them to tell me how to do this one

#### Johan Commelin (May 28 2018 at 13:52):

Are the rings essential to the problem?

#### Johan Commelin (May 28 2018 at 13:53):

Or could you just use semi-quasi-demi-pre-sheaves of types?

#### Kevin Buzzard (May 28 2018 at 13:58):

No it's crucial they're rings

#### Kevin Buzzard (May 28 2018 at 13:58):

because it's a trivial way to make it even harder

#### Kevin Buzzard (May 28 2018 at 13:59):

this is a content-free statement from where I'm standing

#### Kevin Buzzard (May 28 2018 at 13:59):

and if there aren't algorithms which currently prove content-free statements like this

#### Kevin Buzzard (May 28 2018 at 13:59):

then I think that mathematicians will find it hard to learn Lean

#### Kevin Buzzard (May 28 2018 at 13:59):

@Kenny Lau @Mario Carneiro Can you fill in my sorry?

#### Kevin Buzzard (May 28 2018 at 13:59):

Am I missing something easy?

#### Patrick Massot (May 28 2018 at 14:00):

Oh, he went back a couple of stages

#### Kevin Buzzard (May 28 2018 at 14:00):

I removed topology

#### Kevin Buzzard (May 28 2018 at 14:00):

and open immersions

#### Kenny Lau (May 28 2018 at 14:00):

Am I missing something easy?

no

crap

#### Kevin Buzzard (May 28 2018 at 14:00):

is that a provable but hard goal?

#### Kenny Lau (May 28 2018 at 14:00):

well not really hard

i could do it

#### Kenny Lau (May 28 2018 at 14:00):

but not exactly easy

#### Kevin Buzzard (May 28 2018 at 14:01):

Teach me how to do it

I can't do it

and it's obvious

#### Kevin Buzzard (May 28 2018 at 14:01):

and these are my least favourite things in Lean

#### Kevin Buzzard (May 28 2018 at 14:01):

teach me how to kill this pokemon

#### Johan Commelin (May 28 2018 at 14:01):

@Kevin Buzzard you don't only want schoolkid tactic, you also want kenny_lau and mario_carneiro

exactly

Kenny

I'm up to here

#### Kevin Buzzard (May 28 2018 at 14:01):

theorem pre_semi_sheaves_iso (X : Type) (F : pre_semi_sheaf_of_rings X) :
are_isomorphic_pre_semi_sheaves_of_rings
(pre_semi_sheaf_of_rings_pullback F id) F
:=
begin
constructor,
{ constructor,tactic.swap,
{ constructor,tactic.swap,
{ intros U s,
unfold pre_semi_sheaf_of_rings_pullback,
suffices : F.F (id '' U), by simpa using this,
have reluctant_to_use : id '' U = U := by rw set.image_id,
rw reluctant_to_use,
exact s,
},
intro U,
simp,
sorry
},
sorry,
},
sorry,
end


I'm trying

Thanks

#### Kevin Buzzard (May 28 2018 at 14:03):

Are you writing a tactic?

#### Kevin Buzzard (May 28 2018 at 14:03):

Don't try to solve the goal

no

#### Kevin Buzzard (May 28 2018 at 14:03):

try to write a tactic which solves the goal

#### Kenny Lau (May 28 2018 at 14:03):

I don't know how to write tactics

#### Kevin Buzzard (May 28 2018 at 14:03):

because this goal is solved by math_trivial

#### Kevin Buzzard (May 28 2018 at 14:04):

This goal is the nightmare which I could avoid in my case of presheaves

#### Kevin Buzzard (May 28 2018 at 14:04):

but a pre_semi_sheaf does not have res

#### Kevin Buzzard (May 28 2018 at 14:04):

so you have to bite the bullet

#### Kevin Buzzard (May 28 2018 at 14:05):

@Simon Hudon Can you solve my goal with a tactic?

#### Kevin Buzzard (May 28 2018 at 14:05):

https://gist.github.com/kbuzzard/123384f9132d6db8650c3484e42bda81

Last line

#### Kevin Buzzard (May 28 2018 at 14:05):

the pre_semi_sheaves are isomorphic via the identity map

#### Kevin Buzzard (May 28 2018 at 14:05):

but checking the details is apparently a little tricky

#### Kevin Buzzard (May 28 2018 at 14:06):

Would I have exactly the same problems in Mizar?

#### Kevin Buzzard (May 28 2018 at 14:06):

@Assia Mahboubi Would my goal be any easier to solve in Coq?

#### Kevin Buzzard (May 28 2018 at 14:07):

I have isolated a frustration I have with dependent type theory

#### Kevin Buzzard (May 28 2018 at 14:07):

I need to define a map from F U to F (id '' U)

#### Kevin Buzzard (May 28 2018 at 14:07):

where id '' U is the image of the set U under the identity map

#### Kevin Buzzard (May 28 2018 at 14:08):

I define the map by rewriting id '' U = U and then using the identity

#### Kevin Buzzard (May 28 2018 at 14:08):

and I never recover

#### Kevin Buzzard (May 28 2018 at 14:08):

But I don't know any other way of doing it

#### Kevin Buzzard (May 28 2018 at 14:10):

Is there some sort of reason why I should not be proving this goal at all?

#### Simon Hudon (May 28 2018 at 14:14):

How would you prove it without tactics?

#### Kenny Lau (May 28 2018 at 14:15):

he can't function without tactics

#### Kenny Lau (May 28 2018 at 14:15):

you would do eq.drec without tactics

#### Simon Hudon (May 28 2018 at 14:24):

I mean, I don't know any of the context so I'm not sure how the definitions relate to each other

#### Assia Mahboubi (May 28 2018 at 15:06):

@Kevin Buzzard It will take me some time to catch up, the thread is long. Why did you use this equality at all? Aren't F U and F (id '' U) the exact same thing (aka convertible?). How can I play your formalization?

#### Kenny Lau (May 28 2018 at 15:07):

https://gist.github.com/kbuzzard/123384f9132d6db8650c3484e42bda81

#### Kenny Lau (May 28 2018 at 15:07):

@Assia Mahboubi just prove the above

#### Kenny Lau (May 28 2018 at 15:09):

@Kevin Buzzard you know what, I take back my word, it's harder than I thought

#### Assia Mahboubi (May 28 2018 at 15:09):

Hi @Kenny Lau ! Thanks! But I am more ignorant than you think : I meant, what install instructions should I follow. I am not a regular Lean user.

oh, sorry

#### Kenny Lau (May 28 2018 at 15:10):

I think you can try it online

#### Kenny Lau (May 28 2018 at 15:11):

https://leanprover.github.io/live/latest/

#### Assia Mahboubi (May 28 2018 at 15:11):

Ok thanks, I am doing that now.

#### Kevin Buzzard (May 28 2018 at 15:13):

Does one run into the same issues in Coq?

#### Kevin Buzzard (May 28 2018 at 15:13):

Does one run into the same issues in Mizar?

#### Kevin Buzzard (May 28 2018 at 15:14):

Which systems is this easy in?

#### Kevin Buzzard (May 28 2018 at 15:14):

@Assia Mahboubi I suspect you can see what I'm trying to do

#### Kevin Buzzard (May 28 2018 at 15:15):

I'm happy to let a lean expert like Mario or Kenny solve the lean one

#### Kevin Buzzard (May 28 2018 at 15:15):

I am trying to understand to what extent my worldview of mathematics is naive

#### Kenny Lau (May 28 2018 at 15:15):

lol it's been an hour already

#### Kevin Buzzard (May 28 2018 at 15:16):

The challenge was embedded well in a very long thread and I would imagine many have stopped reading

#### Kevin Buzzard (May 28 2018 at 15:17):

One could ask in a new thread, I think this question is sufficiently interesting

#### Kevin Buzzard (May 28 2018 at 15:18):

I am hoping that someone will come up with a curve ball solution of the form "don't prove that, prove something that implies that

#### Kenny Lau (May 28 2018 at 15:19):

I tried to build up an interface

didn't work

#### Assia Mahboubi (May 28 2018 at 15:21):

Thanks @Kenny Lau, it works like a charm. But unfortunately I will have to leave now (and I have not finished to read the problem :disappointed: ). I will definitely look again later.

see you

@Kenny Lau

#### Kevin Buzzard (May 28 2018 at 15:28):

but you would be quicker to implement it than me

what is it

#### Kevin Buzzard (May 28 2018 at 15:28):

and I have to tidy the kitchen anyway

#### Kevin Buzzard (May 28 2018 at 15:28):

I claim that my definition is incomplete

#### Kevin Buzzard (May 28 2018 at 15:28):

as far as Lean is concerned

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

I am missing some extra structure

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

which can be filled in easily

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

Is the "correct" object a pre_semi_sheaf whatever, but also equipped with maps res : F U -> F V whenever U = V

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

plus axiom that res U U = id

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

plus axiom of composition

#### Kevin Buzzard (May 28 2018 at 15:30):

res U V then res V W is res U W

#### Kevin Buzzard (May 28 2018 at 15:30):

Given my stupid annoying structure

#### Kevin Buzzard (May 28 2018 at 15:30):

can it be beefed up to such a structure

#### Kevin Buzzard (May 28 2018 at 15:30):

and for this beefed-up structure

#### Kevin Buzzard (May 28 2018 at 15:30):

can the map be defined to be res

#### Kevin Buzzard (May 28 2018 at 15:30):

and then we deduce the result for the stupid structure

#### Kevin Buzzard (May 28 2018 at 15:31):

My experience with schemes tells me

#### Kevin Buzzard (May 28 2018 at 15:31):

that when the map is res

#### Kevin Buzzard (May 28 2018 at 15:31):

all the hard proofs become rfl

#### Kevin Buzzard (May 28 2018 at 15:31):

maybe not the ring one

#### Kevin Buzzard (May 28 2018 at 15:31):

the ring one we have to use some equiv tactic thing

#### Reid Barton (May 28 2018 at 18:17):

@Kevin Buzzard

definition pre_semi_sheaf_of_rings_pullback_setmap
{α : Type}
{β : Type}
(PR : pre_semi_sheaf_of_rings β)
(f : set α → set β)
: pre_semi_sheaf_of_rings α :=
{ F := λ V,PR.F (f V)
}

theorem pre_semi_sheaves_iso_setmap (X : Type) (F : pre_semi_sheaf_of_rings X) :
are_isomorphic_pre_semi_sheaves_of_rings
(pre_semi_sheaf_of_rings_pullback_setmap F id) F :=
⟨⟨λ (U : set X), id, by apply_instance⟩,
⟨λ (U : set X), id, by apply_instance⟩,
λ _, rfl, λ _, rfl⟩

definition pre_semi_sheaf_of_rings_pullback
{α : Type}
{β : Type}
(PR : pre_semi_sheaf_of_rings β)
(f : α → β)
: pre_semi_sheaf_of_rings α :=
{ F := λ V,PR.F (f '' V)
}

theorem pre_semi_sheaves_iso (X : Type) (F : pre_semi_sheaf_of_rings X) :
are_isomorphic_pre_semi_sheaves_of_rings
(pre_semi_sheaf_of_rings_pullback F id) F
:= begin
convert pre_semi_sheaves_iso_setmap X F,
change pre_semi_sheaf_of_rings_pullback_setmap F (λ U, id '' U) = _,
congr, funext U, simp [set.image_id]
end


#### Kevin Buzzard (May 28 2018 at 18:18):

I was hoping you'd show up

#### Kevin Buzzard (May 28 2018 at 18:18):

I thought you'd like this one

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

I am cooking, will look later. Did you do it?

Yes

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

Convert? What does that do?

#### Reid Barton (May 28 2018 at 18:20):

I split your construction into two pieces: pullback of a presheaf by a functor between sites and the functor between sites induced by a map of spaces

#### Reid Barton (May 28 2018 at 18:20):

convert basically says "this is the term I want to be the proof, aside from some fiddling about the type not being definitionally equal to the desired one"

#### Reid Barton (May 28 2018 at 18:21):

so it generates a new goal which is that the type of the term you provided is the same as the goal type

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

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/ZFC.20equality/near/127204479

Here's how you can use cast as a morphism without any res trickery:

def pre_semi_sheaf_of_rings.cast {α} (FPT : pre_semi_sheaf_of_rings α)
{U V : set α} (e : U = V) : FPT.F U → FPT.F V :=
cast (congr_arg _ e)

instance pre_semi_sheaf_of_rings.cast.is_ring_hom
{α} (FPT : pre_semi_sheaf_of_rings α) {U V : set α} (e : U = V) :
is_ring_hom (FPT.cast e) :=
by subst e; exact is_ring_hom.id

theorem pre_semi_sheaf_of_rings.cast_comp
{α} (FPT : pre_semi_sheaf_of_rings α) {U V W : set α}
(e₁ : U = V) (e₂ : V = W) (a) :
FPT.cast e₂ (FPT.cast e₁ a) = FPT.cast (e₁.trans e₂) a :=
by substs e₂ e₁; exact rfl

theorem presheaves_iso (X : Type) (F : pre_semi_sheaf_of_rings X) :
are_isomorphic_pre_semi_sheaves_of_rings
(pre_semi_sheaf_of_rings_pullback F id) F :=
begin
refine ⟨⟨λ U, F.cast (by simp), by apply_instance⟩,
⟨λ U, F.cast (by simp), by apply_instance⟩, _, _⟩;
{ intros U, funext a,
dsimp [is_identity_morphism_of_pre_semi_sheaves_of_rings,
composition_of_morphisms_of_pre_semi_sheaves_of_rings],
rw F.cast_comp, refl }
end


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

I think you can try it online

I think it's a bad idea to tell people to use the online version. Maybe it's my computer fault, but I find it too slow to be usable. I think it's very bad advertisement. So let me try something new: https://www.math.u-psud.fr/~pmassot/en/misc/index.html @Assia Mahboubi I guess you have a Debian/Ubuntu computer at hand. Could you try using my installation script? It's meant to be a single step, one minute fully setup Lean install (this obviously includes a compiled mathlib).

#### Johan Commelin (May 29 2018 at 08:54):

Does https://www.math.u-psud.fr/~pmassot/files/lean/install_lean.sh contain precompiled mathlib nightlies?

yes

#### Johan Commelin (May 29 2018 at 08:55):

Nice! I guess in this file, right? https://www.math.u-psud.fr/~pmassot/files/lean/.lean.tar.gz

yes

#### Johan Commelin (May 29 2018 at 08:55):

Ok, you should change the topic of your anouncement. This deserves more PR.

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

I think this deserves to be taken up by Mario and Johannes. Right now, I set up an emergency solution. I don't want Assia to go away because Javascript was never meant to run proof assistants

#### Patrick Massot (May 29 2018 at 08:58):

But now I need to stop. This was meant to be a no Lean day. I'll go to my IHES office where I can't install anything on the computer (and nothing Lean related is pre-installed) and get some real work done

Have fun!

#### Assia Mahboubi (May 29 2018 at 08:59):

Hi @Patrick Massot . Yes, it was very slow and I eventually gave up. I was planning to (re)install Lean on my machine today. What is your script doing? Will it be easy for me to update my Lean later? My plan is to look at @Kevin Buzzard 's stack project and he says here that I need a version from nightly of 2018-04-06. Does it matter? And yes, I have Debian/Ubuntu OS.

#### Patrick Massot (May 29 2018 at 09:00):

It does what it says in https://www.math.u-psud.fr/~pmassot/files/lean/install_lean.sh

#### Patrick Massot (May 29 2018 at 09:01):

install VScode using MS debian package, manually install the Lean extension, download Lean 3.4.1 and set the bash path variable, download precompiled mathlib

#### Patrick Massot (May 29 2018 at 09:01):

Let me check you can run Kevin's code using this version of mathlib

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

[sorry, wrong topic]

#### Assia Mahboubi (May 29 2018 at 09:06):

@Patrick Massot Thanks for the answer to my silly question: I should have open the file first. It looks great. I'll wait from a confirmation (from you or from anyone else) and try (I guess that otherwise it's just a matter of changing a couple of lines in your script). Happy no-Lean day.

#### Johan Commelin (May 29 2018 at 09:08):

@Assia Mahboubi It will be super easy to update Lean later.

#### Johan Commelin (May 29 2018 at 09:08):

Patrick's script just puts together the steps that you would otherwise perform manually.

#### Johan Commelin (May 29 2018 at 09:09):

And he has compiled mathlib for you. Which saves you an hour of coffee breaks :wink:

#### Assia Mahboubi (May 29 2018 at 09:09):

Hi @Johan Commelin , thanks for the help. I am trying it now.

#### Patrick Massot (May 29 2018 at 09:14):

It seems you still need to manually copy mathlib to the stacks directory. Maybe I shouldn't have skipped using Sbeastian's elan. So, after running my script, the next steps are: git clone https://github.com/kbuzzard/lean-stacks-project.git then cp -r ~/.lean/_target/ lean-stacks-project then cd lean-stacks-project, lean --make

#### Patrick Massot (May 29 2018 at 09:14):

There will probably be some errors because this repo is still a messy playground

#### Patrick Massot (May 29 2018 at 09:21):

Ok, I confirm I'm able to do that and then open the lean-stacvks-project folder in VScode and open scheme.lean without error. Assia: the first command to learn after opening a Lean file in VScode (and putting the cursor anywhere in that file) is Ctrl-shift-return which opens the Lean message window where all the interesting communication with lean takes place

#### Patrick Massot (May 29 2018 at 09:22):

Now I'll really go to IHES where I'll probably open Zulip anyway, but not VScode

#### Assia Mahboubi (May 29 2018 at 09:27):

Thanks again! Meanwhile I tried the instruction provided in the README.md (using leanpkg) and it is now indeed building stuff. If it goes wrong I''fall back to your suggestion.

#### Assia Mahboubi (May 29 2018 at 09:32):

It's very long (and warms my office) : it seems that a mathlib has been copied and is being re-compiled in a _target/dep sub-directory...

#### Johan Commelin (May 29 2018 at 09:35):

Yes, we know that feeling... (-;

#### Johan Commelin (May 29 2018 at 09:35):

I wasn't joking when I told you about the "hour of coffee breaks"

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

This is exactly what I tried to avoid

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

My instructions should bypass mathlib compilation

#### Patrick Massot (May 29 2018 at 09:39):

(I'm waiting for my train)

Last updated: May 19 2021 at 03:22 UTC