Zulip Chat Archive

Stream: maths

Topic: ZFC equality


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

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:33):

And now here's something which doesn't work

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:33):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:33):

Does that mean that my definition of image is wrong?

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:33):

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:34):

they are definitely not defeq

view this post on Zulip Kenny Lau (May 28 2018 at 09:34):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:34):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:34):

Can you write a better one for me

view this post on Zulip Kenny Lau (May 28 2018 at 09:34):

no, it isn't

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:34):

where they are defeq

view this post on Zulip Kenny Lau (May 28 2018 at 09:34):

you can't

view this post on Zulip Kenny Lau (May 28 2018 at 09:34):

you have to have an existential quantifier

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:34):

can you prove that you can't?

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:34):

in Lean

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:35):

3.4.1

view this post on Zulip Mario Carneiro (May 28 2018 at 09:35):

not in lean

view this post on Zulip Mario Carneiro (May 28 2018 at 09:35):

it's a metatheorem

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:35):

Great.

view this post on Zulip Kenny Lau (May 28 2018 at 09:35):

@Mario Carneiro can it actually be proved?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:35):

probably

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:35):

Well you know what

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:35):

I think defeq is rubbish

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:35):

because those two sets are equal

view this post on Zulip Kenny Lau (May 28 2018 at 09:36):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:36):

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:36):

but not definitionally equal

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:36):

so what has gone wrong?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:36):

nothing is wrong

view this post on Zulip Mario Carneiro (May 28 2018 at 09:36):

defeq is not ZFC equality

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:36):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:37):

I mean equal in the purest form

view this post on Zulip Kenny Lau (May 28 2018 at 09:37):

are they?

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:37):

they are indistinguishable with the tools of ZFC

view this post on Zulip Mario Carneiro (May 28 2018 at 09:37):

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:37):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:37):

In ZFC they are the same object

view this post on Zulip Mario Carneiro (May 28 2018 at 09:37):

in lean they are the same object

view this post on Zulip Kenny Lau (May 28 2018 at 09:37):

sure, but they aren't equal by definition

view this post on Zulip Kenny Lau (May 28 2018 at 09:37):

they are equivalent

view this post on Zulip Kenny Lau (May 28 2018 at 09:37):

exists x, x = y is equivalent to true

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:38):

How is one supposed to prove that stupid lemma anyway?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:38):

ext (by simp)

view this post on Zulip Mario Carneiro (May 28 2018 at 09:38):

I would guess

view this post on Zulip Mario Carneiro (May 28 2018 at 09:38):

actually it's probably already a theorem

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:39):

That's what actually happened

view this post on Zulip Mario Carneiro (May 28 2018 at 09:39):

set.image_id

view this post on Zulip Mario Carneiro (May 28 2018 at 09:39):

why are you proving trivial set theorems?

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:39):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:40):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:40):

are ZFC tools

view this post on Zulip Mario Carneiro (May 28 2018 at 09:40):

that theorem is just as hard in zfc land

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:40):

and here for some reason ZFC tools are not adequate

view this post on Zulip Mario Carneiro (May 28 2018 at 09:40):

the proof is literally no different

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:41):

why does simp fail?

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:41):

This proof is simple

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:41):

That's true for a general mathematician

view this post on Zulip Mario Carneiro (May 28 2018 at 09:41):

I can tell you I have worked in ZFC

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:41):

like for real

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:42):

You mean "not using pen and paper"

view this post on Zulip Kenny Lau (May 28 2018 at 09:42):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:42):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:42):

I guess LaTeX is the true home of ZFC.

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:43):

For most people.

view this post on Zulip Andrew Ashworth (May 28 2018 at 09:43):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:43):

So where do I start?

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:44):

if I want to do it on a computer

view this post on Zulip Kenny Lau (May 28 2018 at 09:44):

I thought Isabelle works in ZFC

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:44):

I don't even know what Isabelle is

view this post on Zulip Mario Carneiro (May 28 2018 at 09:44):

It uses HOL for all the good stuff

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:44):

so Isabelle-ZFC is a thing?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:44):

Isabelle/ZFC is more of a proof of concept

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:44):

that doesn't sound good

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:44):

does it have number fields?

view this post on Zulip Kenny Lau (May 28 2018 at 09:45):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:45):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:45):

Why not Isabelle-ZFC?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:45):

because it is not mature enough

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:45):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:46):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:46):

I have no idea

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:46):

I just play ZFC internally on my own emulator

view this post on Zulip Mario Carneiro (May 28 2018 at 09:46):

Mizar was written by mathematicians for mathematicians

view this post on Zulip Mario Carneiro (May 28 2018 at 09:46):

this is not necessarily a good thing

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:46):

In ZFC

view this post on Zulip Mario Carneiro (May 28 2018 at 09:46):

