ZFC equality

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

And now here's something which doesn't work

[Kevin Buzzard]

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

[Kevin Buzzard]

Does that mean that my definition of image is wrong?

[Kevin Buzzard]

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

[Kenny Lau]

they are definitely not defeq

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Can you write a better one for me

[Kenny Lau]

no, it isn't

[Kevin Buzzard]

where they are defeq

[Kenny Lau]

you can't

[Kenny Lau]

you have to have an existential quantifier

[Kevin Buzzard]

can you prove that you can't?

[Kevin Buzzard]

in Lean

[Kevin Buzzard]

3.4.1

[Mario Carneiro]

not in lean

[Mario Carneiro]

it's a metatheorem

[Kevin Buzzard]

Great.

[Kenny Lau]

@Mario Carneiro can it actually be proved?

[Mario Carneiro]

probably

[Kevin Buzzard]

Well you know what

[Kevin Buzzard]

I think defeq is rubbish

[Kevin Buzzard]

because those two sets are equal

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

but not definitionally equal

[Kevin Buzzard]

so what has gone wrong?

[Mario Carneiro]

nothing is wrong

[Mario Carneiro]

defeq is not ZFC equality

[Kevin Buzzard]

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

[Kevin Buzzard]

I mean equal in the purest form

[Kenny Lau]

are they?

[Kevin Buzzard]

they are indistinguishable with the tools of ZFC

[Mario Carneiro]

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

[Kenny Lau]

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

[Kevin Buzzard]

In ZFC they are the same object

[Mario Carneiro]

in lean they are the same object

[Kenny Lau]

sure, but they aren't equal by definition

[Kenny Lau]

they are equivalent

[Kenny Lau]

exists x, x = y is equivalent to true

[Kevin Buzzard]

How is one supposed to prove that stupid lemma anyway?

[Mario Carneiro]

ext (by simp)

[Mario Carneiro]

I would guess

[Mario Carneiro]

actually it's probably already a theorem

[Kevin Buzzard]

-- 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]

That's what actually happened

[Mario Carneiro]

set.image_id

[Mario Carneiro]

why are you proving trivial set theorems?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

are ZFC tools

[Mario Carneiro]

that theorem is just as hard in zfc land

[Kevin Buzzard]

and here for some reason ZFC tools are not adequate

[Mario Carneiro]

the proof is literally no different

[Kevin Buzzard]

why does simp fail?

[Kevin Buzzard]

This proof is simple

[Kenny Lau]

@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]

That's true for a general mathematician

[Mario Carneiro]

I can tell you I have worked in ZFC

[Kevin Buzzard]

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

[Mario Carneiro]

like for real

[Kevin Buzzard]

You mean "not using pen and paper"

[Kenny Lau]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I guess LaTeX is the true home of ZFC.

[Kevin Buzzard]

For most people.

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

So where do I start?

[Kevin Buzzard]

if I want to do it on a computer

[Kenny Lau]

I thought Isabelle works in ZFC

[Kevin Buzzard]

I don't even know what Isabelle is

[Mario Carneiro]

It uses HOL for all the good stuff

[Kevin Buzzard]

so Isabelle-ZFC is a thing?

[Mario Carneiro]

Isabelle/ZFC is more of a proof of concept

[Kevin Buzzard]

that doesn't sound good

[Kevin Buzzard]

does it have number fields?

[Kenny Lau]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Why not Isabelle-ZFC?

[Mario Carneiro]

because it is not mature enough

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I have no idea

[Kevin Buzzard]

I just play ZFC internally on my own emulator

[Mario Carneiro]

Mizar was written by mathematicians for mathematicians

[Mario Carneiro]

this is not necessarily a good thing

[Kevin Buzzard]

In ZFC

[Mario Carneiro]

in TG set theory

[Kevin Buzzard]

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]

ZFC is an axiom system not a program

[Kevin Buzzard]

I am not CS-wise enough to understand the difference

[Kevin Buzzard]

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

[Kevin Buzzard]

and all things allowed in ZFC are commands

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

sure

[Kevin Buzzard]

I don't know what Mizar is

[Kevin Buzzard]

but I do know what ZFC is

[Kevin Buzzard]

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

[Mario Carneiro]

right, lean doesn't give you a choice here

[Mario Carneiro]

same with most other systems

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

If you got cloned? Lean of course

[Kevin Buzzard]

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

[Mario Carneiro]

because you know lean better than any other system

[Kevin Buzzard]

But Mario, I speak fluent ZFC

[Mario Carneiro]

and you will find that it doesn't matter

[Kevin Buzzard]

It's my native language

[Mario Carneiro]

because you will be struggling with formal details the whole way

[Mario Carneiro]

that's always the way it goes

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

it's one thing to know the theory behind Python

[Kenny Lau]

it's a completely other thing to use Python

[Kevin Buzzard]

I guess

[Kevin Buzzard]

I completely understand that

[Kevin Buzzard]

