# Zulip Chat Archive

## Stream: general

### Topic: Infinity Hotel

#### Reid Barton (Sep 19 2019 at 15:46):

This Proof Ground problem is actually almost exactly a lemma I want. Would somebody (@Floris van Doorn?) like to PR a solution to mathlib?

Maybe as a mathlib lemma, it is more natural to use `equiv`

in place of `bijective`

, and replace the target `nat`

by `denumerable`

#### Mario Carneiro (Sep 19 2019 at 15:58):

I discussed this with floris after the competition. I think it generalizes to embedding B < A when A is an infinite cardinal

#### Kevin Buzzard (Sep 19 2019 at 16:17):

Assuming AC, a+b=max(a,b) so A-B bijects with A-f(B)

#### Floris van Doorn (Sep 19 2019 at 18:19):

Yes, I'm going to PR this to mathlib. The current statement I am proving is

theorem extend_function_of_lt {α β : Type*} {s : set α} (f : s ↪ β) (hs : #s < #α) (h : nonempty (α ≃ β)) : ∃ (g : α ≃ β), ∀ x : s, g x = f x

#### Floris van Doorn (Sep 19 2019 at 18:20):

Here `#`

means `cardinal.mk`

#### Floris van Doorn (Sep 19 2019 at 18:26):

I have already proved this in the case where `#α`

is infinite.

~~Now that I think of this, when ~~`α`

is infinite, I should probably replace the assumption `#s < #α`

with the weaker condition `#(-s : set α) = #α`

(I already proved the lemma that the former implies the latter).

EDIT: Oh wait, then it's false.

#### Mario Carneiro (Sep 20 2019 at 04:20):

@Kevin Buzzard Could you elaborate on that proof? a+b=a does not imply a-b=a for cardinals

#### Kevin Buzzard (Sep 20 2019 at 07:21):

I was imagining the generalisation being this: if B<A is a subset, and |B|<|A|, then any injection f:B -> A can be extended to a bijection A -> A. The proof is: write C=A\B and D=A\f(B) and observe that |C|=|A|=|D|. Did I slip up?

#### Mario Carneiro (Sep 20 2019 at 07:39):

Those facts are all true but I'm not sure how you are arguing them

#### Mario Carneiro (Sep 20 2019 at 07:40):

actually you forgot to assume A is infinite, else |C|=|A| fails

#### Chris Hughes (Sep 20 2019 at 07:41):

I proved something similar as part of algebraic closure.

import set_theory.schroeder_bernstein open set function universes u v w noncomputable theory local attribute [instance] classical.dec lemma thing_aux {X : Type u} {Y : Type v} {Z : Type w} (fxy : X ↪ Y) (fxz : X ↪ Z) (hYZ : (Z ↪ Y) → false) : ↥-range fxy.1 ↪ ↥-range fxz.1 := classical.choice $ or.resolve_left embedding.total $ λ ⟨f⟩, hYZ $ calc Z ↪ range fxz ⊕ ↥-range fxz : (equiv.set.sum_compl _).symm.to_embedding ... ↪ range fxy ⊕ ↥-range fxy : embedding.sum_congr (((equiv.set.range _ fxz.2).symm.to_embedding).trans (equiv.set.range _ fxy.2).to_embedding) f ... ↪ Y : (equiv.set.sum_compl _).to_embedding def thing {X : Type u} {Y : Type v} {Z : Type w} (fxy : X ↪ Y) (fxz : X ↪ Z) (hYZ : (Z ↪ Y) → false) : Y ↪ Z := calc Y ↪ range fxy ⊕ ↥-range fxy : (equiv.set.sum_compl _).symm.to_embedding ... ↪ range fxz ⊕ ↥-range fxz : embedding.sum_congr ((equiv.set.range _ fxy.2).symm.to_embedding.trans (equiv.set.range _ fxz.2).to_embedding) (thing_aux fxy fxz hYZ) ... ↪ Z : (equiv.set.sum_compl _).to_embedding lemma thing_commutes {X : Type u} {Y : Type v} {Z : Type w} (fxy : X ↪ Y) (fxz : X ↪ Z) (hYZ : (Z ↪ Y) → false) (x : X) : thing fxy fxz hYZ (fxy x) = fxz x := have (⟨fxy x, mem_range_self _⟩ : range fxy) = equiv.set.range _ fxy.2 x, from rfl, begin dsimp only [thing, embedding.trans_apply, equiv.trans_apply, function.comp, equiv.to_embedding_coe_fn], simp only [equiv.set.sum_compl_symm_apply_of_mem (mem_range_self _), embedding.sum_congr_apply_inl, equiv.set.sum_compl_apply_inl, embedding.trans_apply, equiv.to_embedding_coe_fn, this, equiv.symm_apply_apply], refl end

#### Chris Hughes (Sep 20 2019 at 07:43):

Somehow the assumption `(Z ↪ Y) → false`

should be turned into `(Z ↪ X) → false`

#### Mario Carneiro (Sep 20 2019 at 07:43):

isn't that just transitivity?

#### Mario Carneiro (Sep 20 2019 at 07:46):

@Kevin Buzzard I think your proof sketch is basically what floris did in the competition

#### Mario Carneiro (Sep 20 2019 at 07:47):

it would be nice to reduce it to a one liner of mathlib lemmas though

#### Mario Carneiro (Sep 20 2019 at 07:50):

Unfortunately I don't see how to apply chris's lemma directly here

#### Mario Carneiro (Sep 20 2019 at 07:51):

it only seems to construct an injection from Y to Z where |Y|<|Z|, and the only obvious candidates are Y=B and Z=A, or Y=f(B) and Z=A, and neither is particularly helpful

#### Mario Carneiro (Sep 20 2019 at 07:54):

In this situation, we want Y=Z=A, but then `(Z ↪ Y) → false`

fails

#### Chris Hughes (Sep 20 2019 at 07:56):

But in the infinite case can we weaken the assumption to `(Z ↪ X) → false`

?

#### Kevin Buzzard (Sep 20 2019 at 07:57):

@Mario Carneiro I don't understand why you're calling it a sketch ;-)