in TG set theory

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:47):

ZFC is an axiom system not a program

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:47):

I am not CS-wise enough to understand the difference

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:47):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:48):

and all things allowed in ZFC are commands

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:48):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:48):

sure

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:48):

I don't know what Mizar is

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:48):

but I do know what ZFC is

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:48):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:49):

right, lean doesn't give you a choice here

view this post on Zulip Mario Carneiro (May 28 2018 at 09:49):

same with most other systems

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:50):

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:50):

If you got cloned? Lean of course

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:50):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:51):

because you know lean better than any other system

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:51):

But Mario, I speak fluent ZFC

view this post on Zulip Mario Carneiro (May 28 2018 at 09:51):

and you will find that it doesn't matter

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:51):

It's my native language

view this post on Zulip Mario Carneiro (May 28 2018 at 09:51):

because you will be struggling with formal details the whole way

view this post on Zulip Mario Carneiro (May 28 2018 at 09:51):

that's always the way it goes

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:51):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:53):

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:53):

it's one thing to know the theory behind Python

view this post on Zulip Kenny Lau (May 28 2018 at 09:53):

it's a completely other thing to use Python

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:53):

I guess

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:53):

I completely understand that

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:53):

I see

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:54):

But this is a really easy problem

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:54):

I just get the CS people to write python for me

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:54):

so they are the same thing

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:54):

Now who wrote ZFC for me?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:54):

but you don't want ZFC, not really

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:55):

I love ZFC Mario

view this post on Zulip Mario Carneiro (May 28 2018 at 09:55):

you want by schoolkid and tactics and magic

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:55):

Yeah and we _need_ schoolkid

view this post on Zulip Mario Carneiro (May 28 2018 at 09:55):

ZFC is an axiom system, it made no magical promises

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:55):

no but you CS guys will just sort all that out

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:55):

that's just some stupid engineering issue

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:55):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:55):

but it's a really important engineering issue for you

view this post on Zulip Kenny Lau (May 28 2018 at 09:55):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:56):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:56):

id(u) is the same as u

view this post on Zulip Kenny Lau (May 28 2018 at 09:56):

no they aren't

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:56):

sure it is

view this post on Zulip Kenny Lau (May 28 2018 at 09:56):

how would you prove it?

view this post on Zulip Mario Carneiro (May 28 2018 at 09:56):

that's not a proof

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:56):

id is a big set of ordered pairs

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:56):

and they're all just (u,u)

view this post on Zulip Kenny Lau (May 28 2018 at 09:56):

a proper class

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:56):

no it's a set

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:56):

don't be silly

view this post on Zulip Mario Carneiro (May 28 2018 at 09:57):

wha...

view this post on Zulip Kenny Lau (May 28 2018 at 09:57):

ok

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

it's a function from U to U

view this post on Zulip Kenny Lau (May 28 2018 at 09:57):

but here it isn't

view this post on Zulip Mario Carneiro (May 28 2018 at 09:57):

ZFC warning

view this post on Zulip Kenny Lau (May 28 2018 at 09:57):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:57):

that's doing to make your job messy

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

so id(u) is equal to u OK

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

so {id(u) : u in U}

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

EQUALS

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

{u : u in U}

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

which

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

EQUALS

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:57):

U

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:58):

I don't understand which bit I missed

view this post on Zulip Kenny Lau (May 28 2018 at 09:58):

you're abusing notations.

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:58):

oh

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:58):

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:58):

you mixed comprehension notation and subset notation

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:58):

I am not clear about what = is in ZFC

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:58):

I forgot the details

view this post on Zulip Mario Carneiro (May 28 2018 at 09:58):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 09:58):

but it just means they're the same object

view this post on Zulip Kenny Lau (May 28 2018 at 09:58):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:59):

and id is a function because ...

view this post on Zulip Kenny Lau (May 28 2018 at 09:59):

but it just means they're the same object

but it needs to be proved

view this post on Zulip Kenny Lau (May 28 2018 at 09:59):

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

view this post on Zulip Kenny Lau (May 28 2018 at 09:59):

you see, the problem is not in the axioms

view this post on Zulip Kenny Lau (May 28 2018 at 09:59):

but in the formality

view this post on Zulip Mario Carneiro (May 28 2018 at 09:59):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 09:59):

and hey presto it's the lean proof

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:00):

right, so ZFC isn't the problem at all

view this post on Zulip Mario Carneiro (May 28 2018 at 10:00):

SIMP CAN PROVE THIS

view this post on Zulip Kenny Lau (May 28 2018 at 10:00):

yes

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:00):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:00):

That's not a tactic, that's magic

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:00):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:00):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:00):

simp can prove this

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:00):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:01):

and the big question is

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:01):

is that going to give you problems down the line

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:01):

by which I mean me

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:01):