I see

[Kevin Buzzard]

But this is a really easy problem

[Kevin Buzzard]

I just get the CS people to write python for me

[Kevin Buzzard]

so they are the same thing

[Kevin Buzzard]

Now who wrote ZFC for me?

[Mario Carneiro]

but you don't want ZFC, not really

[Kevin Buzzard]

I love ZFC Mario

[Mario Carneiro]

you want by schoolkid and tactics and magic

[Kevin Buzzard]

Yeah and we _need_ schoolkid

[Mario Carneiro]

ZFC is an axiom system, it made no magical promises

[Kevin Buzzard]

no but you CS guys will just sort all that out

[Kevin Buzzard]

that's just some stupid engineering issue

[Kevin Buzzard]

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

[Mario Carneiro]

but it's a really important engineering issue for you

[Kenny Lau]

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

[Mario Carneiro]

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

[Kevin Buzzard]

id(u) is the same as u

[Kenny Lau]

no they aren't

[Kevin Buzzard]

sure it is

[Kenny Lau]

how would you prove it?

[Mario Carneiro]

that's not a proof

[Kevin Buzzard]

id is a big set of ordered pairs

[Kevin Buzzard]

and they're all just (u,u)

[Kenny Lau]

a proper class

[Kevin Buzzard]

no it's a set

[Kevin Buzzard]

don't be silly

[Mario Carneiro]

wha...

[Kenny Lau]

ok

[Kevin Buzzard]

it's a function from U to U

[Kenny Lau]

but here it isn't

[Mario Carneiro]

ZFC warning

[Kenny Lau]

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

[Kevin Buzzard]

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

[Mario Carneiro]

that's doing to make your job messy

[Kevin Buzzard]

so id(u) is equal to u OK

[Kevin Buzzard]

so {id(u) : u in U}

[Kevin Buzzard]

EQUALS

[Kevin Buzzard]

{u : u in U}

[Kevin Buzzard]

which

[Kenny Lau]

so id(u) is equal to u OK

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

[Kevin Buzzard]

EQUALS

[Kevin Buzzard]

U

[Kevin Buzzard]

I don't understand which bit I missed

[Kenny Lau]

you're abusing notations.

[Kevin Buzzard]

oh

[Mario Carneiro]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

you mixed comprehension notation and subset notation

[Kevin Buzzard]

I am not clear about what = is in ZFC

[Kevin Buzzard]

I forgot the details

[Mario Carneiro]

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

[Kevin Buzzard]

but it just means they're the same object

[Kenny Lau]

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

[Mario Carneiro]

and id is a function because ...

[Kenny Lau]

but it just means they're the same object

but it needs to be proved

[Kenny Lau]

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

[Kenny Lau]

you see, the problem is not in the axioms

[Kenny Lau]

but in the formality

[Mario Carneiro]

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

[Mario Carneiro]

and hey presto it's the lean proof

[Kevin Buzzard]

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

[Kenny Lau]

right, so ZFC isn't the problem at all

[Mario Carneiro]

SIMP CAN PROVE THIS

[Kenny Lau]

yes

[Kevin Buzzard]

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

[Mario Carneiro]

That's not a tactic, that's magic

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

simp can prove this

[Kevin Buzzard]

There are a whole bunch of distinct things in dependent type theory which I have truly identified in my head

[Kevin Buzzard]

and the big question is

[Kevin Buzzard]

is that going to give you problems down the line

[Kevin Buzzard]

by which I mean me

[Kevin Buzzard]

the ZFCist

[Kevin Buzzard]

I got lucky. I needed a map F U -> F (id '' U)

[Kevin Buzzard]

and I chose wrong. I proved id '' U = U and then did a rewrite and used id.

[Kevin Buzzard]

because they're the SAME OBJECT

[Kevin Buzzard]

and the identity map from an object to itself is called id.

[Mario Carneiro]

this is a better argument

[Kevin Buzzard]

So I used id and instantly got into all manner of trouble the moment I tried to prove things

[Kenny Lau]

1. you don't really work in pure ZFC. you work in ZFC + definitorial expansion + a whole bunch of other things

[Kenny Lau]

in ZFC id '' U isn't even defined

[Kenny Lau]

ZFC says that there exists such an object

[Mario Carneiro]

The dtt analogue of this is called equality reflection

[Kenny Lau]

you're using the axiom of replacement

[Kevin Buzzard]

And then I went back and thought "do you know what -- I could use res!"

[Mario Carneiro]

it says that if x = y then x and y are defeq

[Kenny Lau]

it begins forall A exists B

[Kevin Buzzard]

And I thought "that's funny, because it's an axiom of a functor that res U U = id"

[Kenny Lau]

in ZFC everything is Prop

[Mario Carneiro]

This is needed to typecheck things like id : F U -> F (id '' U)

[Kevin Buzzard]

"so res is the same as id"

[Kevin Buzzard]

and I tried res