#### Mario Carneiro (Sep 20 2019 at 07:57):

you have to reference actual theorems, and also prove the side conditions

#### Mario Carneiro (Sep 20 2019 at 07:58):

ideally the formal proof should actually be that short, but the side conditions are messy here

#### Kevin Buzzard (Sep 20 2019 at 07:58):

The argument would convince any mathematician. That's the level where we operate. What we really need is an interface where I can just say what I said to you and then let tactics do the rest.

#### Kevin Buzzard (Sep 20 2019 at 07:59):

we can try `cases, refl`

on the side conditions or whatever. It's all noise.

#### Mario Carneiro (Sep 20 2019 at 07:59):

you also didn't prove what you claimed to... there are lots of issues with treating that literally as a proof

#### Kevin Buzzard (Sep 20 2019 at 08:00):

Can you give me specific examples of issues? I'd be happy to talk about this but I have to run

#### Kevin Buzzard (Sep 20 2019 at 08:00):

I think my proof is "math-complete"

#### Mario Carneiro (Sep 20 2019 at 08:00):

it's absolutely a sketch, but it's enough hints for a competent mathematician to fill in the rest of the proof

#### Mario Carneiro (Sep 20 2019 at 08:00):

but you should never confuse "enough to communicate the main ideas" with "proof"

#### Johan Commelin (Sep 20 2019 at 08:01):

Isn't that the definition of *proof*?

#### Mario Carneiro (Sep 20 2019 at 08:02):

for one thing, communication depends on the target audience; computers should be treated as a particularly dumb student

#### Mario Carneiro (Sep 20 2019 at 08:04):

it is not really possible to give an actual definition of "proof" if you take that position seriously... in the limit, anything that is logically derivable can be considered "proof by trivial"

#### Mario Carneiro (Sep 20 2019 at 08:06):