the ZFCist

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:01):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:02):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:02):

because they're the SAME OBJECT

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:02):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:02):

this is a better argument

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:02):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:02):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:02):

in ZFC id '' U isn't even defined

view this post on Zulip Kenny Lau (May 28 2018 at 10:03):

ZFC says that there exists such an object

view this post on Zulip Mario Carneiro (May 28 2018 at 10:03):

The dtt analogue of this is called equality reflection

view this post on Zulip Kenny Lau (May 28 2018 at 10:03):

you're using the axiom of replacement

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:03):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:03):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:03):

it begins forall A exists B

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:03):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:03):

in ZFC everything is Prop

view this post on Zulip Mario Carneiro (May 28 2018 at 10:03):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:03):

"so res is the same as id"

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:04):

and I tried res

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:04):

and then all my one page long goals were rfl

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:05):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:05):

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

view this post on Zulip Patrick Massot (May 28 2018 at 10:05):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:05):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:05):

I cannot envisage a single problem doing this in ZFC

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:06):

The issue is making a computer assert this statement?

view this post on Zulip Mario Carneiro (May 28 2018 at 10:06):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:06):

I cannot envisage a single problem doing this in ZFC

no, you would need as many lemmas

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:06):

is metamath ZFC?

view this post on Zulip Kenny Lau (May 28 2018 at 10:06):

ZFC / DTT is not the issue at all

view this post on Zulip Mario Carneiro (May 28 2018 at 10:06):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:07):

I should do a proper survey.

view this post on Zulip Mario Carneiro (May 28 2018 at 10:07):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:07):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:08):

Of course lean is on that list

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:09):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:09):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:09):

because set.image_id is the theorem

view this post on Zulip Mario Carneiro (May 28 2018 at 10:09):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:09):

If simp worked properly, it would solve that goal

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:09):

just by simp

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:09):

because it's simple

view this post on Zulip Kenny Lau (May 28 2018 at 10:09):

Kevin.

view this post on Zulip Kenny Lau (May 28 2018 at 10:09):

it's a minus.

view this post on Zulip Kenny Lau (May 28 2018 at 10:09):

I'm telling simp not to use that theorem.

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

I know

view this post on Zulip Kenny Lau (May 28 2018 at 10:10):

because otherwise the proof would be trivial

view this post on Zulip Mario Carneiro (May 28 2018 at 10:10):

just by simp does prove that theorem

view this post on Zulip Mario Carneiro (May 28 2018 at 10:10):

because it's a simp lemma

view this post on Zulip Mario Carneiro (May 28 2018 at 10:10):

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

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

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

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

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

because it's simple

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

that's all I'm saying

view this post on Zulip Mario Carneiro (May 28 2018 at 10:10):

you defined your own image

view this post on Zulip Mario Carneiro (May 28 2018 at 10:11):

it has no simp lemmas like the real one

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:11):

you guys are just weirdos

view this post on Zulip Kenny Lau (May 28 2018 at 10:11):

Kevin

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:11):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:11):

Maybe it's time I tried Mizar.

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:11):

I'll come back with egg on my face later

view this post on Zulip Kenny Lau (May 28 2018 at 10:12):

I don't really see the issue

view this post on Zulip Kenny Lau (May 28 2018 at 10:12):

I think you're misunderstanding

view this post on Zulip Kenny Lau (May 28 2018 at 10:12):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:12):

if it's not by simp for some reason

view this post on Zulip Mario Carneiro (May 28 2018 at 10:12):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:12):

then it should be by schoolkid

view this post on Zulip Mario Carneiro (May 28 2018 at 10:12):

because it's not magic

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:12):

How can you claim it works well

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:12):

if it cannot even prove id(U)=U

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:12):

when they're the same object

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:13):

That's what I'm hearing :-)

view this post on Zulip Mario Carneiro (May 28 2018 at 10:13):

you are being unusually stubborn today

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:13):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:13):

but I'm a bit deaf

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:13):

I was just doing my ZFC-baiting thing

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:13):

so I don't know what your issue is

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:14):

by simp doesn't work for me

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:14):

does it work for you?

view this post on Zulip Kenny Lau (May 28 2018 at 10:14):

because you're using the wrong image

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:14):

I'm using the image I wrote

view this post on Zulip Kenny Lau (May 28 2018 at 10:14):

use the official image and everything will be fine

view this post on Zulip Kenny Lau (May 28 2018 at 10:14):

of course your new image doesn't have simp lemmas

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:14):

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

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:15):

hmm

view this post on Zulip Mario Carneiro (May 28 2018 at 10:15):

no

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:15):

OK so

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:16):

I can see there might be issues here

view this post on Zulip Kenny Lau (May 28 2018 at 10:16):

@Kevin Buzzard read my point 4 again

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:16):

at least

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:16):