[Kevin Buzzard]

and then all my one page long goals were rfl

[Kevin Buzzard]

because I gave same ZFC answer in two different ways, the first arguably being "more natural for the ZFC-ist", and the second apparently being "more natural for the DTT-ist".

[Kevin Buzzard]

I don't understand why my id is the wrong idea.

[Patrick Massot]

Kevin, formalized maths will be crazy in any system. You can only hope automation will get better at hiding this crazyness. And it seems DTT is better that set theory in order to build automation

[Mario Carneiro]

You can use id like you did, but you need a lemma about it

[Kevin Buzzard]

I cannot envisage a single problem doing this in ZFC

[Kevin Buzzard]

The issue is making a computer assert this statement?

[Mario Carneiro]

this would be WAY harder in metamath because of all the dependencies

[Kenny Lau]

I cannot envisage a single problem doing this in ZFC

no, you would need as many lemmas

[Kevin Buzzard]

is metamath ZFC?

[Kenny Lau]

ZFC / DTT is not the issue at all

[Mario Carneiro]

lean is good at hiding complexity, which is not always a good thing

[Kevin Buzzard]

I should do a proper survey.

[Mario Carneiro]

on the one hand it means you can formalize much bigger statements, on the other it means you don't work as much on parsimony and as a result have to struggle with large goals

[Kevin Buzzard]

Do I have a complete list of "computer programs which help you do ZFC"?

[Mario Carneiro]

Of course lean is on that list

[Kevin Buzzard]

@Kenny Lau No! Simp didn't prove it! You had to write some .set.image gobble-de-gook theorem as well which probably also says "two identical things are equal"

[Kenny Lau]

@Kevin Buzzard no, I had to write -set.image_id to show that it isn't automated

[Kenny Lau]

because set.image_id is the theorem

[Mario Carneiro]

the set_image thing is just to avoid an even more trivial proof

[Kevin Buzzard]

If simp worked properly, it would solve that goal

[Kevin Buzzard]

just by simp

[Kevin Buzzard]

because it's simple

[Kenny Lau]

Kevin.

[Kenny Lau]

it's a minus.

[Kenny Lau]

I'm telling simp not to use that theorem.

[Kevin Buzzard]

I know

[Kenny Lau]

because otherwise the proof would be trivial

[Mario Carneiro]

just by simp does prove that theorem

[Mario Carneiro]

because it's a simp lemma

[Mario Carneiro]

and without the theorem, the proof is ext $ by simp

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

because it's simple

[Kevin Buzzard]

that's all I'm saying

[Mario Carneiro]

you defined your own image

[Mario Carneiro]

it has no simp lemmas like the real one

[Kevin Buzzard]

you guys are just weirdos

[Kenny Lau]

Kevin

[Mario Carneiro]

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

[Kenny Lau]

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

[Kevin Buzzard]

Maybe it's time I tried Mizar.

[Kevin Buzzard]

I'll come back with egg on my face later

[Kenny Lau]

I don't really see the issue

[Kenny Lau]

I think you're misunderstanding

[Kenny Lau]

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

[Kevin Buzzard]

if it's not by simp for some reason

[Mario Carneiro]

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

[Kevin Buzzard]

then it should be by schoolkid

[Mario Carneiro]

because it's not magic

[Kevin Buzzard]

How can you claim it works well

[Kevin Buzzard]

if it cannot even prove id(U)=U

[Kevin Buzzard]

when they're the same object

[Kevin Buzzard]

That's what I'm hearing :-)

[Mario Carneiro]

you are being unusually stubborn today

[Kenny Lau]

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]

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

[Kevin Buzzard]

but I'm a bit deaf

[Kenny Lau]

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

[Kevin Buzzard]

I was just doing my ZFC-baiting thing

[Kenny Lau]

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

[Kenny Lau]

so I don't know what your issue is

[Kevin Buzzard]

by simp doesn't work for me

[Kevin Buzzard]

does it work for you?

[Kenny Lau]

because you're using the wrong image

[Kevin Buzzard]

I'm using the image I wrote

[Kenny Lau]

use the official image and everything will be fine

[Kenny Lau]

of course your new image doesn't have simp lemmas

[Kevin Buzzard]

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

[Kenny Lau]

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]

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

[Kevin Buzzard]

hmm

[Mario Carneiro]

no

[Kevin Buzzard]

OK so

[Kevin Buzzard]

I can see there might be issues here

[Kenny Lau]

@Kevin Buzzard read my point 4 again

[Kevin Buzzard]

at least

[Kevin Buzzard]

from an engineering point of view

[Mario Carneiro]

the theorems only "work" if you apply them

[Kenny Lau]

@Mario Carneiro it doesn't work

[Kevin Buzzard]

No

[Kevin Buzzard]

I'm listening

[Mario Carneiro]

yeah, I messed up the copy there

[Kevin Buzzard]

I understand that I have to apply my theorems