This is trending philosophical, but one property I want the word "proof" to have is that it's objective or at least societally defined, whereas "communication" is context dependent

#### Mario Carneiro (Sep 20 2019 at 08:09):

Really, I prefer to just sidestep the whole matter and only talk about formal proof, which has a proper definition, but it makes it difficult for me to interpret Kevin when he wants a raised eyebrow to constitute a valid proof

#### Patrick Massot (Sep 20 2019 at 08:21):

It depends whose eyebrow it is.

#### Mario Carneiro (Sep 20 2019 at 08:53):

Here's the closest I got to Kevin's sketch, modulo the cardinality fact:

import set_theory.cardinal local prefix `#` := cardinal.mk theorem mk_eq_mk {α β} (h : α ≃ β) : #α = #β := quotient.sound ⟨h⟩ theorem foo {α} {S : set α} (h : #S < #α) : #(-S : set α) = #α := sorry example {X Y Z} (f : X ↪ Y) (g : X ↪ Z) (h₁ : #X < #Y) (h₂ : #Y = #Z) : ∃ e : Y ≃ Z, ∀ x, e (f x) = g x := begin have e1 : #(-set.range f : set _) = #Y := foo (by rwa [← mk_eq_mk (equiv.set.range f f.2)]), have e2 : #(-set.range g : set _) = #Z := foo (by rwa [← h₂, ← mk_eq_mk (equiv.set.range g g.2)]), rw [h₂, ← e2] at e1, cases quotient.exact e1 with e1, classical, refine ⟨(equiv.set.sum_compl _).symm.trans ((equiv.sum_congr _ e1).trans (equiv.set.sum_compl _)), λ x, _⟩, { exact (equiv.set.range f f.2).symm.trans (equiv.set.range g g.2) }, { simp [equiv.set.sum_compl_symm_apply_of_mem, set.mem_range_self], rw (equiv.symm_apply_eq _).2, simp } end

#### Kevin Buzzard (Sep 20 2019 at 09:18):

the cardinal fact is proved like this: If b<a then a=b+(a-b)=max(b,a-b), hence a-b=a.

#### Kevin Buzzard (Sep 20 2019 at 09:19):

Maybe some automatic theorem prover can find that fact about cardinals given what is in mathlib?

#### Kevin Buzzard (Sep 20 2019 at 09:22):

I'm taking a look at your proof. It's annoying that hovering over `equiv.set.sum_compl`

doesn't show me its type -- I think this is because we're in tactic mode.

#### Mario Carneiro (Sep 20 2019 at 09:30):

Note that the cardinal fact as I've stated it is false, so if you think you have proved it you should not trust your proof

#### Mario Carneiro (Sep 20 2019 at 09:31):

it would be pretty difficult to get nitpick or whatever counterexample generator to find why the statement is false too

#### Mario Carneiro (Sep 20 2019 at 09:32):

actually scratch that - the problem is with finite sets so they can probably handle it

#### Mario Carneiro (Sep 20 2019 at 09:34):

In chris's proof he uses calc blocks instead to build the equivs, which looks a bit nicer

#### Kevin Buzzard (Sep 20 2019 at 09:34):

I thought we were talking about the infinite case now. All this a+b=max(a,b) is only true in the infinite case, I've been assuming infinite.

Your proof is extraordinary.

⊢ ⇑(equiv.trans (equiv.symm (equiv.set.sum_compl (set.range ⇑f))) (equiv.trans (equiv.sum_congr (equiv.trans (equiv.symm (equiv.set.range ⇑f _)) (equiv.set.range ⇑g _)) e1) (equiv.set.sum_compl (set.range ⇑g)))) (⇑f x) = ⇑g x

We prove this by saying "...and the diagram obviously commutes". What is going on? This is trivial stuff.

#### Mario Carneiro (Sep 20 2019 at 09:35):

there are side conditions

#### Kevin Buzzard (Sep 20 2019 at 09:35):

I can prove this whole thing by drawing one picture.

#### Mario Carneiro (Sep 20 2019 at 09:35):