from an engineering point of view

view this post on Zulip Mario Carneiro (May 28 2018 at 10:16):

the theorems only "work" if you apply them

view this post on Zulip Kenny Lau (May 28 2018 at 10:16):

@Mario Carneiro it doesn't work

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:16):

No

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:16):

I'm listening

view this post on Zulip Mario Carneiro (May 28 2018 at 10:17):

yeah, I messed up the copy there

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:17):

I understand that I have to apply my theorems

view this post on Zulip Kenny Lau (May 28 2018 at 10:17):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:17):

but in return

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:17):

here's the thing

view this post on Zulip Kenny Lau (May 28 2018 at 10:17):

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

view this post on Zulip Johan Commelin (May 28 2018 at 10:17):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:17):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:17):

in DTT speak

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:18):

theorem they_are_equal : X = Y := by schoolkid

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:18):

Whenever that happens in dependent type theory

view this post on Zulip Kenny Lau (May 28 2018 at 10:18):

@Kevin Buzzard Kevin.

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:18):

I want dependent type theory to now collapse a little

view this post on Zulip Kenny Lau (May 28 2018 at 10:18):

I think this will convince you.

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

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

I think you are focusing on the wrong issue Kevin

view this post on Zulip Kenny Lau (May 28 2018 at 10:20):

you broke the silence >_>

view this post on Zulip Johan Commelin (May 28 2018 at 10:20):

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:22):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:22):

Is this supposed to be rfl?

view this post on Zulip Mario Carneiro (May 28 2018 at 10:22):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:22):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:22):

Is this supposed to be rfl?

I thought we already established that it is not rfl

view this post on Zulip Kenny Lau (May 28 2018 at 10:22):

not in ZFC either

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:22):

So that is not rfl

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:22):

but what was rfl?

view this post on Zulip Kenny Lau (May 28 2018 at 10:22):

rfl is using "forall x, x = x"

view this post on Zulip Mario Carneiro (May 28 2018 at 10:22):

schoolkid_1 is simp!

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:23):

but they can't be reduced to the same thing

view this post on Zulip Mario Carneiro (May 28 2018 at 10:23):

ZFC has no reductions at all

view this post on Zulip Kenny Lau (May 28 2018 at 10:23):

schoolkid_1 is simp!

nope, doesn't work

view this post on Zulip Mario Carneiro (May 28 2018 at 10:23):

In fact rfl is much weaker in ZFC

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:24):

+ equality reflection

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:24):

unknown identifier 'image'

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:24):

I didn't say that

view this post on Zulip Kenny Lau (May 28 2018 at 10:25):

that's what I mean

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:25):

I am just trying to get to the bottom of things

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:25):

but I have never seen refl work for anything

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:25):

and I've never seen by simp work either

view this post on Zulip Kenny Lau (May 28 2018 at 10:25):

and i'm working in ZFC to say that

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:25):

but I'm just trying to put everything together

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:25):

it's hard trying to distinguish between equal things

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

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

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

that's how definitional expansion is supposed to work

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:30):

the ZFC version replaces propext with the axiom of extensionality

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:31):

:-(

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:31):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:31):

I've been repeating the same thing 100 times.

view this post on Zulip Mario Carneiro (May 28 2018 at 10:32):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:32):

all the proofs are "by schoolkid"

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:32):

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:32):

you must be blind

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:33):

but it never just says "by simp"

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:33):

which ones get done by simp

view this post on Zulip Mario Carneiro (May 28 2018 at 10:33):

no because that would be horrible in most proofs

view this post on Zulip Kenny Lau (May 28 2018 at 10:33):

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

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:34):

here we go again

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:34):

Why doesn't it do it for me?

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:34):

That's what I want

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:34):

Make it do it for me

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:34):

simp is rubbish

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:34):

make a proper one

view this post on Zulip Kenny Lau (May 28 2018 at 10:34):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:34):

make schoolkid

view this post on Zulip Mario Carneiro (May 28 2018 at 10:35):

Stop trolling Kevin

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:35):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:35):

I already explained 100 times

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:35):

Why can my brain do it?

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:35):

Aren't I just a computer?

view this post on Zulip Kenny Lau (May 28 2018 at 10:35):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:36):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:36):

how?

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:36):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:36):

with 10 definitions that is 1024 choices

view this post on Zulip Kenny Lau (May 28 2018 at 10:36):

humans are good at small things

view this post on Zulip Kenny Lau (May 28 2018 at 10:36):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:36):

I guess here's a good analogue.

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:37):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:37):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:37):

I square small numbers by lookup

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:37):

they're hard wired

view this post on Zulip Kenny Lau (May 28 2018 at 10:37):

right

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:37):

unlike whatever I said 5 minutes ago

view this post on Zulip Kenny Lau (May 28 2018 at 10:37):