[Kenny Lau]

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

[Kevin Buzzard]

but in return

[Kevin Buzzard]

here's the thing

[Kenny Lau]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

in DTT speak

[Kevin Buzzard]

theorem they_are_equal : X = Y := by schoolkid

[Johan Commelin]

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

[Kevin Buzzard]

Whenever that happens in dependent type theory

[Kenny Lau]

@Kevin Buzzard Kevin.

[Kevin Buzzard]

I want dependent type theory to now collapse a little

[Kenny Lau]

I think this will convince you.

[Kenny Lau]

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

[Mario Carneiro]

I think you are focusing on the wrong issue Kevin

[Kenny Lau]

you broke the silence >_>

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

Is this supposed to be rfl?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

Is this supposed to be rfl?

I thought we already established that it is not rfl

[Kenny Lau]

not in ZFC either

[Kevin Buzzard]

So that is not rfl

[Kevin Buzzard]

but what was rfl?

[Kenny Lau]

rfl is using "forall x, x = x"

[Mario Carneiro]

schoolkid_1 is simp!

[Kenny Lau]

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

[Kenny Lau]

but they can't be reduced to the same thing

[Mario Carneiro]

ZFC has no reductions at all

[Kenny Lau]

schoolkid_1 is simp!

nope, doesn't work

[Mario Carneiro]

In fact rfl is much weaker in ZFC

[Kenny Lau]

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

[Kevin Buzzard]

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]

+ equality reflection

[Kevin Buzzard]

unknown identifier 'image'

[Kenny Lau]

@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]

I didn't say that

[Kenny Lau]

that's what I mean

[Kevin Buzzard]

I am just trying to get to the bottom of things

[Kevin Buzzard]

but I have never seen refl work for anything

[Kenny Lau]

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

[Kevin Buzzard]

and I've never seen by simp work either

[Kenny Lau]

and i'm working in ZFC to say that

[Kevin Buzzard]

but I'm just trying to put everything together

[Kevin Buzzard]

it's hard trying to distinguish between equal things

[Mario Carneiro]

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

[Mario Carneiro]

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]

that's how definitional expansion is supposed to work

[Mario Carneiro]

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]

@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]

the ZFC version replaces propext with the axiom of extensionality

[Kevin Buzzard]

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]

:-(

[Kevin Buzzard]

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

[Kenny Lau]

I've been repeating the same thing 100 times.

[Mario Carneiro]

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

[Kevin Buzzard]

I've been repeating the same thing 100 times.

I know but you didn't fix it yet

[Kevin Buzzard]

all the proofs are "by schoolkid"

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

you must be blind

[Kevin Buzzard]

but it never just says "by simp"

[Kevin Buzzard]

which ones get done by simp

[Mario Carneiro]

no because that would be horrible in most proofs

[Kenny Lau]

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

[Kevin Buzzard]

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]

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

[Kenny Lau]

here we go again

[Kevin Buzzard]

Why doesn't it do it for me?

[Kevin Buzzard]

That's what I want

[Kevin Buzzard]

Make it do it for me

[Kevin Buzzard]

simp is rubbish

[Kevin Buzzard]

make a proper one

[Kenny Lau]

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

[Kevin Buzzard]

make schoolkid

[Mario Carneiro]

Stop trolling Kevin

[Kevin Buzzard]

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

[Kenny Lau]

I already explained 100 times

[Kevin Buzzard]

Why can my brain do it?

[Kevin Buzzard]

Aren't I just a computer?

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

how?

[Kevin Buzzard]

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

[Kenny Lau]

with 10 definitions that is 1024 choices

[Kenny Lau]

humans are good at small things

[Kenny Lau]

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

[Kevin Buzzard]

I guess here's a good analogue.

[Kevin Buzzard]

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

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

[Kenny Lau]

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

[Kevin Buzzard]

I square small numbers by lookup

[Kevin Buzzard]

they're hard wired

[Kenny Lau]

right

[Kevin Buzzard]

unlike whatever I said 5 minutes ago

[Kenny Lau]

humans are good at small things

[Kenny Lau]

id '' U = U is short

[Kevin Buzzard]

and true!

[Kenny Lau]

here we go again

[Kevin Buzzard]

The world just became a smaller place!

[Kevin Buzzard]

Two things became equal!

[Kevin Buzzard]

They are now the same thing, everyone please update your records

[Kevin Buzzard]

Why doesn't it work like that?

[Kevin Buzzard]

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

[Kenny Lau]

you want a tactic to try to expand definitions

[Kevin Buzzard]

I have no clear idea what tactics do

[Kenny Lau]

that will work for small cases

[Kenny Lau]

that will not work for big cases

[Mario Carneiro]

In general that's undecidable

[Kenny Lau]

humans are only good at small things

[Kevin Buzzard]

Maybe learning tactics would help me understand my frustrations better.

[Andrew Ashworth]

Maybe learning tactics would help me understand my frustrations better.