no, you can state the problem by drawing a picture

#### Kevin Buzzard (Sep 20 2019 at 09:36):

There aren't any side conditions. Assuming foo, we can prove the existence theorem. This is a really great example of a proof which can be done by a simple picture.

#### Mario Carneiro (Sep 20 2019 at 09:36):

The only thing I wrote in the proof are side conditions

#### Mario Carneiro (Sep 20 2019 at 09:36):

everything else is indeed being handled by simp

#### Kevin Buzzard (Sep 20 2019 at 09:36):

wow

#### Mario Carneiro (Sep 20 2019 at 09:37):

The proof sketch you gave me essentially covers the first two lines of the proof

#### Mario Carneiro (Sep 20 2019 at 09:37):

you never said what the bijection is or how to build it

#### Mario Carneiro (Sep 20 2019 at 09:38):

that's all "type tetris"

#### Mario Carneiro (Sep 20 2019 at 09:38):

with side conditions in the middle of it all

#### Mario Carneiro (Sep 20 2019 at 09:40):

I think side conditions are the bane of any theorem prover, because there is no good way to write them, which makes it easy to ignore them for expositional purposes in math

#### Kevin Buzzard (Sep 20 2019 at 09:42):

#### Kevin Buzzard (Sep 20 2019 at 09:44):

Where is `equiv.set.sum_compl_symm_apply_of_mem`

in my picture? What is going on?

#### Mario Carneiro (Sep 20 2019 at 09:44):

Where's the bijection? I'm not even sure where f is in the picture

#### Kevin Buzzard (Sep 20 2019 at 09:44):

Two down arrows are f and g.

#### Kevin Buzzard (Sep 20 2019 at 09:45):

The bijection is because I identified the two sets Y and Z, the top halves are the same, and the bottom halves biject by a trivial lemma which I proved elsewhere on the board.

#### Mario Carneiro (Sep 20 2019 at 09:45):

`equiv.set.sum_compl_symm_apply_of_mem `

says that if you are on the top half of the picture then you can go from y to the top half of y

#### Kevin Buzzard (Sep 20 2019 at 09:45):

I am working in the category of sets equipped with a map from X, so somehow the commutativity of the diagrams just all gets swallowed up by the machine.

#### Kevin Buzzard (Sep 20 2019 at 09:46):

Maybe I am using some better structure than you.

#### Mario Carneiro (Sep 20 2019 at 09:46):

in lean there are two additional points in the picture, Y and Z

#### Mario Carneiro (Sep 20 2019 at 09:47):

and maps from Y to the parts of Y

#### Kevin Buzzard (Sep 20 2019 at 09:47):

Aah, this is one of these instances where a mathematician thinks "set-theoretically" and all these issues melt away.

#### Mario Carneiro (Sep 20 2019 at 09:47):

sure I'd love to do that, but DTT

#### Kevin Buzzard (Sep 20 2019 at 09:47):

(all the maps become the identity map in some sense)

#### Mario Carneiro (Sep 20 2019 at 09:48):

actually it doesn't really solve anything, it just removes the function `equiv.set.sum_compl_symm_apply_of_mem`

and leaves the side condition

#### Kevin Buzzard (Sep 20 2019 at 09:48):

Are we missing a tactic which does arguments like this?

#### Mario Carneiro (Sep 20 2019 at 09:48):

meh

#### Mario Carneiro (Sep 20 2019 at 09:48):

"like this" is never enough

#### Mario Carneiro (Sep 20 2019 at 09:49):

I generalize from >1 example

#### Kevin Buzzard (Sep 20 2019 at 09:49):

given that Y \ f(X) bijects with Z \ g(X), figure out the rest yourself. Is that too much for an AI?

#### Mario Carneiro (Sep 20 2019 at 09:49):

Probably not

#### Mario Carneiro (Sep 20 2019 at 09:50):

I can imagine an SMT prover can get this, but when it's all embedded in lean some things get obscured

Last updated: May 14 2021 at 07:19 UTC