humans are good at small things

view this post on Zulip Kenny Lau (May 28 2018 at 10:37):

id '' U = U is short

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:37):

and true!

view this post on Zulip Kenny Lau (May 28 2018 at 10:38):

here we go again

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:38):

The world just became a smaller place!

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:38):

Two things became equal!

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:38):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:38):

Why doesn't it work like that?

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:38):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:38):

you want a tactic to try to expand definitions

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:39):

I have no clear idea what tactics do

view this post on Zulip Kenny Lau (May 28 2018 at 10:39):

that will work for small cases

view this post on Zulip Kenny Lau (May 28 2018 at 10:39):

that will not work for big cases

view this post on Zulip Mario Carneiro (May 28 2018 at 10:39):

In general that's undecidable

view this post on Zulip Kenny Lau (May 28 2018 at 10:39):

humans are only good at small things

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:39):

Maybe learning tactics would help me understand my frustrations better.

view this post on Zulip Andrew Ashworth (May 28 2018 at 10:39):

Maybe learning tactics would help me understand my frustrations better.

yes

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:39):

It's a huge hole in my Lean knowledge

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:39):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:40):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:40):

?

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:40):

it works for you?

view this post on Zulip Kenny Lau (May 28 2018 at 10:40):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:40):

oh you CHEATED

view this post on Zulip Mario Carneiro (May 28 2018 at 10:40):

@[simp] can go on definitions

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:40):

You gave simp a hint

view this post on Zulip Mario Carneiro (May 28 2018 at 10:41):

YES

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:41):

So that hint should have been there alreadyt

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:41):

already

view this post on Zulip Kenny Lau (May 28 2018 at 10:41):

thanks @Mario Carneiro

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:41):

why isn't it a simp lemma?

view this post on Zulip Kenny Lau (May 28 2018 at 10:41):

now I can convince him:

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:41):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:41):

it should be a simp lemma, I fixed

view this post on Zulip Johan Commelin (May 28 2018 at 10:41):

why isn't it a simp lemma?

you mean a simp definition?

view this post on Zulip Kenny Lau (May 28 2018 at 10:41):

@Johan Commelin no, set.image_id

view this post on Zulip Kenny Lau (May 28 2018 at 10:42):

not a definition

view this post on Zulip Johan Commelin (May 28 2018 at 10:42):

Aaah, ok, true

view this post on Zulip Kenny Lau (May 28 2018 at 10:42):

now is @Kevin Buzzard happy?

view this post on Zulip Kenny Lau (May 28 2018 at 10:42):

after the fix I will be able to remove that line

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:42):

Oh!

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:43):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:43):

All i know is that it passes two basic tests

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:43):

(1) it's an equality

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:43):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:43):

image_id is a good simp lemma

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:43):

My entry requirements for simp are pretty low

view this post on Zulip Kenny Lau (May 28 2018 at 10:43):

so is @Kevin Buzzard satisfied now?

view this post on Zulip Mario Carneiro (May 28 2018 at 10:43):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:43):

image_id is a good simp lemma

I feel I could not say that with confidence

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:44):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:44):

Exactly.

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:44):

I want to become a power user

view this post on Zulip Mario Carneiro (May 28 2018 at 10:45):

because it's a global problem with some locality

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:45):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:45):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:45):

appear, other than here

view this post on Zulip Mario Carneiro (May 28 2018 at 10:45):

You could just look at the many many examples in mathlib

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:46):

reading code is so boring

view this post on Zulip Andrew Ashworth (May 28 2018 at 10:46):

only masochistic CS graduate students get interested in software verification

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:46):

that's what CS people do

view this post on Zulip Andrew Ashworth (May 28 2018 at 10:46):

your tips are folklore in CS departments

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:46):

I want to talk to more CS people

view this post on Zulip Andrew Ashworth (May 28 2018 at 10:46):

and that textbook I mentioned yesterday

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:46):

I need simp tips so I can be a power user

view this post on Zulip Mario Carneiro (May 28 2018 at 10:46):

term rewriting and all that?

view this post on Zulip Andrew Ashworth (May 28 2018 at 10:46):

yeah

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:46):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:46):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:47):

and then I knew he'd cracked it

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:48):

Actually, how about this for a tactic

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:48):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:49):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:49):

and calls it schoolkid

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:49):

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

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:51):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:51):

I see

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:51):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:51):

Is that the question?

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:51):

Can I code this in a Lean tactic?

view this post on Zulip Kenny Lau (May 28 2018 at 10:52):

those techniques only work for small cases

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:52):

Are you saying that this is hard

view this post on Zulip Kenny Lau (May 28 2018 at 10:52):

they can't be verified

view this post on Zulip Andrew Ashworth (May 28 2018 at 10:52):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:52):