yes

[Kevin Buzzard]

It's a huge hole in my Lean knowledge

[Kenny Lau]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

?

[Kevin Buzzard]

it works for you?

[Kenny Lau]

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

[Kevin Buzzard]

oh you CHEATED

[Mario Carneiro]

@[simp] can go on definitions

[Kevin Buzzard]

You gave simp a hint

[Mario Carneiro]

YES

[Kevin Buzzard]

So that hint should have been there alreadyt

[Kevin Buzzard]

already

[Kenny Lau]

thanks @Mario Carneiro

[Kevin Buzzard]

why isn't it a simp lemma?

[Kenny Lau]

now I can convince him:

[Kenny Lau]

@[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]

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

[Mario Carneiro]

it should be a simp lemma, I fixed

[Johan Commelin]

why isn't it a simp lemma?

you mean a simp definition?

[Kenny Lau]

@Johan Commelin no, set.image_id

[Kenny Lau]

not a definition

[Johan Commelin]

Aaah, ok, true

[Kenny Lau]

now is @Kevin Buzzard happy?

[Kenny Lau]

after the fix I will be able to remove that line

[Kevin Buzzard]

Oh!

[Kenny Lau]

@[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]

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

[Kevin Buzzard]

All i know is that it passes two basic tests

[Kevin Buzzard]

(1) it's an equality

[Kevin Buzzard]

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

[Mario Carneiro]

image_id is a good simp lemma

[Kevin Buzzard]

My entry requirements for simp are pretty low

[Kenny Lau]

so is @Kevin Buzzard satisfied now?

[Mario Carneiro]

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

[Kevin Buzzard]

image_id is a good simp lemma

I feel I could not say that with confidence

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Exactly.

[Kevin Buzzard]

I want to become a power user

[Mario Carneiro]

because it's a global problem with some locality

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

appear, other than here

[Mario Carneiro]

You could just look at the many many examples in mathlib

[Kevin Buzzard]

reading code is so boring

[Andrew Ashworth]

only masochistic CS graduate students get interested in software verification

[Kevin Buzzard]

that's what CS people do

[Andrew Ashworth]

your tips are folklore in CS departments

[Kevin Buzzard]

I want to talk to more CS people

[Andrew Ashworth]

and that textbook I mentioned yesterday

[Kevin Buzzard]

I need simp tips so I can be a power user

[Mario Carneiro]

term rewriting and all that?

[Andrew Ashworth]

yeah

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and then I knew he'd cracked it

[Mario Carneiro]

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

[Kevin Buzzard]

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]

Actually, how about this for a tactic

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and calls it schoolkid

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I see

[Kevin Buzzard]

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

[Kevin Buzzard]

Is that the question?

[Kevin Buzzard]

Can I code this in a Lean tactic?

[Kenny Lau]

those techniques only work for small cases

[Kevin Buzzard]

Are you saying that this is hard

[Kenny Lau]

they can't be verified

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

@Andrew Ashworth This is exactly the point.

[Kenny Lau]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and I was just assuming it was going to be easy

[Kenny Lau]

the world is imperfect

[Kenny Lau]

computability matters

[Mario Carneiro]

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

[Kevin Buzzard]

that's an engineering problem

[Kevin Buzzard]

you CS guys write great algos

[Kevin Buzzard]

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

[Mario Carneiro]

no that's a fundamental limit on progress

[Kenny Lau]

no, you can't

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

you don't

[Kevin Buzzard]

and which questions look sensible to me like the Langlands Programme

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

including your brain

[Kenny Lau]

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

[Mario Carneiro]

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

[Andrew Ashworth]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

I have plenty of theorems in metamath as evidence

[Mario Carneiro]

but proof engineering is a really important skill

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Mario Carneiro]

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

[Andrew Ashworth]

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]

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

[Mario Carneiro]

but I grant that working with lean encourages good automation practices

[Andrew Ashworth]

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]

what was the solution?

[Andrew Ashworth]

to what?

[Kevin Buzzard]

in ZFC id '' U isn't even defined

Oh what a bore, you're right

[Mario Carneiro]

metamath uses ZFC + classes to get around this

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

it's called using interface to make your life better

[Kevin Buzzard]

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]

@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]

no, I mean the axiom of extensionality.

[Kevin Buzzard]

@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?

[Mario Carneiro]

no

[Kevin Buzzard]

it looks good to me

[Kevin Buzzard]

simple predicate

[Kevin Buzzard]

implies an equality

[Mario Carneiro]

it says p = q in the conclusion

[Kevin Buzzard]

it got over my simp bar

[Mario Carneiro]

that means anything equals anything

[Mario Carneiro]

it's too general

[Kevin Buzzard]

Just apply it sensibly

[Kevin Buzzard]

and stop moaning

[Kevin Buzzard]

don't just apply it randomly

[Kevin Buzzard]

:-/

[Kevin Buzzard]

This is really interesting