@Andrew Ashworth This is exactly the point.

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:52):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:52):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:53):

and I was just assuming it was going to be easy

view this post on Zulip Kenny Lau (May 28 2018 at 10:53):

the world is imperfect

view this post on Zulip Kenny Lau (May 28 2018 at 10:53):

computability matters

view this post on Zulip Mario Carneiro (May 28 2018 at 10:53):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:53):

that's an engineering problem

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:53):

you CS guys write great algos

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:53):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:53):

no that's a fundamental limit on progress

view this post on Zulip Kenny Lau (May 28 2018 at 10:53):

no, you can't

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:54):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:54):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:54):

you don't

view this post on Zulip Kevin Buzzard (May 28 2018 at 10:54):

and which questions look sensible to me like the Langlands Programme

view this post on Zulip Kenny Lau (May 28 2018 at 10:54):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:54):

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

view this post on Zulip Kenny Lau (May 28 2018 at 10:54):

including your brain

view this post on Zulip Kenny Lau (May 28 2018 at 10:54):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:55):

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

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:56):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:56):

I have plenty of theorems in metamath as evidence

view this post on Zulip Mario Carneiro (May 28 2018 at 10:57):

but proof engineering is a really important skill

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:59):

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

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

view this post on Zulip Mario Carneiro (May 28 2018 at 10:59):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 11:00):

but I grant that working with lean encourages good automation practices

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:01):

what was the solution?

view this post on Zulip Andrew Ashworth (May 28 2018 at 11:03):

to what?

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

in ZFC id '' U isn't even defined

Oh what a bore, you're right

view this post on Zulip Mario Carneiro (May 28 2018 at 11:12):

metamath uses ZFC + classes to get around this

view this post on Zulip Mario Carneiro (May 28 2018 at 11:13):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 11:13):

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:16):

it's called using interface to make your life better

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:26):

no, I mean the axiom of extensionality.

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

view this post on Zulip Mario Carneiro (May 28 2018 at 11:27):

no

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:27):

it looks good to me

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:27):

simple predicate

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:27):

implies an equality

view this post on Zulip Mario Carneiro (May 28 2018 at 11:28):

it says p = q in the conclusion

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

it got over my simp bar

view this post on Zulip Mario Carneiro (May 28 2018 at 11:28):

that means anything equals anything

view this post on Zulip Mario Carneiro (May 28 2018 at 11:28):

it's too general

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

Just apply it sensibly

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

and stop moaning

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

don't just apply it randomly

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

:-/

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

This is really interesting

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

this is the hard bit

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

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

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

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

otherwise simp has to be creative when rewriting

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:30):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 11:30):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:30):

That's your job

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:30):

you went to math classe

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:30):

s

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:30):

you know how we think

view this post on Zulip Mario Carneiro (May 28 2018 at 11:30):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:30):

can you write a better interface?

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:31):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:31):

I think you had a more grown-up name

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

view this post on Zulip Johan Commelin (May 28 2018 at 11:31):

I think you had a more grown-up name

math_trivial?

view this post on Zulip Mario Carneiro (May 28 2018 at 11:32):

Mizar is actually stronger axiomatically than lean

view this post on Zulip Kenny Lau (May 28 2018 at 11:32):

why?

view this post on Zulip Mario Carneiro (May 28 2018 at 11:32):

it has a proper class of inaccessibles

view this post on Zulip Johan Commelin (May 28 2018 at 11:32):

But I wouldn't mind have kindergarten or schoolkid

view this post on Zulip Kenny Lau (May 28 2018 at 11:32):

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:32):

but it seems that you are deaf

view this post on Zulip Andrew Ashworth (May 28 2018 at 11:33):

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

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 11:34):

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

view this post on Zulip Mario Carneiro (May 28 2018 at 11:34):

they are organized fairly logically

view this post on Zulip Mario Carneiro (May 28 2018 at 11:35):

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

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:37):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:37):

it's init this and data that

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:37):

when I want set.image_id

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:38):

I type #check set.image_id

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:38):

and it's not there

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:38):

I have no clue where anything is

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:38):

they're just all theorems

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:38):

Can we have a better search?

view this post on Zulip Mario Carneiro (May 28 2018 at 11:38):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:39):

oh!

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:39):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:39):

Does that work with everything?

view this post on Zulip Mario Carneiro (May 28 2018 at 11:39):

it's not even set.something

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:39):

can I import scheme?

view this post on Zulip Mario Carneiro (May 28 2018 at 11:39):

it's data.set.basic

view this post on Zulip Mario Carneiro (May 28 2018 at 11:39):

but vscode will still give it to you

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:39):

I see

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:40):

I should "key on set"

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

view this post on Zulip Kenny Lau (May 28 2018 at 11:45):

are they

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:46):

I am only interested in the Langlands Programme

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:48):

it's called using interface to make your life better

I need better interface search.

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:48):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:49):

Can that be a thing one day?

view this post on Zulip Sean Leather (May 28 2018 at 11:50):

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

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

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:53):

I could do all the costings for that other than salary

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:53):

I have no idea how much you guys get paid

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:53):

the administration would be able to fill in the other boxes

view this post on Zulip Kevin Buzzard (May 28 2018 at 11:54):

I'm meeting with EPSRC in two weeks

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

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

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

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

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

I just wrote a theorem that was in the library

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

yay me

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

#check topological_space.open_immersion_id

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:21):

#check topological_space.id_open_immersion

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:21):

what should it be called?

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:21):

The statement that the identity map is an open immersion

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:21):

I did the other one

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:22):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:22):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:22):

What do the artists say about this one?

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

view this post on Zulip Patrick Massot (May 28 2018 at 12:25):

I'm much slower

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:36):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:36):

But I am stuck on something

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:36):

in my context

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:36):

oh I can answer my own question

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:38):

oh no I can't

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:38):

Ok so there's my x

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:39):

and presheaf_of_types_pullback_under_open_immersion just has some definition

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:39):

which explictly says what its F bit is

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:39):

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

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:40):

I can't unfold presheaf_of_types_pullback_under_open_immersion

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:40):

Do people need more context?

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

view this post on Zulip Patrick Massot (May 28 2018 at 12:41):

Did you try dsimp at x?

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:41):

I did

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:41):

it wasn't very effective

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:41):

it turned presheaf_of_rings_pullback_under_open_immersion

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:41):

into presheaf_of_types_pullback_under_open_immersion

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:42):

and then stopped

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:43):

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

view this post on Zulip Patrick Massot (May 28 2018 at 12:43):

Is it something I can git clone?

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:47):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:47):

can git help me here?

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:47):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:47):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:48):

goofing around

view this post on Zulip Patrick Massot (May 28 2018 at 12:48):

you could create a broken branch

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:48):

Can I do that in VS Code?

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:49):

I only have master

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:49):

I've got it

view this post on Zulip Patrick Massot (May 28 2018 at 12:49):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:50):

Oh crap I didn't stash

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:50):

is that an issue?

view this post on Zulip Patrick Massot (May 28 2018 at 12:50):

maybe not

view this post on Zulip Patrick Massot (May 28 2018 at 12:50):

it wrote that to be on the safe side

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:51):

oops

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:51):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:51):

was what I meant to say

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:52):

line 495, I want to unfold that presheaf_of_types_pullback_under_open_immersion

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:52):

no

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:52):

I want Lean to unfold it

view this post on Zulip Kevin Buzzard (May 28 2018 at 12:52):

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

view this post on Zulip Patrick Massot (May 28 2018 at 13:10):

This is really irritating

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:38):

OK I minimised

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:38):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:39):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:39):

which are a bit like distribs

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:39):

and although the objects are a bit silly

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:39):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:40):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:40):

which I am convinced a computer could have done for me

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:40):

I cut and pasted the definition of pre_semi_sheaf_of_rings_pullback

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:40):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:41):

but the problem is that the unfolding is refl

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:41):

I have to work it out myself

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:41):

This is an independent question

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:46):

Oh cool

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:46):

but OK I have finally minimised my question

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:47):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:47):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:48):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:48):

I'm not sure I can prove that goal

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:48):

I'm not even sure that goal is true

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:48):

but I think it is

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:48):

for some reason it's a pain to prove though

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:49):

I'm hoping the file is fairly self-explanatory

view this post on Zulip Johan Commelin (May 28 2018 at 13:49):

It is "math-true", right?

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:50):

exactly Johan

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:50):

Before I had something which was math-true

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:50):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:50):

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

view this post on Zulip Johan Commelin (May 28 2018 at 13:52):

Are the rings essential to the problem?

view this post on Zulip Johan Commelin (May 28 2018 at 13:53):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:58):

No it's crucial they're rings

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:58):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:59):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:59):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:59):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:59):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 13:59):

Am I missing something easy?

view this post on Zulip Patrick Massot (May 28 2018 at 14:00):

Oh, he went back a couple of stages

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:00):

I removed topology

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:00):

and open immersions

view this post on Zulip Kenny Lau (May 28 2018 at 14:00):

Am I missing something easy?

no

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:00):

crap

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:00):

is that a provable but hard goal?

view this post on Zulip Kenny Lau (May 28 2018 at 14:00):

well not really hard

view this post on Zulip Kenny Lau (May 28 2018 at 14:00):

i could do it

view this post on Zulip Kenny Lau (May 28 2018 at 14:00):

but not exactly easy

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

Teach me how to do it

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

I can't do it

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

and it's obvious

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

and these are my least favourite things in Lean

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