[Kevin Buzzard]

this is the hard bit

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

otherwise simp has to be creative when rewriting

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

That's your job

[Kevin Buzzard]

you went to math classe

[Kevin Buzzard]

s

[Kevin Buzzard]

you know how we think

[Mario Carneiro]

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

[Kevin Buzzard]

can you write a better interface?

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

I think you had a more grown-up name

[Kenny Lau]

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]

I think you had a more grown-up name

math_trivial?

[Mario Carneiro]

Mizar is actually stronger axiomatically than lean

[Kenny Lau]

why?

[Mario Carneiro]

it has a proper class of inaccessibles

[Johan Commelin]

But I wouldn't mind have kindergarten or schoolkid

[Kenny Lau]

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

[Kenny Lau]

but it seems that you are deaf

[Andrew Ashworth]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

they are organized fairly logically

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

it's init this and data that

[Kevin Buzzard]

when I want set.image_id

[Kevin Buzzard]

I type #check set.image_id

[Kevin Buzzard]

and it's not there

[Kevin Buzzard]

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

[Kevin Buzzard]

I have no clue where anything is

[Kevin Buzzard]

they're just all theorems

[Kevin Buzzard]

Can we have a better search?

[Mario Carneiro]

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

[Kevin Buzzard]

oh!

[Kevin Buzzard]

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

[Kevin Buzzard]

Does that work with everything?

[Mario Carneiro]

it's not even set.something

[Kevin Buzzard]

can I import scheme?

[Mario Carneiro]

it's data.set.basic

[Mario Carneiro]

but vscode will still give it to you

[Kevin Buzzard]

I see

[Kevin Buzzard]

I should "key on set"

[Kevin Buzzard]

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.

[Kenny Lau]

are they

[Kevin Buzzard]

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

[Kevin Buzzard]

I am only interested in the Langlands Programme

[Kevin Buzzard]

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]

it's called using interface to make your life better

I need better interface search.

[Kevin Buzzard]

I thought we have google nowadays. Why isn't search easy?

[Kevin Buzzard]

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

[Kevin Buzzard]

Can that be a thing one day?

[Sean Leather]

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

[Andrew Ashworth]

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]

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]

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]

I could do all the costings for that other than salary

[Kevin Buzzard]

I have no idea how much you guys get paid

[Kevin Buzzard]

the administration would be able to fill in the other boxes

[Kevin Buzzard]

I'm meeting with EPSRC in two weeks

[Kevin Buzzard]

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]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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]

I just wrote a theorem that was in the library

[Kevin Buzzard]

yay me

[Kevin Buzzard]

#check topological_space.open_immersion_id

[Kevin Buzzard]

#check topological_space.id_open_immersion

[Kevin Buzzard]

what should it be called?

[Kevin Buzzard]

The statement that the identity map is an open immersion

[Kevin Buzzard]

I did the other one

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

What do the artists say about this one?

[Patrick Massot]

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

[Patrick Massot]

I'm much slower

[Kevin Buzzard]

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

[Kevin Buzzard]

But I am stuck on something

[Kevin Buzzard]

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

[Kevin Buzzard]

in my context

[Kevin Buzzard]

oh I can answer my own question

[Kevin Buzzard]

oh no I can't

[Kevin Buzzard]

Ok so there's my x

[Kevin Buzzard]

and presheaf_of_types_pullback_under_open_immersion just has some definition

[Kevin Buzzard]

which explictly says what its F bit is

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I can't unfold presheaf_of_types_pullback_under_open_immersion

[Kevin Buzzard]

Do people need more context?

[Kevin Buzzard]

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

[Patrick Massot]

Did you try dsimp at x?

[Kevin Buzzard]

I did

[Kevin Buzzard]

it wasn't very effective

[Kevin Buzzard]

it turned presheaf_of_rings_pullback_under_open_immersion

[Kevin Buzzard]

into presheaf_of_types_pullback_under_open_immersion

[Kevin Buzzard]

and then stopped

[Kevin Buzzard]

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

[Patrick Massot]

Is it something I can git clone?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

can git help me here?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

goofing around

[Patrick Massot]

you could create a broken branch

[Kevin Buzzard]

Can I do that in VS Code?

[Kevin Buzzard]

I only have master

[Patrick Massot]

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

[Kevin Buzzard]

I've got it

[Patrick Massot]

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

[Kevin Buzzard]

Oh crap I didn't stash

[Kevin Buzzard]

is that an issue?

[Patrick Massot]

maybe not

[Patrick Massot]

it wrote that to be on the safe side

[Kevin Buzzard]

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

[Kevin Buzzard]

oops

[Kevin Buzzard]

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

[Kevin Buzzard]

was what I meant to say

[Kevin Buzzard]

line 495, I want to unfold that presheaf_of_types_pullback_under_open_immersion

[Kevin Buzzard]

no

[Kevin Buzzard]

I want Lean to unfold it

[Kevin Buzzard]

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