teach me how to kill this pokemon

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

exactly

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

Kenny

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:01):

I'm up to here

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

view this post on Zulip Kenny Lau (May 28 2018 at 14:02):

I'm trying

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:02):

Thanks

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:03):

Are you writing a tactic?

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:03):

Don't try to solve the goal

view this post on Zulip Kenny Lau (May 28 2018 at 14:03):

no

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:03):

try to write a tactic which solves the goal

view this post on Zulip Kenny Lau (May 28 2018 at 14:03):

I don't know how to write tactics

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:03):

because this goal is solved by math_trivial

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:04):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:04):

but a pre_semi_sheaf does not have res

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:04):

so you have to bite the bullet

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:05):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:05):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:05):

Last line

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:05):

the pre_semi_sheaves are isomorphic via the identity map

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:05):

but checking the details is apparently a little tricky

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:06):

Would I have exactly the same problems in Mizar?

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:06):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:07):

I have isolated a frustration I have with dependent type theory

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:07):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:07):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:08):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:08):

and I never recover

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:08):

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 14:10):

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

view this post on Zulip Simon Hudon (May 28 2018 at 14:14):

How would you prove it without tactics?

view this post on Zulip Kenny Lau (May 28 2018 at 14:15):

he can't function without tactics

view this post on Zulip Kenny Lau (May 28 2018 at 14:15):

you would do eq.drec without tactics

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 15:07):

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

view this post on Zulip Kenny Lau (May 28 2018 at 15:07):

@Assia Mahboubi just prove the above

view this post on Zulip Kenny Lau (May 28 2018 at 15:09):

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 15:10):

oh, sorry

view this post on Zulip Kenny Lau (May 28 2018 at 15:10):

I think you can try it online

view this post on Zulip Kenny Lau (May 28 2018 at 15:11):

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

view this post on Zulip Assia Mahboubi (May 28 2018 at 15:11):

Ok thanks, I am doing that now.

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:13):

Does one run into the same issues in Coq?

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:13):

Does one run into the same issues in Mizar?

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:14):

Which systems is this easy in?

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:14):

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

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

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

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 15:15):

lol it's been an hour already

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

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:17):

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 15:19):

I tried to build up an interface

view this post on Zulip Kenny Lau (May 28 2018 at 15:19):

didn't work

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

view this post on Zulip Kenny Lau (May 28 2018 at 15:21):

see you

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

@Kenny Lau

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

I had an idea

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

but you would be quicker to implement it than me

view this post on Zulip Kenny Lau (May 28 2018 at 15:28):

what is it

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

and I have to tidy the kitchen anyway

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

I claim that my definition is incomplete

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

as far as Lean is concerned

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

I am missing some extra structure

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

which can be filled in easily

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

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

plus axiom that res U U = id

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

plus axiom of composition

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:30):

res U V then res V W is res U W

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:30):

Given my stupid annoying structure

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:30):

can it be beefed up to such a structure

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:30):

and for this beefed-up structure

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:30):

can the map be defined to be res

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:30):

and then we deduce the result for the stupid structure

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:31):

My experience with schemes tells me

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:31):

that when the map is res

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:31):

all the hard proofs become rfl

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:31):

maybe not the ring one

view this post on Zulip Kevin Buzzard (May 28 2018 at 15:31):

the ring one we have to use some equiv tactic thing

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

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

I was hoping you'd show up

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

I thought you'd like this one

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

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

view this post on Zulip Reid Barton (May 28 2018 at 18:19):

Yes

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

Convert? What does that do?

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

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

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

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

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

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

view this post on Zulip Patrick Massot (May 29 2018 at 08:55):

yes

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

view this post on Zulip Patrick Massot (May 29 2018 at 08:55):

yes

view this post on Zulip Johan Commelin (May 29 2018 at 08:55):

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

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

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

view this post on Zulip Patrick Massot (May 29 2018 at 08:59):

Have fun!

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

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

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

view this post on Zulip Patrick Massot (May 29 2018 at 09:01):

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

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

[sorry, wrong topic]

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

view this post on Zulip Johan Commelin (May 29 2018 at 09:08):

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

view this post on Zulip Johan Commelin (May 29 2018 at 09:08):

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

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

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

view this post on Zulip Assia Mahboubi (May 29 2018 at 09:09):

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

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

view this post on Zulip Patrick Massot (May 29 2018 at 09:14):

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

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

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

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

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

view this post on Zulip Johan Commelin (May 29 2018 at 09:35):

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

view this post on Zulip Johan Commelin (May 29 2018 at 09:35):

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

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

This is exactly what I tried to avoid

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

My instructions should bypass mathlib compilation

view this post on Zulip Patrick Massot (May 29 2018 at 09:39):

(I'm waiting for my train)


Last updated: May 19 2021 at 03:22 UTC