[Patrick Massot]

This is really irritating

[Kevin Buzzard]

OK I minimised

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

which are a bit like distribs

[Kevin Buzzard]

and although the objects are a bit silly

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

which I am convinced a computer could have done for me

[Kevin Buzzard]

I cut and pasted the definition of pre_semi_sheaf_of_rings_pullback

[Kevin Buzzard]

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

[Kevin Buzzard]

but the problem is that the unfolding is refl

[Kevin Buzzard]

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

[Kevin Buzzard]

I have to work it out myself

[Kevin Buzzard]

This is an independent question

[Johan Commelin]

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

[Kevin Buzzard]

Oh cool

[Kevin Buzzard]

but OK I have finally minimised my question

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

That's my challenge to the CS people, I think

[Kevin Buzzard]

I'm not sure I can prove that goal

[Kevin Buzzard]

I'm not even sure that goal is true

[Kevin Buzzard]

but I think it is

[Kevin Buzzard]

for some reason it's a pain to prove though

[Kevin Buzzard]

I'm hoping the file is fairly self-explanatory

[Johan Commelin]

It is "math-true", right?

[Kevin Buzzard]

exactly Johan

[Kevin Buzzard]

Before I had something which was math-true

[Kevin Buzzard]

and Kenny and Mario kept telling me it could be done by simp

[Kevin Buzzard]

I would like them to tell me how to do this one

[Johan Commelin]

Are the rings essential to the problem?

[Johan Commelin]

Or could you just use semi-quasi-demi-pre-sheaves of types?

[Kevin Buzzard]

No it's crucial they're rings

[Kevin Buzzard]

because it's a trivial way to make it even harder

[Kevin Buzzard]

this is a content-free statement from where I'm standing

[Kevin Buzzard]

and if there aren't algorithms which currently prove content-free statements like this

[Kevin Buzzard]

then I think that mathematicians will find it hard to learn Lean

[Kevin Buzzard]

@Kenny Lau @Mario Carneiro Can you fill in my sorry?

[Kevin Buzzard]

Am I missing something easy?

[Patrick Massot]

Oh, he went back a couple of stages

[Kevin Buzzard]

I removed topology

[Kevin Buzzard]

and open immersions

[Kenny Lau]

Am I missing something easy?

no

[Kevin Buzzard]

crap

[Kevin Buzzard]

is that a provable but hard goal?

[Kenny Lau]

well not really hard

[Kenny Lau]

i could do it

[Kenny Lau]

but not exactly easy

[Kevin Buzzard]

Teach me how to do it

[Kevin Buzzard]

I can't do it

[Kevin Buzzard]

and it's obvious

[Kevin Buzzard]

and these are my least favourite things in Lean

[Kevin Buzzard]

teach me how to kill this pokemon

[Johan Commelin]

@Kevin Buzzard you don't only want schoolkid tactic, you also want kenny_lau and mario_carneiro

[Kevin Buzzard]

exactly

[Kevin Buzzard]

Kenny

[Kevin Buzzard]

I'm up to here

[Kevin Buzzard]

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

[Kenny Lau]

I'm trying

[Kevin Buzzard]

Thanks

[Kevin Buzzard]

Are you writing a tactic?

[Kevin Buzzard]

Don't try to solve the goal

[Kenny Lau]

no

[Kevin Buzzard]

try to write a tactic which solves the goal

[Kenny Lau]

I don't know how to write tactics

[Kevin Buzzard]

because this goal is solved by math_trivial

[Kevin Buzzard]

This goal is the nightmare which I could avoid in my case of presheaves

[Kevin Buzzard]

but a pre_semi_sheaf does not have res

[Kevin Buzzard]

so you have to bite the bullet

[Kevin Buzzard]

@Simon Hudon Can you solve my goal with a tactic?

[Kevin Buzzard]

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

[Kevin Buzzard]

Last line

[Kevin Buzzard]

the pre_semi_sheaves are isomorphic via the identity map

[Kevin Buzzard]

but checking the details is apparently a little tricky

[Kevin Buzzard]

Would I have exactly the same problems in Mizar?

[Kevin Buzzard]

@Assia Mahboubi Would my goal be any easier to solve in Coq?

[Kevin Buzzard]

I have isolated a frustration I have with dependent type theory

[Kevin Buzzard]

I need to define a map from F U to F (id '' U)

[Kevin Buzzard]

where id '' U is the image of the set U under the identity map

[Kevin Buzzard]

I define the map by rewriting id '' U = U and then using the identity

[Kevin Buzzard]

and I never recover

[Kevin Buzzard]

But I don't know any other way of doing it

[Kevin Buzzard]

Is there some sort of reason why I should not be proving this goal at all?

[Simon Hudon]

How would you prove it without tactics?

[Kenny Lau]

he can't function without tactics

[Kenny Lau]

you would do eq.drec without tactics

[Simon Hudon]

I mean, I don't know any of the context so I'm not sure how the definitions relate to each other

[Assia Mahboubi]

@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]

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

[Kenny Lau]

@Assia Mahboubi just prove the above

[Kenny Lau]

@Kevin Buzzard you know what, I take back my word, it's harder than I thought

[Assia Mahboubi]

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.

[Kenny Lau]

oh, sorry

[Kenny Lau]

I think you can try it online

[Kenny Lau]

https://leanprover.github.io/live/latest/

[Assia Mahboubi]

Ok thanks, I am doing that now.

[Kevin Buzzard]

Does one run into the same issues in Coq?

[Kevin Buzzard]

Does one run into the same issues in Mizar?

[Kevin Buzzard]

Which systems is this easy in?

[Kevin Buzzard]

@Assia Mahboubi I suspect you can see what I'm trying to do

[Kevin Buzzard]

I'm happy to let a lean expert like Mario or Kenny solve the lean one

[Kevin Buzzard]

I am trying to understand to what extent my worldview of mathematics is naive

[Kenny Lau]

lol it's been an hour already

[Kevin Buzzard]

The challenge was embedded well in a very long thread and I would imagine many have stopped reading

[Kevin Buzzard]

One could ask in a new thread, I think this question is sufficiently interesting

[Kevin Buzzard]

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]

I tried to build up an interface

[Kenny Lau]

didn't work

[Assia Mahboubi]

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.

[Kenny Lau]

see you

[Kevin Buzzard]

@Kenny Lau

[Kevin Buzzard]

I had an idea

[Kevin Buzzard]

but you would be quicker to implement it than me

[Kenny Lau]

what is it

[Kevin Buzzard]

and I have to tidy the kitchen anyway

[Kevin Buzzard]

I claim that my definition is incomplete

[Kevin Buzzard]

as far as Lean is concerned

[Kevin Buzzard]

I am missing some extra structure

[Kevin Buzzard]

which can be filled in easily

[Kevin Buzzard]

Is the "correct" object a pre_semi_sheaf whatever, but also equipped with maps res : F U -> F V whenever U = V

[Kevin Buzzard]

plus axiom that res U U = id

[Kevin Buzzard]

plus axiom of composition

[Kevin Buzzard]

res U V then res V W is res U W

[Kevin Buzzard]

Given my stupid annoying structure

[Kevin Buzzard]

can it be beefed up to such a structure

[Kevin Buzzard]

and for this beefed-up structure

[Kevin Buzzard]

can the map be defined to be res

[Kevin Buzzard]

and then we deduce the result for the stupid structure

[Kevin Buzzard]

My experience with schemes tells me

[Kevin Buzzard]

that when the map is res

[Kevin Buzzard]

all the hard proofs become rfl

[Kevin Buzzard]

maybe not the ring one

[Kevin Buzzard]

the ring one we have to use some equiv tactic thing

[Reid Barton]

@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]

I was hoping you'd show up

[Kevin Buzzard]

I thought you'd like this one

[Kevin Buzzard]

I am cooking, will look later. Did you do it?

[Reid Barton]

Yes

[Kevin Buzzard]

Convert? What does that do?

[Reid Barton]

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]

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]

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]

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]

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]

Does https://www.math.u-psud.fr/~pmassot/files/lean/install_lean.sh contain precompiled mathlib nightlies?

[Patrick Massot]

yes

[Johan Commelin]

Nice! I guess in this file, right? https://www.math.u-psud.fr/~pmassot/files/lean/.lean.tar.gz

[Patrick Massot]

yes

[Johan Commelin]

Ok, you should change the topic of your anouncement. This deserves more PR.

[Patrick Massot]

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]

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

[Patrick Massot]

Have fun!

[Assia Mahboubi]

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]

It does what it says in https://www.math.u-psud.fr/~pmassot/files/lean/install_lean.sh

[Patrick Massot]

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]

Let me check you can run Kevin's code using this version of mathlib

[Johan Commelin]

[sorry, wrong topic]

[Assia Mahboubi]

@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]

@Assia Mahboubi It will be super easy to update Lean later.

[Johan Commelin]

Patrick's script just puts together the steps that you would otherwise perform manually.

[Johan Commelin]

And he has compiled mathlib for you. Which saves you an hour of coffee breaks :wink:

[Assia Mahboubi]

Hi @Johan Commelin , thanks for the help. I am trying it now.

[Patrick Massot]

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]

There will probably be some errors because this repo is still a messy playground

[Patrick Massot]

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]

Now I'll really go to IHES where I'll probably open Zulip anyway, but not VScode

[Assia Mahboubi]

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]

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]

Yes, we know that feeling... (-;

[Johan Commelin]

I wasn't joking when I told you about the "hour of coffee breaks"

[Patrick Massot]

This is exactly what I tried to avoid

[Patrick Massot]

My instructions should bypass mathlib compilation

[Patrick Massot]

(I'm waiting for my train)